形式邏輯筆記/第六章

第六章證明

一堆命題序列，由premises（前件）推論到結論。

本文使用 Fitcher 的演繹證明格式，證明與排版產生器請參此網站：https://mrieppel.github.io/fitchjs/

6.1 命題邏輯基本律

從自然演繹系統開始。

邏輯操作子有有引入律 indroducion rule 和消去律 elimination rule。

重新迭代律

reiteration 重新迭代律(R)：重複自己。
推論右邊的數字x代表引用某律到第x行。

1  |_  P    Premise
2  |   P    1  Reit #　第1行重複自身

conjunction聯集&

有A和B兩個命題，就能證明A&B存在。

引入律(&I)

1  |   P          Premise
2  |_  Q          Premise
3  |   (P & Q)    1,2  &I #　套用第1和第2行

消去律(&E)

1  |   (P & Q)    Premise
2  |   P          1  &E # P&Q推論P存在
3  |   Q          1  &E #P&Q也可以推論Q存在

disjunction交集∨

若 A 存在可推論A∨B存在。不管B實際上是假的還是真的。

引入律(∨I)

...
5  |   Q          
6  |   (Q v S)    5  vI

消去律(∨E)：首先要消去A∨B的B，需要證明¬B。

1  | (P v Q)   
2  |  ~Q        
3  |_  P   1,2  vI

如果用上述的證明器會比較 tricky，他不用這個證明規則，要用⊥引入（可以視爲矛盾的意思？）和⊥消除原則，讓各起源於∨左項和右項2個子證明結果證出左項，再進行消除。

Problem: (P v Q), ~Q |- P

1  |   (P v Q)    Premise
2  |_  ~Q         Premise
3  | |_  P        Assumption
4  | |   P        3  Reit
5  | |_  Q        Assumption
6  | |   ~Q       2  Reit
7  | |   ⊥        5,6  ⊥I
8  | |   P        7  (EFQ)
9  |   P          1,3-4,5-8  vE

conditional條件→

假設寫完之後加橫線

1 | A 
2 |_ B

我們要假設某個特殊狀況出現，可以用次證明，往右縮排加直線，然後再給定特殊情況的前線：

假設寫完之後加短橫線

1 | A # 1,2 是母證明的假設
2 |_ B 
3 | |_ C # 3 底下是子證明，假設的最後加橫線
4 | | ...

引入律(→I)

假設子證明假設 C 可推演到結論 G，那麼可以做條件引入，如：

1  |   ...
2  |_  B                Premise
3  | |_ C              Assumption
4  | |   ...
5  | |   D        3  ∨I
6  |   (C → D)    3-5  →I

證明案例：

Problem: A, B |- (A → (A ∨ B))

1  |   A                Premise
2  |_  B                Premise
3  | |_  A              Assumption
4  | |   (A ∨ B)        3  ∨I
5  |   (A → (A ∨ B))    3-4  →I #用連字號連結子證明起訖，子證明結束（叫做解除 discharge）。

子證明結束後不能再次開啓，另外一個證明需要解除所有的子證明。

若是要引入→引入律，那就要在子證明出現前件（p→q的q）

消去律(→E)

1 | A->B
2 | A
3 | B