演繹定理1
さトぅー
「ここから本番」
■例1
{φ} |- (ψ⇒φ)
proof
1 φ [ax]
2 (φ⇒(ψ⇒φ)) [Ax1]
3 (ψ⇒φ) [⇒el 1,2]
■
さトぅー
「(φ⇒(ψ⇒φ))、つまりAx1は3行目に公理"φ⇒"をつけた形をしている。
Ax1のみの1行の証明もあるけど、実は別のやり方でも証明できる」
■例2
{} |- (φ⇒(ψ⇒φ))
proof
-----------------------------
さトぅー
「例1の全部の行の最初に"φ⇒"をつけたい。
まず、例1の1行目は消したいφになってる。
これはthm0.0でやった」
例1
1 φ [ax]
↓翻訳
----------------------------
1 (φ⇒φ) [thm0.0]
------------------------------
さトぅー
「例1の2行目はG0の論理的公理になっている。
このときは論理的公理,Ax1,⇒elの順で"φ⇒"をつける」
例1
2 (φ⇒(ψ⇒φ)) [Ax1]
↓翻訳
-------------------------------
2 (φ⇒(ψ⇒φ)) [Ax1]
3 ((φ⇒(ψ⇒φ))⇒(φ⇒(φ⇒(ψ⇒φ)))) [Ax1]
4 (φ⇒(φ⇒(ψ⇒φ))) [⇒el 2,3]
------------------------------
さトぅー
「例1の3行目は⇒elになってる。
このときは先に"φ⇒"をつけた行が使えるように、Ax2,⇒el,⇒elの順で"φ⇒"をつける」
例1
1 φ [ax]
2 (φ⇒(ψ⇒φ)) [Ax1]
3 (ψ⇒φ) [⇒el 1,2]
↓翻訳
-------------------------------
1 (φ⇒φ) [thm0.0]
:
:
4 (φ⇒(φ⇒(ψ⇒φ))) [⇒el 2,3]
5 ((φ⇒(φ⇒(ψ⇒φ)))⇒((φ⇒φ)⇒(φ⇒(ψ⇒φ)))) [Ax2]
6 ((φ⇒φ)⇒(φ⇒(ψ⇒φ))) [⇒el 4,5]
7 (φ⇒(ψ⇒φ)) [⇒el 1,6]
■
さトぅー
「はあ……はあ」バタッ
エーリル
「あまりの証明の長さにさトぅーさんが疲労で倒れた！」
天々城
「この言語は証明の長さを犠牲にしてルールを減らしている。
慣れるのは早いがコントロールは難しい」
さトぅー
「まあ、慣れるのは簡単なんだけどね」ムクリ
エーリル
「さトぅーさんが復活した！」
さトぅー
「実はこんなことが成り立つの」
■meta thm0.0
Tを公理の集合とする。
T∪{φ} |- ψ
ならば
T |- (φ⇒ψ)
エーリル
「metaって？」
天々城
「やはりこの話は回避できないか……」
さトぅー
「今まで命題論理を私たちが知ってる言語で定義したわよね。
つまり、「命題論理」を作る土台のような言語を黙って使っていた」
エーリル
「その「土台」になる言語はどう定義するの？」
さトぅー
「「「「命題論理」の土台になる言語」の土台になる言語」ってことよね」
エーリル
「……定義が止まらなくなる」
さトぅー
「大体そんな感じ。
だから今は、とりあえずどこかのスタート地点に立って、命題論理っていう簡単な言語を理解しようってわけ」
天々城
「メタ 定理っていうのは命題論理の土台の言語での定理だ。
もし記号|-を使うとこう書けるだろう」
{T∪{φ}|-ψ} |- (T |- (φ⇒ψ))
天々城
「「証明できること」が証明できるっていうんだから曼荼羅感あるよナ」
エーリル
「暗黙で使ってる言語もあったのね。
当たり前か、じゃないと何も喋れない」
さトぅー
「何も喋れないっていうのが核心突いてる気がするわ」
エーリル
「メタはなんとなくわかったけど、"∪"ってなに？」
天々城
「公理Tって論理式の集合だよナ。
例えばTを{ψ,(ψ⇒ψ)}ってことにして、{φ}と合わせて新しい論理式の集まり{ψ,(ψ⇒ψ),φ}を作りたい。
これを{ψ,(ψ⇒ψ)}∪{φ}と書くわけだ」
エーリル
「集まりと集まりの足し算ってこと？」
天々城
「今はそういう認識でOK。
いずれわかるときがくる」
エーリル
「いずれわかるときがくる……」
天々城
「さトぅーさん、証明の長さに関する帰納法で証明するんだろ？
証明の長さは定義したか？」
さトぅー
「まだね。しないとまずいか」
天々城
「証明には1行目とか2行目とかの長さがあったナ」
エーリル
「うん。3行の証明が7行になった」
天々城
「ここで"証明の長さ"を定義しよう」
■証明の長さの定義
証明φ_1,……,φ_nについて、有限列の個数nを証明の長さと定義する。
エーリル
「ようは行数のことね」
proof
天々城
「T∪{φ} |- ψだとしよう」
天々城
「もし1行の証明があるなら、1行目に書けるのは証明の定義から公理か論理的公理しかない。
Ax1,Ax2,Ax3、あとは自分が勝手に決めた公理Tかφだけだ。
ψがφじゃないなら次の順で"φ⇒"を最初につける」
1 ψ [公理か論理的公理]
↓翻訳
1 ψ [公理か論理的公理]
2 (ψ⇒(φ⇒ψ)) [Ax1]
3 (φ⇒ψ) [⇒el 1,2]
エーリル
「あ、なるほど。例2であったパターンだ」
天々城
「問題はψがφのとき、これはthm0.0で解決した」
1 φ [T∪{φ}]
↓翻訳
1 (φ⇒φ) [thm0.0]
エーリル
「thm0.0はこれを見越していた？」
天々城
「だいたい論理のはじめに出会うけどナ。
これで1行の証明はT |- (φ⇒ψ)にできた」
エーリル
「次は2行の証明？」
天々城
「いや、長さは指定しない」
エーリル
「……へ？」
天々城
「どこかの相手を倒したら次の相手も倒せるとする。
だから1体目を倒したら2体目も倒せるし、2体目を倒したら3体目も倒せるじゃん？」
エーリル
「わかった」
さトぅー
「脳筋か。しかも"数学的帰納法"とか名前教えないの？」
天々城
「名前だけ覚えて定義をわかってないヤツは数弱以前に紀元前なのでは」
さトぅー
「あんまり強い言葉を使わないでくれる？
気持ちはわかるけど」
天々城
「すまん。研究室の隅で反省してくる」ドンヨリ
さトぅー
「あーもう、私がやるわ。
n+1行の証明があるときを考える。
n+1行目で使えるのは公理、論理的公理、φ、⇒elの4パターンしかない」
エーリル
「あー、例2がそうだったね」
さトぅー
「公理、論理的公理、φのときは1行の証明と同じように翻訳すればいい。
だから残りは⇒elのときだけ」
:
:
n+1 ψ [⇒el i,j]
さトぅー
「i行目とj行目を使って⇒elしてるから絶対に次の形をしてないといけない。
記号が足りないからφjっていう論理式を追加するよ」
:
:
i φi [T∪{φ}から証明できる]
:
:
j (φi⇒ψ) [T∪{φ}から証明できる]
:
:
n+1 ψ [⇒el i,j]
エーリル
「そっか。⇒elが使えるならこれしかない」
さトぅー
「さっき天々城みたいに言うならこうかな。
『n行以下はもう全部倒して(φ⇒ψ)の形にできた』」
エーリル
「i行とj行はn行以下。ってことは……？」
:
:
i φi [T∪{φ}から証明できる]
:
:
j (φi⇒ψ) [T∪{φ}から証明できる]
:
:
n+1 ψ [⇒el i,j]
↓翻訳
さトぅー
「どの行になるかわからないから、IとJって行を追加するよ」
:
:
I (φ⇒φi) [数学的帰納法の仮定より、Tから証明できる]
:
:
J (φ⇒(φi⇒ψ)) [数学的帰納法の仮定より、Tから証明できる]
J+1 ((φ⇒(φi⇒ψ))⇒((φ⇒φi)⇒(φ⇒ψ))) [Ax2]
J+2 ((φ⇒φi)⇒(φ⇒ψ)) [⇒el J,J+1]
J+3 (φ⇒ψ) [⇒el I,J+2]
さトぅー
「ほらね」
エーリル
「そっか。だからAx2がいるのね。
例2はこれをしてたのか」
さトぅー
「うん。これでT |- (φ⇒ψ)が言えた」
■
天々城
「やったぜ」
さトぅー
「あ、復活した」
