数理論理3:構文論

今回は
・言語に対して,その言語の定理式の全体が定まること
をLKと呼ばれる流儀で述べます.

以下,言語,その言語の論理式の集合Σを任意に固定します.

(定義3-1)論理式の任意の集合の対(Ψ,Ω)をシーケントと呼び,Σから導出可能なシーケントの全体は,次の1.から16.(3.から16.を推論規則と呼びます)を満たす最小の集合です.以下,この集合に(Ψ,Ω)が属することを Ψ \longrightarrow Ω で表します.

xが変数記号,tが項,A,Bが論理式,CがΣの元,X,Yが論理式の(空でもよい)有限列ならば

1.{}\longrightarrow{C}
2.{A}\longrightarrow{A}

3.{X}\longrightarrow{Y}ならば{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}
4.{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{Y}

5.{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{¬A,Y}
6.{X}\longrightarrow{A,Y}ならば{¬A,X}\longrightarrow{Y}

7.{A,B,X}\longrightarrow{Y}ならば{A∧B,X}\longrightarrow{Y}
8.{X}\longrightarrow{A,Y}かつ{X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A∧B,Y}

9.{X}\longrightarrow{A,B,Y}ならば{X}\longrightarrow{A∨B,Y}
10.{A,X}\longrightarrow{Y}かつ{B,X}\longrightarrow{Y}ならば{A∨B,X}\longrightarrow{Y}

11.{A,X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A→B,Y}
12.{X}\longrightarrow{A,Y}かつ{B,X}\longrightarrow{Y}ならば{A→B,X}\longrightarrow{Y}

13.{X}\longrightarrow{A,Y}ならば{X}\longrightarrow{∀xA,Y}
  ただし,X,Yの各論理式にxの自由出現はないとします(これを固有変数条件と呼びます).
14.{A内のxの全ての自由出現をtに置き換えたもの,X}\longrightarrow{Y}ならば{∀xA,X}\longrightarrow{Y}
  ただし,置き換えにより新たな束縛は生じないとします(これを代入可能条件と呼びます).

15.{A,X}\longrightarrow{Y}ならば{∃xA,X}\longrightarrow{Y}
  ただし,固有変数条件は満たされているとします.
16.{X}\longrightarrow{A内のxの全ての自由出現をtに置き換えたもの,Y}ならば{X}\longrightarrow{∃xA,Y}
  ただし,代入可能条件は満たされているとします.

なお,(定義3-1)も(定義1-2)のように「適当な・・・によって・・・と表せるもの」という表現も可能です.そして

・ {X}\longrightarrow{Y}を X \longrightarrow Y 或いは Σ \vdash\longrightarrow Y と書きます.また,とくに Σ \vdash \longrightarrow A を Σ \vdash A(Σが空集合ならば \vdash A)と書き,これを「AはΣの構文論的帰結」或いは「AはΣの定理式」或いは「AはΣから証明可能」(Σ が空集合ならば「Aは定理式」或いは「Aは証明可能」)と読みます.
・ (定義3-1)の集合は帰納的に定義されているので,1.または2.から{X}\longrightarrow{Y}に至る過程に現れるΣの元は有限個です.従って,Σ \vdash\longrightarrow Yならば,Σの有限部分集合Σ’が存在して Σ’ \vdash\longrightarrow Y となります.
・ 固有変数条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,px→∀xpx が定理式になってしまいます.
・ 代入可能条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,∀xpxx→∃x∀ypxy が定理式になってしまいます.

(例3-1)x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow(¬(∀xpx))→∃x(¬px)
となるには,11. により
 ¬(∀xpx)\longrightarrow∃x(¬px)
となればよく,それには,6. により
 \longrightarrow∀xpx,∃x(¬px)
となればよく,それには,13. により
 \longrightarrowpy,∃x(¬px)
となればよく,それには,16. により
 \longrightarrowpy,¬py
となればよく,それには,5. により
 py\longrightarrowpy
となればよく,2. により,(¬(∀xpx))→∃x(¬px)は定理式です.

(例3-2 https://en.wikipedia.org/wiki/Drinker_paradox )シーケントは集合の対なので,その集合の要素を複製することが可能です.したがって,x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow∃x(px→∀xpx)
となるには
 \longrightarrow∃x(px→∀xpx),∃x(px→∀xpx)
となればよく,それには
 \longrightarrowpx→∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrow∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,py→∀xpx
となればよく,それには
 px,py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy
となればよいので,∃x(px→∀xpx)は定理式です.

こうした手続きを上下を逆にして次のツールが生成するような図で表したものをその定理式の証明図と呼びます.http://bach.istc.kobe-u.ac.jp/seqprover/

(参考)
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK