8 Natural Deduction

Universal Quantification

We will introduce introduction and elimination rules for the universal and the existential quantifiers. But in order to even be able to state the rules, we must explain what we mean by an instance of a quantified formula of the form $\mathrm{\forall }x\phi$ or $\mathrm{\exists }x\phi$.

Instance

If $a$ is a constant, we let $\phi (a/x)$ be the formula that results from $\phi$ when we substitute $a$ for every free occurrence of the variable $x$ in $\phi$. The formula $\phi (a/x)$ is an instance of the quantified formulas $\mathrm{\forall }x\phi$ and $\mathrm{\exists }x\phi$, respectively.

We start now with the elimination rule for the universal quantifier.

⊕
Universal Elimination

Universal Elimination

You may write an instance $\phi (a/x)$ of a universally quantified formula $\mathrm{\forall }x\phi$ if the latter is available on a prior line of the derivation.

The rationale for universal elimination is that we are entitled to write that an individual $a$ satisfies a given condition if we are given that all individuals do.

Let us look at the universal elimination rule in action.

The introduction rule for the universal quantifier requires more care. In order to be able to write $\mathrm{\forall }x\phi (x)$ by itself on a line, we should convince ourselves we have the means to establish some arbitrary instance $\phi (a/x)$ where the constant $a$ does not occur in an undischarged assumption.

⊕
Universal Introduction

Universal Introduction

You may write a universally quantified formula $\mathrm{\forall }x\phi$ if some instance $\phi (a/x)$ is available on a prior line and $a$ occurs neither in $\phi$ nor in an undischarged assumption.

Let us look at some applications of the rule.

Existential Quantification

We now introduce introduction and elimination rules for the existential quantifier.

⊕
Existential Introduction

Existential Introduction

You may write an existentially quantified formula $\mathrm{\exists }x\phi$ provided an instance $\phi (a/v)$ is available on a prior line of the derivation

The rationale for existential introduction is that we are entitled to write that something satisfies a condition if we are given that an individual $a$ does.

Here is the rule of existential introduction in action.

The elimination rule for the existential quantifier is more subtle. Suppose we want to reason from an existential generalization of the form $\mathrm{\exists }x\phi (x)$ to some formula $\psi$. The elimination rule for the existential tells us that the step is justified if we have the means to establish a conditional $\phi (a/v)\to \psi$ where $a$ is a constant that occurs neither in $\psi$ nor $\mathrm{\exists }x\phi$ nor in an earlier open assumption.

⊕
Existential Elimination

Existential Elimination

You may write $\psi$ if the existentially quantified formula $\mathrm{\exists }x\phi$ and the conditional $\phi (a/x)\to \psi$ are available at prior lines provided that $a$ occurs neither in neither in $\psi$ nor in $\mathrm{\exists }x\phi$ nor in an undischarged assumption.

Common Mistakes and Strategies

Much of the advice for the construction of proofs in propositional logic carries over to quantificational logic. In order to prove a universal or existential generalization from a set of premises, it helps to work backwards and with a view to being in a position to use the relevant introduction rule. And to reason forward from a universal or existential generalization, we should use the relevant elimination rules.

One important observation is that the elimination rule for the universal quantifier should not be applied to formulas that are not universally quantified formulas. The rule may be applied, for example, to the universal quantification $\mathrm{\forall }x(Px\to Qx)$ to obtain an instance such as $Pa\to Qa$. It would, however, be a mistake to attempt to apply the rule to the formula $\mathrm{\forall }xPx\to \mathrm{\forall }xQx$, which, unlike the first, is just a conditional. The key is to be aware of what is the main connective in the relevant formula and to make sure to apply the rule that corresponds to it.

One more potential pitfall is the failure to apply the rules for quantification once at a time. The elimination rule for the universal quantifier does not allow an immediate transition from a formula such as $\mathrm{\forall }x\mathrm{\forall }yRxy$ to $Rab$. We should instead distinguish two steps: one from the original formula to $\mathrm{\forall }yRxy$ and a further one from this formula to the instance $Rab$.

Let us now look at some further examples.

Exercises

1. Provide a natural deduction proof in order to justify each of the claims below:

   1. $\mathrm{\exists }xPx\to \mathrm{\exists }xQx,\mathrm{\forall }xPx⊢\mathrm{\exists }xQx$

   2. $\mathrm{\exists }xPx\wedge \mathrm{\exists }xQx,\mathrm{\neg }\mathrm{\exists }x(Px\wedge Qx),\mathrm{\forall }x(Rx\to Px)⊢\mathrm{\exists }x\mathrm{\neg }Rx$

   3. $\mathrm{\forall }x(Px\to \mathrm{\neg }Qx),\mathrm{\forall }x(Rx\to Qx)⊢\mathrm{\forall }x(Rx\to \mathrm{\neg }Px)$

   4. $\mathrm{\forall }x(Px\to (\mathrm{\exists }yRxy\to Qx)),\mathrm{\neg }\mathrm{\exists }yQy⊢\mathrm{\forall }y(Py\to \mathrm{\forall }z\mathrm{\neg }Ryz)$

   5. $\mathrm{\forall }x(Px\to \mathrm{\forall }y(Rxy\to Py),\mathrm{\exists }x(Qx\wedge Px)⊢\mathrm{\exists }x(Qx\wedge \mathrm{\forall }y(Rxy\to Py))$