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 $\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$ or $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$, we can work backward by justifying the sentence we want by $\forall $I or $\exists $I and trying to find a proof of the corresponding premise of that rule. And to work forward from a quantified sentence, we apply $\forall $E or $\exists $E, as the case may be.
Specifically, suppose you want to prove $\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$. To do so using $\forall $I, we would need a proof of $\mathcal{A}(\U0001d4b8)$ for some name $\U0001d4b8$ which does not occur in any undischarged assumption. To apply the corresponding strategy, i.e., to construct a proof of $\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$ by working backward, is thus to write $\mathcal{A}(\U0001d4b8)$ above it and then to continue to try to find a proof of that sentence.
Line number

Subproof level

Formula

Justification


0

$\mathrm{\vdots}$



$n$ 
0

$\mathcal{A}(\U0001d4b8)$


$n+1$ 
0

$\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$

$\forall $I $n$

$\mathcal{A}(\U0001d4b8)$ is obtained from $\mathcal{A}(\U0001d4cd)$ by replacing every free occurrence of $\U0001d4cd$ in $\mathcal{A}(\U0001d4cd)$ by $\U0001d4b8$. For this to work, $\U0001d4b8$ 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 $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$ we similarly write a sentence above it that can serve as a justification for an application of the $\exists $I rule, i.e., a sentence of the form $\mathcal{A}(\U0001d4b8)$.
Line number

Subproof level

Formula

Justification


0

$\mathrm{\vdots}$



$n$ 
0

$\mathcal{A}(\U0001d4b8)$


$n+1$ 
0

$\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$

$\exists $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 $\forall $I we have to pick a name $\U0001d4b8$ which does not occur in the proof (so far), for $\exists $I we may and in general must pick a name $\U0001d4b8$ which already occurs in the proof. Just like in the case of $\vee $I, it is often not clear which $\U0001d4b8$ 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 $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$ generally always works and you won’t have to backtrack. Working forward from an existentially quantified sentence takes into account not just $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$ but also whatever sentence $\mathcal{B}$ you would like to prove. It requires that you set up a subproof above $\mathcal{B}$, wherein $\mathcal{B}$ is the last line, and a substitution instance $\mathcal{A}(\U0001d4b8)$ of $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$ as the assumption. In order to ensure that the condition on $\U0001d4b8$ that governs $\exists $E is satisfied, chose a name $\U0001d4b8$ which does not already occur in the proof.
Line number

Subproof level

Formula

Justification


0

$\mathrm{\vdots}$



$m$ 
0

$\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$


0

$\mathrm{\vdots}$



$n$ 
open subproof,
1

$\mathcal{A}(\U0001d4b8)$

AS

1

$\mathrm{\vdots}$



$k$ 
1

$\mathcal{B}$


$k+1$ 
close subproof,
0

$\mathcal{B}$

$\exists $E $m$, $n$–$k$

You’ll then continue with the goal of proving $\mathcal{B}$, but now inside a subproof in which you have an additional sentence to work with, namely $\mathcal{A}(\U0001d4b8)$.
Lastly, working forward from $\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$ means that you can always write down $\mathcal{A}(\U0001d4b8)$ and justify it using $\forall $E, for any name $\U0001d4b8$. Of course, you wouldn’t want to do that willynilly. Only certain names $\U0001d4b8$ will help in your task of proving whatever goal sentence you are working on. So, like working backward from $\exists \U0001d4cd\mathcal{A}(\U0001d4cd)$, you should work forward from $\forall \U0001d4cd\mathcal{A}(\U0001d4cd)$ only after all other strategies have been applied.
Let’s consider as an example the argument $\forall x(A(x)\to B)\therefore \exists xA(x)\to 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

$\forall x(A(x)\to B)$

PR

0

$\mathrm{\vdots}$



$n$ 
0

$\exists xA(x)\to 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 $\to $E, $\mathrm{\neg}$E, $\vee $I, $\forall $E, or $\exists $I. In our case, that means, working backward from the conclusion:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall x(A(x)\to B)$

PR

$2$ 
open subproof,
1

$\exists xA(x)$

AS

1

$\mathrm{\vdots}$



$n1$ 
1

$B$


$n$ 
close subproof,
0

$\exists xA(x)\to B$

$\to $I $2$–($n1$)

Our next step should be to work forward from $\exists 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

$\forall x(A(x)\to B)$

PR

$2$ 
open subproof,
1

$\exists xA(x)$

AS

$3$ 
open subproof,
2

