logic - A or B = B or A 证明（自然演绎）

Question

这个问题感觉应该比我做的更简单，所以我的最终问题是：有没有更简单的方法来做到这一点？在逻辑上我们知道

A v B = B v A

但是在自然演绎中，我们使用我们的 v-Introductions、RAA 等来证明这些等价性。在解决一个实践问题的过程中，我遇到了证明这个交换性质的需要，但发现它非常困难。在我看来，证明将像这样开始：

1. A v B            given
2.     ¬(B v A)     assume
3.     ¬B ^ ¬A      2, deMorgan's
4.     ¬A           3, ^-elimination
5.     ¬B           3, ^-elimination
6.     ¬A ^ ¬B      4, 5, ^-I
7.     ¬(A v B)     6, deMorgan's
?. B v A            2, 7 RAA

现在我们发现自己处于必须证明 deMorgan 的境地。没有更简单的 A v B = B v A 证明吗？

Answer 1

您可以创建真实的表格并进行比较

 A    | B     | A v B
true  | true  | true
true  | false | true
false | true  | true
false | false | false


 A    | B     | B v A
true  | true  | true
true  | false | true
false | true  | true
false | false | false

表相等，表达式相等。

Answer 2

如果不为您解决整个问题，请尝试以下方法：

Assume A
Prove that A => (BvA)
Assume B
Prove that B => (BvA)
So (AvB) => (BvA)     [That's v-intro, at least it is in Lemon's system which you appear to be using]

You've been given AvB. So modus ponens gives you BvA.

Answer 3

以下证明使用了 Klement 的证明检查器。更多信息可以在forallx文本中找到。两者的链接如下。

析取引入 (∨I) 允许以不同的顺序重建析取。

使用析取消除 (∨E) 引用析取本身（第 1 行）完成最后一行的证明，第一个析取子证明（第 2-3 行）达到预期结果，第二个析取子证明（第 4-5 行）到达在期望的结果。

---

参考

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/