作者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