第5章 自然演繹(2)

証明系の健全性

ある証明系において、Φ├{PS}AならばΦ|=Aという証明系を健全であるという。
（PSの推論規則においてΦからAが導けるならばΦを満たすすべての解釈はAを満たす）

証明系の完全性

ある証明系において、Φ|=AならばΦ├{PS}Aという証明系を完全であるという。

5.5 自然演繹(NK)の健全性

Φ├{PS}AならばΦ|=Aと同等な証明として
すべての証明木Πに対してΦ(Π)|=Concl(Π)を証明する
（Φ(Π)は証明木Πの仮定の集合　Φ(Π)={A|i:A∈Asmp(Π)}

(鄯) 基底段階
Πが仮定規則で構成される証明木ならば、明らかにΦ(Π)|=Concl(Π)である。また排中律はConcl(Π)が恒真であるので、Φ(Π)|=Concl(Π)である。

(鄱) 帰納段階
・⊃導入のケース
Π1はすでに証明済みであるとして、Πについて証明する。

• Π1は証明木
• {i:A}∪Asmp(Π1)は部分関数である。
  • 意味：Aの番号はiだよんってこと
• Concl(Π1)=B
• Π={(ε,A⊃B)}∪1・Discharge(Π1,i:A)

I|=Φ(Π)かつI(A)=trueとなる任意の解釈Iをとる。

• i:A∈Asmp(Π)のとき
  • Asmp(Π)=Asmp(Discharge(Π1,i:A))=Asmp(Π1)-{i:A}
  • ∴Asmp(Π)∪{i:A}=Asmp(Π1)
  • Φ(Π)∪{i:A}=Φ(Π1)
  • I|=Φ(Π)かつI(A)=trueなので上の式からI|=Φ(Π1)がいえる
  • よってI(B)=true
• i:A∈Asmp(Π)でないとき
  • Asmp(Π)=Asmp(Discharge(Π1,i:A))=Asmp(Π1)
  • ∴Asmp(Π)=Asmp(Π1)
  • Φ(Π)=Φ(Π1)
  • I|=Φ(Π)なので上の式からI|=Φ(Π1)がいえる
  • よってI(B)=true

・∀導入のケース
Π1はすでに証明済みであるとして、Πについて証明する。

• Π1は証明木
• Π={(ε,∀xA)}∪Π1
• Concl(Π1)=A[y/x]
• Concl(Π)=∀xA
• Asmp(Π)=Asmp(Π1)

であり、yはアイゲンバリアブル条件を満たすとする。

• I|=Φ(Π)となる任意の解釈Iをとる。
• d∈|I|となるdを任意に選ぶと、必ずI{x→d}A=true。
• I|=Φ(Π)であるから、アイゲンバリアブル条件により、I{y→d}|=Φ(Π1)
• Φ(Π1)|=A[y/x]なので、I{y→d}|=A[y/x]…I{y→d}A[y/x]=true
• 補題4.4.5の2よりI{y→d}A[y/x]=I{y→d}{x→d}A
• 補題4.4.3の6よりI{y→d}{x→d}A=I{x→d}A=true

よってI|=∀xA