0

私は以下を解決しようとしましたが、それを確認する手段がありません....または、ウルフラムはこれを行いますか? オペレーター（スコープ）の扱いが正確かどうかわかりません...知っていますか？すべての 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 に当てはまる場合、それは特定の 1 つの x に確かに当てはまるということです。したがって、最初の前提の普遍的なインスタンス化により、 が得られますP(a)-->R(a)。同様に、第 3 の前提は、Q(x) となる x が少なくとも 1 つあることを示しているため、これらの x の 1 つを「a」と呼び、 を主張すると言えますQ(a)。

証明R(a)できるところまで来たら、実存的一般化を使用して最終的な結論を得ることができます。

于 2014-02-07T03:20:04.363 に答える
1

あなたの推論の構造が合理的であるという点で、@MattClarkeに同意しません。自然演繹法には従いません。たとえば、ボックス化された証明ではQ、and ~Q(~否定に使用しています) と結論付けPます。しかし、ボックス内で複数の仮定を使用できるようにする自然な演繹規則はありません (たとえあったとしても、そのような規則が正当化できたとしても、ボックス化された証明の結果は、Pあなたが主張しているように見えるだけではなく、むしろ、(Q /\ ~Q) --> P矛盾から何かを演繹することを可能にする自然な演繹規則がすでに存在するため、これは些細なことです)。

OPからは、正確に何を証明したいのかがはっきりしません。3 つの前提からALL x. (P(x) --> R(x))、ALL x. (P(x) \/ ~Q(x))、およびEX x. Q(x)を証明したいと思っているだけですEX x. R(x)。

証明したい数式は存在量指定子で始まるので、exists-introduction によって取得されます。しかし、最初に前提から始めます。

 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)ます ( があるので、少なくとも 1 つが真でなければなりません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 に答える