Preuve formelle pour P → Q ≡ ¬P ∨ Q dans Fitch

Question

J'essaie de construire une preuve formelle pour 'P → Q ≡ ∨P ∨ Q' dans Fitch. Je sais que c'est vrai, mais comment le prouver?

Answer 1

J'ai finalement réussi à le résoudre:

assez simple en fait

Answer 2

Compte tenu p ⇒ q, utilisez le système Fitch pour prouver ¬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 

But ~ p | q Complet