Natural Deduction in Predicate Logic

“The grand aim of all science is to cover the greatest number of empirical facts by logical deduction from the smallest possible number of hypotheses or axioms.”
—Albert Einstein

Although logical entailment A⊨BA \vDash B is our gold standard for deciding whether a formula BB logically follows from a formula AA, it is not feasible to directly check infinitely many possible models to confirm that every models where AA is true also makes BB true.

So instead, we need a proof system for Predicate Logic; then instead of checking all possible models, it suffices to find a step-by-step argument showing that BB follows from AA using sound (truth-preserving) inference rules.

As with Propositional Logic, logicians have studied many different proof systems for Predicate Logic. Here we focus on Natural Deduction, as it has the closest connection to traditional proofs in mathematics and Computer Science.

Natural Deduction for Predicate Logic is just a simple extension of Natural Deduction for Propositional Logic . That is, just keep the same rules as before, and then add four new rules (introduction and elimination rules for the two kinds of quantifier).

The ∀E\forall E Rule

We start with a relatively simple rule. The ∀E\forall E rule explains what directly follows from a universally quantified formula:

∀x P(x)P(t) ∀E{\large \frac{\forall x\ P(x)}{P(t)}}{\small~{\forall}E}

where tt is an arbitrary term.

Example

If we know (or have assumed)

∀x (Q(x)→R(x))\forall x\ \bigl(Q(x)\to R(x)\bigr)

we can use ∀E\forall E to immediately conclude consequences such as

  • Q(42)→R(42)Q(42)\to R(42)
  • Q(c)→R(c)Q(c)\to R(c)
  • Q(2)→R(2)Q(\sqrt 2)\to R(\sqrt 2)

The ∀I\forall I Rule

If the ∀E\forall E allows us to derive consequences from a universally quantified formula, the ∀I\forall I rule explains how to prove (most directly) that a universally quantified statement is true:

x is fresh (not free in any assumption)⋮P(x)P(x) ∀I{\large \frac{ \qquad \begin{array}{c} \begin{array}{|c} x~\mathrm{is~fresh~\scriptsize(not~free~in~any~assumption)} \\ \hline \vdots \\ P(x) \end{array}\\[20pt] \end{array} \qquad } {P(x)}} {\small~{\forall}I}

That is, if we can prove some formula P(x)P(x) knowing absolutely nothing about xx, then our proof is completely generic (would work for any value of xx) and hence ∀x P(x)\forall x\ P(x) is true.

Example

Knowing nothing about xx, we can still show that

x∈R → x2≥0.x\in\mathbb{R} \ \to \ x^2 \geq 0.

By ∀I\forall I, it immediately follows that

∀x (x∈R → x2≥0)\forall x\ (x\in\mathbb{R} \ \to \ x^2 \geq 0)

which can be abbreviated as

∀x∈R (x2≥0).\forall x\in\mathbb{R} \ (x^2 \geq 0).

The ∃I\exists I Rule

The ∃I\exists I rule explains the most direct route to proving an existential formula true:

P(t)∃x P(x) ∃I{\large \frac{P(t)}{\exists x\ P(x)}}{\small~{\exists}I}

where tt is an arbitrary term.

The idea is that the easist way to prove something with a property exists is to find such a thing.

Example

Since we know that 42<42+142 < 42+1, it follows immediately by ∃I\exists I that:

  • ∃x (x<42+1)\exists x\ (x < 42+1).
  • ∃y (y<y+1)\exists y\ (y < y+1).
  • ∃z (42<42+z)\exists z\ (42 < 42+z).
  • ∃w (42<w)\exists w\ (42 < w).

Applying the ∃I\exists I rule again to the first of these formulas, we can infer further consequences including:

  • ∃a ∃x (x<a+1)\exists a\ \exists x\ (x < a+1).
  • ∃b ∃x (x<42+b)\exists b\ \exists x\ (x < 42+b).
  • ∃c ∃x (x<c)\exists c\ \exists x\ (x < c).

The ∃E\exists E Rule

Finally, the ∃E\exists E rule explains how we can derive direct consequences from an existentially-quantified formula:

  ∃x P(x)P(z)⋮CC ∃E{\large \frac{ \begin{array}{c} ~ \\ ~ \\ \exists x\ P(x)\end{array} \qquad \begin{array}{c} \begin{array}{|c} P(z) \\ \hline \vdots \\ {\cal C}\end{array}\\[20pt] \end{array} \qquad } {{\cal C}} {\small~{\exists}E} }

where zz is a variable not free in any assumption.

That is, if we know something exists with property PP, we can give a specific name zz to that thing. All we know about zz is that it has property PP, but if just knowing that allows us to prove a conclusion C{\cal C} then C{\cal C} must be true.

The name zz we chose for the thing that exists is essentially arbitrary; we just have to choose any variable name (xx,yy,zz,…) that isn’t already being used in our proof. Since the name we choose doesn’t matter and is just a temporary choice inside our proof, we don’t let that name appear in our ultimate conclusion C{\cal C}.

Example

Suppose we know ∀x R(x)→Q(x)\forall x\ R(x)\to Q(x) (i.e., everything with property RR also has property QQ) and ∃k R(k)\exists k\ R(k) (i.e., there exists something having property RR).

Let’s see how to use the above rules to prove ∃x Q(x)\exists x\ Q(x) (i.e., there exists something having property QQ).

Since our second assumption tells us there exists an individual with property RR, we can give that individual a name, say aa; we know nothing about aa except that R(a)R(a) is true.

Then we can apply ∀E\forall E to the first assumption and conclude R(a)→Q(a)R(a)\to Q(a). By →E\to E, it follows that Q(a)Q(a). Finally, by ∃I\exists I, we can conclude ∃x Q(x)\exists x\ Q(x).

Since we proved our conclusion ∃x Q(x)\exists x\ Q(x) from the assumption that R(a)R(a) is true (knowing nothing else about aa), and the conclusion ∃x Q(x)\exists x\ Q(x) doesn’t mention our temporary variable aa, we can use ∃E\exists E to turn our assumption ∃k R(k)\exists k\ R(k) into the conclusion ∃x Q(x)\exists x\ Q(x).