Fitch系统的逻辑推理答案

【问题标题】：Logic deduction with Fitch systemFitch系统的逻辑推理
【发布时间】：2013-04-12 01:21:31
【问题描述】：

我正在研究一些逻辑，但我发现了一个我无法解决的困难，

我如何从前提 p=>q 证明 ¬q=>¬p？

谢谢

【问题讨论】：

我认为它直接来自定义。
欢迎来到 SO！鉴于这是一个协作网站，我们非常鼓励您展示您迄今为止所做的工作。请发布您尝试过的证明。

标签： logic proof fitch-proofs

【解决方案1】：

使用惠誉系统：

p=>q............前提
。| ¬q............假设
.|.| p............假设
.|.| q............隐含消除：1,3
.|.| ¬q............重复：2
。| p=>¬q............蕴涵介绍：5
。| ¬p............否定介绍：1,6
¬q=>¬p............含意介绍：7

不是那么整齐的布局，但每个“缩进”代表在假设的帮助下完成的子证明。

【讨论】：

【解决方案2】：

去除冗余步骤进行微调：

使用惠誉系统：

p=>q............前提
| ¬q............假设
|.| p............假设
|.| ¬q............重复：2
| p=>¬q............含意介绍：4
| ¬p............否定介绍：1,5
¬q=>¬p............含意介绍：6

【讨论】：

【解决方案3】：

这是一个使用 Fitch 风格的证明检查器的证明。规则的解释在 forallx 中。这两份参考资料都可以在线获得，并在下面列出：

参考

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/

【讨论】：