目標を持った証明についての基本的な質問 $\exists x P(x)$
Velleman、How To Prove It？では、フォームの目標を証明することを学びます $\exists x P(x)$ ゴールから存在記号を抽出し、任意の変数xに値を割り当てて、導出することによって $\exists x P(x)$導入された仮定から。以下の例では、証明するために$\exists y[y+2x=0]$ （1）、 $y$ それに値を割り当てます $-2x$ （2）そしてこの仮定（3）から目標を導き出します。
- $\exists y[y+2x=0]$
- $ [y=-2x] \rightarrow [y+2x=0]$
- $ [y=-2x] \space \land \exists y[y+2x=0] \rightarrow [y+2x=0]$
yへの値の割り当てを証明の与えられたものの1つとしてどのように仮定することができるのか私は本当に理解していません。数学的な平等は論理的にトートロジーとして扱われるので、どのような証明でも無制限に仮定することができますか？
回答
「私たちは $y$ それに値を割り当てます $−2x$「おそらくあなたが考えていることを意味するものではありません。私たちは仮定しません $y$ - $y$は命題ではないので、私たちはそれを仮定することはできません。私たちはその提案を想定していません$[y]$、どちらか。私たちがしていることは、「あなたが知っているなら$y$ この特別な値に設定されました、 $y = -2x$、それならこれはすべてうまくいく。」
したがって、「$y = -2x$"。これは自動ではありません。舞台裏の代数を実行して、の特別な価値を見つける必要がありました。 $y$このすべてを機能させます。その代数は表示されていません。の値の正しい選択から始めるだけです$y$。したがって、$y = -2x$、つまり、「$[y = -2x]$"（本当です）。
その仮定は結果をもたらします。特に、あなたは導き出すことができるはずです $$ [y = -2x] \rightarrow [y+2x = 0] $$ に沿って $$ y + 2x = (-2x) + 2x = 0 \text{.} $$ これには代数の使用が必要です。論理だけを使用してこの加算を実行する方法はありません。加法逆元に関する代数的事実を知っている必要があります。
だからあなたは得る $[y = -2x] \rightarrow [y+2x = 0]$。これにより、推測することができます$\exists y [y+2x=0]$、あなたは実際にどの専門分野を知っているので $y$ これを真実にします、すなわち $y = -2x$。
3行目は少し奇妙に見えます。私たちが実際に持っているのは $$ \left( [y = -2x] \rightarrow [y+2x = 0] \right) \rightarrow \exists y[y+2x = 0] \text{.} $$ つまり、「専門化以来 $y = -2x$ 作る $y + 2x = 0$、私たちは存在すると結論します $y$ そのような $y+2x = 0$。" それ $y$ です $-2x$。
これをどのように書き出すのですか？条件文を作成したことに注意してください： "if$y$ です $-2x$、その後 $y+2x = 0$。 "これはサブプルーフになります。
... 何とか何とか何とか ...
しましょう $y = -2x$。観察する$y+2x = (-2x)+2x = 0$。だから私たちは推測します$\exists y [y+2x = 0]$。
... 何とか何とか何とか ...
議論の形式は何ですか？
- しましょう $y = \{\text{a value that works}\}$。この例では、代数を使用してその値を見つけます。
- 存在記号で定量化された述語の式が、変数の割り当てによって真になることに注意してください。 $y$ 前のステップの値に。
- の値が存在すると結論付ける $y$これにより、存在記号の述語が真になります。（つまり、最初のステップで展示したものです。）
「」の2つの異なる使用法によって引き起こされる少しの混乱があるかもしれないと私は思います。$y$「証明フォームのステートメントでは、 $$ \left( [y = -2x] \rightarrow [y+2x = 0] \right) \rightarrow \exists y[y+2x = 0] \text{.} $$ 右側の変数 $y$存在記号に拘束されます。構文スコープは、数量化された句が終了するまでのみです。それを別の変数に置き換えて、意味的に同等のステートメントを取得することができます。 $$ \left( [y = -2x] \rightarrow [y+2x = 0] \right) \rightarrow \exists z[z+2x = 0] \text{.} $$ これはまだ有効な推論です。
左側の、 $x$ そして $y$定量化されていないように見えるので、それらは自由（束縛の反意語）変数です。自由変数は、最大の囲みスコープで暗黙的に全称記号化されます。その数量化を明示的にする場合、構文の妥当性を維持するために右側の束縛変数を変更する必要があります。（つまり、次のステートメントがあると構文エラーになります$y$ ネストされた句で2回バインドされます。 $y$ 2つの互いに素な節でバインドできますが、2つは $y$sは同じ値である必要はありません。）したがって、暗黙の数量化では、 $$ \forall x \forall y \left( \left( [y = -2x] \rightarrow [y+2x = 0] \right) \rightarrow \exists z[z+2x = 0] \right) \text{.} $$
コメントであなたが提案したので、私はこれについて議論します $$ \left( [y = -2x] \rightarrow [y+2x = 0] \right) \rightarrow \left( [y = -2x] \rightarrow \exists z[z+2x = 0] \right) \text{.} $$ これは、上記の証明フォームよりもはるかに弱く、その理由は、の無制限の使用に関係しています。$y$ そして $x$右側の括弧内の意味で。左側の括弧で囲まれた意味は次のとおりです。
いくつかの証拠で、あなたが事実を持っているなら」$y = -2x$「すでに確立されているなら、あなたは事実を推測するかもしれません」$y + 2x = 0$"。
これには、コンテキスト内の暗黙的に全称記号化された変数の状態に、それが含まれている、または暗示されている必要があります。 $y = -2x$結果を得るために。同様に、右側の括弧で囲まれた意味は次のように述べています。
（先行詞、左側の括弧で囲まれた含意がすでに確立されていると仮定します）何らかの証拠で、あなたが事実を持っている場合 "$y = -2x$「すでに確立されているなら、あなたは事実を推測するかもしれません」$\exists z [z + 2x = 0]$"。
この右側の含意は明白な主張をしません」$\exists z [z + 2x = 0]$ 「真である」。それは、「暗黙的に全称記号化された変数の状態」というはるかに弱い主張をします。 $x$ そして $y$ あなたの文脈ではそれを含むか暗示する必要があります $y = -2x$そして、あなたは推測するかもしれません$\exists z [z + 2x = 0]$ 本当です」。
だが "$\exists z [z + 2x = 0]$"は自由変数から独立している必要があります$y$。（同等に、 "$\exists y [y + 2x = 0]$"は自由変数から独立している必要があります$y$、自由変数以来 $y$ この定量化された条項では言及されていません。）
作成したバージョンは、（自由変数）コンテキストで存在記号の結果のみをアサートするため、脆弱です。 $y = -2x$。だが$\exists z [z+2x = 0]$すべてのコンテキストで真である必要があります（マテリアルが関係を持っている場合$[y = -2x] \leftrightarrow [y+2x=0]$）、バインドされていない変数の値に関係なく $x$ そして $y$。