第6章シークェント計算(4)

Gの完全性の証明（続き）

復習
公平な導出木
ΦとΨ（各辺の無限経路のある位置以上の位置に存在し続ける論理式の和集合）

任意のシークェントに対して公平な導出木が存在する。

→展開レベルの小さいものから展開する。

補題6.7.6
※このとき、有限な公理で終了していない経路についても検討する対象とする。このため公平な導出木について定義したΦとΨに、有限な経路を含めた新しいΦとΨについて以下の定理が成り立つ。
公平な導出木Πに対して次が成り立つ

A∈Φ∩ΨならばAは原子論理式ではない

A∧B∈ΦならばA∈ΦかつB∈Φ。A∧B∈ΨならばA∈ΨかつB∈Ψ。

A∨B∈ΦならばA∈ΦまたはB∈Φ。A∨B∈ΨならばA∈ΨまたはB∈Ψ。

A⊃B∈ΦならばA∈ΨまたはB∈Φ。A⊃B∈ΨならばA∈ΦかつB∈Ψ。

（シークェント計算を見るとなんとなくわかりそう）

∃xA∈Φならばある変数yに対してA[y/x]∈Φである。∀xA∈Ψならばある変数yに対してA[y/x]∈Ψである。

∀xA∈Φかつt∈Hsならば、A[t/x]∈Φである。∃xA∈Φかつt∈HsならばA[t/x]∈Ψである。

（証明）
1について（背理法で証明）
2について。どこかで推論規則（L∧）による展開が行われるから、成り立つ。同様に、どこかで推論規則（R∧）による展開が行われるから、成り立つ。
3について。どこかで推論規則（L∨）による展開が行われるから、成り立つ。同様に、どこかで推論規則（R∨）による展開が行われるから、成り立つ。
（省略）
7について。有限の経路ではこのケースは存在しない。無限の経路に置いては、公平性の条件より存在する。

完全性

証明…プリントに書いた