oupoの日記

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

logic

数学ガールゲーデル編では表現定理の証明が省略されている
体系には足し算なんて用意されていないのにたとえばどうやって三項関係を表現するんだろうと気になる。これはだいたい予想がついた。
- 二項関係 $x< y$ を表現する論理式は、 $y$ が属していて任意の $k$ について $k$ が属するなら $k+1$ が属していて $x$ が属さないような数の集合がある(という意味を期待する論理式)
- 三項関係 $x+y=z$ は $y\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$ が定理であること、など簡単なところからボトムアップに攻めていくことにした
次のような成果が得られた
- $p$ と $p\to q$ が定理ならば $q$ が定理
- $p \vee q$ が定理⇔ $q \vee p$ が定理
- $q$ が定理ならば $p \to q$ は定理
- $\neg p$ が定理ならば $p \to q$ は定理
- $p\to q$ と $r \vee p$ が定理ならば $r \vee q$ は定理
- $p\to q$ と $q\to r$ が定理ならば $p\to r$ は定理
- $p\to q$ と $p \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$ が定理であることと $p$ と $q$ がともに定理であることは同値
- $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 q$ と $r$ が定理のとき $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)$ が定理だとすると体系が矛盾するんじゃないか？と予想がついて示した
ここでに再挑戦。演繹定理を使えばと公理からスタートして有限回の推論の連鎖でにたどりつくのであればが定理だといえる。まだ演繹定理の証明は読んでいないのだけど、演繹定理を今は無条件に認めるものとして示してみる。
証明のスケッチはこんな感じ
- $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 q$ と $p\to r$ が定理のとき $p\to (q\wedge r)$ が定理
- $p\to q$ が定理のとき $\exists v(p)\to \exists v(q)$ が定理
- $p$ が自由な $v$ をもたないとき、 $\exists v(p)\to p$ が定理
演繹定理を使わないでが定理であることを示せた！←イマココ
この過程で得た補助的な定理
- $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)