数理論理学(鹿島亮)5

自然演繹の完全性を証明する章

極大無矛盾集合を用いた証明をする

閉論理式の任意の集合Γ(有限集合でも無限集合でも良い)

任意の閉論理式φ

Γ ⊨ φ ならば Γ ⊢ φ

特にΓが空集合の場合は「φが恒真ならば仮定なしにφを導出することができる」になる

注釈

Γ ⊨ φ ⇔ Γ ⊢ φ

のことを完全性定理という場合もある

定義5.1.2 (矛盾・無矛盾) inconsistent

Γは任意の論理式の集合(有限集合でも無限集合でも良い)

Γ ⊢ ⊥であることを「Γは矛盾するという」

そうでないこと(すなわちΓ ⊬ ⊥であること)を「Γは無矛盾である」という

矛盾する集合の例

{φ∧ψ, ¬φ}

{φ, ψ, ¬(φ∧ψ)}

{¬∀xφ, ¬∃x¬φ}

これ難しい……

ドモルガンの法則だと思うけれど

教科書書いてあるじゃん！

命題論理のも合わせて、証明の方法がぱっと浮かばないので、暇な時にやりたい

矛盾する導出図を書く

補題5.1.3

論理式の集合Γに関して、以下の3条件は同値である

a Γは矛盾する

b どんな論理式φについてもΓ⊢φ

c ある論理式φが存在して、Γ⊢φかつΓ⊢¬φ

証明5.1.3

a ⇒ b

自然演繹に矛盾規則があることからいえる

詳しく一応書いてみる

Γは矛盾するとはΓ⊢⊥のことであった

Γ⊢⊥とは、

Γのある有限部分集合Γ'が存在して、「解消されていない仮定の集合がΓ'で、結論が⊥の導出図が存在すること」

そのような導出図において、矛盾規則を適用することで⊥からφが導ける

b ⇒ c

明らかである

詳しく一応書いてみる

どんな論理式φについてもΓ⊢φであるから

Γ⊢φもΓ⊢¬φも導ける

c ⇒ a

¬除去規則があることからいえる

詳しく一応書いてみる

ある論理式φが存在して、Γ⊢φ

Γのある有限部分集合Γ'が存在して、「解消されていない仮定の集合がΓ'で、結論がφの導出図が存在すること」

ある論理式φが存在して、Γ⊢¬φ

Γのある有限部分集合Γ''が存在して、「解消されていない仮定の集合がΓ''で、結論が¬φの導出図が存在すること」

二つの導出図をくっつけて、¬除去規則を適用することで⊥を導くことができる

このとき Γ⊢⊥となる

Γ', Γ''はΓの有限部分集合であるので、その和集合Γ'∪Γ''もΓの有限部分集合

なので、Γ'∪Γ'はΓの有限部分集合であり、解消されていない仮定の集合がΓ'∪Γ'で、結論が¬φの導出図が存在している

よってΓは矛盾する

補題5.1.4

論理式の集合Γと任意の論理式φに対して以下が成り立つ

1 Γ∪{φ}は矛盾する ⇔ Γ⊢¬φ

2 Γ∪{¬φ}は矛盾する ⇔ Γ⊢φ

証明5.1.4

1⇒

Γ∪{φ}⊢⊥とする

⊥を導く導出図において、

解消されていない仮定にφが存在する場合

¬導入規則を適用することで、φが仮定から解消され、¬φが得られる

よってΓ⊢¬φ がいえる

解消されていない仮定にφが存在しない場合

爆発律を適用することで Γ⊢¬φ がいえる

1⇐

Γ⊢¬φとする

仮定φと、¬除去規則からΓ∪{φ}⊢⊥がいえる

2⇒

Γ∪{¬φ}⊢⊥とする

⊥を導く導出図において、

解消されていない仮定に¬φが存在する場合

背理法を適用することで、¬φが仮定から解消され、φが得られる

よってΓ⊢φ がいえる

解消されていない仮定に¬φが存在しない場合

爆発律を適用することで Γ⊢¬φ がいえる

2⇐

Γ⊢φとする

仮定¬φと、¬除去規則からΓ∪{¬φ}⊢⊥がいえる

補題5.1.5

Γは論理式の任意の集合

φは任意の論理式

Γ∪{φ}、Γ∪{¬φ}の両方が矛盾するならば、Γも矛盾する

証明5.1.5

この両方が矛盾するならば、補題5.1.4(1⇒ 2⇒)より

Γ⊢¬φ かつ Γ⊢φ

補題5.1.3より、Γは矛盾する

補題5.1.6

記号

Γは論理式の任意の集合

φは任意の論理式

x,yは任意の変数記号

主張

気になったこと

例を探す

∃xφにyが現れる場合の反例

φをy≠xとする

Γにyが現れる場合の反例

y≠a ∈ Γ, φをa=xとする

証明5.1.6

方針

対偶を示す

証明

yがΓにも∃xφにも現れない場合

すると以下の導出図が、Γ∪{∃xφ}の有限部分集合から⊥を導くものになっている

…

…

∃xφ ⊥ 𝜜

⊥

よって、Γ∪{∃xφ}は矛盾することになる

メモ

yが∃xφに現れるなら、変数条件を満たさなくなるので∃除去ができない

つまり、∃除去ができない場合ある

yがΓか∃xφに現れる場合

が成り立つ

記号

Γは閉論理式の任意の集合

主張

Γが無矛盾ならば、Γのモデルが存在する

モデル存在定理を用いた完全性定理の証明

方針

対偶を示す

証明

Γ⊬φを仮定してΓ⊭φであることを示す

補題5.1.4(2)より、Γ∪{¬φ}は無矛盾である

モデル存在定理より、Γ∪{¬φ}のモデルMが存在する

「Γ∪{¬φ}のモデルM」はΓの要素をすべて真にして、¬φを真にする。すなわちφを偽にする

このMの存在はΓ⊭φを表している

定理5.1.7の逆は演習問題

系5.1.8 閉論理式の集合に関する二条件

「無矛盾である」「モデルを持つ」は同値である

証明

定理5.1.7と定理5.1.7の逆が成り立つことから

定義「Γの未使用変数は無限である」

Γを閉論理式の任意の集合とする

Γ中に出現しない変数記号が無限個であること

Γの未使用変数は無限である例

Γが有限集合の場合、Γの未使用変数は無限である

1つの論理式が使える変数の個数は有限個であるので、Γが有限集合の場合は変数の個数は高々有限個になる

Γの未使用変数は有限である例

変数記号は可算無限個ある

そのすべてを並べて以下のように呼ぶ

x1,x2,x3…… (5.1)

この列の最初のn個の変数記号x1,x2,x3……,xnを使って、「対象領域の要素の個数がn個以上である」という意味の閉論理式を作ることができる

それをεnとよぶ

例 ε3

∃x1∃x2∃x3((¬(x1=x2)∧¬(x1=x3))∧¬(x2=x3))

