Doubts: Proof of Deduction Theorem

Question

I am reading Robert Wolf's A Tour Through Mathematical Logic and am enjoying it. But the author omits proofs for the Deduction and Generalization Theorems. I looked through Intermediate Logic by Bostock for a proof and it has a rather descriptive one.

But the author uses a set of three axioms.

• $\vdash P \to (Q \to P) $
• $\vdash (P \to (Q\to R)) \to ((P \to Q) \to (P \to R))$
• $ \vdash (\lnot Q \to \lnot P) \to (P \to Q) $

So to prove the base case in an Inductive proof the author uses the first axiom. That is to prove " If $\Gamma \cup \{P\} \vdash Q $ then $\Gamma \vdash P \to Q $ " he first treats the case when $Q$ is an Axiom. Then he says $ Q \to (P \to Q) $ is also an axiom and hence by Modus Ponens $ (P \to Q) $ is proveable without assumptions.

But when reading I thought these axioms constituted only an example of a First Order Theory. Then how were they used to prove the Deduction Theorem which is stated for an arbitrary First Order Theory $\Gamma$? Must a First Order Theory necessarily consist of these Axioms or something similar? What am I missing?

Answer 1

I think your confusion may arise from a misinterpretation of the Deduction Theorem, and of the terms "theory" and "proof system". In proof theory, a proof system $\mathscr P$ defines the context you are working in. It defines (in meta-language):

• What the formulas are that we can use, e.g. that if $P, Q$ are formulas, then so are $P \to Q$ and $\neg P$. (We also accept some so-called literals, which are formulas that don't consist of other formulas.)
• What the axioms are, i.e. what formulas $P$ we accept to be "true" without proof. In the above, examples are given by $Q \to(P \to Q)$ for all formulas $P$ and $Q$.
• What the rules of inference are, i.e. in what ways we can derive new "true" formulas from formulas known to be "true". For example, modus ponens allows us to infer that $Q$ is "true" if both $P \to Q$ and $P$ are "true".

Note that I write "true" in quotes. This is because it really means provable by means of the proof system $\mathscr P$. Only at a later stage can we judge if this notion agrees with what we intuitively regard as true (basically, this amounts to the question if $\mathscr P$ "makes sense").

In the same context of proof theory, a theory $\Gamma$ is usually defined as simply a collection of formulas, as they are defined above. To clear all ambiguity, we might refer to $\mathscr P$-theories.

---

The notation $\Gamma \vdash P$ now means: If we accept $\Gamma$ as "true", then the proof system allows us to prove $P$. So effectively we enhance our system to have the formulas from $\Gamma$ as extra axioms, with which we can prove things.

Now the Deduction Theorem can be interpreted properly; it says the following:

Deduction Theorem If there is a proof of $Q$ from $\Gamma, P$, then there also is a proof of $P \to Q$ from $\Gamma$.

In the case described by you, there is a trivial proof of $Q$, since $Q$ is an axiom. Together with the axiom $Q \to (P \to Q)$ and modus ponens, this means there is also a proof of $P \to Q$. That we did not use $P$ or any formula from $\Gamma$ does not, of course, influence the fact that we can prove $P \to Q$.

---

In conclusion, the Deduction Theorem is a theorem about (theories $\Gamma$ in) the proof system $\mathscr P$. It is not a theorem about the conceptual logical framework around $\mathscr P$ that we might also colloquially describe as a "theory". I hope that clears a bit of the fog for you — this whole dichotomy between reasoning within and about a proof system, together with the associated terminology, definitely takes time to get used to.