数理論理学(鹿島亮)4

自然演繹の健全性を示す章

証明とは

「前提がすべて正しければ結論も正しい」というものを保証するもの

正しい可能性/正しくない可能性は

その論理式を真にするストラクチャー/その論理式を偽にするストラクチャーと考えられる

どんな導出図に関しても、解消されていない仮定がすべて真となるようなストラクチャーにおいては必ず真になる

【定理】4.1.1

健全性定理

任意の導出図𝜜

その結論φ

解消されていない仮定 ψ1, ψ2, … , ψn

互いに異なる変数x1,x2,…,xk

これ以外の変数記号は𝜜中に出現しない

任意のストラクチャーM

Mの対象領域Dの任意の要素の名前a1,a2,…,ak

Dの要素の名前すべてを定数記号と認めると、a1~akは定数記号となる

としたとき以下が成り立つ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(φ*) = 真 (4.1)

ψ1*は、ψ1中に自由出現するx1,x2,…,xkがあればそれぞれの名前a1,a2,…,akに置き換えて得られるD拡大閉論理式

n = 0のときは、 (4.1)は単に M(φ*) = 真 を表す

証明の流れ

導出図𝜜の大きさに関する帰納法をする

導出図𝜜の大きさとは、𝜜中に出現する論理式の個数のこと

𝜜が単独の論理式の場合を証明する

そして帰納法を回していく

𝜜1,𝜜2,𝜜3は𝜜よりも小さい導出図

パターン1

… 𝜜1

φ1

-----

φ

パターン2

… 𝜜1 … 𝜜2

φ1 　 φ2

---------------

φ

パターン3

… 𝜜1 … 𝜜2 … 𝜜3

φ1 　 φ2　 φ3

--------------------------

φ

証明

導出図の大きさが1

𝜜が単独の論理式φで、これが仮定であり同時に結論である場合

仮定の個数はn=1

(4.1)は

M(φ*) = 真 ならば M(φ*) = 真

これは明らかに成り立つ

𝜜が等号公理で得られた単独の論理式t=tの場合

仮定の個数はn=0

(4.1)は単に

M(φ*) = 真すなわちM((t=t)*) = 真

これを証明すれば良い

M((t=t)*) = M(t*=t*)

つまり項t中に自由出現する変数x1~xkをa1~akで代入したものだと思う

x1,x2,…,xk以外の変数記号は𝜜中に出現しないので、t中にはx1,x2,…,xk以外の変数記号は出現しない

なのでt*は定数記号a1~akと関数記号からなるD拡大閉項である

ストラクチャーによって、定数記号と関数記号の解釈が決まるので、D拡大閉項t*の解釈が再帰的に定まる(拡大閉項の値の定義3.2.3)

拡大閉論理式の定義より、M(t*=t*) = 真 ⇔ M(t*) = M(t*)

M(t*) = M(t*) は明らかに成り立つ

よって、M((t=t)*) = M(t*=t*) = 真

M(φ*) = 真となる

𝜜が推論規則を使って構成された導出図の場合(帰納法回していく部分)

一番下に適用された推論規則の種類によって場合わけをする

→導入を適用した場合

𝜜が以下の場合

…

…　　𝜜1

θ

--------------

ρ→θ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((ρ→θ)*) = 真

を証明すれば良い

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 (4.2)

となっていると仮定して、M((ρ→θ)*) = 真を示す

M(ρ) = 真 の場合

ρが解消されていない仮定として𝜜1中に出現する場合

帰納法の仮定M(ψ1*) = M(ψ2*) = … = M(ψn*) = M(ρ) = 真 ならばM(θ*) = 真

(4.2)より、M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真でもあるので、M(ρ) = 真と合わせて、M(θ*) = 真と言える

→の真理値の定義より、M((ρ→θ)*) = 真

ρが解消されていない仮定として𝜜1中に出現しない場合(出現する場合と照明はほぼ同じ)

帰納法の仮定M(ψ1*) = M(ψ2*) = … = M(ψn*) ならばM(θ*) = 真

(4.2)より、M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真でもあるので、M(θ*) = 真と言える

→の真理値の定義より、M((ρ→θ)*) = 真

M(ρ) = 偽 の場合

→の真理値の定義より、M((ρ→θ)*) = 真

→除去を適用した場合

𝜜が以下の場合

…　　　　　…

…　　𝜜1　　…　𝜜2

ρ→φ　　　　ρ

----------------------------------

φ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((ρ→θ)*) = 真

を示せば良い

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψnが𝜜2中にある

としても一般性は失われない

つまり、M(ψ1*) = M(ψ2*) = … = M(ψn'*) = M(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 ならば M(φ*) = 真

を示せば良い

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn'*) = 真 ならば M((ρ→θ)*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真という仮定を使うと、M(ψ1*) = M(ψ2*) = … = M(ψn'*) = 真 である

よって M((ρ→φ)*) = 真

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真と仮定を使うとM(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 である

よって M(ρ*) = 真

→の真理値の定義より

M(φ*) = 真

∃導入を適用した場合

𝜜が以下の場合

…　　　　

…　　𝜜1　

----------------------------------

∃xρ

対象領域の要素M(t*)の名前をcとする

xはこの導出図に出現する変数記号である

xはx1,x2,…,xkのどれかと一致する

互いに異なる変数x1,x2,…,xk

これ以外の変数記号は𝜜中に出現しない

という仮定があるため

ここではx1がxであると仮定する

こういう仮定をしても一般性は失われない

仮にxiがxであったとしても、同様の証明が行えるから？

xiのiに依存しない証明

もっといえば変数名に依存しない証明

変数名を付け直しても証明に問題はない

つまり仮にxiがxだったとしても、変数名を付け直してx1がxであるとできる？

証明

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((∃xρ)*) = 真 を証明すれば良い

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真

帰納法の仮定

∃導入では、仮定を落とさない

推論規則適用前の論理式と適用後の論理式が同じ仮定を持っているとは限らない

そのため、

*の定義(なので実際には必要十分条件ではあると思う)

x1がxであるため

より細かくステップを踏むなら

これも同値だと思う

定理3.2.5

∃の真理値の定義

x, x2,…,xkは異なる変数であり、a2,a3,…,ak中に束縛変数xがが出現しないからOKな気がする

⇒ M((∃xρ)*) = 真

*の定義

上の議論の正当性(代入を変化させても論理式の実態が変わらないこと)はxがx1であることや、x1,x2,…,xkが互いに異なる変数記号でa1,a2,…,ak中に変数記号が出現しないことなどから保証される

まぁなんで保証されるかの証明は書かれていないけど…

証明大変そうー

∃除去を適用した場合

𝜜が以下の場合

…　　　　　…

…　　𝜜1　　…　𝜜2

∃xρ　　　　φ

φ

yがxと異なる場合

以下の仮定をしても一般性を失わない

x1がx、x2がyである

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψnが𝜜2中にある

∃除去適用条件から以下がなりたっている

yの不出現条件

yはρ,φ,ψn'+1, ψn'+2, … , ψn中に自由出現しない

yとxが同じ変数だと、∃xρは∃yρとなる

ρ中にyが出現しても、yは束縛される

∃yρにはyは自由出現してないので、∃除去適用条件を満たしている

今回はxとyが異なっているので、ρ中に出現しないかだけを見れば良い

(4.1)を示す。すなわち

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 (4.3)

を仮定して、M(φ*) = 真 であることを示せば良い

証明

M(∃xρ*) = 真

𝜜1は𝜜より小さい導出図なので、帰納法の仮定が成り立つ。M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であることを仮定しているので成り立つ。

*の定義より

x1がx、x2がyであるため

∃xρ中にxは自由出現しないため、xにa1を代入しても真理値は変わらない

∃xρ中にyは自由出現しないため、yにa2を代入しても真理値は変わらない

∃の真理値の定義より

a3,…,ak中に変数記号が出現せず、x3,…,xk, xが互いに異なる変数であることから、代入の順番を入れ替えて大丈夫

ここで、このbを使って代入$を以下のように定義する

$は*のyに対する代入をa2からbに変更したものである

[a1/x1][b/y][a3/x3]…[ak/xk]

$の定義より

(4.3)とyの不出現条件から

M(ψn'+1$) = M(ψn'+2$) = … = M(ψn$) = 真 となる

というような感じで、x2で代入しても論理式は変わらないし、yは出現しないのでyに代入しても変わらない

M(ψn'+1*) = M(ψn'+1$), M(ψn'+2*) = M(ψn'+2$), …, M(ψn*) = M(ψn$) がこのことから成り立つ

(4.3)からさらにこれらが、すべて真であると言える

M(φ$) = 真 となる

$の定義より

yの不出現条件より、yに代入しなくても同じ論理式

x2はyである。yの不出現条件より、x2に代入しても同じ論理式

M(φ*) = 真

*の定義より

yがxと一致する場合

yがxと異なる場合と同様にできるらしい

yの不出現条件

yは∃xρ,φ,ψn'+1, ψn'+2, … , ψn中に自由出現しない

xが出現しない場合

yがxと異なる場合と同様にできるらしい

以下の場合は演習4.1で行う

∧導入を適用した場合

∧除去を適用した場合

∨導入を適用した場合

∨除去を適用した場合

¬導入を適用した場合

¬除去を適用した場合

背理法を適用した場合

爆発律を適用した場合

∀導入を適用した場合

∀除去を適用した場合

等号規則を適用した場合

健全性定理を使うと次のようなことがすぐ言える

解消されていない仮定無しに⊥を結論とする導出図は存在しない

解消されていない仮定無しに単独の命題記号Aを結論とする導出図は存在しない

仮定suc(x)=suc(y)から結論x=yを導く導出図は存在しない

証明

解消されていない仮定無しに⊥を結論とする導出図が存在すると仮定する

互いに異なる変数x1,x2,…,xk

これ以外の変数記号は導出図中に出現しない

あるストラクチャーMにして、健全性定理を適用する

健全性定理より、

M(⊥*) = 真

a1,a2,…,akはMの対象領域Dの任意の要素の名前

⊥中に変数記号は出現しないので、M(⊥*) = M(⊥)

真理値の定義より、M(⊥) = 偽

真 = M(⊥*) = M(⊥) = 偽

となる

各論理式は真か偽のどちらかの真理値を持つので、これは矛盾する

よって、解消されていない仮定無しに⊥を結論とする導出図は存在しない

⊥から命題記号への一般化って感じがする

証明

解消されていない仮定無しに単独の命題記号Aを結論とする導出図は存在すると仮定する

M(A) = 偽 となるようなストラクチャーに対して、健全性定理を適用する

健全性定理より、

M(A*) = 真

a1,a2,…,akはMの対象領域Dの任意の要素の名前

命題記号A中に変数記号は出現しないので、M(A*) = M(A)

真 = M(A*) = M(A) = 偽 となる

これは矛盾する

解消されていない仮定無しに単独の命題記号Aを結論とする導出図は存在しない

ik.icon

めちゃくちゃな反論だけど、M(A) = 偽 となるようなストラクチャーが取れない

つまり、単独の命題記号Aには真のストラクチャーしか割り当てられないなら、問題なさそう

仮定suc(x)=suc(y)から結論x=yを導く導出図は存在しない

証明

仮定suc(x)=suc(y)から結論x=yを導く導出図は存在すると仮定する

このとき、教科書p47のストラクチャーHを使う

健全性定理より、

H(suc(x)=suc(y)*) = 真 ならば H((x=y)*) = 真

H(suc(x)=suc(y)) = 真 ならば H(x=y) = 真 となるとは限らない

p47 (3.3) H(∀x∀y(suc(x)=suc(y) → x=y)) = 偽

矛盾するので、仮定suc(x)=suc(y)から結論x=yを導く導出図は存在しない

4.2意味論的帰結

⊨(ダブルターンスタイル)の使用法

φは閉論理式

Γは閉論理式の集合

無限でも有限でも良い

(すべてのγ∈Γに対してM(γ)=真) ならば M(φ)=真

が任意のストラクチャーで成り立っていることを

Γ ⊨ φ と表記する

「φはΓの意味論的帰結」と読む

Γのすべてのモデルでφが真といっても同じ

γ1,γ2,…,γn ⊨ φ と書いても良い

Γ = {γ1,γ2,…,γn}のとき

この記法ではΓが空集合の場合

⊨ φ と書く

φが恒真

Γ ⊭ φ

Γのモデルであって、φが偽となるストラクチャーが存在すること

をこのように表記する

定理4.2.2(健全性定理)

閉論理式の任意の集合Γ(無限集合でも有限集合でも良い)および、任意の閉論理式φに対して次が成り立つ

Γ⊢φ ならば Γ⊨φ

証明

Γ⊢φ の定義から

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

その導出図をAとする

Aに対して、定理4.1.1を適用する

任意のストラクチャーMとして、Γ0のすべての要素γに対してM(γ)=真 ならば M(φ) = 真

任意のストラクチャーMがΓ0のモデルならば、M(φ) = 真

つまり、Γ0⊨φといえる

Γのモデルすべては、Γ0のモデルになるので

Γ⊨φといえる

よって、Γ⊢φ ならば Γ⊨φ が成り立っている

例

群の公理をΓGとする

ΓG⊢φ ならば ΓG⊨φ

が健全性定理より成り立つ

群の公理からφが証明できるならば、φはどんな群においても成り立つ (4.6)

ある意味自明な事実だが、重要

(4.6)の逆、φはどんな群においても成り立つならば、群の公理からφが証明できる

はまったく自明じゃない

φで記述された性質が偶然にすべての群で成り立っていたとしても、群の公理だけからその性質が証明できる保証はないように思える

演習問題

4.1 定理4.1.1で省略されている部分を補う

∧導入を適用した場合

𝜜が以下の場合

…　　　　　…

…　　𝜜1　　…　𝜜2

ρ　　　　θ

----------------------------------

ρ∧θ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((ρ∧θ)*) = 真

を示す

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψnが𝜜2中にある

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn'*) = 真 ならば M(ρ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 を使うと、M(ρ*) = 真

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 ならば M(θ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 を使うと M(θ*) = 真

∧の真理値の定義

M((ρ∧θ)*) = 真

∧除去を適用した場合

𝜜が以下の場合

…

…　　𝜜1

ρ∧θ

----------------------------------

ρ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

を示す

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((ρ∧θ)*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 を使うと、M((ρ∧θ)*) = 真

∧の真理値の定義より

M(ρ*) = 真 かつ M(θ*) = 真

よって、M(ρ*) = 真

𝜜が以下の場合

…

…　　𝜜1

φ∧ψ

----------------------------------

ψ

同様に証明可能

∨導入を適用した場合

𝜜が以下の場合

…

…　　𝜜1

ρ

----------------------------------

ρ∨θ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((ρ∨θ)*) = 真

を示す

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 を使うと、M(ρ*) = 真

∨の真理値の定義より

M((ρ∨θ)*) = 真 ⇔ M(ρ*) = 真 または M(θ*) = 真

よって、M((ρ∨θ)*) = 真

𝜜が以下の場合

…

…　　𝜜1

θ

----------------------------------

ρ∨θ

同様に証明する

∨除去を適用した場合

𝜜が以下の場合

…　　　　　…　　　　　…

…　　𝜜1　　…　𝜜2　　… 𝜜3

ρ∨θ　　　　χ　　　　χ

--------------------------------------------------

χ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(χ*) = 真

を示す

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψn''が𝜜2中にある

ψn''+1, ψn''+2, … , ψnが𝜜3中にある

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn'*) = 真 ならば M((ρ∨θ)*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真であるから、M((ρ∨θ)*) = 真 である

∨の真理値の定義より、以下の3通りの場合が考えられる

M(ρ) = 真 と M(θ) = 真 の場合

M(ρ) = 真 であり、M(θ) = 偽 の場合

M(ρ) = 偽 であり、 M(θ) = 真 の場合

M(ρ) = 真 と M(θ) = 真 の場合 の場合

ρが解消されていない仮定として𝜜2中に出現する場合

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn''*) = M(ρ) = 真 ならばM(χ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真であり、M(ρ) = 真 であるから、M(χ*) = 真

ρが解消されていない仮定として𝜜2中に出現しない場合場合

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn''*) = 真 ならばM(χ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真であるから、M(χ*) = 真

M(ρ) = 真 であり、M(θ) = 偽 の場合

上記と全く同じ証明をする

M(ρ) = 偽 であり、M(θ) = 真 の場合

上記の証明を少し変える

𝜜2に関する帰納法の仮定ではなく、𝜜3に関する帰納法の仮定を利用していく

¬導入を適用した場合

𝜜が以下の場合

…

…　　𝜜1

⊥

----------------------------------

¬ρ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((¬ρ)*) = 真

を示す

M(ρ) = 真 の場合

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(⊥*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であるので、M(⊥*) = 真

⊥の真理値の定義より、M(⊥*) = 偽であるから、これは矛盾する

よって、M(ρ) = 偽

¬の真理値の定義より

M(¬ρ) = 真

M(ρ) = 偽 の場合

¬の真理値の定義より

M(¬ρ) = 真

¬除去を適用した場合

𝜜が以下の場合

…　　　　　…

…　　𝜜1　　…　𝜜2

¬ρ　　　　ρ

----------------------------------

⊥

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(⊥*) = 真

を示す

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψnが𝜜2中にある

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn'*) = 真 ならば M(¬ρ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であるから M(¬ρ*) = 真

¬の真理値の定義より

M(ρ*) = 偽

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であるから M(ρ*) = 真

M(ρ*) = 偽であり、M(ρ*) = 真であるから矛盾している

よって、M(⊥*) = 真

背理法を適用した場合

𝜜が以下の場合

…

…　　𝜜1

⊥

----------------------------------

ρ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

を示す

M(¬ρ) = 真 の場合

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(⊥*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であるので、M(⊥*) = 真

⊥の真理値の定義より、M(⊥*) = 偽であるから、これは矛盾する

よって、M(¬ρ) = 偽

¬の真理値の定義より

M(ρ) = 真

M(¬ρ) = 偽 の場合

¬の真理値の定義より

M(ρ) = 真

爆発律を適用した場合

𝜜が以下の場合

…

…　　𝜜1

⊥

----------------------------------

ρ

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(ρ*) = 真

を示す

𝜜1に関する帰納法の仮定

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M(⊥*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 であるので、M(⊥*) = 真

⊥の真理値の定義より、M(⊥*) = 偽であるから、これは矛盾する

よって、M(ρ) = 真

∀導入を適用した場合

𝜜が以下の場合

…　　　　

…　　 𝜜1　

----------------------------------

∀xρ

yがxと異なる場合

∀導入適用条件から以下がなりたっている

yは𝜜1中の解消されていない仮定の中にも、∀xρの中にも自由出現しない変数記号でxに代入可能なもの

yの不出現条件

yはρ,ψ1, ψ2, … , ψn中に自由出現しない

以下の仮定をしても一般性を失わない

x1がx、x2がyである

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 ならば M((∀xρ)*) = 真

を示す

このとき、yの不出現条件からψ*=ψ$(b)となる

bは任意の要素の任意の名前

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真と仮定すると、M(ψ1$(b)) = M(ψ2$(b)) = … = M(ψn$(b)) = 真である

帰納法の仮定より

$(b)の定義より

a3…akが名前であることや、x3,…,xk,xは異なる変数であるから代入の順番を入れ替えられる

x1すなわちxは束縛されており、∀xρに出現しないから

M(∀xρ*) = 真

*の定義より

$(b)を定義して、ψ*とψ$が同じことを示して、帰納法の仮定使って、　∀の定義を使って、最終的にφ*にするって流れ

言われれば補完できるけど、一人では浮かばなかったなぁと

∀除去を適用した場合

𝜜が以下の場合

…　　　　

…　　 𝜜1　

∀xρ　

----------------------------------

対象領域の要素M(t*)の名前をcとする

以下の仮定をしても一般性を失わない

x1がxである

を示す

M((∀xρ)*) = 真

帰納法の仮定より

*の定義

x1がxであるため、x1は束縛されており、代入しても論理式は変わらない

なので、cをxに代入しても問題ない

定理3.2.5

xは自由出現してないので、x1にa1を代入しても変わらない

*の定義より

等号規則を適用した場合

𝜜が以下の場合

…　　　　　…

…　　𝜜1　　…　𝜜2

----------------------------------

𝜜中の解消されていない仮定 ψ1, ψ2, … , ψnのうち

ψ1, ψ2, … , ψn'が𝜜1中にある

ψn'+1, ψn'+2, … , ψnが𝜜2中にある

𝜜1に関する帰納法の仮定

𝜜2に関する帰納法の仮定

M(ψn'+1*) = M(ψn'+2*) = … = M(ψn*) = 真 ならば M((t = s)*) = 真

M(ψ1*) = M(ψ2*) = … = M(ψn*) = 真 を使うと M((t = s)*) = 真

よって

M((t = s)*) = 真

M(t* = s*) = 真

M(t*) = M(s*)

真理値の定義から

定理3.2.5 より

メモ

定理3.2.5が使えそう

M(s) = M(t)ならば……

M(t=s)= 真 ⇔M(s) = M(t)

これを導きたい

4.2

演習問題2.7の続き

c

aと同じ制限のもとで、「奇数に1を足したものは必ず偶数である」と読むことができる論理式を作れ

∀n( Odd(n)→Even(suc(n)) )

d

「cで作った論理式を結論として解消されていない仮定がない導出図」は存在しないことを示せ

∀n( Odd(n)→Even(suc(n)) )を結論として解消されていない仮定がない導出図があると仮定する

健全性定理より、∀n( Odd(n)→Even(suc(n)) )が真となる

ここで∀n( Odd(n)→Even(suc(n)) )が偽となるようなストラクチャーが存在する

これは、あるnについて、Odd(n)が真でEven(suc(n))が偽となるようなストラクチャー

対象領域{0}

M(suc(0)) = 0

M(Odd(0)) = 真

M(Even(0)) = 偽

よって、矛盾するので、

∀n( Odd(n)→Even(suc(n)) )を結論として解消されていない仮定がない導出図は存在しない