ゲーデルの体系Pで遊んだ記録

  • 数学ガールゲーデル編では表現定理の証明が省略されている
  • 体系Pには足し算なんて用意されていないのにたとえばどうやって三項関係x+y=zを表現するんだろうと気になる。これはだいたい予想がついた。

    • 二項関係x< yを表現する論理式は、yが属していて任意のkについてkが属するならk+1が属していてxが属さないような数の集合がある(という意味を期待する論理式)
    • 三項関係x+y=zy\le zかつ\{y,z\}\in\{\{0,x\},\{1,x+1\},\{2,x+2\},\cdots\}のように

  • 表現定理の証明を読んでみようとゲーデルの論文にあたる
  • 「この定理の証明には原理的な困難は無いし、また、かなり手間がかかるので、概略を述べるにとどめる」(´・ω・`)
  • じゃあとりあえず自明と書かれている定数関数を表現する論理式があることを示してみようか〜。これには二項関係x=yを表現する論理式があることを示せばいいだろう
  • 論理式p: x_1 = y_1について、m=nならばp\<\bar m,\bar n\>が証明可能、m>nならば\rm not(p\<\bar m,\bar n\>)が証明可能なことは示せた!あとはm< nだけだ!これには論理式\neg(0 = fx_1)が証明可能なことを示せばいい!
  • 話を簡単にするため\neg(0 = 1)を考える。これに挑戦してみる…しかし、とても難しい…
  • というのも、\neg(fx_1 = 0)は公理なのだけれど、=の定義がやっかいで、そこからすぐにこの=の両辺を入れ替えた\neg(0 = fx_1)が示せるわけではないのだ。x_1 = y_1\forall x_2(x_2(x_1) \to x_2(y_1))の省略形と定義されている
  • そこでまずは任意の論理式pについて\neg \neg p \to pが定理であること、など簡単なところからボトムアップに攻めていくことにした
  • 次のような成果が得られた

    • pp\to qが定理ならばqが定理
    • p \vee qが定理⇔q \vee pが定理
    • qが定理ならばp \to qは定理
    • \neg pが定理ならばp \to qは定理
    • p\to qr \vee pが定理ならばr \vee qは定理
    • p\to qq\to rが定理ならばp\to rは定理
    • p\to qp \vee rが定理ならばq \vee rは定理
    • p\to pは定理
    • p\to \neg \neg pは定理
    • (p\to q)\to (\neg q\to \neg p)は定理
    • \neg \neg p\to pは定理
    • p\to (p \wedge p)は定理
    • (p \wedge q)\to pは定理
    • (p \wedge q)\to (q \wedge p)は定理
    • (p\to q)\to ( (r \wedge p)\to (r \wedge q))は定理
    • p \wedge qが定理であることとpqがともに定理であることは同値
    • p' \to pが定理なら(p\to q)\to (p'\to q)は定理
    • p \to p'が定理なら(q\to p)\to (q\to p')は定理
    • q\to (p\to (p \wedge q))は定理
    • p\to qrが定理のときp\to (q \wedge r)は定理
    • p\to q\forall v(p)が定理のとき\forall v(q)は定理
    • p\to \exists v(p)は定理
    • \forall v(p)\to \exists v(p)は定理

  • しかし\neg(fx_1 = 0)がやっかいな原因\forallを解きほぐすことができなかった。

    A⇔A'が定理のときA∨B⇔A'∨Bが定理、¬A⇔¬A'が定理…と示していけば、任意の論理式の中のAをA'に置き換えても定理であるかどうかは変わらないということがいえるかな…と妄想

    さっきの妄想、「A→A'が定理のとき、∀vA→∀vA'が定理」が示せられなさそうなんだよな

    といった感じ。

  • そんな中、本屋で数理論理学の基礎・基本を立ち読みしてたら、\forall v (p\to q) \to (\forall v(p) \to \forall v(q))というのを発見!おお、これだ!と思ってその日帰ってから自力で示そうとするも歯が立たず。次の日この本を買ってきて、それを参考にして示す

  • 新たに次の成果が得られた

    • p\to p'q\to q'が定理のとき(p\wedge q)\to (p'\wedge q')が定理
    • p\wedge (p\to q)\to qは定理
    • \forall v (p)\wedge \forall v (p\to q)\to \forall v(q)は定理
    • p\wedge q\to rが定理ならばp\to (q\to r)が定理
    • \forall v (p\to q)\to (\forall v(p)\to \forall v(q))は定理
    • p\to qが定理のとき\forall v(p)\to \forall v(q)は定理

  • \forallに関する強力な武器が得られたので腕ならしに\exists x_2(\forall x_1(x_2(x_1)))を示す。
    その過程で\alphaが定理のとき、(\alpha\to p)\to p、さらに(p\rightleftharpoons \alpha)\rightleftharpoons pが定理であることを得る。
  • 数理論理学の基礎・基本をぱらぱらと読んで演繹定理というものを知って、え?となる。じゃあ、p\to \forall v(p)が定理ってこと?などとぼんやり考える
  • 寝ぼけていて、明らかにおかしい証明を書いてp\to \forall v(p)が定理なことを示せた!と勘違いする
  • 演繹定理からp\to \forall v(p)が示せるというのも間違いだった。演繹定理には自由変数を持たない論理式という条件があった
  • よく考えたらp\to \forall v(p)が定理だとすると体系が矛盾するんじゃないか?と予想がついて示した
  • ここで\neg(0=1)に再挑戦。演繹定理を使えば0=1と公理からスタートして有限回の推論の連鎖で1=0にたどりつくのであれば0=1\to 1=0が定理だといえる。まだ演繹定理の証明は読んでいないのだけど、演繹定理を今は無条件に認めるものとして示してみる。

    証明のスケッチはこんな感じ

    • 0 = 1
    • \forall x_2(x_2(0)\to x_2(1))
    • x_2(0)\to x_2(1)
    • 内包公理で0のみが属する集合を作る
    • \exists x_2(\forall x_1(x_2(x_1)\rightleftharpoons x_1=0))
    • \exists x_2(x_2(0) \wedge x2(1)\rightleftharpoons 1=0)
    • \exists x_2(1=0)
    • 1=0

  • このスケッチのやり方通りで示せた!やったね

    この過程で得た補助的な定理

    • p\to qp\to rが定理のときp\to (q\wedge r)が定理
    • p\to qが定理のとき\exists v(p)\to \exists v(q)が定理
    • pが自由なvをもたないとき、\exists v(p)\to pが定理

  • 演繹定理を使わないで0=1\to 1=0が定理であることを示せた!←イマココ

    この過程で得た補助的な定理

    • p\to (q\to r)が定理のとき(p\wedge q)\to rが定理
    • ( (p\to q)\wedge (q\to r))\to (p\to r)が定理
    • pが自由なvをもたず、p\to (q\to r)が定理のときp\to (\forall v(q)\to \forall v(r))が定理
    • pが自由なvをもたず、p\to (q\to r)が定理のときp\to (\exists v(q)\to \exists v(r))が定理

雑感

  • 0=1\to 1=0が示せたときはやったー!って思ったんだけど概略じゃあそれがあんまり伝わらないですね
  • 形式的体系Pについてわかることが少しづつ増えていく感覚は、暗かった場所に少しづつあかりが灯されるみたいで面白かったです
  • とはいえなかなか神経がすり減ります(~_~;)
筆者: oupo (連絡先: oupo.nejiki@gmail.com)