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

出自Tan Kian-ting的維基
跳至導覽 跳至搜尋
行 95： 行 95：
1  |  ...
1  |  ...
2  |_  B                Premise
2  |_  B                Premise
3  | |_ C              Assumption
3  | |_ C              Assumption # want D
4  | |  ...
4  | |  ...
5  | |  D        3  ∨I
5  | |  D        3  ∨I
行 120： 行 120：


<pre>
<pre>
1 | A->B
1 | A→B
2 | A
2 | A
3 | B
3 | B
</pre>
</pre>
===biconditional雙向條件↔===
*引入律（↔I）
<pre>
1 | |_ A
2 | |  B
3 | |_ B want A
4 | |  A
5 | A↔B  1-2, 3-4 ↔I
</pre>
*消去律（↔E）
:其一
<pre>
1 | A↔B
2 | A
3 | B  1,2 ↔E
</pre>
:另一
<pre>
1 | A↔B
2 | B
3 | A  1,2 ↔E
</pre>
===negation否定¬===
先假設A存在，最後發現推演出來的命題有互相矛盾的狀況，則否定¬A。
<pre>
m | |_ C #for reductio
n | | B
n+1 | | ¬B
n+2 | ¬C ¬I m-(n+1)
</pre>
==6.2 衍生律 (derived rule)==
爲了證明方便，將常用的證明策略稱爲衍生律，用來簡化證明。
* dilemma rule(DIL)：
<pre>
m | AvB
n | A->C
o | B->C
  | C DIL m,n,o
</pre>
* modus tollens (MT)：
<pre>
m | A->B
n | ~B
  | ~A MT m,n
</pre>
* hypothetical syllogism(HS)：
<pre>
m | A->B
n | B->C
  | A->C HS m,n
</pre>
==6.3 替換律==
===commutivity (Comm) 交換律===
*(A&B)⇔(B&A)
*(AvB)⇔(BvA)
*(A↔B)⇔(B↔A)
===double negation (DN) 雙重否定===
*~~A⇔A
===De Morgan's Laws (DeM) 笛摩根定律===
*~(AvB)⇔(~A&~B)
*~(A&B)⇔(~Av~B)
==6.4 量化邏輯律==
∀x P x, ∃x P x 的 substitition instance （替代實例），就是 P c，c 是實例化常量。c可以是變數、wff 和常數。
===全稱量詞(universal qualifier)===
*全稱消去 ∀E
<pre>
m | ∀x P x
  | P a  ∀E m
</pre>
*全稱引入 ∀I
我們不能枚舉任何的變量，來達到全稱引入。我們就用一個人工變數 a（不賦予任何意義）來做證明：
<pre>
m | P a
  | ∀ x P x  ∀I m
其中 a 不能出現於任何未消除的假設
</pre>
*存在引入 ∃I
<pre>
m | P c
  | ∃ x P x  ∃I m
</pre>
*存在消除 ∃E
**假設有人工變數i，使得P x推演到B，那麼∃x P x 可證明 B
<pre>
m | ∃x P x
n |  |_ Ai
p |  | B
  | B      ∃E m, n-p
* c 不能出現於B、子證明之外，以及 P x裏面。
</pre>
===qualifier negation（量詞否定，QN）===
*(~∀x Px)⇔(∃x ~Px)
*(~∃x Px)⇔(∀x ~Px)
==6.5同一性的律==
就算所有謂詞都讓 x, y 都有相同的證明值，但是不代表 x, y 是相同的。
*同一性引入(=I)
<pre>
| c = c =I
</pre>
*同一性消除(=E)
<pre>
m | c = d
n | A
  | Ac↺d =E m,n #↺代表所有c用d或是所有d用c替代
