The only formal proof rule for quantifiers we haven’t covered it ∃Elim.
It works just like the informal method Existential Instantiation, by allowing us to talk about the object we know exists from an existential claim.
Say we know ∃xP(x). Then we need to start a subproof by boxing a constant with an arbitrary name [a].
But we don’t leave the rest of the subproof assumption blank. We don’t want to talk about a totally arbitrary member of the domain. We want to talk about the object we know exists with property P.
(Of course, there could be several such objects. We just need to talk arbitrarily about any one of them.)
Then, if we can prove some random sentence R, which does not have the name “a” in it, we can export R out of the subproof with ∃Elim. When we do so, we must cite the existential sentence that we are eliminating, plus the subproof that we created.
Let’s see an example.
In case you can’t get it the citation for the last line is ∃Elim;2,3-6. Think of it like proof by cases, vElim, where we first needed to cite the disjunction we were eliminating, and then all the subproofs.
Here we first cite the existential we are eliminating, then the single subproof in which we talk about that existential.
Also notice that the sentence on line 6 is identical to line 7. With ∃Elim we export the last line, just like in vElim.
The use of arbitrary names here is very similar to ∀Intro (Universal Generalization). The arbitrary name cannot appear anywhere outside the subproof.
Since the last line of the subproof gets exported, that means that the boxed constant “a” cannot appear in the last line.