「形式邏輯筆記/第六章」修訂間的差異

出自Tan Kian-ting的維基
跳至導覽 跳至搜尋
行 5: 行 5:
一堆命題序列,由premises(前件)推論到結論。
一堆命題序列,由premises(前件)推論到結論。


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


==6.1 命題邏輯基本律==
==6.1 命題邏輯基本律==
行 11: 行 11:
從自然演繹系統開始。
從自然演繹系統開始。
* 邏輯操作子有有引入律 indroducion rule 和消去律 elimination rule。
* 邏輯操作子有有引入律 indroducion rule 和消去律 elimination rule。
===重新迭代律===
* reiteration 重新迭代律(R):重複自己。
* reiteration 重新迭代律(R):重複自己。
* 推論右邊的數字x代表引用某律到第x行。
* 推論右邊的數字x代表引用某律到第x行。
行 18: 行 20:
</pre>
</pre>


*conjunction交集:有A和B兩個命題,就能證明A&B存在。
===conjunction聯集&===
**引入律(&I)
有A和B兩個命題,就能證明A&B存在。
 
*引入律(&I)
<pre>
<pre>
1  |  P          Premise
1  |  P          Premise
行 25: 行 29:
3  |  (P & Q)    1,2  &I # 套用第1和第2行
3  |  (P & Q)    1,2  &I # 套用第1和第2行
</pre>
</pre>
**消去律(&E)
*消去律(&E)


<pre>
<pre>
1  |  (P & Q)    Premise
1  |  (P & Q)    Premise
2 |  P          1  &E # P&Q推論P存在
2 |  P          1  &E # P&Q推論P存在
3  |  Q          1  &E #P&Q也可以推論P存在
3  |  Q          1  &E #P&Q也可以推論Q存在
</pre>
 
===disjunction交集∨===
 
若 A 存在可推論A∨B存在。不管B實際上是假的還是真的。
 
*引入律(∨I)
 
<pre>
...
5  |  Q         
6  |  (Q v S)    5  vI
</pre>
 
*消去律(∨E):首先要消去A∨B的B,需要證明¬B。
 
<pre>
1  | (P v Q) 
2  |  ~Q       
3  |_  P  1,2  vI
</pre>
</pre>

於 2022年7月3日 (日) 14:57 的修訂

第六章 證明

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