数理論理３：構文論

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

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

（定義３－１）論理式の任意の集合の対（Ψ，Ω）をシーケントと呼び，Σから導出可能なシーケントの全体は，次の１．から16．（３．から16．を推論規則と呼びます）を満たす最小の集合です．以下，この集合に（Ψ，Ω）が属することを Ψ $\longrightarrow$ Ω で表します．

ｘが変数記号，ｔが項，Ａ，Ｂが論理式，ＣがΣの元，Ｘ，Ｙが論理式の（空でもよい）有限列ならば

１．｛｝$\longrightarrow$｛Ｃ｝
２．｛Ａ｝$\longrightarrow$｛Ａ｝

３．｛Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝
４．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ｙ｝

５．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛￢Ａ，Ｙ｝
６．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝ならば｛￢Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝

７．｛Ａ，Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ∧Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝
８．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ｘ｝$\longrightarrow$｛Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ∧Ｂ，Ｙ｝

９．｛Ｘ｝$\longrightarrow$｛Ａ，Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ∨Ｂ，Ｙ｝
10．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝かつ｛Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ∨Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝

11．｛Ａ，Ｘ｝$\longrightarrow$｛Ｂ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛Ａ→Ｂ，Ｙ｝
12．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝かつ｛Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛Ａ→Ｂ，Ｘ｝$\longrightarrow$｛Ｙ｝

13．｛Ｘ｝$\longrightarrow$｛Ａ，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛∀ｘＡ，Ｙ｝
　　ただし，Ｘ，Ｙの各論理式にｘの自由出現はないとします（これを固有変数条件と呼びます）．
14．｛Ａ内のｘの全ての自由出現をｔに置き換えたもの，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛∀ｘＡ，Ｘ｝$\longrightarrow$｛Ｙ｝
　　ただし，置き換えにより新たな束縛は生じないとします（これを代入可能条件と呼びます）．

15．｛Ａ，Ｘ｝$\longrightarrow$｛Ｙ｝ならば｛∃ｘＡ，Ｘ｝$\longrightarrow$｛Ｙ｝
　　ただし，固有変数条件は満たされているとします．
16．｛Ｘ｝$\longrightarrow$｛Ａ内のｘの全ての自由出現をｔに置き換えたもの，Ｙ｝ならば｛Ｘ｝$\longrightarrow$｛∃ｘＡ，Ｙ｝
　　ただし，代入可能条件は満たされているとします．

なお，（定義３－１）も（定義１－２）のように「適当な・・・によって・・・と表せるもの」という表現も可能です．そして

・　｛Ｘ｝$\longrightarrow$｛Ｙ｝を Ｘ $\longrightarrow$ Ｙ 或いは Σ $\vdash$ Ｘ $\longrightarrow$ Ｙ と書きます．また，とくに Σ $\vdash$ $\longrightarrow$ Ａ を Σ $\vdash$ A（Σが空集合ならば $\vdash$ A）と書き，これを「ＡはΣの構文論的帰結」或いは「ＡはΣの定理式」或いは「ＡはΣから証明可能」（Σ が空集合ならば「Ａは定理式」或いは「Ａは証明可能」）と読みます．
・　（定義３－１）の集合は帰納的に定義されているので，１．または２．から｛Ｘ｝$\longrightarrow$｛Ｙ｝に至る過程に現れるΣの元は有限個です．従って，Σ $\vdash$ Ｘ $\longrightarrow$ Ｙならば，Σの有限部分集合Σ’が存在して Σ’ $\vdash$ Ｘ $\longrightarrow$ Ｙ となります．
・　固有変数条件を満たさない代入を許すと，例えば，ｘが変数記号，ｐが１項述語記号ならば，ｐｘ→∀ｘｐｘ が定理式になってしまいます．
・　代入可能条件を満たさない代入を許すと，例えば，ｘが変数記号，ｐが１項述語記号ならば，∀ｘｐｘｘ→∃ｘ∀ｙｐｘｙ が定理式になってしまいます．

（例３－１）ｘ，ｙが異なる変数記号，ｐが１項述語記号ならば
　$\longrightarrow$（￢（∀ｘｐｘ））→∃ｘ（￢ｐｘ）
となるには，11. により
　￢（∀ｘｐｘ）$\longrightarrow$∃ｘ（￢ｐｘ）
となればよく，それには，６. により
　$\longrightarrow$∀ｘｐｘ，∃ｘ（￢ｐｘ）
となればよく，それには，13. により
　$\longrightarrow$ｐｙ，∃ｘ（￢ｐｘ）
となればよく，それには，16. により
　$\longrightarrow$ｐｙ，￢ｐｙ
となればよく，それには，５. により
　ｐｙ$\longrightarrow$ｐｙ
となればよく，２. により，（￢（∀ｘｐｘ））→∃ｘ（￢ｐｘ）は定理式です．

（例３－２ https://en.wikipedia.org/wiki/Drinker_paradox ）シーケントは集合の対なので，その集合の要素を複製することが可能です．したがって，ｘ，ｙが異なる変数記号，ｐが１項述語記号ならば
　$\longrightarrow$∃ｘ（ｐｘ→∀ｘｐｘ）
となるには
　$\longrightarrow$∃ｘ（ｐｘ→∀ｘｐｘ），∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　$\longrightarrow$ｐｘ→∀ｘｐｘ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$∀ｘｐｘ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$ｐｙ，∃ｘ（ｐｘ→∀ｘｐｘ）
となればよく，それには
　ｐｘ$\longrightarrow$ｐｙ，ｐｙ→∀ｘｐｘ
となればよく，それには
　ｐｘ，ｐｙ$\longrightarrow$ｐｙ，∀ｘｐｘ
となればよく，それには
　ｐｙ$\longrightarrow$ｐｙ，∀ｘｐｘ
となればよく，それには
　ｐｙ$\longrightarrow$ｐｙ
となればよいので，∃ｘ（ｐｘ→∀ｘｐｘ）は定理式です.

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

（参考）
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK