数理論理学(鹿島亮)8

数理論理学(鹿島亮)7

さまざまな証明体系を扱う章

ヒルベルト流体系とシークエント計算を扱う

簡単のために、等号無しの部分だけを扱う

以下の閉論理式10個からなる集合をEとよぶ

Identity

∀x(x=x)

suc-eq

∀x∀y((x=y)→(suc(x)=suc(y)))

⨂-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→((x⨂u)=(y⨂v)))

⨀-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→((x⨀u)=(y⨀v)))

⨁-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→((x⨁u)=(y⨁v)))

P-eq

∀x∀y((x=y)→(P(x)→P(y)))

Q-eq

∀x∀y((x=y)→(Q(x)→Q(y)))

R-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→(R(x,u)→R(y,v)))

⧀-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→((x⧀u)→(y⧀v)))

=-eq

∀x∀y∀u∀v(((x=y)∧(u=v))→((x=u)→(y=v)))

自然演繹で等号公理と等号規則のどちらも使用しないで導出できることを、

$ ⊢^{(≠)}と表す

次の定理定理8.1.1は等号公理と等号規則がないとして論理式集合Eを公理として扱うことで代用ができることを示している

この意味で、自然演繹から等号規則を取り除くことは本質的な制限ではない

定理8.1.1 論理式の任意の集合Γと任意の論理式φに対して、以下の2条件は同値である

1. Γ ⊢ φ

2. Γ, E$ ⊢^{(≠)} φ

証明

次の3つを示せば十分である

主張a

Eの要素はすべて自然演繹で証明できる。すなわち

⊢ Identity

⊢ suc-eq

……

⊢ =-eq

主張b

任意の項tに対して

E$ ⊢^{(≠)} t=t

主張c

任意の論理式φ、任意の変数記号x、およびφ中のxに代入可能な任意の項s,tに対して

E$ ⊢^{(≠)} (t=s)→(φ[t/x]→φ[s/x])

上記の主張を使って、1,2の同値性を以下のように証明できる

1→2の証明

Γ ⊢ φ を表す導出図がある

このとき、等号公理を使っている部分を、主張bから得られる導出図を使って置き換える

同様に、等号規則を使っている部分を、主張cから得られる導出図を使って次のように置き換える

(t=s)→(φ[t/x]→φ[s/x]) t=s

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

(φ[t/x]→φ[s/x]) φ[t/x]

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

φ[s/x]

これによって、Γ, E$ ⊢^{(≠)} φを表す導出図が得られる

2→1の証明

Γ, E$ ⊢^{(≠)} φを表す導出図がある

その中で、Eの要素が解消されていない過程として使われている部分を、主張aで得られる導出図を使って置き換える

これによって、Γ ⊢ φを表す導出図が得られる

ik.icon推論規則の代わりに公理を入れても同じように扱えるの便利なんだろうなと

Eの論理式を弱めたり、論理式を削除したら、より弱い「=」の概念を扱うことができそう

したがって、定理8.1.1 を示すには主張a,b,cを示せば十分である

主張a,bは演習問題

主張cを証明するために主張dを証明する

主張d

記号

u,s,tは任意の項

xは任意の変数記号

主張

E$ ⊢^{(≠)} (t=s)→(u[t/x]=u[s/x])

主張dの証明

uの長さに関する帰納法をする

ik.iconたぶん論理式の複雑さの項バージョンのことだと思うけど、項の複雑さって用語じゃなくて項の長さという単語でやっている

uの長さが1のとき

uが変数記号のとき

uがxのとき

u[t/x]はt

u[s/x]はs

よって、(t=s)→(u[t/x]=u[s/x])は(t=s)→(t=s)となる

したがって、E$ ⊢^{(≠)} (t=s)→(u[t/x]=u[s/x])が成り立つ

uがxでないとき

u[t/x]にxは出現しないので、代入しても変化しないからuと等しく

u[s/x]にxは出現しないので、代入しても変化しないからuと等しい

よって、(u[t/x]=u[s/x]) ⇔ u = u

Identityから∀除去をしてu = uが導出できるので、E$ ⊢^{(≠)} (t=s)→(u[t/x]=u[s/x])

uが定数記号のとき

