“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 \vDash B\) is our gold standard for deciding whether a formula \(B\) logically follows from a formula \(A\), it is not feasible to directly check infinitely many possible models to confirm that every models where \(A\) is true also makes \(B\) 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 \(B\) follows from \(A\) 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 (typically including constructive plus classical extensions). 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).
We start with a relatively simple rule. The \(\forall E\) rule explains what directly follows from a universally quantified formula: \[ {\large \frac{\forall x\ P(x)}{P(t)}}{\small~{\forall}E} \] where \(t\) is an arbitrary term.
Example
If we know (or have assumed) \[ \forall x\ \bigl(Q(x)\to R(x)\bigr) \] we can use \(\forall E\) to immediately conclude consequences such as
If the \(\forall E\) allows us to derive consequences from a universally quantified formula, the \(\forall I\) rule explains how to prove (most directly) that a universally quantified statement is true:
\[ {\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)\) knowing absolutely nothing about \(x\), then our proof is completely generic (would work for any value of \(x\)) and hence \(\forall x\ P(x)\) is true.
Example
Knowing nothing about \(x\), we can still show that \[ x\in\mathbb{R} \ \to \ x^2 \geq 0. \] By \(\forall I\), it immediately follows that \[ \forall x\ (x\in\mathbb{R} \ \to \ x^2 \geq 0) \] which can be abbreviated as \[ \forall x\in\mathbb{R} \ (x^2 \geq 0). \]
The \(\exists I\) rule explains the most direct route to proving an existential formula true: \[ {\large \frac{P(t)}{\exists x\ P(x)}}{\small~{\exists}I} \] where \(t\) 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+1\), it follows immediately by \(\exists I\) that:
Applying the \(\exists I\) rule again to the first of these formulas, we can infer further consequences including:
Finally, the \(\exists E\) rule explains how we can derive direct consequences from an existentially-quantified formula:
\[ {\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 \(z\) is a variable not free in any assumption.
That is, if we know something exists with property \(P\), we can give a specific name \(z\) to that thing. All we know about \(z\) is that it has property \(P\), but if just knowing that allows us to prove a conclusion \({\cal C}\) then \({\cal C}\) must be true.
The name \(z\) we chose for the thing that exists is essentially arbitrary; we just have to choose any variable name (\(x\),\(y\),\(z\),…) 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 \({\cal C}\).
Example
Suppose we know \(\forall x\ R(x)\to Q(x)\) (i.e., everything with property \(R\) also has property \(Q\)) and \(\exists k\ R(k)\) (i.e., there exists something having property \(R\)). > Let’s see how to use the above rules to prove \(\exists x\ Q(x)\) (i.e., there exists something having property \(Q\)). > Since our second assumption tells us there exists an individual with property \(R\), we can give that individual a name, say \(a\); we know nothing about \(a\) except that \(R(a)\) is true. > Then we can apply \(\forall E\) to the first assumption and conclude \(R(a)\to Q(a)\). By \(\to E\), it follows that \(Q(a)\). Finally, by \(\exists I\), we can conclude \(\exists x\ Q(x)\). > Since we proved our conclusion \(\exists x\ Q(x)\) from the assumption that \(R(a)\) is true (knowing nothing else about \(a\)), and the conclusion \(\exists x\ Q(x)\) doesn’t mention our temporary variable \(a\), we can use \(\exists E\) to turn our assumption \(\exists k\ R(k)\) into the conclusion \(\exists x\ Q(x)\).
Previous: 2.2 Predicate Formulae