[雑記]ヒルベルト流で排中律の証明

『論理と計算のしくみ』
岩波書店、2007

↑の本の演習問題。わからなかったのでWebで探したが、ろくにリソースがなかった。
あれこれやっていたらできたが、ひょっとすると他にも探す人がいるかもしれないのでここに書いておく。
以下大半の人には宇宙語だと思うが、気にしないように。

「⊃から∨への変換」ができればすぐできるのはわかっていたのだが、それが難しかった。
必要そうな定理をかたっぱしから証明している内に10以上の証明ができた。丸々1週間ほど、暇さえあればこればかりやっていた気がする。
論理学で言うところの「証明」は本当にパズルなので、慣れれば楽しい。紙とペンだけあればできるし。
自然演繹法やシーケント計算にくらべてヒルベルト流には苦手意識があったが、排中律の証明はラスボス級に難しかったので、もうヒルベルト流なら大体証明できる気がしてきた。

ヒルベルト流とは、演繹手法の1つ。以下の公理(型)とmodus ponensだけを使って証明を行なう。
([a][b][i]だけという定義もたまに見る気がする。これはその3つに∧と∨の公理をくわえたもの)。

[a]φ⊃(ψ⊃φ)

[b](φ⊃(ψ⊃χ))⊃)((φ⊃ψ)⊃(φ⊃χ))

[c]φ⊃(ψ⊃φ∧ψ)

[d]φ∧ψ⊃φ

[e]φ∧ψ⊃ψ

[f]φ⊃φ∨ψ

[g]ψ⊃φ∨ψ

[h](φ⊃χ)⊃)((ψ⊃χ)⊃(φ∨ψ⊃χ))

[i](￢φ⊃￢ψ)⊃(ψ⊃φ)

■ メタ定理の証明
以下の証明パターンは頻出なので先に証明しておく。

[A]前提付加 φ⊃ψ|-χ⊃(φ⊃ψ)

(1)φ⊃ψ    [仮定]

(2)(φ⊃ψ)⊃(χ⊃(φ⊃ψ))    [公理a]

(3)χ⊃(φ⊃ψ)    [(1)(2)MP]

[B]前件と後件に前件を φ⊃ψ|-(χ⊃φ)⊃(χ⊃ψ)

(1)φ⊃ψ    [仮定]

(2)χ⊃(φ⊃ψ)    [メタ定理A]

(3)(χ⊃φ)⊃(χ⊃ψ)    [(2),公理b]

[C]三段論法 φ⊃ψ, ψ⊃χ|-φ⊃χ

(1)φ⊃ψ    [仮定]

(2)ψ⊃χ    [仮定]

(3)(φ⊃ψ)⊃(φ⊃χ)    [(2)メタ定理B]

(4)(φ⊃χ)    [(3)(1)MP]

[D]前件と後件に後件を φ⊃ψ|-(ψ⊃χ)⊃(φ⊃χ)

(1)φ⊃ψ    [仮定]

(2)(ψ⊃χ)⊃(φ⊃(ψ⊃χ))    [公理a]

(3)(φ⊃(ψ⊃χ))⊃((φ⊃ψ)⊃(φ⊃χ))    [公理b]

(4)(ψ⊃χ)⊃((φ⊃ψ)⊃(φ⊃χ))    [(2)(3)メタ定理C]

(5)[(ψ⊃χ)⊃(φ⊃ψ)]⊃[(ψ⊃χ)⊃(φ⊃χ)]    [(4)公理b]

(6)(ψ⊃χ)⊃(φ⊃ψ)    [(1)メタ定理A]

(7)(ψ⊃χ)⊃(φ⊃χ)    [(5)(6)MP]

■ 補助定理
必要な定理がいくつかあるので先に証明する。

[1]同一律 φ⊃φ

(1)φ⊃((φ⊃φ)⊃φ)    [公理a]

(2)(φ⊃(φ⊃φ))⊃(φ⊃φ)    [(1)と公理b]

(3)φ⊃(φ⊃φ)    [公理a]

(4)φ⊃φ    [(2)(3)MP]

[2]二重否定除去 ￢￢φ⊃φ

(1)￢￢φ⊃(￢￢￢￢φ⊃￢￢φ)    [公理a]

(2)(￢￢￢￢φ⊃￢￢φ)⊃(￢φ⊃￢￢￢φ)    [公理i]

