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

【问题标题】：How would one prove ((p ⇒ q) ⇒ p) ⇒ p, using the Fitch system如何使用 Fitch 系统证明 ((p ⇒ q) ⇒ p) ⇒ p
【发布时间】：2017-02-16 23:57:26
【问题描述】：

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

为了解决这个问题，我开始假设 (p ⇒ q) ⇒ p)
这是正确的吗？

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

【问题讨论】：

我为另一个问题提供的证明使用了矛盾介绍，因此可能无法接受：stackoverflow.com/a/53454649/6055422 根据皮尔斯规则，维基百科中有证明：en.wikipedia.org/wiki/Peirce%27s_law 但考虑到以下限制，它们可能也不起作用你可以使用的规则。

标签： logic implication fitch-proofs

【解决方案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

【讨论】：

此解决方案中的许多步骤不能简单地使用 10 条推理规则得出，即 And Intro、And Elim、Or Inro、Or Elim、Neg Intro、Neg Elim、Impl Intro、 Impl Elim、Biconditional Intro 和 Biconditional Elim。我不能使用命题解析：(p ⇒ q) ⇔ (¬p ∨ q)。在 (p ⇒ q) ⇒ p 的证明中，我必须使用我提到的这 10 条规则来证明 (p ⇒ q) ⇔ (¬p ∨ q)
@AndrewGuo 你对p ⇒ q的定义是什么？
p 暗示 q（我的评论必须是 15 个字符的长度，所以我会加上这个括号）
@AndrewGuo 一句话，即'p蕴含q'不是一个定义。 p ⇒ q 的普遍接受的定义正是¬p ∨ q，我在回答中使用了它。如果你想要(p ⇒ q) ⇔ (¬p ∨ q) 的证明，你必须提供(p ⇒ q) 的定义。