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
n
0
𝒜(𝒸)
n+1
0
𝓍𝒜(𝓍)
I n

𝒜(𝒸) 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 n+1.)

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
n
0
𝒜(𝒸)
n+1
0
𝓍𝒜(𝓍)
I n

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
m
0
𝓍𝒜(𝓍)
0
n
open subproof, 1
𝒜(𝒸)
AS
1
k
1
k+1
close subproof, 0
E m, nk

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 x(A(x)B)xA(x)B. To start constructing a proof, we write the premise at the top and the conclusion at the bottom.

Line number
Subproof level
Formula
Justification
1
0
x(A(x)B)
PR
0
n
0
xA(x)B

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
1
0
x(A(x)B)
PR
2
open subproof, 1
xA(x)
AS
1
n1
1
B
n
close subproof, 0
xA(x)B
I 2–(n1)

Our next step should be to work forward from xA(x) on line 2. For that, we have to pick a name not already in our proof. Since no names appear, we can pick any name, say ‘d

Line number
Subproof level
Formula
Justification
1
0
x(A(x)B)
PR
2
open subproof, 1
xA(x)
AS
3
open subproof, 2
A(d)
AS
2
n2
2
B
n1
close subproof, 1
B
E 2, 3–(n2)
n
close subproof, 0
xA(x)B
I 2–(n1)

Now we’ve exhausted our primary strategies, and it is time to work forward from the premise x(A(x)B). Applying E means we can justify any instance of A(𝒸)B, regardless of what 𝒸 we choose. Of course, we’ll do well to choose d, since that will give us A(d)B. Then we can apply E to justify B, finishing the proof.

Line number
Subproof level
Formula
Justification
1
0
x(A(x)B)
PR
2
open subproof, 1
xA(x)
AS
3
open subproof, 2
A(d)
AS
4
2
A(d)B
E 1
5
2
B
E 4, 3
6
close subproof, 1
B
E 2, 35
7
close subproof, 0
xA(x)B
I 26

Now let’s construct a proof of the converse. We begin with

Line number
Subproof level
Formula
Justification
1
0
xA(x)B
PR
0
n
0
x(A(x)B)

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, x(A(x)B), leads us to look for a proof of A(d)B:

Line number
Subproof level
Formula
Justification
1
0
xA(x)B
PR
0
n1
0
A(d)B
n
0
x(A(x)B)
I n1

And working backward from A(d)B means we should set up a subproof with A(d) as an assumption and B as the last line:

Line number
Subproof level
Formula
Justification
1
0
xA(x)B
PR
2
open subproof, 1
A(d)
AS
1
n2
1
B
n1
close subproof, 0
A(d)B
I 2–(n2)
n
0
x(A(x)B)
I n1

Now we can work forward from the premise on line 1. That’s a conditional, and its consequent happens to be the sentence B we are trying to justify. So we should look for a proof of its antecedent, xA(x). Of course, that is now readily available, by I from line 2, and we’re done:

Line number
Subproof level
Formula
Justification
1
0
xA(x)B
PR
2
open subproof, 1
A(d)
AS
3
1
xA(x)
I 2
4
1
B
E 1, 3
5
close subproof, 0
A(d)B
I 24
6
0
x(A(x)B)
I 5

Practice exercises

A. Use the strategies to find proofs for each of the following arguments and theorems:

  1. 1.

    AxB(x)x(AB(x))

  2. 2.

    x(AB(x))AxB(x)

  3. 3.

    x(A(x)B(x))(xA(x)xB(x))

  4. 4.

    x(A(x)B(x))(xA(x)xB(x))

  5. 5.

    AxB(x))x(AB(x))

  6. 6.

    x(A(x)B)xA(x)B

  7. 7.

    x(A(x)B)xA(x)B

  8. 8.

    x(A(x)yA(y))

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. 1.

    xR(x,x)xyR(x,y)

  2. 2.

    xyz[(R(x,y)R(y,z))R(x,z)]
    xy[R(x,y)z(R(y,z)R(x,z))]

  3. 3.

    xyz[(R(x,y)R(y,z))R(x,z)],
    xy(R(x,y)R(y,x))
    xyz[(R(x,y)R(x,z))R(y,z)]

  4. 4.

    xy(R(x,y)R(y,x))
    xyz[(R(x,y)R(x,z))u(R(y,u)R(z,u))]

  5. 5.

    ¬xy(A(x,y)¬A(y,y))

C. Use the strategies to find proofs for each of the following arguments and theorems:

  1. 1.

    xA(x)Bx(A(x)B)

  2. 2.

    AxB(x)x(AB(x))

  3. 3.

    x(AB(x))AxB(x))

  4. 4.

    x(A(x)yA(y))

  5. 5.

    x(yA(y)A(x))

These require the use of IP. Use only the basic rules of TFL in addition to the basic quantifier rules.