uにxが出現しないので同様に成り立つ

uの長さがk+1のとき

uがsuc(u1)のとき

省略…ik.icon

uが(u1⨂u2)のとき

u1、u2の項の長さはk+1未満なので帰納法の仮定より以下が成り立つ

E$ ⊢^{(≠)} (t=s)→(u1[t/x]=u1[s/x])

E$ ⊢^{(≠)} (t=s)→(u2[t/x]=u2[s/x])

⨂-eqに∀除去規則を適用して以下が得られる

E$ ⊢^{(≠)}((u1[t/x]=u1[s/x])∧(u2[t/x]=u2[s/x])) → ((u1[t/x]⨂u2[t/x]) = (u1[s/x]⨂ u2[s/x]))

これらから、E$ ⊢^{(≠)} (t=s)→((u1⨂u2)[t/x]=(u1⨂u2)[s/x]) すなわち、E$ ⊢^{(≠)} (t=s)→(u[t/x]=u[s/x]) が得られる

uが(u1⨀u2)のとき

省略…ik.icon

uが(u1⨁u2)のとき

省略…ik.icon

【再掲】主張c

任意の論理式φ、任意の変数記号x、およびφ中のxに代入可能な任意の項s,tに対して

E$ ⊢^{(≠)} (t=s)→(φ[t/x]→φ[s/x])

主張cの証明

任意の項t,sに対して以下が成り立つ

E$ ⊢^{(≠)} (t=s)→(s=t) (8.1)

これは=-eqとIdentityにそれぞれ∀除去をして得られる論理式

((t=s)∧(t=t))→((t=t)→(s=t))

t=t

から得られる

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

φが原子論理式のとき

φが命題記号や⊥のとき(項を含まない場合)

変数xが出現しないので、代入しても変わらない

よって、φ[t/x]、φ[s/x]はφと変わらない

したがって、E$ ⊢^{(≠)} (φ[t/x]→φ[s/x]) だからE$ ⊢^{(≠)} (t=s)→(φ[t/x]→φ[s/x])

もっと複雑な場合書かなきゃだik.icon

後で修正

φが項を含むとき

例えばφがP(u)のとき

P-eqに∀除去をすることで

(u[t/x]=u[s/x])→(P(u[t/x])→P(u[s/x]))が得られる

主張dより

(t=s)→(u[t/x]=u[s/x])

したがって、E$ ⊢^{(≠)} (t=s)→(P(u[t/x])→P(u[s/x])) が得られる

他の場合も同様

φが複合論理式のとき

φが¬ψという形のとき

E$ ⊢^{(≠)} (t=s)→(¬ψ[t/x]→¬ψ[s/x]) を示したい

帰納法の仮定より

E$ ⊢^{(≠)} (s=t)→(ψ[s/x]→ψ[t/x]) が成り立つ

よって、E$ ⊢^{(≠)}(s=t)→(¬ψ[t/x]→¬ψ[s/x])

ik.icon(s=t)を仮定して→除去を行い、ψ[s/x]を仮定して→除去を行い、ψ[t/x]を得る。ここで、¬ψ[t/x]を仮定する。ψ[t/x]と¬ψ[t/x]から⊥を得て、ψ[s/x]に対して¬導入をして¬ψ[s/x]を得て、→導入を¬ψ[t/x]に対してする。最後に→導入を(s=t)にして、(s=t)→(¬ψ[t/x]→¬ψ[s/x]) が得られる。

(8.1)より

E$ ⊢^{(≠)} (t=s)→(s=t)

したがって、

E$ ⊢^{(≠)}(t=s)→(¬ψ[t/x]→¬ψ[s/x])

他の形の場合も難しくないらしいので教科書では省略されているik.icon

時間ある時にやりたいik.icon

次節では「等号公理と等号規則を取り除いた自然演繹」と同等な体系を与える

$ ⊢^{(≠)} ⇔ φはSで証明可能

が任意の論理式φに対して成り立つような体系Sを与える

教科書では等号が必要になる議論がないため、論理式の定義を変更して、論理式を構成する記号に等号が含まれていないことにする。

これを「言語に等号が含まれない」という

