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

Question

在惠誉中，我试图构造((p⇒q)⇒p)⇒p的一个形式证明。我知道这是真的，但我怎么证明呢？

我只能使用和介绍，和Elim，或Inro，或Elim，Neg Intro，Neg Elim，Impl Intro，Impl Elim，Biconditional，和Biconditional Elim。

Answer 1

下面的证明使用的是凯特姆的惠誉风格的验证检查器。符号和规则的描述用forallx表示。链接到这两个都在下面。

​

​

一个稍微不同的版本是在哲学堆栈交换：https://philosophy.stackexchange.com/a/55395/29944，这将是另一个地方，试图获得这样的问题的答案。

参考文献

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

P.D. Magnus，Tim Button，J. Robert Loftis重新混合和修订，由Aaron Thomas-Bolduc，Richard Zach，forallx Calgary Remix: A Introduction to Formal Logic，2018年冬季。http://forallx.openlogicproject.org/