Формальное доказательство для P → Q ≡ ¬P ∨ Q в Fitch

Question

Я пытаюсь построить формальное доказательство для 'P → Q ≡ ¬P ∨ Q' в Fitch. Я знаю, что это правда, но как я могу это доказать?

Answer 1

я, наконец, удалось решить:

довольно прямо вперед на самом деле

Answer 2

Учитывая р ⇒ д, используйте Fitch системы, чтобы доказать ¬p ∨ д.

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 Завершить