⊢と$ ⊢^{(≠)}の概念を区別する必要がなくなるので議論がすっきりする

ヒルベルト流体系

ヒルベルト流と呼ばれる体系$ C_Hを定義する

教科書注釈※1

推論規則がモーダスポネンスを含む少数しかなく、自然演繹にあるような仮定を解消する規則がない体系のことを一般にヒルベルト流とよんでいる

CHの公理から出発してCHの推論規則を適用していき、結論に至る論理式の樹上配置を「CHにおける論理式φの証明図」とよぶ

公理

¬⊥

矛盾の定義的な？ik.icon

¬¬φ→φ

二重否定除去っぽいik.icon

φ→(ψ→φ)

→導入っぽいik.icon

(φ→(ψ→ρ))→((φ→ψ)→(φ→ρ))

(φ→(ψ→ρ))がφ∧ψ→ρ、(φ→ψ)→(φ→ρ)がφ∧(φ→ψ)→ρみたいなものik.icon

φ∧ψをφ∧(φ→ψ)に置き換えられますよー的な公理かなik.icon

φ→(ψ→(φ∧ψ))

(φ∧ψ)→φ

∧除去っぽいik.icon

(φ∧ψ)→ψ

∧除去っぽいik.icon

φ→(φ∨ψ)

∨導入っぽいik.icon

ψ→(φ∨ψ)

∨導入っぽいik.icon

(φ→ρ)→((φ→ρ)→((φ∨ψ)→ρ))

(φ→ρ)、(φ→ρ)、(φ∨ψ)からρがいえるって感じの∨除去っぽい公理ik.icon

(φ→ψ)→((φ→¬ψ)→¬φ)

(φ→ψ)∧(φ→¬ψ)から¬φがいえるって感じの否定の導入っぽい公理ik.icon

推論規則

モーダスポネンス

φ→ψ φ

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

∀

φ→ψ[y/x]

-----------------------注

φ→∀xψ

∃

ψ[y/x]→φ

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

∃xψ→φ

注：xは変数記号。yはφ中にも∀xψの中にも∃xψの中にも自由出現しない変数記号で、ψ中のxに代入可能なもの

CHにおける証明図の例

https://scrapbox.io/files/68a4c032c1e5e239d65ea428.jpeg

このようにヒルベルト流の体系では、結論は短い論理式なのに証明の途中には長い複雑な論理式が登場するということがしばしばある

2025/8/20 17:00

CHは自然演繹と同等である。すなわち以下が成り立つ

定理8.2.1

言語には等号が含まれないとする

任意の論理式φに対して次の二条件は同値である

1. CHでφが証明できる。すなわちCHにおけるφの証明図が存在する

2. 自然演繹でφが証明できる。すなわちφを結論として解消されていない仮定がない自然演繹の導出図が存在する

証明

1→2

方針

CHの各公理が自然演繹で証明できること

CHの各推論規則について、その前提が自然演繹で証明できる場合には結論も自然演繹で証明できることを示せば良い

ik.iconすると、CHの証明図から公理や推論規則を適用している部分について書き換えを行えばいい

ik.iconまず公理の書き換えを行うと、公理を導出する仮定のない状態になる自然演繹の導出図が得られる。

仮定がないのでその前提が自然演繹で証明できる場合という条件を満たしているので、結論も自然演繹で証明することができ導出図が得られる。

証明

https://scrapbox.io/files/68a4cd18b473a818ae79b89e.jpeg

https://scrapbox.io/files/68a4cd1b3ace773cef446d4c.jpeg

https://scrapbox.io/files/68a4cd1e5d955ab477d1f1db.jpeg

https://scrapbox.io/files/68a4cd21bc5b478dcae289e9.jpeg

2→1の証明

Aを自然演繹の任意の導出図とし、その結論をφ解消されていない仮定をψ1,ψ2,…,ψn

このとき、次が成り立つ

n=0ならばCHにおけるφの証明が存在する

n>0ならばCHにおける(ψ1∧ψ2∧…∧ψn)→φの証明が存在する

ik.iconこれが成り立つことを示す意味があんまりわかっていない……

n=0の時だけ示せば定理8.2.1を示すには十分な気がしてしまう

実際に帰納法回すときにこれが必要になるのかもなぁ

Aは任意の導出図であって、仮定のない導出図ではないから

閉論理式に対して帰納法がうまく回せないから任意の論理式に対して考えるのに似ているのかも？

このことをAの大きさに関する帰納法で示せば良い

教科書によるとこの詳細はかなり面倒らしい

ik.icon後回ししようかな……

(ψ1∧ψ2∧…∧ψn)→φについては、ψ1,ψ2,…,ψnを∧で結ぶ順番や括弧のかかり方に依存しないことも示す必要がある

自然演繹の健全性と完全性は統合を含まない設定で同様に成り立つ。このことと定理8.2.1から以下が成り立つ

定理8.2.2

言語には等号が含まれていないとする

任意の論理式φに対して次の条件1,2は同値である

さらにφが閉論理式の場合は3も同値である

条件

1. CHでφが証明できる。

2. 自然演繹でφが証明できる。

3. φは恒真である

シークエント計算と呼ばれる体系LKを定義する

Γ, Δなどのギリシャ大文字は有限個の論理式をカンマで区切って並べた列を表す

定義8.3.1 シークエント

有限この論理式をカンマで区切って、「⇒」の左右に並べた

φ1,φ2,……,φn ⇒ ψ1,ψ2,……,ψm

という形の記号列をシークエントとよぶ

n,mは0でも良い

注意事項

シークエントの左右を区切るための記号 ⇒ と

論理式中の「ならば」の記号 → を混合しないようにする

n,mが0の場合も⇒は必ず書く必要がある

「⇒」だけのからのシークエントも立派なシークエント

シークエント計算はシークエントを単位として推論を進めていく体系のこと

公理としていくつかのシークエントがしてされており、推論規則はシークエントからシークエントを導く形になっている

LKの公理から出発してLKの推論規則を適用していき最終的にシークエント Γ⇒Δ へ至るシークエントの樹上配置を「LKにおける Γ⇒Δ の証明図」とよび、そのような証明図が存在することを「LKにおいて Γ⇒Δ が証明できる」という

公理

φ ⇒ φ

という形のシークエントすべて

両辺に同一の論理式が1つずつだけ存在するシークエント

⊥ ⇒

左辺が⊥ 1つで、右辺が空のシークエント

推論規則

Γ ⇒ Δ

---------------------- weakening 左

φ, Γ ⇒ Δ

Γ ⇒ Δ

---------------------- weakening 右

Γ ⇒ Δ, φ

φ, φ, Γ ⇒ Δ

---------------------- contraction 左

φ, Γ ⇒ Δ

Γ ⇒ Δ, φ, φ

---------------------- contraction 右

Γ ⇒ Δ, φ

Γ, φ, ψ, ∏ ⇒ Δ

---------------------- exchange 左

Γ, ψ, φ, ∏ ⇒ Δ

Γ ⇒ Δ, φ, ψ, ∑

---------------------- exchange 右

Γ ⇒ Δ, ψ, φ, ∑

φ, Γ ⇒ Δ

---------------------- ∧左

φ∧ψ, Γ ⇒ Δ

φ, Γ ⇒ Δ

---------------------- ∧左

ψ∧φ, Γ ⇒ Δ

Γ ⇒ Δ, φ　Γ ⇒ Δ, ψ

--------------------------------- ∧右

Γ ⇒ Δ, φ∧ψ

φ, Γ ⇒ Δ　ψ,Γ ⇒ Δ

--------------------------------- ∨左

φ∨ψ, Γ ⇒ Δ

Γ ⇒ Δ, φ

---------------------- ∨右

Γ ⇒ Δ, φ∨ψ

Γ ⇒ Δ, φ

---------------------- ∨右

Γ ⇒ Δ, ψ∨φ

Γ ⇒ Δ, φ　ψ, ∏ ⇒ ∑

--------------------------------- →左

φ→ψ, Γ, ∏ ⇒ Δ, ∑

φ, Γ ⇒ Δ, ψ

--------------------------------- →右

Γ ⇒ Δ, φ→ψ

Γ ⇒ Δ, φ

---------------------- ¬左

¬φ, Γ ⇒ Δ

φ, Γ ⇒ Δ

