((p ⇒ q) ⇒ p) ⇒ p 的形式证明答案

【问题标题】：Formal proof for ((p ⇒ q) ⇒ p) ⇒ p((p ⇒ q) ⇒ p) ⇒ p 的形式证明
【发布时间】：2017-03-16 15:51:21
【问题描述】：

我正在尝试为 ((p ⇒ q) ⇒ p) ⇒ p 构建一个正式的证明。在惠誉。我知道这是真的，但我该如何证明呢？

我只能使用 And Intro、And Elim、Or Inro、Or Elim、Neg Intro、Neg Elim、Impl Intro、Impl Elim、Biconditional Intro 和 Biconditional Elim。

【问题讨论】：

相关：How would one prove ((p ⇒ q) ⇒ p) ⇒ p, using the Fitch system
您能展示一下到目前为止您尝试过的内容吗？
起初我尝试使用 p => q 作为假设 [link]imgur.com/a/NnSou，但我进入了 ((p=>q)) => p => p。现在我尝试 ((p=>q) = > p) 作为假设，但我不知道如何获得 => p。
我刚刚发现这是皮尔斯定律。我认为没有像 p=>q 这样的前提是不可能达到 ((p=>q)) => p => p 的。

标签： logic implication fitch-proofs

【解决方案1】：

以下证明使用 Klement 的 Fitch 风格的证明检查器。符号和规则的描述在forallx中。两者的链接如下。

Philosophy Stack Exchange 上有一个稍微不同的版本：https://philosophy.stackexchange.com/a/55395/29944 那将是另一个尝试获得此类问题答案的地方。

参考文献

Kevin Klement 的 JavaScript/PHP Fitch 风格的自然演绎证明编辑器和检查器http://proofs.openlogicproject.org/

P。 D. Magnus、Tim Button 以及 J. Robert Loftis 的添加，由 Aaron Thomas-Bolduc、Richard Zach 混音和修订，forallx Calgary Remix: An Introduction to Formal Logic，2018 年冬季。http://forallx.openlogicproject.org/

【讨论】：