第5章 自然演繹

数理論理学

5.1 自然演繹による証明

\forall y \left[ \forall x(P(x) \supset Q(x)) \wedge P(y) \supset Q(y) \right]
を証明する。
こういうときは、勝手に選んだ値y=aを決める。
\forall x(P(x) \supset Q(x)) \wedge P(y) \supset Q(y)
が成り立つことを示せば、任意のaについて、
\forall y \left[ \forall x(P(x) \supset Q(x)) \wedge P(y) \supset Q(y) \right]
を証明できる。

この証明を木構造で表すと（めんどい）

証明木と推論規則

証明木を定義する

  • Asmp(Π)：証明木Πの上の仮定
  • Concl(Π)：証明木Πの結論
  • 恒偽命題：⊥は常に偽

ここから定義

  1. 仮定規則：仮定番号を決めると仮定が決まる。仮定は証明木である。
  2. ∧導入：Π={(ε,A∧B)}∪1・Π1∪2・Π2は証明木
    • AとBを結論とする証明木からA∧Bの証明木を作ることができる。
    • つまりA∧Bを証明したければ、A,Bを独立に証明すればよい
  3. ∧削除：
    • A∧Bを結論とする証明木からAとBをそれぞれ結論とする証明木を作ることができる。
  1. ∨導入：Π={(ε,A∧B)}∪1・Π1∪2・Π2は証明木
    • AとBを結論とする証明木からA∨Bの証明木を作ることができる。
    • つまりA∧Bを証明したければ、AかBのどちらかを証明すればよい
  2. ∨削除：[i:A]を仮定として結論をCとする証明木と、[i:B]を仮定として結論をCとする証明木があるとする。
    • A∨Bが成り立つならば、A,Bは仮定ではない→Cは成り立つとしてよい。ということ
    • ∨削除は場合分けを行っている。
    • 仮定[i:A],[i:B]は消去された
  3. ⊃導入
    • 仮定[i:A]から結論Bが導ける証明木があるとすると、A⊃Bを結論として持つ証明木がある。
    • 仮定[i:A]は消去された
  4. ⊃削除
    • A⊃BとAを両方導けるのならば、Bは導かれたとしてよい
  5. ⊥削除
    • 仮定が矛盾しているならば、任意のAが証明できる。
  6. ∀導入（難解）
    • 仮定で用いていない変数xについては∀xAを推論することができる。
    • 仮定集合のどの論理式においても自由でない変数を選ばなければならない：アイゲンバリアブル条件
    • ちなみにその選ぶ変数をアイゲンバリアブルという。
  7. ∀削除
    • ∀xAが成り立っているなら、xに任意のtを入れたA[t/x]も成り立つ。
    • A[t/x]を証明するために∀xAを証明するのはやりすぎの感がありますが…
  8. ∃導入
    • A[t/x]が成り立っているなら、∃xAも成り立つ（そりゃそうだ）
  9. ∃削除(難解)
    • ∃xAが成り立っていて、仮定[i:A[y/x] ]についてBを結論として導けるならば、Bは成り立つ。ただしyはアイゲンバリアブル条件を満たさなければならない。
  10. 排中律
    • Aと¬Aはどちらかが成り立つ。
    • （疑わしいとして物議を醸した→計算可能性の議論（古典論理から外れるのでこの講義の範囲外ｗ））

AがΦから証明できた⇒Φ├NKA

証明系の健全性

健全性：Φ├NKAならばΦ|=A