logic - 致力于逻辑 - 惠誉系统

Question

与逻辑和惠誉系统作斗争，

给定 (p ⇒ ¬q) 和 (¬q ∧ p ⇒ r) 和 p，我正在尝试使用 Fitch System 来证明 r。

关于我应该如何进行的任何想法？

Answer 1

您还可以尝试其他形式的证明系统，这些系统可用作计算机实现的证明检查器。使用Isabelle的结构化证明语言，您可以这样编写证明：

theory Scratch
imports Main
begin

notepad
begin
  assume 1: "p ⟶ ¬ q"
    and 2: "¬ q ∧ p ⟶ r"
    and 3: p
  have "¬ q" using 1 and 3 ..
  then have "¬ q ∧ p" using 3 ..
  with 2 have r ..
end

end

Answer 2

1. (p ⇒ ¬q)
2. (¬q ∧ p ⇒ r)
3. p
4. ¬q（1 3 隐含消除）
5. ¬q ^ p (2 4 和介绍)
6. r (2 5 隐含消除) ---> END

Answer 3

以下证明使用 Klement 的 Fitch 式自然演绎证明检查器。规则说明可在forallx中找到。

前三行是前提。第 4 行来自条件消除 (→E)，第 5 行来自连词介绍 (∧I)，最后一行来自条件消除。

---

参考

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/