</pre>
==6.6證明的策略==
==6.9 soundness and completeness==
*A |- B 和 A |= B的關係？
*沒有 invalid 的 argument 的證明系統是 sound。也就是 valid 的證明前項可以推出 valid 的證明後項。（A|-B -> A|=B）
*證明系統若是 sound 的，則給出的 theorem 公理會是全真句。
*若是任何 A |= B 則 A |- B，則具有完備性 completeness，就是任何為真的命題可以證明出來。
*哥德爾證明謂詞邏輯是完備性的（註：自然數的證明就不是了）。

於 2022年7月3日 (日) 17:20 的修訂

第六章 證明

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

biconditional雙向條件↔

  • 引入律（↔I）
1 | |_ A
2 | |  B

3 | |_ B want A
4 | |  A
5 | A↔B  1-2, 3-4 ↔I
  • 消去律（↔E）
其一
1 | A↔B
2 | A
3 | B  1,2 ↔E
另一
1 | A↔B
2 | B
3 | A  1,2 ↔E

negation否定¬

先假設A存在，最後發現推演出來的命題有互相矛盾的狀況，則否定¬A。 

m | |_ C #for reductio
n | | B
n+1 | | ¬B
n+2 | ¬C ¬I m-(n+1)

6.2 衍生律 (derived rule)

爲了證明方便，將常用的證明策略稱爲衍生律，用來簡化證明。

  • dilemma rule(DIL)：
m | AvB
n | A->C
o | B->C
  | C DIL m,n,o
  • modus tollens (MT)：
m | A->B
n | ~B
  | ~A MT m,n
  • hypothetical syllogism(HS)：
m | A->B
n | B->C
  | A->C HS m,n

6.3 替換律

commutivity (Comm) 交換律

  • (A&B)⇔(B&A)
  • (AvB)⇔(BvA)
  • (A↔B)⇔(B↔A)

double negation (DN) 雙重否定

  • ~~A⇔A

De Morgan's Laws (DeM) 笛摩根定律

  • ~(AvB)⇔(~A&~B)
  • ~(A&B)⇔(~Av~B)

6.4 量化邏輯律

∀x P x, ∃x P x 的 substitition instance （替代實例），就是 P c，c 是實例化常量。c可以是變數、wff 和常數。

全稱量詞(universal qualifier)

  • 全稱消去 ∀E
m | ∀x P x
  | P a  ∀E m
  • 全稱引入 ∀I

我們不能枚舉任何的變量，來達到全稱引入。我們就用一個人工變數 a（不賦予任何意義）來做證明： 

m | P a
  | ∀ x P x  ∀I m
其中 a 不能出現於任何未消除的假設
  • 存在引入 ∃I
m | P c
  | ∃ x P x  ∃I m


  • 存在消除 ∃E
    • 假設有人工變數i，使得P x推演到B，那麼∃x P x 可證明 B
m | ∃x P x
n |  |_ Ai
p |  | B
  | B       ∃E m, n-p
* c 不能出現於B、子證明之外，以及 P x裏面。

qualifier negation（量詞否定，QN）

  • (~∀x Px)⇔(∃x ~Px)
  • (~∃x Px)⇔(∀x ~Px)

6.5同一性的律

就算所有謂詞都讓 x, y 都有相同的證明值，但是不代表 x, y 是相同的。

  • 同一性引入(=I)
| c = c =I
  • 同一性消除(=E)
m | c = d
n | A 
  | Ac↺d =E m,n #↺代表所有c用d或是所有d用c替代

6.6證明的策略

6.9 soundness and completeness

  • A |- B 和 A |= B的關係？
  • 沒有 invalid 的 argument 的證明系統是 sound。也就是 valid 的證明前項可以推出 valid 的證明後項。（A|-B -> A|=B）
  • 證明系統若是 sound 的，則給出的 theorem 公理會是全真句。
  • 若是任何 A |= B 則 A |- B，則具有完備性 completeness，就是任何為真的命題可以證明出來。
  • 哥德爾證明謂詞邏輯是完備性的（註：自然數的證明就不是了）。
取自「https://kianting.info/wiki/index.php?title=形式邏輯筆記/第六章&oldid=1732」