存在例化についての質問
存在例化を理解するのに苦労していました。私の教科書（Rosen-Discrete Mathematics and its Applications）は、存在例化について次のように述べています。
存在例化は、∃xP（x）が真であることがわかっている場合に、P（c）が真であるドメインに要素cがあると結論付けることができる規則です。ここでcの任意の値を選択することはできませんが、P（c）が真であるacでなければなりません。通常、cが何であるかについての知識はなく、存在することだけがわかります。存在するので、名前（c）を付けて、議論を続けることができます。
これは、特定の実存的なステートメントについては私には理にかなっています。
たとえば、次のステートメントについて考えてみます。 $\exists x\in \mathbb{Z}$ $(x + 1 = 2)$。命題関数を構成する整数は1つだけです（$x + 1 = 2$）true（つまり、 $1$）。したがって、新しいシンボルであることは私には理にかなっています$c$ 「を作る1つの整数」という名前を付けるために作成することができます $x + 1 = 2$ 本当」。
ただし、ステートメントを検討してください $\exists x\in \mathbb{Z}$ $(x * 0 = 0)$。命題関数を作る多くの整数があります（$x * 0 = 0$）true（例： $1$、 $2$、 $3$）。
この場合、新しいシンボルを作成すると $c$、この記号は「を作る整数の1つ」という名前です $x * 0 = 0$ 本当」？少し曖昧なので、この記号の意味を正しく理解しているのではないかと思いました。
明確にしていただきありがとうございます。
回答
ただし、ステートメントを検討してください $\exists x\in \mathbb{Z}$ $(x * 0 = 0)$。命題関数を作る多くの整数があります（$x * 0 = 0$）true（例： $1$、 $2$、 $3$）。
この場合、新しいシンボルを作成すると $c$、この記号は「を作る整数の1つ」という名前です $x * 0 = 0$ 本当」？
はい、まさにそれです。だから..の使用にもかかわらず..$c$は、私たちが話しているオブジェクトを正確に知っていることを示唆していますが、実際にはそうではありません。問題の式を満たすオブジェクトが少なくとも1つあることはまだわかっています。しかし、さらに推論を行うには、「それらのオブジェクトの1つ」について話すことができる必要があります。そのために、このシステムは個別の定数を使用します。もちろん、それが非常に一定であることを確認する必要があります。証明の他の場所では、他のオブジェクトを参照するためにすでに使用されていませんでした。
使用しない他の正式な証明システムがあることに注意してください。 $c$ この場合、変数を変数のままにしてください。これには、話している特定のオブジェクトが実際にはわからないという提案の利点があります...しかし、欠点は、取得したときに証明に行が表示されることです。残りの証明の文脈から外れると、自由変数があります...そしてそれは確かに一部の人々が代わりに定数を使用するのに十分な欠点です。
これをすべて処理する1つの方法は、定数と変数以外のオブジェクトを指す3番目の方法セットを用意することだと思うことがあります。これは、この非常に存在するインスタンス化に実際に使用するシンボルであり、いくつかのプロパティ。ただし、どれがどれかはわかりません。つまり、完全に任意ではなく（通常の変数のように）、特定のプロパティでもありません（定数のように）。しかし、私は正式なシステムがそのようなことをするのを感じたことがありません。