I was having some trouble understanding existential instantiation. My textbook (Rosen - Discrete Mathematics and its Applications) states this about existential instantiation:
Existential instantiation is the rule that allows us to conclude that there is an element c in the domain for which P(c) is true if we know that ∃xP(x) is true. We cannot select an arbitrary value of c here, but rather it must be a c for which P(c) is true. Usually we have no knowledge of what c is, only that it exists. Because it exists, we may give it a name (c) and continue our argument.
This makes sense to me for certain existential statements.
For example, consider the statement $\exists x\in \mathbb{Z}$ $(x + 1 = 2)$. There is only one integer that makes the propositional function ($x + 1 = 2$) true (namely, $1$). Therefore, it makes sense to me that a new symbol $c$ can be created to name "the one integer that makes $x + 1 = 2$ true".
However, consider the statement $\exists x\in \mathbb{Z}$ $(x * 0 = 0)$. There are many integers that make the propositional function ($x * 0 = 0$) true (ex. $1$, $2$, $3$).
In this case, when we create a new symbol $c$, is this symbol naming "one of the integers that makes $x * 0 = 0$ true"? I find this slightly ambiguous, so I was wondering if I was understanding the meaning of this symbol correctly.
Please clarify and thank you for your time.
Yes, that is exactly it. So .. even though the use of $c$ suggests that we know exactly which object we are talking about, this is in fact not the case. We still only know that there is at least one object that satisfies the formula in question. But, in order to do our further reasoning, we need to be able to talk about 'one of those objects' and for that, this system uses an individual constant.... although you of course need to make sure that that very constant wasn't used elsewhere in the proof already to refer to some other object.
Please note that there are other formal proof systems that don;t use $c$ in this case, but keep the variable a variable, which has the advantage of the suggestion that you indeed do not know what specific object you are talking about ... but the drawback is that you now get lines in the proof that, when taken out of context of the rest of the proof, would have a free variable ... and that is indeed drawback enough for some people to use constants instead.
I have sometimes thought that maybe one way to deal with all this is to have a third set of ways to point to objects other than constants and variables: symbols that you would indeed use for this very existential instantiation, and which denote 'some object with some property, though we don;t know which one', i.e. not completely arbitrary (like a normal variable), but also not specific (like a constant). I have never sen formal systems do anything like that though.