無限集合{ε1,ε2,ε3,…}の未使用変数は0個である

定理5.2.1 モデル存在定理・変数条件付き

記号

Γは閉論理式の任意の集合

主張

Γが無矛盾でΓの未使用変数は無限であるならば、Γのモデルが存在する

記号

φは任意の論理式

はφ中の変数記号

φ# はφ中の変数記号xi(i=1,2,…)の出現をそれぞれx2iに書き換えた論理式

例 ε3#

∃x2∃x4∃x6((¬(x2=x4)∧¬(x2=x4))∧¬(x4=x6))

Γ# は集合Γのすべての要素に# を施した集合

流れ

定理5.1.7の文面のΓをいったんΓ# に変換して定理5.2.1を適用することで、定理5.1.7が示される

示したいこと

ア 閉論理式の集合Γが無矛盾ならば、Γ# も無矛盾である

イ Γ# の未使用変数は無限である

ウ Γ# のモデルは必ずΓのモデルにもなる

証明イ

イは明らか

Γ# の中には、列(5.1)の奇数番目の変数記号x1,x3,x5,…が出現しないため

ア・ウ 証明のためにの定理

どんな閉論理式φについても以下が成り立つ

φ ⊢ φ# かつ φ# ⊢ φ (5.3)

これの証明は演習問題

証明ア

方針

対偶を示す

Γ# が矛盾するなら、Γが矛盾する

Γ# が矛盾するとき、Γ# の有限部分集合{γ1#, γ2#,…,γn#}から⊥を導出することができる

ところで(5.3)から、γi ⊢ γi#である

よって、{γ1, γ2,…,γn}から、⊥が導出できる

証明ウ

(5.3)より γi# ⊢ γi である

したがって、健全性定理からγi#を真にするどんなストラクチャーもγiを真にする

よって、Γ# のモデルは必ずΓのモデルにもなる

主張

Γが無矛盾ならば、Γのモデルが存在する

証明

Γが無矛盾と仮定する

アより、Γ#は無矛盾である

イより、Γ#の未使用変数記号は無限である

定理5.2.1 より、Γ#のモデルが存在する

ウより、Γ#のモデルはΓのモデルにもなる

証明終了

定理5.2.1 モデル存在定理・変数条件付きの証明が目標になる

モデル存在定理・変数条件付き⇒モデルの存在定理⇒完全性定理

5.3極大無矛盾集合

FとBは変数記号の任意の集合

ただし、F∩B = ∅ を満たすものとする

FとBを固定して議論を進める

定義

論理式の集合 FormulaF,B = {φ | φは論理式で、FVar(φ)⊆F, BVar(φ)⊆B}

自由出現する変数をF、束縛出現する変数をBにそれぞれ制限した論理式全体の集合

集合全体は集合にならないみたいだけど

論理式って有限の文字列だし、自然数といい感じに対応させることができて、集合になりそうな感じはする

項の集合 TermF = {t | tは項で、Var(t)⊆F}

変数をFだけに制限した項全体の集合

この定義からすぐに述べられること

tはφ中のxに代入可能

ことのことはFとBに共通の記号かないことからわかる

証明的なやつ

(FVar(φ)\{x})∪Var(t) ⊆ F

FVar(φ)\{x} = FVar(∀xφ) ⊆ F

Var(t)⊆F かつ FVar(φ)\{x} ⊆ Fであるから、 (FVar(φ)\{x})∪Var(t) ⊆ F

BVar(φ)⊆B

BVar(φ) ⊆ BVar(φ)∪{x} = BVar(∀xφ) ⊆ B

定義5.3.1 極大 存在証拠

ΓはFormulaF,Bに関して極大である

任意の論理式φに対して次が成り立つ

φ∈FormulaF,B ならば φ∈Γまたは¬φ∈Γ

ΓはTermFの存在証拠を持つ

矛盾していますが……

だから、KeySetF,Bが無矛盾であるという条件があるのかもしれない

定義5.3.2 KeySetF,B

ΓをFormulaF,Bの任意の部分集合とする

以下の三条件が成り立つことをΓはKeySetF,Bであるという

1 Γは無矛盾である

2 ΓはFormulaF,Bに関して極大である

3 ΓはTermFの存在証拠を持つ

1,2の条件は極大無矛盾と呼ばれる概念に相当する

補題5.3.3 KeySetF,Bの性質

記号

1~4において

φ,ψはFormulaF,Bの任意の要素

5,6において

xはBの任意の要素

φは∀xφ∈FormulaF,Bとなる任意の論理式

ΓがKeySetF,Bならば以下が成り立つ

1 φ∧ψ ∈ Γ ⇔ φ∈Γ かつ ψ∈Γ

2 φ∨ψ ∈ Γ ⇔ φ∈Γ または ψ∈Γ

3 φ→ψ ∈ Γ ⇔ φ∉Γ または ψ∈Γ

4 ¬φ ∈ Γ ⇔ φ∉Γ

1⇒

φ∧ψ ∈ Γとする

背理法

φ∈Γ でないとする

ΓはKeySetF,Bであるから、FormulaF,Bに関して極大である

よって、¬φ∈Γとなる

しかし{φ∧ψ,¬φ}は矛盾する

これはΓの無矛盾性に反する

よってφ∈Γ である

同様にψ∈Γであるといえる

1 ⇐

φ∈Γ かつ ψ∈Γとする

背理法

φ∧ψ∈Γ でないとする

Γの極大性から¬(φ∧ψ)∈Γとなる

しかし{φ,ψ,¬(φ∧ψ)}は矛盾する

これはΓの無矛盾性に反する

よってφ∧ψ∈Γ である

2 ⇒

φ∨ψ ∈ Γ とする

背理法

φ∈Γ でも ψ∈Γでもないとする

Γの極大性から¬φ∈Γかつ¬ψ∈Γとなる

しかし{φ∨ψ,¬φ,¬ψ}は矛盾する

これはΓの無矛盾性に反する

よってφ∈Γまたはψ∈Γである

2 ⇐

φ∈Γ または ψ∈Γとする

φ∈Γであるとき

背理法

φ∨ψ ∈ Γでないとする

Γの極大性から¬(φ∨ψ) ∈ Γとなる

しかし{φ, ¬(φ∨ψ)}は矛盾する

これはΓの無矛盾性に反する

よってφ∨ψ ∈ Γである

ψ∈Γであるときも同様に証明する

3 ⇒

φ→ψ ∈ Γ を仮定する

(φ∉Γ または ψ∈Γ) でないとする

つまり、φ∈Γ かつψ∉Γとする

Γの極大性から¬ψ∈Γとなる

しかし{φ→ψ, φ, ¬ψ}は矛盾する

これはΓの無矛盾性に反する

よってφ→ψ ∈ Γ である

3 ⇐

φ∉Γ または ψ∈Γ を仮定する

