如何使用 Fitch 系统证明 ((p ⇒ q) ⇒ p) ⇒ p

Question

仅供参考，我使用的逻辑程序无法进行矛盾引入。这一点很可能是无关紧要的，因为我非常怀疑我是否需要使用任何形式的矛盾来证明这一点。

在尝试解决这个问题时，我首先假设 (p ⇒ q) ⇒ p)
这是正确的吗？

如果是这样，接下来怎么办？如果解决方案看起来如此明显，请原谅我。

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

Answer 2

这（可能）不是最优雅的。我用

=>

表示蕴涵，用

~

表示否定。

1.  | (p => q) => p            ; Assumption
2.  | | p                      ; Assumption
3.  | | p                      ; Restatement (line 2)
4.  | p => p                   ; Implication introduction (lines 2-3)
5.  | | ~p                     ; Assumption
6.  | | ~p                     ; Restatement (line 5)
7.  | ~p => ~p                 ; Implication introduction (lines 5-6)
8.  | | ~p                     ; Assumption
9.  | | | ~q                   ; Assumption
10. | | | ~p                   ; Restatement (line 8)
11. | | ~q => ~p               ; Implication introduction (lines 9-10)
12. | | | p                    ; Assumption
13. | | | | ~q                 ; Assumption
14. | | | | p                  ; Restatement (line 12)
15. | | | ~q => p              ; Implication introduction (lines 10-11)
16. | | | ~(~q)                ; Negation introduction (lines 11, 15)
17. | | | q                    ; Negation elimination (line 16)
18. | | p => q                 ; Implication introduction (lines 12-17)
19. | | p                      ; Implication elimination (lines 1, 18)
20. | ~p => p                  ; Implication introduction (lines 8-19)
21. | ~(~p)                    ; Negation introduction (lines 7, 20)
22. | p                        ; Negation elimination (line 21)
23. ((p => q) => p) => p       ; Implication introduction (lines 1-22)
Conclusion: ((p => q) => p) => p