0

我试图解决以下问题，但我无法检查它....或者 wolfram 会这样做吗？我不知道我对运算符（范围）的处理是否是 occrect...你知道吗？对于所有 x：颠倒的 A 运算符（通用性）

there exists an x: inverted E operator (existence)

for all x(P(x) -> R(x)), for all x(P(x) v not_Q(x)); there exists an x(Q(x)) hold under partial correctness: there exists an x(R(x))

证明：在此处输入图像描述

4

2 回答 2

2

您的推论结构是合理的，但缺少将您从量化陈述带到特定然后再回到量化的步骤。

说这P-->Q与第一个前提“等价”是不正确的：这是将谓词陈述曲解为命题陈述。你可以说的是，如果第一个前提对所有 x 都成立，那么它肯定对一个特定的 x 成立。所以第一个前提的通用实例化可以给你P(a)-->R(a)。类似地，由于第三个前提告诉我们至少有一个 x 使得 Q(x)，我们可以说让我们称其中一个 x 为“a”，因此声称Q(a)。

一旦你达到了你已经证明的地步，你就R(a)可以使用存在泛化来得到你的最终结论。

于 2014-02-07T03:20:04.363 回答
1

我不同意@MattClarke，因为您的推理结构是合理的。它不遵守自然扣除的规则。例如，您的盒装证明假设Q和~Q（我~用于否定）并得出结论P。但是没有自然的演绎规则允许您在一个盒子内使用多个假设（即使有，并且这样的规则可能是合理的，那么装箱证明的结果并不P像您声称的那样，而是暗示(Q /\ ~Q) --> P，这是微不足道的，因为已经有一个自然的演绎规则允许我们从矛盾中推断出任何东西）。

从 OP 来看，我并不清楚你到底想证明什么。我只是假设从三个前提ALL x. (P(x) --> R(x))中，ALL x. (P(x) \/ ~Q(x))，并且EX x. Q(x)你想证明EX x. R(x)。

由于您要证明的公式以存在量词开头，因此它将通过存在介绍获得。但首先我们从前提开始：

 1 ALL x. (P(x) --> R(x)) premise  
 2 ALL x. (P(x) \/ ~Q(x)) premise  
 3 EX x. Q(x)             premise

存在消除规则打开一个框（框将用大括号{和表示}）并允许我们得出一个公式，该公式在假设存在适用该规则的存在公式的证人的情况下是可证明的，即

 4 { for an arbitrary but fixed y that is not used outside this box
 5 Q(y)                   assumption  
 6 P(y) \/ ~Q(y)          ALL-e 2

在这一点上，我们应用了析取消除，这相当于案例分析是否P(y)成立~Q(y)（至少其中一个必须为真，因为我们有P(y) \/ ~Q(y)）。每个箱子都有自己的盒子

 7 {  
 8 P(y)                   assumption  
 9 P(y) --> R(y)          ALL-e 1  
10 R(y)                   -->-e 9, 8  
11 }  
12 {
13 ~Q(y)                  assumption  
14 bottom                 bottom-i 5, 14  
15 R(y)                   bottom-e 15  
16 }  
17 R(y)                   \/-e 6, 7-11, 12-16  
18 EX x. R(x)             EX-i 17  
19 }  
20 EX x. R(x)             EX-e 3, 4-19
于 2014-03-31T11:32:43.987 回答