Chapter 37 Proofs with quantifiers
In chapter 18 we discussed strategies for constructing proofs using the basic rules of natural deduction for TFL. The same principles apply to the rules for the quantifiers. If we want to prove a quantifier sentence or , we can work backward by justifying the sentence we want by I or I and trying to find a proof of the corresponding premise of that rule. And to work forward from a quantified sentence, we apply E or E, as the case may be.
Specifically, suppose you want to prove . To do so using I, we would need a proof of for some name which does not occur in any undischarged assumption. To apply the corresponding strategy, i.e., to construct a proof of by working backward, is thus to write above it and then to continue to try to find a proof of that sentence.
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
|
|
0
|
|
|
|
0
|
|
I
|
is obtained from by replacing every free occurrence of in by . For this to work, must satisfy the special condition. We can ensure that it does by always picking a name that does not already occur in the proof constructed so far. (Of course, it will occur in the proof we end up constructing—just not in an assumption that is undischarged at line .)
To work backward from a sentence we similarly write a sentence above it that can serve as a justification for an application of the I rule, i.e., a sentence of the form .
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
|
|
0
|
|
|
|
0
|
|
I
|
This looks just like what we would do if we were working backward from a universally quantified sentence. The difference is that whereas for I we have to pick a name which does not occur in the proof (so far), for I we may and in general must pick a name which already occurs in the proof. Just like in the case of I, it is often not clear which will work out, and so to avoid having to backtrack you should work backward from existentially quantified sentences only when all other strategies have been applied.
By contrast, working forward from sentences generally always works and you won’t have to backtrack. Working forward from an existentially quantified sentence takes into account not just but also whatever sentence you would like to prove. It requires that you set up a subproof above , wherein is the last line, and a substitution instance of as the assumption. In order to ensure that the condition on that governs E is satisfied, chose a name which does not already occur in the proof.
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
|
|
0
|
|
|
|
0
|
|
|
|
open subproof,
1
|
|
AS
|
|
1
|
|
|
|
1
|
|
|
|
close subproof,
0
|
|
E , –
|
You’ll then continue with the goal of proving , but now inside a subproof in which you have an additional sentence to work with, namely .
Lastly, working forward from means that you can always write down and justify it using E, for any name . Of course, you wouldn’t want to do that willy-nilly. Only certain names will help in your task of proving whatever goal sentence you are working on. So, like working backward from , you should work forward from only after all other strategies have been applied.
Let’s consider as an example the argument . To start constructing a proof, we write the premise at the top and the conclusion at the bottom.
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
0
|
|
|
|
0
|
|
|
The strategies for connectives of TFL still apply, and you should apply them in the same order: first work backward from conditionals, negated sentences, conjunctions, and now also universal quantifiers, then forward from disjunctions and now existential quantifiers, and only then try to apply E, E, I, E, or I. In our case, that means, working backward from the conclusion:
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
open subproof,
1
|
|
AS
|
|
1
|
|
|
|
1
|
|
|
|
close subproof,
0
|
|
I –()
|
Our next step should be to work forward from on line . For that, we have to pick a name not already in our proof. Since no names appear, we can pick any name, say ‘’
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
open subproof,
1
|
|
AS
|
|
open subproof,
2
|
|
AS
|
|
2
|
|
|
|
2
|
|
|
|
close subproof,
1
|
|
E , –()
|
|
close subproof,
0
|
|
I –()
|
Now we’ve exhausted our primary strategies, and it is time to work forward from the premise . Applying E means we can justify any instance of , regardless of what we choose. Of course, we’ll do well to choose , since that will give us . Then we can apply E to justify , finishing the proof.
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
open subproof,
1
|
|
AS
|
|
open subproof,
2
|
|
AS
|
|
2
|
|
E
|
|
2
|
|
E ,
|
|
close subproof,
1
|
|
E , –
|
|
close subproof,
0
|
|
I –
|
Now let’s construct a proof of the converse. We begin with
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
0
|
|
|
|
0
|
|
|
Note that the premise is a conditional, not an existentially quantified sentence, so we should not (yet) work forward from it. Working backward from the conclusion, , leads us to look for a proof of :
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
0
|
|
|
|
0
|
|
|
|
0
|
|
I
|
And working backward from means we should set up a subproof with as an assumption and as the last line:
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
open subproof,
1
|
|
AS
|
|
1
|
|
|
|
1
|
|
|
|
close subproof,
0
|
|
I –()
|
|
0
|
|
I
|
Now we can work forward from the premise on line . That’s a conditional, and its consequent happens to be the sentence we are trying to justify. So we should look for a proof of its antecedent, . Of course, that is now readily available, by I from line , and we’re done:
Line number
|
Subproof level
|
Formula
|
Justification
|
---|---|---|---|
0
|
|
PR
|
|
open subproof,
1
|
|
AS
|
|
1
|
|
I
|
|
1
|
|
E ,
|
|
close subproof,
0
|
|
I –
|
|
0
|
|
I
|
Practice exercises
A. Use the strategies to find proofs for each of the following arguments and theorems:
-
1.
-
2.
-
3.
-
4.
-
5.
-
6.
-
7.
-
8.
Use only the basic rules of TFL in addition to the basic quantifier rules.
B. Use the strategies to find proofs for each of the following arguments and theorems:
-
1.
-
2.
-
3.
-
4.
-
5.
C. Use the strategies to find proofs for each of the following arguments and theorems:
-
1.
-
2.
-
3.
-
4.
-
5.
These require the use of IP. Use only the basic rules of TFL in addition to the basic quantifier rules.