形式邏輯筆記/第六章

導航：首頁 > 程式語言、邏輯學>形式邏輯筆記> 形式邏輯筆記/第六章

第六章 證明

一堆命題序列，由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