$A(d)$

AS

2

$\mathrm{\vdots}$



$n2$ 
2

$B$


$n1$ 
close subproof,
1

$B$

$\exists $E $2$, $3$–($n2$)

$n$ 
close subproof,
0

$\exists xA(x)\to B$

$\to $I $2$–($n1$)

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

Subproof level

Formula

Justification


$1$ 
0

$\forall x(A(x)\to B)$

PR

$2$ 
open subproof,
1

$\exists xA(x)$

AS

$3$ 
open subproof,
2

$A(d)$

AS

$4$ 
2

$A(d)\to B$

$\forall $E $1$

$5$ 
2

$B$

$\to $E $4$, $3$

$6$ 
close subproof,
1

$B$

$\exists $E $2$, $3$–$5$

$7$ 
close subproof,
0

$\exists xA(x)\to B$

$\to $I $2$–$6$

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

Subproof level

Formula

Justification


$1$ 
0

$\exists xA(x)\to B$

PR

0

$\mathrm{\vdots}$



$n$ 
0

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

Subproof level

Formula

Justification


$1$ 
0

$\exists xA(x)\to B$

PR

0

$\mathrm{\vdots}$



$n1$ 
0

$A(d)\to B$


$n$ 
0

$\forall x(A(x)\to B)$

$\forall $I $n1$

And working backward from $A(d)\to 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

$\exists xA(x)\to B$

PR

$2$ 
open subproof,
1

$A(d)$

AS

1

$\mathrm{\vdots}$



$n2$ 
1

$B$


$n1$ 
close subproof,
0

$A(d)\to B$

$\to $I $2$–($n2$)

$n$ 
0

$\forall x(A(x)\to B)$

$\forall $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, $\exists xA(x)$. Of course, that is now readily available, by $\exists $I from line $2$, and we’re done:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\exists xA(x)\to B$

PR

$2$ 
open subproof,
1

$A(d)$

AS

$3$ 
1

$\exists xA(x)$

$\exists $I $2$

$4$ 
1

$B$

$\to $E $1$, $3$

$5$ 
close subproof,
0

$A(d)\to B$

$\to $I $2$–$4$

$6$ 
0

$\forall x(A(x)\to B)$

$\forall $I $5$

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

1.
$A\to \forall xB(x)\therefore \forall x(A\to B(x))$

2.
$\exists x(A\to B(x))\therefore A\to \exists xB(x)$

3.
$\forall x(A(x)\wedge B(x))\leftrightarrow (\forall xA(x)\wedge \forall xB(x))$

4.
$\exists x(A(x)\vee B(x))\leftrightarrow (\exists xA(x)\vee \exists xB(x))$

5.
$A\vee \forall xB(x))\therefore \forall x(A\vee B(x))$

6.
$\forall x(A(x)\to B)\therefore \exists xA(x)\to B$

7.
$\exists x(A(x)\to B)\therefore \forall xA(x)\to B$

8.
$\forall x(A(x)\to \exists 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.
$\forall xR(x,x)\therefore \forall x\exists yR(x,y)$

2.
$\forall x\forall y\forall z[(R(x,y)\wedge R(y,z))\to R(x,z)]$
$\therefore \forall x\forall y[R(x,y)\to \forall z(R(y,z)\to R(x,z))]$ 
3.
$\forall x\forall y\forall z[(R(x,y)\wedge R(y,z))\to R(x,z)],$
$\forall x\forall y(R(x,y)\to R(y,x))$
$\therefore \forall x\forall y\forall z[(R(x,y)\wedge R(x,z))\to R(y,z)]$ 
4.
$\forall x\forall y(R(x,y)\to R(y,x))$
$\therefore \forall x\forall y\forall z[(R(x,y)\wedge R(x,z))\to \exists u(R(y,u)\wedge R(z,u))]$ 
5.
$\mathrm{\neg}\exists x\forall y(A(x,y)\leftrightarrow \mathrm{\neg}A(y,y))$
C. Use the strategies to find proofs for each of the following arguments and theorems:

1.
$\forall xA(x)\to B\therefore \exists x(A(x)\to B)$

2.
$A\to \exists xB(x)\therefore \exists x(A\to B(x))$

3.
$\forall x(A\vee B(x))\therefore A\vee \forall xB(x))$

4.
$\exists x(A(x)\to \forall yA(y))$

5.
$\exists x(\exists yA(y)\to A(x))$
These require the use of IP. Use only the basic rules of TFL in addition to the basic quantifier rules.