φ∉Γ である場合

φ→ψ ∈ Γ でないとする

Γの極大性から¬(φ→ψ)∈Γ, ¬φ∈Γとなる

しかし{¬(φ→ψ), ¬φ}は矛盾する

これはΓの無矛盾性に反する

よって、φ→ψ ∈ Γ

ψ∈Γである場合

φ→ψ ∈ Γ でないとする

Γの極大性から¬(φ→ψ)∈Γとなる

しかし{ψ, ¬(φ→ψ)} は矛盾する

これはΓの無矛盾性に反する

φ→ψ ∈ Γである

4 ⇒

¬φ ∈ Γと仮定する

φ∉Γ でないとする。

つまりφ∈Γ

しかし{¬φ, φ} は矛盾する

これはΓの無矛盾性に反する

φ∉Γである

4 ⇐

φ∉Γと仮定する

¬φ ∈ Γでないとする

つまり¬φ ∉ Γ

Γの極大性から¬φ∈Γ, φ ∈ Γとなる

しかし{¬φ, φ} は矛盾する

これはΓの無矛盾性に反する

¬φ ∈ Γ

5 ⇒

これはΓの無矛盾性に反する

5 ⇐

∀xφ ∉ Γを仮定する

Γの極大性より¬∀xφ ∈ Γ

¬∃x¬φ ∈ Γと仮定する

ここで、{∀xφ, ¬∃x¬φ}は矛盾する

これはΓの無矛盾性に反する

¬∃x¬φ ∉ Γ

よってΓの極大性により∃x¬φ ∈ Γ

であった。今まではφ ∈ Γが属さないから¬φ ∈ Γというパターンが多かったが、¬φ ∈ Γが属さないからφ ∈ Γということも当然言える

6 ⇒

6 ⇐

∃xφ ∉ Γと仮定する

∃xφ ∉ Γなので、極大性から¬∃xφ ∈ Γ

ここで、¬∀x¬φ∈ Γであると仮定してみる

{¬∃xφ, ¬∀x¬φ}は矛盾する(はず……な)ので、Γの無矛盾性に反する。

したがって、¬∀x¬φ ∉ Γ。極大性より∀x¬φ ∈ Γ

これはΓの無矛盾性に反する。

5 ⇐をそのまま証明する

このとき、∀xφ ∉ Γと仮定する。

極大性より¬∀xφ ∈ Γ

¬∃x¬φ ∈ Γと仮定する

{¬∀xφ, ¬∃x¬φ}は矛盾する(はず)。

Γの無矛盾性に反するので、¬∃x¬φ ∉ Γと言える

Γの極大性より∃x¬φ ∈ Γ

よって∀xφ ∉ Γではなかった

つまり∀xφ ∈ Γ

6 ⇐をそのまま証明する

∃xφ ∈ Γ でない、すなわち∃xφ ∉ Γと仮定する

極大性より¬∃xφ ∈ Γ

ここで¬∀x¬φ∈ Γであると仮定する

しかし{¬∃xφ, ¬∀x¬φ}は矛盾する(はず)ので、これはΓの無矛盾性に反する。

よって、¬∀x¬φ ∉ Γ

極大性より ∀x¬φ ∈ Γ

よって、∃xφ ∈ Γ

補題5.3.4 KeySetの構成

Γが以下の3条件を満たすとき

Γ ⊂ FormulaF,B

Γは無矛盾

Fの要素でΓに現れない変数記号が無限個ある

次の2条件を満たす集合Γ+が存在する

Γ ⊆ Γ+ ⊆ FormulaF,B

Γ+はKeySetF,Bである

証明

Γをうまく膨らませていくと求めるΓ+が得られることを示す

FormulaF,Bは可算無限集合である

論理式全体は可算無限集合になるので、その部分集合であるFormulaF,Bも高々可算の集合になる

FormulaF,Bの要素を列挙する

φ1, φ2, φ3, φ4,…… (5.4)

FormulaF,Bを一意に列挙することは可能か？

論理式は文字列なので、辞書順でソートして列挙していけそう

a,aa,ab,ac,…az,aaa,……ってなっちゃうか

可算無限個のものだし、文字数でソートして、同じ文字数なら辞書順で列挙するとかの方がいいのかな？

a,b,c,…,z,aa,ab,…az,ba……

0→A

1→B

2→C

3→A∨B

4→A∨C

そして論理式の集合の無限列 Γ0 ⊆ Γ1 ⊆ Γ2 ⊆… を次で定義する

Γ0 = Γ

Γi+1

= Γi

if Γi∪{φi+1}が矛盾するとき

= Γi∪{φi+1}

else if Γi∪{φi+1}が無矛盾で、φiが∃論理式でないとき

else if Γi∪{φi+1}が無矛盾で、φiが∃xψという形(∃論理式)あるとき

y はΓi∪{∃xψ}に出現しない変数記号をFの中から毎回新しく持ってくる

※始めにΓ0に現れないFの要素が無限個あり、各jでΓjからΓj+1を作る際には有限個の変数記号しか増えていないので、条件を満たす変数記号yが必ず存在する

このように定義された列の無限和をΓ+とする

Γ+が題意の条件を満たすことを示す

Γ ⊆ Γ+ ⊆ FormulaF,B であること

これはΓ+の構成方法から明らか

Γ+はKeySetF,Bである

すなわち

Γ+は無矛盾である

Γ+はFormulaF,Bに関して極大である

Γ+はTermFの存在証拠を持つ

Γ+は無矛盾である

次のことが成り立つ

任意のi≥0について、Γiは無矛盾である (5.5)

証明(数学的帰納法)

Γ0は定理の前提より無矛盾である

Γkが無矛盾ならばΓk+1が無矛盾であることは、Γk+1の定義と補題5.1.6から成り立つ

Γk+1は定義から以下の3通りに分けれる

Γk+1 = Γk

Γkは無矛盾であるので、Γk+1も無矛盾である

Γk+1 = Γk∪{φk+1}

このとき、Γk∪{φk+1}は無矛盾であるので、Γk+1も無矛盾である

φk+1は∃xψという形である

仮にΓ+は矛盾すると仮定する

このときΓ+ ⊢ ⊥であるから、解消されていない論理式 であるΓ+ の有限部部分集合{γ1,γ2,…γn}が存在して、それらから⊥を導く導出図が存在する

γ1,γ2,…γnはΓ+の要素なので、それぞれの論理式は適当なΓjの要素である

mを十分大きくとれば、{γ1,γ2,…γn} ⊆ Γm となる

するとΓm ⊢ ⊥ つまり、Γmは矛盾することになる

これは(5.5)に反する。

よって、Γ+は矛盾していない

Γ+はFormulaF,Bに関して極大である

ψをFormulaF,Bの任意の要素とする

ψと¬ψのどちらもΓ+に入っていないと仮定する

