2,633
次編輯
Tankianting(討論 | 貢獻) |
Tankianting(討論 | 貢獻) |
||
行 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 | | 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,就是任何為真的命題可以證明出來。 | |||
*哥德爾證明謂詞邏輯是完備性的(註:自然數的證明就不是了)。 |