logic - Fitch系统的逻辑推理

Question

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

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

谢谢

Answer 1

Fine tuning with the removal of a redundant step:

Using the Fitch System:

1. p=>q............Premise
2. | ¬q............Assumption
3. |.| p............Assumption
4. |.| ¬q............Reiteration: 2
5. | p=>¬q............Implication Introduction: 4
6. | ¬p............Negation Introduction: 1,5
7. ¬q=>¬p............Implication Introduction: 6

Answer 2

使用惠誉系统：

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

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

Answer 3

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

---

参考

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

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