Recall the syllogisms from a previous lecture. The general form of a syllogism is
- ∀x :(P (x) ⇒ Q (x)) [major premise]
- P (c) [minor premise]
- Q (c) [conclusion]
In our system, we don't have syllogism as a separate rule of inference, but it's easy to see how to translate any syllogism into our system: (for specific relations P and Q, and a specific constant c).
|
1 |
|
Premise |
|
2 |
|
Premise |
|
3 |
|
∀Elim, by line 1, with x = c |
|
4 |
|
⇒Elim, by lines 2,3, with φ = P = c and ψ = Q = c |
Eliminating a quantifer via ∀Elim and ∃Elim is often merely an intermediate step, where the quantifer will be reintroduced later. This moves the quantifcation from being explicit to implicit, so that we can use other inference rules on the body of the formula. When this is done, it is very important to pay attention to the restrictions on ∀Intro, so that we don't accidentally "prove" anything too strong.
Example 4.13
, for the particular case of φ = R (x, y) (other cases all similar).
|
1 |
|
Premise |
|
2 |
|
∃Elim, line 1 |
|
3 |
|
∀Elim, line 2 |
|
4 |
|
∃Intro, line 3 |
|
5 |
|
∀Intro, line 4 |
Remember that in line 5, for ∀Intro, we must verify that q is arbitrary. It is, since it was introduced in line 3 by ∀Elim, and there hasn't been an intervening ∃Elim between lines 3 and 5.
We cannot instead conclude in line 4 that ∀x :(R (x, q)) by ∀Intro, since variable p was introduced by ∃Elim in line 2, and therefore not arbitrary.
Exercise 4.3.1.1
Let's reverse the previous proof goal: 
for the particular case of φ = R (x, y) (other cases all
similar). This statement does not hold in general. So, what's the problem with the following "proof"?
|
1 |
|
Premise |
|
2 |
|
∀Elim, line 1 |
|
3 |
|
∃Elim, line 2 |
|
4 |
|
∀Intro, line 3 |
|
5 |
|
∃Intro, line 4 |
The ∀Intro principle is actually very familiar. For instance, after having shown 
we then claimed this was really true for arbitrary propositions instead of just a,b.
(We actually went a bit further, generalizing individual propositions to entire (arbitrary) WFFs φ,ψ. This could only be done because in any particular interpretation, a
formula φ will either be true or false, so replacing it by a proposition still preserves the important part of the proof-of-equivalence.)
The ∀Intro is also used in many informal proofs. Consider: "If a number n is prime, then ...". This translates to "prime (n) ⇒ ...", where n is arbitrary. We are entirely used to thinking of this as "∀n : (prime (n) ⇒ ...)" even though "n" was introduced as if it were a particular number.
- 1809 reads