(3)(￢φ⊃￢￢￢φ)⊃(￢￢φ⊃φ)    [公理i]

(4)￢￢φ⊃(￢￢φ⊃φ)    [(1)(2)(3)メタ定理C]

(5)￢￢φ⊃￢￢φ     [同一律]

(6)(￢￢φ⊃￢￢φ)⊃(￢￢φ⊃φ)    [(4)公理b]

(7)￢￢φ⊃φ    [(5)(6)MP]

[3]二重否定付加 φ⊃￢￢φ

(1)￢￢￢φ⊃￢φ    [二重否定除去]

(2)φ⊃￢￢φ    [(1)公理i]

[4]対偶の逆 (φ⊃ψ)⊃(￢ψ⊃￢φ)

(1)(￢￢φ⊃￢￢ψ)⊃(￢ψ⊃￢φ)    [公理i]

(2)ψ⊃￢￢ψ    [二重否定付加]

(3)(φ⊃ψ)⊃(φ⊃￢￢ψ)    [(2)メタ定理B]

(4)￢￢φ⊃φ    [二重否定除去]

(5)(φ⊃￢￢ψ)⊃(￢￢φ⊃￢￢ψ)    [(4)メタ定理D]

(6)(￢￢φ⊃￢￢ψ)⊃(￢ψ⊃￢φ)    [公理i]

(7)(φ⊃ψ)⊃(￢ψ⊃￢φ)    [(3)(5)(6)メタ定理C]

[5]∨から∨への変換 φ∨ψ⊃ψ∨φ

(1)φ⊃ψ∨φ    [公理g]

(2)ψ⊃ψ∨φ    [公理f]

(3)(φ⊃ψ∨φ)⊃((ψ⊃ψ∨φ)⊃(φ∨ψ⊃ψ∨φ))    [公理h]

(4)φ∨ψ⊃ψ∨φ    [(3)(2)(1)MP]

[6]MPみたいなやつ φ⊃((φ⊃ψ)⊃ψ)

(1)(φ⊃ψ)⊃(φ⊃ψ)    [同一律]

(2)((φ⊃ψ)⊃φ)⊃((φ⊃ψ)⊃ψ)    [(1)公理b]

(3)φ⊃[((φ⊃ψ)⊃φ)⊃((φ⊃ψ)⊃ψ)]    [(2)定理A]

(4)[φ⊃((φ⊃ψ)⊃φ)]⊃[φ⊃((φ⊃ψ)⊃ψ)]    [(3)公理b]

(5)φ⊃((φ⊃ψ)⊃φ)    [公理a]

(6)φ⊃((φ⊃ψ)⊃ψ)

[7]⊃から∨への変換 (φ⊃ψ)⊃(￢φ∨ψ)

(1)￢φ⊃￢φ∨ψ    [公理f]

(2)￢(￢φ∨ψ)⊃￢￢φ    [(1)公理i]

(3)￢(￢φ∨ψ)⊃φ    [(2)と二重否定除去とメタ定理A]

(4)φ⊃((φ⊃ψ)⊃ψ)    [MPみたいなやつ]

(5)￢(￢φ∨ψ)⊃((φ⊃ψ)⊃ψ)    [(3)(4)メタ定理A]

(6)((φ⊃ψ)⊃ψ)⊃(￢ψ⊃￢(φ⊃ψ))    [公理i]

(7)￢(￢φ∨ψ)⊃(￢ψ⊃￢(φ⊃ψ))    [(5)(6)メタ定理A]

(8)[￢(￢φ∨ψ)⊃￢ψ]⊃[￢(￢φ∨ψ)⊃￢(φ⊃ψ)]    [(7)公理b]

(9)ψ⊃￢φ∨ψ    [公理g]

(10)￢(￢φ∨ψ)⊃￢ψ    [(9)対偶の逆]

(11)￢(￢φ∨ψ)⊃￢(φ⊃ψ)    [(8)(10)MP]

(12)(φ⊃ψ)⊃(￢φ∨ψ)    [11公理i]

■ 排中律の証明
ここまでできればあとは一瞬。

[8]排中律 φ∨￢φ

(1)(φ⊃φ)⊃(￢φ∨φ)    [⊃から∨への変換]

(2)φ⊃φ    [同一律]

(3)￢φ∨φ    [(1)(2)MP]

(4)￢φ∨φ⊃φ∨￢φ    [∨から∨への変換]

(5)φ∨￢φ    [(3)(4)MP]