We now present an axiom system for propositional logic, which will consist of an infinite set of axioms and a single rule of inference. A derivation of a well-formed formula from a set of formulas will consist of a finite sequence of formulas each of whose members will either be an axiom or a premise or the output of an application of the rule of inference to prior members of the sequence.
There is one ingredient we will use for the specification of the infinite set of axioms. If \(\varphi\) is a propositional formula whose propositional variables are \(p_1, ..., p_n\) and \(\psi_1\), …, \(\psi_n\) are propositional formulas, we write \[ \varphi[\psi_1/p_1, ..., \psi_n/p_n] \] for the well-formed formula that results from \(\varphi\) when each propositional variable \(p_i\) is substituted for the well-formed formula \(\psi_i\). We will call \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) a substitution instance of \(\varphi\).
Definition 6.1 (Uniform Substitution) Given a well-formed formula \(\varphi\) whose propositional variables are among \(p_1, \dots, p_n\) and well-formed formulas \(\psi_1, \dots, \psi_n\), define \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) inductively:
If \(\varphi\) is \(p_i\), \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) is \(\psi_i\).
If \(\varphi\) is \(\neg \chi\), \(\varphi[\psi_1/p_1, ..., \psi_n/p_m]\) is \(\neg \chi[\psi_1/p_1, ..., \psi_n/p_m]\).
If \(\varphi\) is \((\chi \to \rho)\), then \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) is \((\chi[\psi_1/p_1, ..., \psi_n/p_n]\to \rho[\psi_1/p_1, ..., \psi_n/p_n])\).
We are now in a position to define the set of axioms of the system:
Definition 6.2 (Axiom) A well-formed formula \(\varphi\) is an axiom if, and only if, it is a substitution instance of one of the well-formed formulas below: \[ \begin{array}{lll} A1 & & p \to (q \to p)\\ A2 & & (p \to (q \to r)) \to ((p \to q) \to (p \to r))\\ A3 & & (\neg p \to \neg q) \to ((\neg p \to q) \to p) \end{array} \]
We will use a single rule of inference, which we call Modus Ponens (MP). The rule in question will enable us to move from two formulas of the form \(\varphi\) and \((\varphi \to \psi)\) to the formula \(\psi\).
\[\tag{MP} \varphi, \ (\varphi \to \psi)/\psi \]
Definition 6.3 (Derivability) A well-formed formula \(\varphi\) is derivable from a set of well-formed formulas \(\Gamma\), written \(\Gamma \vdash \varphi\), if, and only if, there is a finite sequence of well-formed formulas \((\chi_1, \dots , \chi_n)\) such that
\(\chi_n = \varphi\)
for each \(m \leq n\), either
Such a finite sequence \(( \chi_1, ..., \chi_n )\) is called a derivation (or a proof) of \(\varphi\) from \(\Gamma\).
So, a formula appears in a derivation if, and only if, it is either an axiom or a premise or the output of an application of modus ponens to two earlier members of the sequence.
Definition 6.4 (Theorem) A well-formed formula \(\varphi\) is a theorem, written \(\vdash \varphi\), if, and only if, \(\emptyset \vdash \varphi\).
We will write \(\nvdash \varphi\) to indicate that \(\varphi\) is not a theorem.
Here is a simple example of a derivation:
Example 6.1 \(\vdash p \to p\) \[ \begin{array}{llll} 1 & & p \to ((p \to p) \to p) & A1[p/p, (p \to p)/q]\\ 2 & & (p \to ((p \to p) \to p))\to ((p \to (p \to p)) \to (p \to p)) & A2[p/p, (p \to p)/q, p/r]\\ 3 & & (p \to (p \to p)) \to (p \to p) & \text{MP} \ 1, 2\\ 4 & & p \to (p \to p) & A1[p/p, p/q]\\ 5 & & p \to p & \text{MP} \ 3, 4\\ \end{array} \]
It is not difficult to generalize this argument into a schematic derivation of \(\varphi \to \varphi\) from no premises: \[ \vdash \varphi \to \varphi \] We will soon develop a library of subroutines, which will facilitate the discussion of the question of whether a given formula is derivable from a set of formulas.
We will rely on a very general result. First, some notational conventions. We write \(\Gamma, \varphi\) to abbreviate: \(\Gamma \cup \{\varphi\}\). And we will similarly write \(\varphi \vdash \psi\) to abbreviate: \(\{\varphi\} \vdash \psi\).
Theorem 6.1 Given a set of well-formed formulas \(\Gamma\) and two well-formed formulas \(\varphi\) and \(\psi\), \(\Gamma, \varphi \vdash \psi\) if, and only if, \(\Gamma \vdash \varphi \to \psi\).
One direction is simple:
Theorem 6.2 Given a set of well-formed formulas \(\Gamma\) and two well-formed formulas \(\varphi\) and \(\psi\), if \(\Gamma \vdash \varphi \to \psi\), then \(\Gamma, \varphi \vdash \psi\).
Proof. To obtain a derivation of \(\psi\) from \(\Gamma, \varphi\), we may extend a derivation of \(\varphi \to \psi\) from \(\Gamma\) with two additional steps: \(\varphi\), which being a member of \(\Gamma, \varphi\), is available as a premise, and \(\psi\) which is the output of Modus Ponens when applied to \(\varphi \to \psi\) and \(\varphi\).
The other direction is the deduction theorem, which requires a more involved justification:
Theorem 6.3 (The Deduction Theorem) Given a set of well-formed formulas \(\Gamma\) and two well-formed formulas \(\varphi\) and \(\psi\), if \(\Gamma, \varphi \vdash \psi\), then \(\Gamma \vdash \varphi \to \psi\).
Proof. Choose a set of formulas \(\Gamma\) and a formula \(\varphi\). We will use a complete induction on \(n\) to prove that for every non-zero \(n\):
That is, we argue that
So, we begin with the assumption:
We want to prove that
Consider a derivation of \(\psi\) from \(\Gamma, \varphi\) of the form: \[ ( \chi_1, ..., \chi_{n}) \] That means that \(\chi_{n}= \psi\).
There are four cases to consider:
Case 1. \(\psi\) is a logical axiom.
Here is a derivation of \(\varphi \to \psi\) from \(\Gamma\): \[ \begin{array}{lll} 1 & & \psi \to (\varphi \to \psi) & A1[\psi/p, \varphi/q]\\ 2 & & \psi & \\ 3 & & \varphi \to \psi & \text{MP} \ 1, 2\\ \end{array} \]
Case 2. \(\psi \in \Gamma\)
Here is a similar derivation of \(\varphi \to \psi\) from \(\Gamma\): \[ \begin{array}{lll} 1 & & \psi \to (\varphi \to \psi) & A1[\psi/p, \varphi/q]\\ 2 & & \psi & \\ 3 & & \varphi \to \psi & \text{MP} \ 1, 2\\ \end{array} \] Case 3. \(\psi = \varphi\)
Since \(\vdash \varphi \to \varphi\), a derivation of \(\varphi \to \varphi\) is a derivation of \(\varphi \to \psi\) from \(\Gamma\). Therefore \(\Gamma \vdash \varphi \to \psi\).
Case 4. \(\chi_k = (\chi_l \to \psi)\) for some \(k, l < n\)
That means that \((\chi_l \to \psi)\) and \(\chi_l\) are each in the sequence, which means that there are derivations \((\chi_1 \dots, \chi_l \to \psi)\) and \((\chi_1, \dots, \chi_l)\) of each formula \(\chi_l \to \psi\) and \(\chi_l\) from \(\Gamma, \varphi\) of length \(< n\).
Since both derivations have length strictly less than \(n\), by inductive hypothesis, \(\Gamma \vdash \varphi \to (\chi_l \to \psi)\) and \(\Gamma \vdash \varphi \to \chi_l\).
To build a derivation of \(\varphi \to \psi\) from \(\Gamma\), we may concatenate derivations of \(\varphi \to (\chi_1 \to \psi)\) and \(\varphi \to \chi_l\), respectively, from \(\Gamma\): \[ \begin{array}{llll} & & ... & \\ & & \vdots & \\ k & & \varphi \to (\chi_l \to \psi) & \Gamma \vdash \varphi \to (\chi_l \to \psi) \\ & & \vdots & \\ m & & \varphi \to \chi_l & \Gamma \vdash \varphi \to \chi_l\\ & & \vdots & \\ n& & ((\varphi \to (\chi_1 \to \psi)) \to ((\varphi \to \chi_l)\to (\varphi \to \psi)) & A2[\varphi/p,\chi_l/q,\psi/r]\\ n+1& & (\varphi \to \chi_l)\to (\varphi \to \psi) & \text{MP} \ k, n\\ n+2 & & \varphi \to \psi & \text{MP} \ m, n+1\\ \end{array} \] We conclude that given \(\Gamma\) and \(\varphi\), if \(( \chi_1, ..., \chi_n)\) is a derivation of a formula \(\psi\) from \(\Gamma, \varphi\), then \(\Gamma \vdash \varphi \to \psi\).
The deduction theorem encodes a common method of proof in mathematics. When you want to establish a conditional \(\varphi \to \psi\) in a mathematical context, you may adjoin \(\varphi\) to the body of mathematical assumptions in place \(\Gamma\) and once \(\psi\) is justified on that basis, you may conclude that \(\varphi \to \psi\) is a deductive consequence of the original assumptions.
We will now make use of the Deduction Theorem in order to prove a variety of helpful facts, which will facilitate the use of the axiom system.
Lemma 6.1 \(\vdash (\varphi \to \psi) \to ((\psi \to \chi)\to (\varphi \to \chi))\)
Proof. Given the Deduction Theorem, it suffices to note: \[ \{\varphi \to \psi \} \vdash (\psi \to \chi) \to (\varphi \to \chi). \] But given the Deduction Theorem, this reduces to: \[ \{ \varphi \to \psi, \psi \to \chi\} \vdash \varphi \to \chi, \] and \[ \{\varphi \to \psi, \psi \to \chi, \varphi\} \vdash \chi. \] But it is simple to provide a derivation of \(\chi\) from \(\{\varphi \to \psi, \psi \to \chi, \varphi\}\): \[ \begin{array}{llll} 1 & & \varphi \to \psi & \text{Premise} \\ 2 & & \varphi & \text{Premise} \\ 3 & & \psi & \text{MP} \ 1, 2 \\ 4 & & \psi \to \chi & \text{Premise} \\ 5 & & \chi & MP \ 3, 4\\ \end{array} \]
Lemma 6.2 \(\vdash (\neg \psi \to \neg \varphi) \to (\varphi \to \psi)\)
Proof. Given the Deduction Theorem, it suffices to note: \[ \{\neg \psi \to \neg \varphi\}\vdash \varphi \to \psi, \] which would in turn follow from the observation: \[ \{\neg \psi \to \neg \varphi, \varphi\} \vdash \psi. \] We provide a derivation of \(\psi\) from \(\{\neg \psi \to \neg \varphi, \varphi\}\): \[ \begin{array}{llll} 1 & & \neg \psi \to \neg \varphi & \text{Premise}\\ 2 & & \varphi \to (\neg \psi \to \varphi) & A1[\varphi/p,\neg \psi/q]\\ 3 & & \varphi & \text{Premise}\\ 4 & & \neg \psi \to \varphi & \text{MP} \ 2, 3\\ 5 & & (\neg \psi \to \neg \varphi) \to ((\neg \psi \to \varphi) \to \psi) & A3[\psi/p, \varphi/q]\\ 6 & & (\neg \psi \to \varphi) \to \psi & \text{MP} \ 1, 5\\ 7 & & \psi & \text{MP} \ 4, 6 \end{array} \]
Lemma 6.3 \(\vdash \neg \neg \varphi \to \varphi\)
Proof. Given the Deduction Theorem, it suffices to note: \[ \neg \neg \varphi \vdash \varphi \] Here is a derivation of \(\varphi\) from \(\neg \neg \varphi\): \[ \begin{array}{llll} 1 & & \neg \neg \varphi \to (\neg \varphi \to \neg \neg \varphi) & A1[\neg\neg\varphi/p, \neg \varphi/q]\\ 2 & & \neg \neg \varphi & \text{Premise} \\ 3 & & \neg \varphi \to \neg \neg \varphi & \text{MP} \ 1, 2 \\ 4 & & (\neg \varphi \to \neg \neg \varphi) \to ((\neg \varphi \to \neg \varphi) \to \varphi) & A3[\varphi/p, \neg \varphi/q]\\ 5 & & (\neg \varphi \to \neg \varphi) \to \varphi & \text{MP} \ 3, 4\\ 6 & & \neg \varphi \to \neg \varphi & \vdash \neg \varphi \to \neg \varphi\\ 7 & & \varphi & \text{MP} \ 5, 6 \end{array} \]
Lemma 6.4 \(\vdash \varphi \to \neg \neg \varphi\)
Proof. We exploit the last two observations to produce a simple derivation of \(\varphi \to \neg \neg \varphi\): \[ \begin{array}{llll} 1 & & \neg \neg \neg \varphi \to \neg \varphi & \text{Lemma} \ 3.3\\ 2 & & (\neg \neg \neg \varphi \to \neg \varphi) \to (\varphi \to \neg \neg \varphi) & \text{Lemma} \ 3.2\\ 3 & & \varphi \to \neg \neg \varphi & \text{MP} \ 1, 2 \end{array} \]
Lemma 6.5 \(\vdash (\varphi \to \psi) \to (\neg \psi \to \neg \varphi)\)
Proof. Given the Deduction Theorem, it suffices to establish: \[ \{\varphi \to \psi \} \vdash \neg \psi \to \neg \varphi, \] and \[ \{\varphi \to \psi, \neg \psi\} \vdash \neg \varphi. \] Here is a derivation of \(\neg \varphi\) from \(\{\varphi \to \psi, \neg \psi\}\): \[ \begin{array}{llll} 1 & & \varphi \to \psi & \\ 2 & & \psi \to \neg \neg \psi & \text{Lemma} \ 3.4\\ 3 & & \neg \neg \varphi \to \varphi & \text{Lemma} \ 3.3\\ 4 & & (\neg \neg \varphi \to \varphi) \to ((\varphi \to \psi) \to (\neg \neg \varphi \to \psi)) & \text{Lemma} \ 1 \\ 5 & & (\varphi \to \psi) \to (\neg \neg \varphi \to \psi) & \text{MP} \ 3, 4 \\ 6 & & \neg \neg \varphi \to \psi & \text{MP} \ 1, 4 \\ 7 & & (\neg \neg \varphi \to \psi) \to ((\psi \to \neg \neg \psi) \to (\neg \neg \varphi \to \neg \neg \psi)) & \text{Lemma} \ 4.1 \\ 8 & & (\psi \to \neg \neg \psi) \to (\neg \neg \varphi \to \neg \neg \psi) & \text{MP} \ 6, 7\\ 9 & & \neg \neg \varphi \to \neg \neg \psi & \text{MP} \ 2, 8\\ 10 & & (\neg \neg \varphi \to \neg \neg \psi) \to (\neg \psi \to \neg \varphi) & \text{Lemma} \ 3.2\\ 11 & & \neg \psi \to \neg \varphi & \text{MP} \ 9, 10 \end{array} \]
Exercise 6.1 Use these lemmas in order to justify: \[ \vdash (\varphi \to \neg \varphi) \to \neg \varphi \]
Lemma 6.6 \(\vdash \neg \varphi \to (\varphi \to \psi)\)
Proof. Given the Deduction Theorem, it suffices to show: \[ \{\neg \varphi, \varphi \}\vdash \psi \] Here is an outline of a derivation of \(\psi\) from \(\{\neg \varphi, \varphi\}\): \[ \begin{array}{llll} 1 & & \neg \varphi \to (\neg \psi \to \neg \varphi) & A1[\neg \varphi/p, \neg \psi/q] \\ 2 & & \neg \varphi & \text{Premise}\\ 3 & & (\neg \psi \to \neg \varphi) & \text{MP 1, 2}\\ 4 & & \varphi \to \psi & 3, \ \text{Lemma 3.2}\\ 5 & & \varphi & \text{Premise}\\ 6 & & \psi & \text{MP 4, 5}\\ \end{array} \]
Definition 6.5 (Consistency) A set of formulas \(\Gamma\) is consistent if, and only if, \(\bot\) is not derivable from \(\Gamma\). That is, \(\Gamma\) is consistent if, and only if, \(\Gamma \nvdash \bot\).
We write that a set \(\Gamma\) is inconsistent if, and only if, \(\Gamma\) is not consistent. That is, \(\Gamma\) is inconsistent if, and only if, \(\Gamma \vdash \bot\). Recall the definition of \(\bot\) in terms of \(\top\): \[ \bot := \neg \top. \] Since \(\top\) is an abbreviation for the formula \(p \to p\), \(\bot\) is an abbreviation for \(\neg (p \to p)\).
Proposition 6.1 Given a set of formulas \(\Gamma\) and a formula \(\varphi\), \[ \begin{array}{lll} \Gamma \vdash \varphi & \text{iff} & \Gamma, \neg \varphi \ \ \text{is inconsistent}.\\ \end{array} \]
Proof. We discuss one direction at a time.
(\(\Rightarrow\)) We argue that if \(\Gamma \vdash \varphi\), then \(\Gamma, \neg \varphi \vdash \bot\).
To that purpose we use the fact that a derivation of \(\varphi\) from \(\Gamma\) is automatically a derivation of \(\varphi\) from the larger set \(\Gamma, \neg \varphi\). We use this fact to produce a derivation of \(\bot\) from \(\Gamma, \neg \varphi\). \[ \begin{array}{llll} 1 & & \neg \varphi \to (\neg \bot \to \neg \varphi) & A1[\neg \varphi/p, \bot/q] \\ 2 & & \neg \varphi & \text{Premise}\\ 3 & & \neg \bot \to \neg \varphi & \text{MP 1, 2}\\ 4 & & \varphi \to \bot & \text{3, Lemma 3.2}\\ 5 & & \varphi & \Gamma, \neg \varphi \vdash \varphi\\ 6 & & \bot & \text{MP 4, 5}\\ \end{array} \]
(\(\Leftarrow\)) We want to prove that if \(\Gamma, \neg \varphi \vdash \bot\), then \(\Gamma \vdash \varphi\).
We use the Deduction Theorem to move from \(\Gamma, \neg \varphi \vdash \bot\) to \(\Gamma \vdash \neg \varphi \to \bot\). Since \(\Gamma, \neg \varphi \vdash \top\), by lemma 3.4, \(\Gamma, \neg \varphi \vdash \neg \neg \top\), which means \(\Gamma, \neg \varphi \vdash \neg \bot\). So, by the Deduction Theorem, \(\Gamma \vdash \neg \varphi \to \neg \bot\).
We now outline a derivation of \(\varphi\) from \(\Gamma\): \[ \begin{array}{llll} 1 & & \neg \varphi \to \neg \bot & \Gamma \vdash \neg \varphi \to \neg \bot \\ 2 & & (\neg \varphi \to \neg \bot) \to ((\neg \varphi \to \bot) \to \varphi) & A3[\varphi/p, \bot/q]\\ 3 & & (\neg \varphi \to \bot) \to \varphi & \text{MP 1, 2}\\ 4 & & \neg \varphi \to \bot & \Gamma \vdash \neg \varphi \to \bot \\ 5 & & \varphi & \text{MP 3, 4}\\ \end{array} \]
We now define what is for a set of formulas to be maximal consistent.
Definition 6.6 (Maximal Consistency) A set of formulas \(\Gamma\) is maximal consistent if, and only if,
\(\Gamma\) is consistent, and
for every \(\varphi\), if \(\Gamma, \varphi\) is consistent, then \(\varphi \in \Gamma\).
Proposition 6.2 Given a maximal consistent set of formulas \(\Gamma\) and two formulas \(\varphi\) and \(\psi\),
\(\Gamma \vdash \varphi\) if, and only if, \(\varphi \in \Gamma\).
\(\neg \varphi \in \Gamma\) if, and only if, \(\varphi \notin \Gamma\).
\(\varphi \to \psi \in \Gamma\) if, and only if \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\).
Proof. Given a maximal consistent set of formulas \(\Gamma\) and two formulas \(\varphi\) and \(\psi\), consider each claim at a time.
(\(\Rightarrow\)) We argue that if \(\Gamma \vdash \varphi\), then \(\varphi \in \Gamma\).
Suppose \(\Gamma \vdash \varphi\). We proceed by reductio. Suppose \(\varphi \notin \Gamma\). By definition of maximal consistency, if \(\Gamma\) is maximal consistent and \(\varphi \notin \Gamma\), then \(\Gamma, \varphi\) is inconsistent. But since \(\Gamma \vdash \varphi\), by proposition 3.6, \(\Gamma, \neg \varphi\) is inconsistent as well. It follows that \(\Gamma\) is inconsistent, which contradicts its maximal consistency.4 This is problem 3 in assignment 2. We conclude that \(\varphi \in \Gamma\).
(\(\Leftarrow\)) We argue that if \(\varphi \in \Gamma\), then \(\Gamma \vdash \varphi\).
If \(\varphi \in \Gamma\), then there is a one-line derivation of \(\varphi\) from \(\Gamma\).
(\(\Rightarrow\)) We argue that if \(\neg \varphi \in \Gamma\), then \(\varphi \notin \Gamma\).
Suppose \(\neg \varphi \in \Gamma\). Then, by 1 above, \(\Gamma \vdash \neg \varphi\). Since \(\Gamma\) is consistent, \(\Gamma \nvdash \varphi\), which, by 1 above, means \(\varphi \notin \Gamma\).5 If \(\Gamma \vdash \varphi\) and \(\Gamma \vdash \neg \varphi\), then \(\Gamma \vdash \bot\). This is because by lemma 3.6, \(\Gamma \vdash \neg \varphi \to (\varphi \to \bot)\).
(\(\Leftarrow\)) We show that if \(\varphi \notin \Gamma\), then \(\neg \varphi \in \Gamma\).
Suppose \(\varphi \notin \Gamma\). Since \(\Gamma\) is maximal consistent, \(\Gamma, \varphi\) is inconsistent. Given lemmas 3.3 and 3.4, \(\Gamma, \varphi\) is inconsistent if, and only if, \(\Gamma, \neg \neg \varphi\) is inconsistent. So, since \(\Gamma, \neg \neg \varphi\) is inconsistent, we conclude, by proposition 3.6, that \(\Gamma \vdash \neg \varphi\). So, by 1 above, \(\neg \varphi \in \Gamma\).
(\(\Rightarrow\)) We argue that if \(\varphi \to \psi \in \Gamma\), then if \(\varphi \in \Gamma\), then \(\psi \in \Gamma\).
Suppose \(\varphi \to \psi \in \Gamma\). Then, given 1 above, \(\Gamma \vdash \varphi \to \psi\). Now: if \(\varphi \in \Gamma\), then \(\Gamma \vdash \varphi\) and \(\Gamma \vdash \psi\), whence \(\psi \in \Gamma\).
(\(\Leftarrow\)) We show that if \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\), then \(\varphi \to \psi \in \Gamma\).
Suppose \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\).
If \(\varphi \notin \Gamma\), then given 2 above, \(\neg \varphi \in \Gamma\). Since lemma 3.6 gives us that \(\vdash \neg \varphi \to (\varphi \to \psi)\) and \(\Gamma \vdash \neg \varphi\), we infer \(\Gamma \vdash \varphi \to \psi\). So, given 1, \(\varphi \to \psi \in \Gamma\).
If \(\psi \in \Gamma\), then since \(\vdash \psi \to (\varphi \to \psi)\), \(\Gamma \vdash \varphi \to \psi\). So, given 1, \(\varphi \to \psi \in \Gamma\).