作者dryman (dryman)
看板PLT
标题[问题] sequent calculus
时间Sun Jul 4 17:39:28 2010
我要问一个很蠢的问题：
|- P <-> Q
该怎麽拆解？
发现它并不存在於 sequent calculus 的规则内
难道说我只能把它转成
|- (P->Q) Λ (Q->P) 来做吗？
（而且这样还不能写这是哪一条规则！只能说by definition <-> is xxxxx）
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 140.112.46.31
1F：→ xcycl:就根据定义啊，把 P<->Q 定义成底下的形式没问题。 07/04 19:10
2F：→ xcycl:证明也是会 by theorem 来引用，不可能每次都从头推到尾 07/04 19:11
3F：→ dryman:谢谢 第一次写这种证明，所以有点战战兢兢XD 07/04 22:47