惠誉中P→Q≡≡P∨Q的形式证明

Question

我试图在惠誉中构造'P→Q≡≡P∨Q'的形式证明。我知道这是真的，但我怎么证明呢？

Answer 1

我终于设法解决这个问题：

相当直截了当实际上

Answer 2

已知P⇒Q，使用惠誉系统证明¬p∨Q值。

1. p => q   Premise 
2. ~(~p | q)  Assumption 
3.  ~p   Assumption 
4.  ~p | q  Or Introduction: 3 
5. ~p => ~p | q Implication Introduction: 3, 4 
6.  ~p    Assumption 
7.  ~(~p | q)  Reiteration: 2 
8. ~p => ~(~p | q) Implication Introduction: 6, 7 
9. ~~p    Negation Introduction: 5, 8 
10. p    Negation Elimination: 9 
11. q    Implication Elimination: 1, 10 
12. ~p | q   Or Introduction: 11 
13. ~(~p | q) => ~p | q  Implication Introduction: 2, 12 
14. ~(~p | q)     Assumption 
15. ~(~p | q) => ~(~p | q)  Implication Introduction: 14, 14 
16. ~~(~p | q)     Negation Introduction: 13, 15 
17. ~p | q      Negation Elimination: 16 

Goal〜p | q完成