Rules with ∀
Just as with our propositional logic operators, there will be two inference rules for each of our predicate logic quanitifiers – an “introduction rule and an “elimination” rule.
In this section, we will see the two inference rules for the universal (∀) quantifier.
For all elimination
For all elimination allows us to take a claim that uses a universal quantifier – a statement about ALL individuals in a domain – and make the same statement about a specific individual in the domain. After all, if the statement is true for ALL individuals, then it follows that it should be true for a particular individual. We can formalize the rule as follows:
∀ x P(x)
∀e: -----------
P(v) where v is a particular individual in the domainHere is a simple example showing the syntax of the ∀e rule. It shows that given the premises: All humans are mortal and Socrates is a human, that we can prove that Socrates is mortal:
∀ x (isHuman(x) → isMortal(x)), isHuman(Socrates) ⊢ isMortal(Socrates)
{
1. ∀ x (isHuman(x) → isMortal(x)) premise
2. isHuman(Socrates) premise
3. isHuman(Socrates) → isMortal(Socrates) ∀e 1 Socrates
4. isMortal(Socrates) →e 3 2
}We can read the justification ∀e 1 Socrates as: “for all elimination of the for-all statement on line 1, plugging in the individual Socrates”.
For all introduction
If we can show that a property of the form P(a) holds for an arbitrary member a of a domain, then we can use for all introduction to conclude that the property must hold for ALL individuals in the domain – i.e., that ∀ x P(x). We can formalize the fule as follows:
{ a (a is fresh)
... P(a) }
∀i: ---------------
∀ x P(x) Here is a simple example showing the syntax of the ∀i rule: “Everyone is healthy; everyone is happy. Therefore, everyone is both healthy and happy.”:
∀ x isHealthy(x), ∀ y isHappy(y) |- ∀ z(isHealthy(z) ∧ isHappy(z))
{
1. ∀ x isHealthy(x) premise
2. ∀ y isHappy(y) premise
3. {
4. a
5. isHealthy(a) ∀e 1 a
6. isHappy(a) ∀e 2 a
7. isHealthy(a) ∧ isHappy(a) ∧i 5 6
}
8. ∀ z (isHealthy(z) ∧ isHappy(z)) ∀i 3
}If we wish to introduce a for-all statement, the pattern is:
-
Open a subproof and introduce an arbitrary/fresh individual in the domain (in the example above, we used
a). It MUST be a name that we have not used elsewhere in the proof. The idea is that your individual could have been anyone/anything in the domain. -
When you introduce your individual, you do NOT include a justification on that line
-
If you have other for-all statements available within the scope of the subproof, then it is often useful to use
∀eto plug your fresh individual into them. After all, if those statements are true for ALL individuals, then they are also true for your fresh individual. -
If you are trying to prove something of the form
∀ x P(x), then you need to reachP(a)by the end of the subproof. You need to show that your goal for-all statement holds for your fresh individual. In our case, we wished to prove∀ z (isHealthy(z) ∧ isHappy(z)), so we reachedisHealthy(a) ∧ isHappy(a)by the end of the subproof. -
After the subproof, you can use
∀ito introduce a for-all statement for your last claim in the subproof – that since the individual could have been anyone, then the proposition holds for ALL individuals. The∀ijustification needs the line number of the subproof. -
When you use
∀i, it does not matter what variable you introduce into the for-all statement. In the example above, we introduced∀ z– but that was only to match the goal conclusion in the proof. We could have instead introduced∀ x,∀ y,∀ people, etc. We would use whatever variable we chose in the rest of that proposition – i.e.,∀ z (isHealthy(z) ∧ isHappy(z)), or∀ people (isHealthy(people) ∧ isHappy(people)), etc.
Examples
In this section, we will look at several proofs involving the universal quantifier.
Example 1
Suppose we wish to prove the following sequent:
∀ x P(x) ⊢ ∀ y P(y)This will let us show that it doesn’t matter what variable we use with a universal quantifier – both ∀ x P(x) and ∀ y P(y) are saying the same thing: for all individuals, P holds for that individual.
Since the top-level operator of our conclusion is a for-all statement, we see that we will need to use for all introduction. Following the pattern above, we open a subproof and introduce a fresh individual, a. Since we wish to introduce the for-all statement ∀ y P(y), then we know we need to reach P(a) by the end of our subproof:
∀ x P(x) ⊢ ∀ y P(y)
{
1. ∀ x P(x) premise
2. {
3. a //our fresh individual
//need: P(a)
}
//want to use ∀i to conclude ∀ y P(y)
}Since we have an available for-all statement in our subproof (∀ x P(x), from line 1), then we use ∀e to plug a into it:
∀ x P(x) ⊢ ∀ y P(y)
{
1. ∀ x P(x) premise
2. {
3. a //our fresh individual
4. P(a) ∀e 1 a
//need: P(a)
}
//want to use ∀i to conclude ∀ y P(y)
}At that point, we see that we have exactly the proposition we wanted to end our subproof – P(a). All that remains is to use ∀i to state that since a could have been anyone, that the proposition we reached at the end of subproof 2 must hold for all individuals. Here is the completed proof:
∀ x P(x) ⊢ ∀ y P(y)
{
1. ∀ x P(x) premise
2. {
3. a //our fresh individual
4. P(a) ∀e 1 a
//need: P(a)
}
//want to use ∀i to conclude ∀ y P(y)
5. ∀ y P(y) ∀i 2
}Example 2
Suppose we wish to prove that, given the following premises in the domain of people:
- All students have a phone and/or a laptop
- Everyone is a student
Then we can conclude:
- Everyone has a phone and/or a laptop
First, we identify the following predicates:
isStudent(x)- whether person x is a studenthasPhone(x)- whether person x has a phonehasLaptop(x)= whether person x has a laptop
Then, we can translate our premises and goal conclusion to predicate logic:
- All students have a phone and/or a laptop translates to:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) - Everyone is a student translates to:
∀ x isStudent(x) - Everyone has a phone and/or a laptop translates to:
∀ x (hasPhone(x) ∨ hasLaptop(x))
We need to prove the following sequent:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))As with our previous example, we see that we are trying to prove a for-all statement (∀ x (hasPhone(x) ∨ hasLaptop(x))). This means we will need to open a subproof and introduce a fresh individual – perhaps bob. By the end of the subproof, we must show that our goal for-all statement holds for that individual – that hasPhone(bob) ∨ hasLaptop(bob). We start the proof as follows:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) premise
2. ∀ x isStudent(x) premise
3. {
4. bob
//goal: hasPhone(bob) ∨ hasLaptop(bob)
}
//use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
}We have two available for-all statements within the subproof – ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) and ∀ x isStudent(x). Since those propositions hold for all individuals, they also hold for bob. We use Ae to plug in bob to those two propositions:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) premise
2. ∀ x isStudent(x) premise
3. {
4. bob
5. isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob) ∀e 1 bob
6. isStudent(bob) ∀e 2 bob
//goal: hasPhone(bob) ∨ hasLaptop(bob)
}
//use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
}Line 5 is an implies statement the form p → q, and line 6 is a statement of the form p. Thus we can use →e to conclude hasPhone(bob) ∨ hasLaptop(bob) (the “q” in that statement) – which is exactly what we needed to end the subproof. All that remains is to apply our ∀i rule after the subproof. Here is the completed proof:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) premise
2. ∀ x isStudent(x) premise
3. {
4. bob
5. isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob) ∀e 1 bob
6. isStudent(bob) ∀e 2 bob
7. hasPhone(bob) ∨ hasLaptop(bob) →e 5 6
//goal: hasPhone(bob) ∨ hasLaptop(bob)
}
//use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
8. ∀ x (hasPhone(x) ∨ hasLaptop(x)) ∀i 3
}Example 3
Next, suppose we wish to prove the following sequent:
∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)We again see that the top-level operator of what we are trying to prove is a universal quantifier. We use our strategy to open a subproof, introduce a fresh individual (maybe a), and plug that individual into any available for-all statements. Since we wish to prove ∀ x ¬S(x), then we will want to reach ¬S(a) by the end of the subproof. Here is a sketch:
∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
1. ∀ x (S(x) → Pz(x)) premise
2. ∀ x (Pz(x) → D(x)) premise
3. ∀ x ¬D(x) premise
4. {
5. a
6. S(a) → Pz(a) ∀e 1 a
7. Pz(a) → D(a) ∀e 2 a
8. ¬D(a) ∀e 3 a
//goal: ¬S(a)
}
//use ∀i to conclude ∀ x ¬S(x)
}Now, we see that our goal is to reach ¬S(a) by the end of the subproof – so we need to prove something whose top-level operator is a NOT. We recall that we have a strategy to prove NOT(something) from propositional logic – we open a subproof, assuming something (S(a), in our case), try to get a contradiction, and use NOT introduction after the subproof to conclude NOT (something) (¬S(a) for us). Here is the strategy:
∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
1. ∀ x (S(x) → Pz(x)) premise
2. ∀ x (Pz(x) → D(x)) premise
3. ∀ x ¬D(x) premise
4. {
5. a
6. S(a) → Pz(a) ∀e 1 a
7. Pz(a) → D(a) ∀e 2 a
8. ¬D(a) ∀e 3 a
9. {
10. S(a) assume
//goal: contradiction
}
//use ¬i to conclude ¬S(a)
//goal: ¬S(a)
}
//use ∀i to conclude ∀ x ¬S(x)
}We can complete the proof as follows:
∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
1. ∀ x (S(x) → Pz(x)) premise
2. ∀ x (Pz(x) → D(x)) premise
3. ∀ x ¬D(x) premise
4. {
5. a
6. S(a) → Pz(a) ∀e 1 a
7. Pz(a) → D(a) ∀e 2 a
8. ¬D(a) ∀e 3 a
9. {
10. S(a) assume
11. Pz(a) →e 6 10
12. D(a) →e 7 11
13. ⊥ ¬e 12 8
//goal: contradiction
}
//use ¬i to conclude ¬S(a)
14. ¬S(a) ¬i 9
//goal: ¬S(a)
}
//use ∀i to conclude ∀ x ¬S(x)
15. ∀ x ¬S(x) ∀i 4
}