Comment prouver (p ⇒ q) ⇒ p) ⇒ p, en utilisant le système Fitch

Question

FYI, le programme logique que j'utilise ne peut pas faire des introductions de contradictions. Ce point est probablement hors de propos, car je doute fort que je doive utiliser n'importe quelle forme de contradiction pour cette preuve. Dans ma tentative pour résoudre ce problème, j'ai commencé par supposer (p ⇒ q) ⇒ p)
Est-ce correct?

Si oui, que faire ensuite? Pardonnez-moi si la solution semble si évidente.

Answer 1

(p ⇒ q) ⇒ p 
((p ⇒ q) ⇒ p) ∨ (p ⇒ p)  ; (X ⇒ X) and Or introduction 
((p ⇒ q) ∨ p) ⇒ p    ; (X ⇒ Z) ∨ (Y ⇒ Z) |- (X ∨ Y ⇒ Z) 
((¬p ∨ q) ∨ p) ⇒ p    ; (p ⇒ q) ⇔ (¬p ∨ q) 
((¬p ∨ p) ∨ q) ⇒ p    ; (X ∨ Y) ∨ Z |- (X ∨ Z) ∨ Y 
(true ∨ q) ⇒ p     ; (¬X ∨ X) ⇔ true 
true ⇒ p      ; (true ∨ X) ⇔ true 
p        ; Implication elimination 
((p ⇒ q) ⇒ p) ⇒ p    ; Implication introduction