作者Favonia (小西风最乖了*^^*)
看板logic
标题Re: [请益] 反证法
时间Tue Apr 3 22:39:30 2012
※ 引述《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