論理式列 (5.4) の中のm番目とn番目がそれぞれψ, ¬ψであるとする

ψと¬ψどちらもΓ+に入らないなら、

Γm-1∪{ψ} と Γn-1∪{¬ψ} が両方矛盾している

したがって、k = max(n,m)とすると、Γk-1∪{ψ}, Γk-1∪{¬ψ} が両方とも矛盾することになる

補題5.1.5により、Γk-1が矛盾する

これは(5.5)に反する

よって、ψと¬ψのどちらかはΓ+に入っている

Γ+はTermFの存在証拠を持つ

∃xψを任意の∃論理式とする。

仮定∃xψ ∈ Γ+からあるmについて∃xψ ∈ Γm である

また ∃xψ はFormulaF,Bの要素なので、論理式列(5.4)のn番目に登場するとする

k = max(m,n-1)とするとΓkが矛盾することになるが、これは(5.5)に反する

k=m≥n-1のとき

Γn-1∪{∃xψ}で矛盾するので、Γn = Γn-1と定義される

しかし、仮定よりあるmについて∃xψ ∈ Γm であった

よって Γk = Γm ⊇ Γn-1∪{∃xψ} なので、 Γkは矛盾してしまう

k = n-1>m のとき

仮定よりあるmについて∃xψ ∈ Γm である

Γn-1∪{∃xψ}は矛盾するので、Γn = Γn-1と定義される

しかし、 Γn-1 ⊇ Γm ⊇ {∃xψ}なので、Γn-1 = Γn-1∪{∃xψ}

よって、Γk = Γn-1 は矛盾してしまう

5.4モデル存在定理

(再掲)定理5.2.1 モデル存在定理・変数条件付き

記号

Γは閉論理式の任意の集合

主張

Γが無矛盾でΓの未使用変数は無限であるならば、Γのモデルが存在する

証明

証明に使う記号

Γは閉論理式の任意の集合

BはΓ中に出現する変数記号全体の集合

Γは閉論理式なので、そこに出現する変数記号は全て束縛出現である

FはΓ中に出現しない変数記号全体

M ストラクチャー

証明の中身

F,Bに対して、補題5.3.4を適用すると、

Γ+が得られる

Γ+は Γ ⊆ Γ+ ⊆ FormulaF,B かつ Γ+はKeySetF,Bである

Γ+を使ってストラクチャーMを定義する

ストラクチャーM を定めるのに決める必要があるもの

対象領域 D

定数記号の解釈

zero,one,two, omega, unity, rt

関数記号の解釈

⊕, ⊙, ⊗,suc

= 以外の述語の解釈

⧀, P, Q, R

命題記号の真理値

対象領域 D

TermF上の2項関係 ~ を次で定義する

s ~ t ⇔ (s=t) ∈ Γ+

これは同値関係になる(演習問題)

そしてTermFの~による商集合TermF/~を対象領域Dとする

〘t〙= { s | s∈TermsF かつ t~s }

というように項tを代表元とする同値類を〘t〙と書く

D = { 〘t〙 | t∈TermsF }

TermFそのものをモデルとして思いたいが、そのままだと=が困るから~で割って考える

以上の定義から、TermsFの任意の要素s,tに関して以下が成り立つ

〘s〙 = 〘t〙 ⇔ ( (s=t) ∈ Γ+) (5.7)

証明

〘s〙 = 〘t〙⇒ ( (s=t) ∈ Γ+)

t ∈〘t〙である

2項関係 ~ の定義より t~t ⇔ (t=t) ∈ Γ+

(t=t) ∈ Γ+であることは成り立つ。よってt~tである

∀x(x=x)∈Γ+であることから、5 ⇒より(t=t)∈Γ+

∀x(x=x)∈Γ+であることは、¬∀x(x=x)∈Γ+であるとすると、Γ+が矛盾することから極大性と無矛盾性から示せる

t∈TermsF かつ t~t なので、t ∈〘t〙

仮定より〘s〙 = 〘t〙であるから、t ∈〘s〙

同値類の定義より、t∈TermsF かつ t~sよって、t~sがいえる。

t~s ⇔ (s=t) ∈ Γ+だったので、証明終了

( (s=t) ∈ Γ+) ⇒〘s〙 = 〘t〙

( (s=t) ∈ Γ+) を仮定して、u ∈〘s〙⇒ u ∈〘t〙とu ∈〘t〙⇒ u ∈〘s〙を証明する必要がある

〘s〙 = 〘t〙 は　〘s〙⊆〘t〙かつ〘t〙⊆〘s〙の略記

u ∈〘s〙⇒ u ∈〘t〙

u ∈〘s〙であるとき、 u∈TermsF かつs~u である。

よって、(s=u) ∈ Γ+となる

{(s=t), (s=u)} ∈ Γ+であるから、極大性と無矛盾性から、(t=u)∈ Γ+が示せる

よって、u ~ t である。u∈TermsFであったので、u ∈〘t〙となる

よって〘s〙⊆〘t〙

〘t〙⊆〘s〙

同様に証明可能

定数記号の解釈

two^M = 〘two〙(5.8)

three^M = 〘three〙

……

関数記号の解釈

suc^M(〘t〙) = 〘suc(t)〙

〘s〙⊗^M〘t〙= 〘s⊗t〙

〘s〙⊕^M〘t〙= 〘s⊕t〙

〘s〙⊙^M〘t〙= 〘s⊙t〙

D上の関数として矛盾なく定義されていることを示すために以下の内容を証明する必要がある

演習問題でやる

述語記号の解釈

Q^M(〘t〙)=真 ⇔ Q(t) ∈ Γ+

〘s〙⧀^M〘t〙=真 ⇔〘s⧀t〙∈ Γ+

P^M,R^M も同様.

D上の述語として矛盾なく定義されていることを示すために以下の内容を証明する必要がある

演習問題でやる

命題記号の解釈

