29.3 ∀Elim: Universal Instantiation
In informal proofs Universal Instantiation allows you to instantiate a universal quantifier with a particular name.
∀Elim for formal proofs works the exact same way. Let’s see if you can figure out how to use it.
When you do ∀Elim, you must replace every instance of the variable with the same name.
For example, this doesn’t work:
Line 2 isn’t even a sentence, since it has a free variable.
But it also does not work if we tried to leave the quantifier in to close the variable. For example, say everybody likes themselves.
It’s not valid to replace just one of the xs with “pia”.
Just because everyone likes themselves, it doesn’t follow that everyone likes Pia!
So when we use ∀Elim, we have to actually eliminate the quantifier, and replace every instance of the variable with the same name.
But since ∀x holds for every object in the domain, you can do ∀Elim on the same quantifier as many times as you’d like.
Often times the argument will tell you want names you need to instantiate, like when you proved P(a)&P(b) above. But sometimes it won’t.
In that case, always first use the name “a”, just like we always use the letter “x” for the first variable we need.
Recall this argument from Section 29.1:
1.Every animal in the shelter is a dog or a cat.
2. An animal is ready for adoption if and only if it’s been cleared.
3. All cats must be checked for fleas to be cleared.
4. All dogs must be washed to be cleared.
5. Floyd is a new animal in the shelter, who hasn’t been washed or checked for fleas.
6. There’s an animal not ready for adoption.
Now let’s see if you can complete a formal proof of it. We’ll use R() for ready for adoption, and B() for being cleared. You can figure out the rest!