※ 引述《Favonia (小西風最乖了*^^*)》之銘言：
: 推 rewqrewwq:不用排中律的話，假設P搞出~P，就是證明了P -> ~P 02/09 11:38
: → rewqrewwq:也等同於 ~P or ~P (A->B等價於~A or B)，也就證明了 ~P 02/09 11:39
對也不對。在零階直覺邏輯中這些都等價：
1. 排中律: A or ~A
2. Peirce: ((A -> B) -> A) -> A
3. De Morgan
4. 你用的古典邏輯定理: (A -> B) <-> (~ A or B)
5. 反證法: ~~A -> A
6. ...
（族繁不及備載）
所以你的論證方法還是用了跟排中律等價的東西。但
(P -> ~P) -> ~P 在零階直覺邏輯裡面確實可以證明。濫
用 Curry-Howard 對應我可以寫下 simply-typed lambda
term:
| lam x:(P -> ~P) . lam y:P . x y y
上面這個 term 的 type 是 (P -> ~P) -> ~P, 對應
到（某一版本的）零階直覺邏輯中定理 (P -> ~P) -> ~P
的證明。簡單來說上面那行已經證明了這個定理了。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.30.39