各命題記号X(∈{A,B,C)について、

M(X) = 真 ⇔ X ∈ Γ+

以上がストラクチャーMの定義

これがΓのモデルを示すために、任意の閉論理式φについて

φ ∈ Γ+ ならば M(φ) = 真 (5.16)

が成り立つことを示す。

しかしこれをφの複雑さに関する帰納法で扱うのは難しい。

例

しかし、このような名前〘t〙などを含んだ論理式は Γ+の要素ではない。

tという項を含んだ論理式は Γ+の要素だったりはする。

Γ+はFormulaF,Bのサブセットであり、FormulaF,Bは論理式の集合のサブセットである

ここでいう、論理式はD拡大論理式ではない論理式。

名前を含んだ論理式はΓ+ の要素でないから、帰納法の仮定として使えない。

そこで(5.16)を拡張して、任意の項sと任意の論理式φに対して次の命題を帰納法で示すことにする。

記号

x1,x2,…,xnはBの任意の要素で互いに異なる変数記号

t1,t2,…,tnはTermFの任意の要素

sは任意の項

φは任意の論理式

主張

以下の条件を満たすなら、(ア)、(イ)が成り立つ

Var(s) ⊆ {x1,x2,…,xn}

FVar(φ) ⊆ {x1,x2,…,xn}

BVar(φ) ⊆ B

(ア)

M(s^♣︎) = 〘s^♡〙

(イ)

M(φ^♣︎)= 真 ⇔ (φ^♡ ∈ Γ+)

ただし

アをsの長さに関する帰納法で証明する

イをφの複雑さに関する帰納法で証明する

目標の(5.1.6)はイの⇐の特別な場合(n=0)なので、これによって証明が完了する

アの証明

sが定数記号のとき

たとえばtwoのとき

M(two^♣︎) = M(two)

定数記号なので代入しても変わらない

= two^M

ストラクチャーの定義より

=〘two〙

Mのtwoの解釈の定義(5.8)より

=〘two^♡〙

定数記号なので代入しても変わらない

他の定数記号も同様に証明する

sが変数記号xiのとき

M(xi^♣︎) = M(〘ti〙)

代入した結果(♣︎の定義より)

= 〘ti〙

ストラクチャーの定義(拡大閉項の値の定義)より

tがDの要素の名前のとき、M(t)はその要素である

= 〘xi^♡〙

♡の定義より

i=0からi=nまで同様に証明可能

sが関数記号を含む項

たとえば t⊗u のとき

M((t⊗u)^♣︎) = M((t^♣︎)⊗(u^♣︎))

代入

= M(t^♣︎) ⊗^M M(u^♣︎)

ストラクチャーの定義より

= 〘t^♡〙⊗^M 〘u^♡〙

帰納法の仮定より

(t⊗u)^♣︎ よりもt^♣︎、u^♣︎は文字数が少ないので成り立つ

=〘(t^♡)⊗(u^♡)〙

関数記号⊗の解釈(5.9)より

= 〘(t⊗u)^♡〙

代入の性質？より

他の関数記号の場合も同様に証明できる

よってアが示される

イの証明

φ がt=uのとき

M((t=u)^♣︎) = 真 ⇔ M((t)^♣︎ = (u)^♣︎) = 真

代入の分配

⇔ M(t^♣︎) = M(u^♣︎)

真理値の定義(3.2.4)より

⇔〘t^♡〙=〘u^♡〙

アより

⇔ ((t^♡) = (u^♡)) ∈ Γ+

(5.7)

⇔ (t = u)^♡ ∈ Γ+

代入を括った

φ が=以外の述語記号からなる原始論理式

たとえばQ(t)のとき

M(Q(t)^♣︎) = 真 ⇔ M(Q(t^♣︎)) = 真

♣︎をtに直接代入する形にする

⇔Q^M(M(t^♣︎)) = 真

ストラクチャーの定義

⇔Q^M(〘t^♡〙) = 真

アより

⇔Q(t^♡)∈ Γ+

5.12述語記号の解釈より

⇔Q(t)^♡∈ Γ+

それ以外の場合も同様に証明できる

φ が命題記号たとえばAのとき

M(A^♣︎) = 真

⇔ M(A) = 真

代入しても変わらないため

⇔ A ∈ Γ+

5.15 命題記号の解釈より

⇔ A^♡ ∈ Γ+

代入しても変わらないため

φが⊥のとき

ストラクチャーにおける真理値定義3.2.4よりM(⊥) = 偽

一方Γ+無矛盾であることから、⊥ ∉ Γ+である

したがって、M(⊥) = 偽 ⇔ ⊥ ∉ Γ+

よって、M(⊥) = 真 ⇔ ⊥ ∈ Γ+

φが複合論理式

φがψ∧ρのとき

M((ψ∧ρ)^♣︎) = 真

⇔ M((ψ)^♣︎∧(ρ)^♣︎) = 真

代入の分配

⇔M(ψ^♣︎) = 真　かつ　M(ρ^♣︎) = 真

真理値の定義

⇔ψ^♡∈Γ+ かつ　ρ^♡∈Γ+

帰納法の仮定より

⇔(ψ^♡∧ρ^♡)∈Γ+

補題5.3.3(1)

⇔((ψ∧ρ)^♡)∈Γ+

φがψ∨ρのとき

M((ψ∨ρ)^♣︎) = 真

⇔ M((ψ)^♣︎∨(ρ)^♣︎) = 真

代入の分配

⇔M(ψ^♣︎) = 真　または　M(ρ^♣︎) = 真

真理値の定義

⇔ψ^♡∈Γ+ または　ρ^♡∈Γ+

帰納法の仮定より

⇔(ψ^♡∨ρ^♡)∈Γ+

補題5.3.3(2)

⇔((ψ∨ρ)^♡)∈Γ+

φがψ→ρのとき

M((ψ→ρ)^♣︎) = 真

⇔ M((ψ)^♣︎→(ρ)^♣︎) = 真

代入の分配

⇔M(ψ^♣︎) = 偽　または　M(ρ^♣︎) = 真

真理値の定義

⇔ψ^♡∉Γ+ または　ρ^♡∈Γ+

帰納法の仮定より

⇔(ψ^♡→ρ^♡)∈Γ+

補題5.3.3(3)

⇔((ψ→ρ)^♡)∈Γ+

φが¬ψのとき

M(¬ψ^♣︎) = 真

⇔M(ψ^♣︎) = 偽

真理値の定義より

⇔ψ^♡∉Γ+

帰納法の仮定より

⇔(¬ψ^♡)∈Γ+

補題5.3.3(4)

φが∀xψのとき

M(∀xψ^♣︎) = 真

⇔M((∀xψ)^♣︎-) = 真

♣︎-は♣︎からxに対する代入を取り除いたもの

真理値の定義より

帰納法の仮定より

♡-は♡からxに対する代入を取り除いたもの

対象領域の定義より、Dの要素である同値類〘t〙の要素はTermF

⇔(∀xψ^♡-)∈Γ+

補題5.3.3(5)

⇔(∀xψ^♡)∈Γ+

φが∃xψのとき

M(∃xψ^♣︎) = 真

⇔M(∃xψ^♣︎-) = 真

♣︎-は♣︎からxに対する代入を取り除いたもの

真理値の定義より

帰納法の仮定より

♡-は♡からxに対する代入を取り除いたもの

対象領域の定義より、Dの要素である同値類〘t〙の要素はTermF

⇔(∃xψ^♡-)∈Γ+

補題5.3.3(6)

⇔(∃xψ^♡)∈Γ+

完全性定理・モデル存在定理の応用の一つ

定義5.5.1 コンパクト性定理

記号

Γは閉論理式の任意の無限集合

主張

Γのすべての有限部分集合がモデルを持つならば、Γ自身もモデルを持つ

その逆も成り立つ

証明

対偶を証明する

Γはモデルを持たない

⇔ Γは矛盾する

系5.1.8より

⇔ Γのある有限部分集合が矛盾

矛盾の定義より

Γは矛盾するとは、Γのある有限部分集合(Γ'と呼ぶ)から⊥を導くことができること同値

このとき矛盾の定義から、Γ'のある有限部分集合としてΓ'を取れば、⊥を導くことができる

よって、Γ'すなわちΓのある有限部分集合も矛盾する

⇔ Γのある有限部分集合はモデルを持たない

系5.1.8より

コンパクト性定理の文面には自然演繹における証明可能性⊢の概念は登場せず、論理式とその意味についてだけ述べている

モデル理論など証明体系に興味のない分野でよく使われる

コンパクト性定理は論理式の表現能力や論理式によって規定されるストラクチャーの性質を分析する際の重要な道具となる

定理5.2.2 次の条件を任意のストラクチャーMに対して成り立たせるような閉論理式φは存在しない

主張

M(φ) ⇔ Mの対象領域の要素数は有限である

記号

εiは次のような論理式

M(εn) = 真 ⇔ Mの対象領域の要素数はn個以上である

証明

このようなφが存在すると仮定する

いま論理式の無限集合

{φ, ε1, ε2, ε3,…}　(5.18)

を考える

この集合の全ての有限部分集合はモデルを持つ

例

{φ, ε2, ε7, ε25}のモデルとしては、対象領域の要素数が25のストラクチャーを持ってくればよい

一般にεの添え字の一番大きい数が対象領域の要素数となるストラクチャーを持ってくればいい

したがって、コンパクト性定理よりこの集合はモデルを持つ

しかしそれは不可能である

なぜなら対象領域の要素数に関する条件

「有限」、「1個以上」、「2個以上」……

「1個以上」、「2個以上」……だけならば、対象領域の要素数が無限個で満たせる

をすべて同時に満たすようなストラクチャーは存在しないからである

よって最初の仮定が間違っているので、このようなφが存在しない

M(φ) ⇔ Mの対象領域の要素数は無限であるの証明

¬φも閉論理式となる

M(¬φ) ⇔ Mの対象領域の要素数は有限である

となる

¬φは存在しない

φは存在しない

任意のストラクチャーMに対して成り立たせるような閉論理式¬φは存在しないとき、

φも存在しないといえる？

言えるみたいです。

モデルが存在するしない。の定義とかを使ったりすればいいみたい

一般に¬じゃなくて複合論理式に対して、部分論理式？にいえるかな？

ψ∧ρの少なくともどっちかψ,ρは存在しない論理式

対象領域の要素数が無限個のときにモデルを持つ論理式の集合は{ε1, ε2, ε3,…}のように考えることができる。が、対象領域の要素数が有限個のときにモデルを持つ論理式の集合を考えるのはできないらしい。

メモ。無限論理と一階述語論理の関係とかが関係しているらしい

コンパクト性定理を利用すれば逆にこういうことを表現する論理式は作れるということも、その論理式を具体的に構成せずに証明できるだろうか？

あんまりないらしい

定理5.5.3

群論への応用

飛ばします

コンパクト性定理を数理論理学以外の数学へ応用する例としては、超準解析が有名

演習問題1

https://scrapbox.io/files/68114c4f4520741c1c7a50e1.jpeg

https://scrapbox.io/files/68114c53da666a667ef6fc2a.jpeg

https://scrapbox.io/files/68114c56c46235c59f6cfd01.jpeg

演習問題2

定理5.1.7の逆を示す

主張

Γのモデルが存在すればΓは無矛盾である

記号

Γは閉論理式の任意の集合

証明

Γのモデルが存在すると

Γのすべての要素φに対してM(φ) = 真となるストラクチャーMが存在する

ここで、Γは矛盾すると仮定する

すなわち、Γのあるの有限部分集合Γ'から⊥が導ける

健全性定理(Γ' ⊢ ⊥ ならば Γ' ⊨ ⊥)より

Γ' ⊨ ⊥ がなりたつ

すべてのγ ∈ Γ' に対してM(γ) = 真 (Γ'がモデルを持つ)　ならば M(⊥) = 真

ΓのモデルはΓ'のモデルであるので、Γ'のモデルが存在する

よって M(⊥) = 真

これは⊥の真理値の定義に反する

よって、Γは矛盾しない

演習問題3

定理5.2.1を用いた定理5.1.7の証明中に挙げられた性質(5.3)が任意の閉論理式φについて成り立つことを証明せよ

-----------↓あんまり納得してない時の記述のメモ-----------------------------------------

主張

φ⊢φ# かつ φ#⊢φ

記号

φは任意の閉論理式

φ# はφ中の変数記号xi(i=1,2,…)の出現をそれぞれx2iに書き換えた論理式

証明

メモ

閉論理式に対して直接、複雑さの帰納法を回すのができないので、いったん論理式全体に対して考えるっぽい？

完全性定理とかもそう

論理記号の個数に関する帰納法で閉論理式に対して頑張ることもできるらしい？

任意の論理式ψ対して、次の主張を証明をする

(ψ)♣︎ ⊢ (ψ#)♡ かつ (ψ#)♡ ⊢ (ψ)♣︎

ψが閉論理式のとき、求める5.3になる

kは十分に大きく取る

(ψ)♣︎ ⊢ (ψ#)♡について、論理式の複雑さによる帰納法で証明する

ψが原子論理式の場合

ψが単独の命題記号や⊥など、変数が出現しない場合

(ψ)♣︎ は ψと変わらない

(ψ#)♡はψ#と変わらない

さらにψ#はψと変わらない

よって、

(ψ)♣︎ ⊢ (ψ#)♡

⇔ ψ ⊢ ψ

これは明らかに成り立つ

ψ中に変数x1,x2,…xnが出現する場合

kはnよりも大きい

よって、(ψ)♣︎ は (ψ#)♡ と変わらない

したがって、(ψ)♣︎ ⊢ (ψ#)♡ が成り立つ

ψが複合論理式の場合

ψが¬ρのとき

ρはψよりも複雑さが小さいので、帰納法の仮定より(ρ)♣︎ ⊢ (ρ#)♡ が成り立つ

(ψ)♣︎ = (¬ρ)♣︎ = ¬(ρ♣︎)

(ρ)♣︎ ⊢ (ρ#)♡ ならば ¬((ρ)♣︎) ⊢ ¬((ρ#)♡)

よって帰納法の仮定より、(ψ)♣︎から¬((ρ#)♡) が導出できる

¬((ρ#)♡) = (¬(ρ#))♡ = ((¬ρ)#)♡ = (ψ#)♡

よって、(ψ)♣︎から(ψ#)♡が導出できる

ψがρ1∧ρ2のとき

ρ1はψよりも複雑さが小さいので、帰納法の仮定より(ρ1)♣︎ ⊢ (ρ1#)♡ が成り立つ

ρ2はψよりも複雑さが小さいので、帰納法の仮定より(ρ2)♣︎ ⊢ (ρ2#)♡ が成り立つ

(ψ)♣︎ = (ρ1∧ρ2)♣︎ = ρ1♣︎∧ρ2♣︎

(ρ1)♣︎ ⊢ (ρ1#)♡ かつ (ρ2)♣︎ ⊢ (ρ2#)♡ ならば ρ1♣︎∧ρ2♣︎ ⊢ (ρ1#)♡∧(ρ2#)♡

よって帰納法の仮定より、 ρ1♣︎∧ρ2♣︎ ⊢ (ρ1#)♡∧(ρ2#)♡

(ρ1#)♡∧(ρ2#)♡ = …… = ((ρ1∧ρ2)#)♡

よって、(ψ)♣︎から(ψ#)♡が導出できる

ψがρ1∨ρ2のとき

ρ1はψよりも複雑さが小さいので、帰納法の仮定より(ρ1)♣︎ ⊢ (ρ1#)♡ が成り立つ

ρ2はψよりも複雑さが小さいので、帰納法の仮定より(ρ2)♣︎ ⊢ (ρ2#)♡ が成り立つ

(ψ)♣︎ = (ρ1∨ρ2)♣︎ = ρ1♣︎∨ρ2♣︎

(ρ1)♣︎ ⊢ (ρ1#)♡ かつ (ρ2)♣︎ ⊢ (ρ2#)♡ ならば ρ1♣︎∨ρ2♣︎ ⊢ (ρ1#)♡∨(ρ2#)♡

よって帰納法の仮定より、 ρ1♣︎∨ρ2♣︎ ⊢ (ρ1#)♡∨(ρ2#)♡

(ρ1#)♡∨(ρ2#)♡ = …… = ((ρ1∨ρ2)#)♡

よって、(ψ)♣︎から(ψ#)♡が導出できる

ψがρ1→ρ2のとき

ρ1はψよりも複雑さが小さいので、帰納法の仮定より(ρ1)♣︎ ⊢ (ρ1#)♡ が成り立つ

ρ2はψよりも複雑さが小さいので、帰納法の仮定より(ρ2)♣︎ ⊢ (ρ2#)♡ が成り立つ

(ψ)♣︎ = (ρ1→ρ2)♣︎ = ρ1♣︎→ρ2♣︎

(ρ1)♣︎ ⊢ (ρ1#)♡ かつ (ρ2)♣︎ ⊢ (ρ2#)♡ ならば ρ1♣︎→ρ2♣︎ ⊢ (ρ1#)♡→(ρ2#)♡

よって帰納法の仮定より、 ρ1♣︎→ρ2♣︎ ⊢ (ρ1#)♡→(ρ2#)♡

(ρ1#)♡→(ρ2#)♡ = …… = ((ρ1→ρ2)#)♡

よって、(ψ)♣︎から(ψ#)♡が導出できる

ψが∀x3ρのとき

ρはψよりも複雑さが小さいので、帰納法の仮定より(ρ)♣︎ ⊢ (ρ#)♡ が成り立つ

(∀x3ρ)♣︎ = (∀3xρ)♣︎-

∀除去

よって帰納法の仮定により、(ρ#)♡

∀導入

教科書のやり方

(∀x3ρ)♣︎ = (∀x3ρ)♣︎-

ここが少し引っかかってる？

⇒ ρ♣︎

⇒ (ρ#)♡

帰納法の仮定より

⇒ ∀x6((ρ#)♡-)

∀導入

P(x203)

------------ ∀導入

∀x6P(x6)

= (∀x6(ρ#))♡

= ((∀x3ρ)#)♡

証明の方針

♣︎k ♥ k

任意の論理式ψに対して、あるkが存在して、以下のような書き換えができる

メモ

(∀x3ρ)♣︎ ⊢ (ρ#)♡

(∀x3ρ)♣︎ = (∀x3ρ)♣︎-

(∀x3ρ)♣︎- ⊢ ρ♣︎

ρ♣︎ ⊢ (ρ#)♡

帰納法の仮定より

(∀xρ)♣︎- ⊢ (ρ#)♡

ψが∃x3ρのとき

(∃x3ρ)♣︎ = (∃x3ρ)♣︎-

⇒ ρ♣︎

⇒ (ρ#)♡

帰納法の仮定より

⇒ ∀x6((ρ#)♡-)

∀導入

= (∀x6(ρ#))♡

= ((∀x3ρ)#)♡

φが原始論理式のとき

φ中にxが出現しない場合

φとφ#もφと変わらないので明らかに題意は成り立つ

例

φが単独の命題記号や⊥の場合

φ中にxが出現する場合

φがx1=x2のとき

これは閉論理式じゃないので考えなくていい

うーん。これは閉論理式じゃないけど、束縛したら閉論理式になる。

こういう感じで帰納法をまわそうとしても閉論理式が漏れなく構成できないから、ダメっぽい

φがQ(x1)のとき

φがx1⧀x2のとき

φがP(x1)のとき

φがR(x1,x2)のとき

をそれぞれ証明する

φが複合論理式のとき

任意のk変数記号k

-----------↑あんまり納得してない時の記述のメモ-----------------------------------------

任意の論理式ψ対して、次の主張を証明をする

任意のkに対して、ψに現れる変数記号の番号がすべてk以下なら、(ψ)♣︎ ⊢ (ψ#)♡ かつ (ψ#)♡ ⊢ (ψ)♣︎

証明の方針

ψの複雑さが0のとき、任意のkについて成り立つことを示す

次にψの複雑さについて、数学的帰納法を回す。

証明

複雑さが0のψは以下の場合に分けられる。

(t1=t2)

Q(t1)

(t1⧀t2)

P(t1)

R(t1,t2)

単独の命題記号A,B,C

t1,t2は、変数記号の番号がすべてk以下の任意の項である

例

ψがP(t1)のとき

ψ♣︎ = P(t1)♣︎ = P(t1♣︎) = P((t1#)♡) = P(t1#)♡ = (P(t1)#)♡ = (ψ#)♡

よって、(ψ)♣︎ ⊢ (ψ#)♡ かつ (ψ#)♡ ⊢ (ψ)♣︎

φが他の場合も同様

よって、任意のkに対してψの複雑さが0のとき、(ψ)♣︎ ⊢ (ψ#)♡ かつ (ψ#)♡ ⊢ (ψ)♣︎が成り立つ

kを任意に固定する

(kを十分大きく取れば、ψに任意の数変数記号が出現しても(ψ)♣︎ ⊢ (ψ#)♡ かつ (ψ#)♡ ⊢ (ψ)♣︎と言える感じかな？)

ψの複雑さが0のとき

上記で証明済み

ψの複雑さがnのとき

量化子が絡む場合のみ証明を行い、量化子が絡まない場合については省略する

ψが∀xρの形の場合

xは(5.1)の変数列に出現する

xがxiだとする

i>kのとき

「ψに現れる変数記号の番号がすべてk以下なら」という条件を満たさない

証明完了

i≤kのとき

(ψ)♣︎ ⊢ (ψ#)♡について

(ψ)♣︎

= (∀xiρ)♣︎

= ∀xi(ρ♣︎')

∀除去

= ρ♣︎

⇒ (ρ#)♡

帰納法の仮定

⇒ ∀x2i((ρ#)♡')

∀導入

= (∀x2i((ρ#))♡

= ((∀xiρ)#)♡

= (ψ#)♡

(ψ#)♡ ⊢ (ψ)♣︎について

(ψ#)♡

= ((∀xiρ)#)♡

= (∀x2i((ρ#))♡

= ∀x2i((ρ#)♡')

∀除去

= (ρ#)♡

⇒ ρ♣︎

帰納法の仮定

⇒ ∀xi(ρ♣︎')

∀導入

= (∀xiρ)♣︎

= (ψ)♣︎

演習問題4

既に証明済み

演習問題5

ΓがKeySetF,BでΓ⊢φでφ∈FormulaF,Bであるならば、φ∈Γとなることを示せ

証明

φ∉Γであると仮定する

Γの極大性よって、¬φ∈Γとなる

ΓがKeySetF,Bであるので、

φ∈FormulaF,BとΓの極大性により、φ∈Γまたは¬φ∈Γである

φ∈Γが成り立つとき、¬φ∈ΓであるのでΓの無矛盾性に反する

¬φ∈Γが成り立つときについて考える

¬φ∈Γなので、仮定集合が¬φで、結論が¬φの過程と結論が重なった論理式が書ける

つまりΓ⊢¬φ

Γ⊢φかつΓ⊢¬φである

補題5.1.3より、Γ⊢φかつΓ⊢¬φ ことは、Γが矛盾することと同値である

これは、Γが無矛盾であることに反する

よってφ∈Γである

演習問題6

(5.6)~が同値関係であることを示せ

s~t の定義は s= t ∈ Γ+

証明

同値関係とは

反射律

対称律

推移律

を満たすもの

反射律

任意のsについて、(s = s) ∈ Γ+ は成り立つ

Γ+はKeySetなので、(s = s) ∉ Γ+を仮定すると

極大性により、¬(s = s)∈Γ+

¬(s = s) ⊢ ⊥ となるので、これはΓ+の無矛盾性に反する

よって(s = s) ∈ Γ+

対称律

任意のs,tについて、(s = t) ∈ Γ+ ならば(t = s) ∈ Γ+は成り立つ

(s = t) ∈ Γ+ かつ (t = s) ∉ Γ+を仮定する

極大性により、¬(t = s) ∈ Γ+

(s = t), ¬(t = s) ⊢ ⊥ となるので、これはΓ+の無矛盾性に反する

よって、(s = t) ∈ Γ+ ならば(t = s) ∈ Γ+

推移律

任意のs,t,uについて、(s = t) ∈ Γ+ かつ (t = u) ∈ Γ+ ならば (s = u) ∈ Γ+は成り立つ

(s = t) ∈ Γ+ かつ (t = u) ∈ Γ+ かつ (s = u) ∉ Γ+ と仮定する

極大性により、¬(s = u) ∈ Γ+

(s = t), (t = u), ¬(s = u) ⊢ ⊥ となるので、これはΓ+の無矛盾性に反する

よって、(s = t) ∈ Γ+ かつ (t = u) ∈ Γ+ ならば (s = u) ∈ Γ+

(5.10) t1~t2 ならば suc(t1) ~ suc(t2)

任意のt1,t2に対して、(t1=t2)∈Γ+ かつ (suc(t1) = suc(t2))∉Γ+ を仮定する

極大性により、¬ (suc(t1) = suc(t2)) ∈ Γ+

(t1=t2), ¬(suc(t1) = suc(t2)) ⊢ ⊥ なので、これはΓ+の無矛盾性に反する

任意のt1,t2に対して、(t1=t2)∈Γ+ ならば (suc(t1) = suc(t2))∈Γ+ が成り立つ

(5.11) (s1~s2 かつ t1~t2)ならば (s1⊗t1) ~ (s2⊗t2)

任意のs1,s2,t1,t2に対して、(s1=s2)∈Γ+ かつ (t1=t2)∈Γ+ かつ ((s1⊗t1)= (s2⊗t2))∉Γ+ を仮定する

極大性により、¬ ((s1⊗t1) = (s2⊗t2))∈ Γ+

(s1=s2), (t1=t2) , ¬ ((s1⊗t1) = (s2⊗t2)) ⊢ ⊥ なので、これはΓ+の無矛盾性に反する

任意のt1,t2に対して、(s1=s2)∈Γ+ かつ (t1=t2)∈Γ+ ならば ((s1⊗t1)= (s2⊗t2))∈Γ+ が成り立つ

⊕, ⊙については、(5.11)と同様に示せる

(5.13) t1~t2 ならば (Q(t1)∈Γ+ ⇔ Q(t2)∈Γ+)

任意のt1,t2に対して、(t1=t2)∈Γ+ かつ Q(t1)∈Γ+ かつ Q(t2)∉Γ+ を仮定する

極大性により、¬Q(t2)∈ Γ+

(t1=t2), Q(t1),¬Q(t2) ⊢ ⊥ なので、これはΓ+の無矛盾性に反する

任意のt1,t2に対して、(t1=t2)∈Γ+ ならば (Q(t1)∈Γ+ ⇒ Q(t2)∈Γ+) が成り立つ

任意のt1,t2に対して、(t1=t2)∈Γ+ ならば (Q(t2)∈Γ+ ⇒ Q(t1)∈Γ+) が成り立つことも同様に示せる

P,Rも同様

(5.14) (s1~s2 かつ t1~t2)ならば( (s1⧀t1)∈Γ+ ⇔ (s2⧀t2)∈Γ+ )

任意のs1,s2,t1,t2に対して、(s1=s2)∈Γ+ かつ (t1=t2)∈Γ+ かつ (s1⧀t1)∈Γ+ かつ (s2⧀t2)∉Γ+ を仮定する

極大性により、 ¬(s2⧀t2)∈ Γ+

(s1=s2), (t1=t2), (s1⧀t1), ¬(s2⧀t2) ⊢ ⊥ なので、これはΓ+の無矛盾性に反する

任意のs1,s2,t1,t2に対して、((s1=s2)∈Γ+ かつ (t1=t2)∈Γ+) ならば ((s1⧀t1)∈Γ+ ⇒ (s2⧀t2)∈Γ+) が成り立つ

任意のs1,s2,t1,t2に対して、((s1=s2)∈Γ+ かつ (t1=t2)∈Γ+) ならば ((s2⧀t2)∈Γ+ ⇒ (s1⧀t1)∈Γ+ ) が成り立つ