29.2 ∃Intro: Existential Generalization
Last section we learned how to do Existential Generalization in informal proofs. Now we learn how to do the same thing in formal proofs.
Existential Generalization is how we reason to an existential, so it is the analog of ∃Intro.
Here’s how it works:
1. P(a) Premise
2. ExP(x) EIntro;1
If we know any claim about a particular, like P(a), then it holds for something: ExP(x).
Also, when you do EIntro, you get to choose any variable, as long as it does not create a scope conflict. That is, as long as the same variable is not already used inside the scope of the new existential you are creating.
Your turn to try.
Notice that when you use EIntro, the new existential becomes the widest scope operator.
That means that you must pay attention to how to first build up the parts inside of it.