---------------------- ¬右

Γ ⇒ Δ, ¬φ

φ[t/x], Γ ⇒ Δ

---------------------- ∀左注1

∀xφ, Γ ⇒ Δ

Γ ⇒ Δ, φ[y/x]

---------------------- ∀右注2

Γ ⇒ Δ,∀xφ

φ[y/x], Γ ⇒ Δ

---------------------- ∃左注2

∃xφ, Γ ⇒ Δ

Γ ⇒ Δ, φ[t/x]

---------------------- ∃右注1

Γ ⇒ Δ, ∃xφ

Γ ⇒ Δ, φ　φ, ∏ ⇒ ∑

---------------------- カット

Γ, ∏ ⇒ Δ, ∑

注1

xは変数記号。tはφ中のxに代入可能な項

注2

xは変数記号。yはΓ, Δ中にも∀xφ中にも∃xφ中の中にも自由出現しない変数記号で、φ中のxに代入可能なもの

yのことをeigenvariableとよぶ

LKにおける証明図の例

https://scrapbox.io/files/68adf6de0e2b494a8e5b09ee.png

https://scrapbox.io/files/68adf6e1f5cb59a949582bd8.png

LKはシークエントを導く体系ではあるが、左辺が空で右辺が論理式ひとつのシークエント(⇒φ)が証明できることを「φが証明できる」とみなせば自然演繹と同等になる。正確には次が成り立つ

定理8.3.2

言語には統合が含まれないとする。任意の論理式φに対して次の二条件は同値である

1. LKでシークエント(⇒φ)が証明できる

2. 自然演繹でφが証明できる

証明1⇒2

証明の流れ

一般にシークエント Γ⇒Δ に対して論理式 (Γ⇒Δ)^formula (これを「シークエント Γ⇒Δ を翻訳した論理式」とよぶ) を次で定義する

(ψ1,ψ2,…,ψm ⇒ φ1,φ2,…,φn)^formula

= (ψ1∧ψ2∧…∧ψm → φ1∨φ2∨,…,∨φn) m>0, n>0のとき

= ¬(ψ1∧ψ2∧…∧ψm) m>0, n=0のとき

= (φ1∨φ2∨,…,∨φn) m=0, n>0のとき

= ⊥ m=0, n=0のとき

次のことを証明する

LKの各公理を翻訳した論理式が自然演繹で証明できる

LKの各推論規則について、その前提を翻訳した論理式が自然演繹で証明できる場合には結論を翻訳した論理式も自然演繹で証明できる

これによって題意が示される

LKにおける証明図

を上記を使って自然演繹の導出図に置き換えることができるからだと思うik.icon

証明

https://scrapbox.io/files/68adf6990d8a00184395d4c5.png

https://scrapbox.io/files/68adf69c06a933bbd80ed5c5.png

https://scrapbox.io/files/68adf6a07b107492fdd2d6a3.png

https://scrapbox.io/files/68adf6a359bc1cf57a90935f.png

https://scrapbox.io/files/68adf6a6038b7d9be8ff8f4e.png

https://scrapbox.io/files/68adf6a9be8d4915690653ed.png

https://scrapbox.io/files/68adf6ac6481f3c39b62d79e.png

https://scrapbox.io/files/68adf6af210c12920ce6d25e.png

https://scrapbox.io/files/68adf6b35f86c2d92990a5f8.png

https://scrapbox.io/files/68adf6b66481f3c39b62d7b9.png

https://scrapbox.io/files/68adf6b912e60b75e9a5930b.png

https://scrapbox.io/files/68adf6bc4bac79872018aab4.png

https://scrapbox.io/files/68adf6bf6f758129cd579ed4.png

https://scrapbox.io/files/68adf6c23c1a7f95d9b54a67.png

https://scrapbox.io/files/68adf6c5c564908ce5d6b7f4.png

証明2⇒1

証明の流れ

次の事実を自然演繹の導出図Aの大きさに関する帰納法で示す

Aを自然演繹の任意の導出図とし、その結論をφ、解消されていない仮定をψ1,ψ2,…,ψnとすると、シークエント(ψ1,ψ2,…,ψn ⇒ φ)がLKで証明できる