フィッチスタイルの自然演繹のやり方

完全に個人のメモ。復習+忘れた時に思い出す用。範囲としては論理学をつくるp214~p235。気が向いたら述語を自然演繹で導出対象にするやり方も書くかも。

論理学をつくる

式集合の充足可能性の検査には真理表、タブロー、などの複数のやり方があり、自然演繹もそれの一種。

導出線と前提棒

(1) P → Q (前提)
(2) Q → R (前提)
(3) R → S (仮定)
(4) P      (仮定)
(5) Q      (4)と(1)より {P → Q, P}
(6) R      (2)と(5)より {Q → R, Q}
(7) S      (3)と(6)より {R → S, R}
(8) P → S (4)と(7)より {P⊨S}
(9) (R → S) → (P → S) (3)と(8)より

上記だとどの式がどの前提に依存しているのかわかりにくい。 仮定が生きてるスコープを表すために、導出線、仮定の宣言に前提棒というシンタックスを導入する

• パソコンでノートを作る都合上、導出線をインデントで表す。
• 前提棒を式下の---------で表す。

(1) P → Q (前提)
(2) Q → R (前提)
-----------
    (3) R → S (仮定)
    -----------
        (4) P      (仮定)
        ------
        (5) Q      (4)と(1)より {P → Q, P}
        (6) R      (2)と(5)より {Q → R, Q}
        (7) S      (3)と(6)より {R → S, R}
    (8) P → S (4)と(7)より {P⊨S}
(9) (R → S) → (P → S) (3)と(8)より

• 導出棒上の演繹は自分が書かれた導出棒より浅い(左)に存在する前提を参照することはできない。

演繹規則

表記

• 適応した演繹規則を導出した論理式の右側にやや空白をあけて表記する
  • 本ブログではスペース4個とする
• みやすさの観点から、同じ階層の導出ではこの規則表記を一番長い論理式のスペースに合わせる

例

P       Prem
P→Q    Prem
Q       →elim

前提規則(premiss rule:Prem)

• (1)導出開始時の最初の前提棒状に書ける論理式の個数に制限はない。 例:(i)
• (2)それ以外の前提棒の上には一つしか論理式をかけない。 例:(ii)

(i)

P → q Prem
¬Q∧R   Prem
S→¬P  Prem
------

(ii)

P → q Prem
¬Q∧R   Prem
S→¬P  Prem
-----------
    P  Prem
    -------

繰り返し規則(rule of repetition: Rep)

• その導出の前提棒の上にある式を繰り返し書いて良い。

    P    Prem
    ---------
    P    Rep
P → P    → intro

復活規則(rule of reiteration:Reit)

• 依存している導出(有効なスコープである前提)を繰り返し書いても良い。

例

(P → Q) ∧ ¬Q    Prem
---------------------
P → Q    ∧ elim
¬Q        ∧ elim
    P         Prem
    ---------
    P → Q    Reit
    Q         → elim
    ¬Q        Reit

→除去規則(→ elimination: → elim)

• A → B と A が同じ導出に出てきたら、Bをその導出中に書き加えて良い

P →Q    Prem
P        Prem
---------
P →Q    Rep
P        Rep
Q        → elim

→導入規則(→ introduction: → intro)

• 前提AからBへの導出を含んでいるならば、A→Bをその導出後の項目に書き加えて良い。

P→Q    prem
Q→R    prem
    P         prem
    ----
    P → Q    reit
    Q         → elim
    Q→R      reit
    R         →elim
P → R    → intro

∧除去規則(∧ elimination: ∧ elim)

• A ∧ Bが導出の一項目として現れているなら、A,Bいずれもその同じ導入の項目として書き足して良い。

A ∧ B    Prem
A        ∧ elim

あるいは

A ∧ B    Prem
B        ∧ elim

∧導入規則(∧ introduction:∧ intro)

• AとBがいずれも同じ導出の項目として現れているなら、A∧Bをその導出の一項目として書き足して良い。　

A
B
A ∧ B    ∧ intro

↔︎除去規則(↔︎ elimination:↔︎ elim)

• A ↔ ︎BとA(あるいはB)が導出に一項目として現れていたら、その導出にもう片方のB(あるいはA)を書き加えて良い。

A ↔︎ B
A
B        ↔︎ elim

↔︎導入規則(↔︎ introduction:↔︎ intro)

• A → BとB → Aが一つの導出に一項目として現れてきていたら、その導出にA ↔ ︎︎︎Bを書き加えて良い。

A → B
B → A
A ↔︎ B    ↔︎ intro

¬削除規則(¬ elimination: ¬ elim)

• ¬¬Aの導出に¬Aを書き加えて良い

¬¬A

A    ¬ elim

¬導入規則(¬ introduction:¬ intro)

• Aを仮定とした導出から矛盾(contradiction)が発生した場合、導出の次の項目に¬Aを加えて良い

    A    prem
    ---------
    ...
    B
    ...
    ¬B    contradiction !
¬A    ¬ intro

∨除去規則(∨ elimination:∨ elim)

• A ∨ B,A→C,B→Cが導出に出てきた場合、Cを書き加えて良い

A ∨ B
A→C
B→C
C      ∨ elim

∨導入規則(∨ introduction:∨ intro)

• AかBが同じ導出において以前に一項目として出てきているなら、A ∨ Bを書き加えて良い

A
A ∨ B    ∨ intro

B
A ∨ B    ∨ intro

矛盾記号(⊥)の導入

• contradiction!を論理定項として使うとほかの∨ elimや→ introなどのオペランドとして使えるのでより演繹の自由度が上がる。
• 矛盾記号⊥を導入する。

¬elim*

• 矛盾する式集合(A,¬A)が導出に現れた場合、⊥をその導出に書き加えて良い

A
¬A

⊥ 

• ※矛盾記号の¬elim*を導入する場合、これまでの¬elimの規則はDNという名前に変更する

¬intro*

    A
    --
    ⊥
¬A

自然演繹の攻略法

【攻略法:→を目指すには】

• A → Bに達したい時,Aを前提とし、一番下にBが出てくるような導出を構成し、→ introによってA → Bを得るようにする

【攻略法:∧を目指すには】

• A ∧ Bに至りたかったら、AとBをそれぞれ別個に得るようにし、そのあとに∧ introを用いると良い。

【攻略法:間接証明】

• ¬Aを仮定して矛盾を起こして¬¬Aを導出し、¬elimでAを得ることができる。
  • 個人的に背理法のような戦略だと思う