Lesson 14

Using the concept of proof from a set of expressions, we can simplify even proofs of validity (where no premises are needed). This is done by exploiting three interesting results, stated next. These results formalize three patterns of thought very common in mathematical reasoning: they could be called the deduction technique, arguing by contradiction, and justified generalization.

In the deduction technique we wish to prove \(\phi \Rightarrow \psi\) and we argue thus: “Let us assume that \(\phi\) holds...”

Theorem (The Deduction Technique). \(\Delta \cup \{\phi\} \vdash \psi\) if and only if \(\Delta \vdash \phi \Rightarrow \psi\).

Proof. If \(\Delta \vdash \phi \Rightarrow \psi\), then trivially \(\Delta \cup \{ \phi \} \vdash \psi\), by applying once modus ponens.

In the other direction, it is not as straightforward and remains as an exercise.◼ The next proof method is perhaps even more familiar: To show \(\phi\), we assume \(\neg \phi\) and arrive at a contradiction. Formally, a contradiction can be defined as the expression \(\psi \land \neg \psi\), where \(\psi\) is some arbitrary expression; if \(\psi \land \neg \psi\) can be proved from \(\Delta\), then all expressions, including all other contradictions, can be proved as tautological implications. If \(\Delta \vdash \phi\), for any expression \(\phi\) (including the contradictions mentioned above), then we say that \(\Delta\) is inconsistent; otherwise, if no contradiction can be proved from \(\Delta\), we say \(\Delta\) is consistent.

Theorem (Arguing by Contradiction). If \(\Delta \cup \{ \neg \phi \}\) is inconsistent, then \(\Delta \vdash \phi\).

Proof. Suppose that \(\Delta \cup \{ \neg \phi \}\) is inconsistent. Then \(\Delta \cup \{ \neg \phi \} \vdash \phi\) (along with any other expression). By the deduction technique, we know that \(\Delta \vdash \neg \phi \Rightarrow \phi\), which is equivalent to \(\phi\). Formally, our proof adds to the proof of \(\neg \phi \Rightarrow \phi\) the sequence \(…\), \(\neg \phi \Rightarrow \phi\), \(\phi\), the former as a Boolean axiom, the latter by modus ponens. \(\square\)◼

The last argument in the proof (proving \(\phi\) from \(\neg \phi \Rightarrow \phi\)) is very common, and quite routine. It involves proving an expression which is the “Boolean consequence” of already proven expressions. In the future we shall telescope such steps, bringing in Boolean consequences without much ado.

In mathematics we frequently end our proofs as follows: “… and since \(x\) was taken to be an arbitrary integer, the proof is complete.” This type of argument can be formalized:

Theorem (Justified Generalization). Suppose that \(\Delta \vdash \phi\), and \(x\) is not free in any expression of \(\Delta\). Then \(\Delta \vdash \forall x \phi\).

Proof. Consider a proof \(S = (\phi_{1}, …, \phi_{n})\) of \(\phi\) from \(\Delta\) (that is, \(\phi_{n} = \phi\)). We shall prove by induction on \(i\) that there is a proof of \(\forall x \phi_{i}\) from \(\Delta\), for \(i = 0, …, n\). The result will follow, taking \(i = n\).

The statement is vacuously true when \(i = 0\), so suppose it is true for all \(j < i\), where \(i \leq n\). The proof of \(\forall x \phi_{i}\) includes all proofs of the expressions \(\forall x \phi_{j}\), \(1 \leq j < i\), and certain new expressions that prove \(\forall x \phi_{i}\). These new expressions depend on \(\phi_{i}\).

If \(\phi_{i}\) is in \(\Lambda\) (that is, it is a logical axiom), then \(\forall x \phi_{i}\) is an axiom as well, and can be added to the proof. If \(\phi_{i}\) is in \(\Delta\) (that is, it is a non-logical axiom), then we know \(x\) is not free in \(\phi_{i}\), and thus we add the sequence \(…\), \(\phi_{i}\), \((\phi_{i} \Rightarrow \forall x \phi_{i})\), \(\forall x \phi_{i}\). The first is a non-logical axiom, the second an axiom from group AX3, and the last is added by modus ponens.

If finally \(\phi_{i}\) was obtained from some \(\phi_{j}\), and \(\phi_{j} \Rightarrow \phi_{i}\) by modus ponens, by induction our proof now includes \(\forall x \phi_{j}\) and \(\forall x (\phi_{j} \Rightarrow \phi_{i})\). We add to the proof the expressions \[\forall x (\phi_{j} \Rightarrow \phi_{i}) \Rightarrow ((\forall x \phi_{j}) \Rightarrow (\forall x \phi_{i})), \quad (\forall x \phi_{j}) \Rightarrow (\forall x \phi_{i}), \quad \text{and}\quad \forall x \phi_{i}.\] The first is an axiom of group AX4, while the second and the third are obtained by modus ponens.◼