歸謬證法反證法?

反證法是指用 RAA, 或是證明否逆命命題, 或是排中律證明的。而用 law of contradiction 並不是反證法,因為在構造式證明中, Law of contradiction \neg (P \wedge \neg P) 是成立的,而 RAA 則是構造式證明中唯一被拿掉的公設。證明如下:

對於 Law of contradiction,我們可以用 conjunction elimination, implication 推出來,不需要其他的條件:
0. P \wedge \neg P by assumption
1. P, by conjunction elimination from 0.
2. \neg P \equiv P \rightarrow \bot, by conjunction elimination from 0.
3. \bot, by modus ponens from 1. 2.
4. P \wedge \neg P \rightarrow \bot \equiv \neg (P \wedge \neg P), by conditional proof discharging (1)

而另外一種反證法的形式,講的是 (\neg Q \rightarrow \neg P) \rightarrow (P \rightarrow Q),跟 RAA 是 tautology,先證明 RAA 這邊開始:

0. \neg Q, by assumption
1. \neg Q \rightarrow \neg P, by assumption
2. P, by assumption
3. \neg P \equiv P \rightarrow \bot, by modus ponens from 0. 1.
4. \bot, by modus ponens from 2. 3.
5. \neg Q \rightarrow \bot \equiv \neg \neg Q, by discharging 0. and 4.
6. Q, by RAA from 5.
7. P \rightarrow Q, by discharging from 2. and 5.
8. (\neg Q \rightarrow \neg P) \rightarrow (P \rightarrow Q), by discharging from 1. and 7.

再來是這個否逆命題推回 RAA:
0. \neg P, by assumption
1. \neg \neg P, by assumption
2. \neg P \rightarrow \neg \neg P, by discharging 0. and 1.
3. \neg P \rightarrow P, by 否逆命題
4. P, by MP from 0. 3.
5. \neg \neg P \rightarrow P, by discharging 1. 4.
(0. 1. 應該分別假設兩次, 再各自消掉就是了)

所以在 meta-language 的層次上證明,RAA 與「否逆命題與原命題等價」是等價的,另外 RAA 又比排中律弱,可以從排中律推到 RAA,但反過來卻不行。(排中律有多強啊 … 錯了,請看下面的回覆 orz

Advertisements

3 thoughts on “歸謬證法反證法?

  1. 最後一句看不懂耶。

    我以前以為反證法講的就是用排中律證東西。這麼一看才發現一般用到的只是 ¬ ¬ P → P 而已。

    • 以下用 agda code 來表示:
      先證明 disjunction 可以用 conjunction 以及 negation 組合出來,從 disjunction 出發的話是構造式的,不需要用到 RAA 就可以得到,但是反過來,就必須要用到 RAA。

      classical-or : ∀ {P Q} → ¬ (¬ P × ¬ Q) → P ⊎ Q
      classical-or ¬[¬P∧¬Q] = RAA (λ ¬[P∨Q] → ¬[¬P∧¬Q] ((λ x → ¬[P∨Q] (inj₁ x)) , λ x → ¬[P∨Q] (inj₂ x)))

      另外一邊方向是直觀的。接下來證明 Law of contradiction,雖然上面用演繹法(deduction)寫了五行, 但是在 agda 下只要 …

      non-con : ∀ {P} → ¬ (P × ¬ P)
      non-con (p , ¬p) = ¬p p

      原本要各寫一行的 elimination rule 跟 introduction rule 在左邊就變成 pattern matching 跟右邊的 application。

      最後的 law of excluded middle 就將以上兩個證明組合起來,把 law of contradiction 中的 P 換成 \neg P,就會得到 \neg (\neg P \wedge \neg (\neg P)),接下來根據 disjunction 等價,就會得到 P \vee \neg P 成立。

      EM : ∀ {P} → P ⊎ ¬ P
      EM {P} = classical-or non-con

    • 另外,因為 propositional calculus 上的 completeness 性質,只需要檢驗其語意,就可以確保有 derivation 可以演繹出其目標的述句,其證明有非構造式的以及構造式的(根據 curry-howard isomorphism 來看,也就是有個演算法給定述句就可以構造出 derivation)。而 completeness 性質則可以將繁複的演繹證明,直接從語意來判定,所以不需要真正將演繹做出來,就可以說明有效性了。

      雖然難的部份都是說明了有效性之後,我們要怎麼推出演繹的過程 …

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s