形式邏輯筆記/第六章
於 2022年7月3日 (日) 14:57 由 Tankianting（討論 | 貢獻） 所做的修訂
第六章 證明
一堆命題序列，由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