Editing Deduction theorem (section)

==Proof of the deduction theorem==

We prove the deduction theorem in a Hilbert-style deductive system of propositional calculus.{{sfn|Franks}}

Let <math>\Delta </math> be a set of formulas and <math>A</math> and <math>B</math> formulas, such that <math>\Delta \cup \{A\} \vdash B </math>. We want to prove that <math>\Delta \vdash A \to B </math>.

Since <math>\Delta \cup \{A\} \vdash B </math>, there is a proof of <math>B</math> from <math>\Delta \cup \{A\}</math>. We prove the theorem by induction on the proof length ''n''; thus the induction hypothesis is that for any <math>\Delta</math>, <math>A</math> and <math>B</math> such that there is a proof of <math>B</math> from <math>\Delta \cup \{A\}</math> of length up to ''n'', <math>\Delta \vdash A \to B </math> holds.

If ''n'' = 1 then <math>B</math> is member of the set of formulas <math>\Delta \cup \{A\}</math>. Thus either <math>B=A</math>, in which case <math>A \to B </math> is simply <math>A \to A </math>, which is derivable by substitution from ''p'' → ''p'', which is derivable from the axioms, and hence also <math>\Delta \vdash A \to B </math>, or <math>B</math> is in <math>\Delta</math>, in which case <math>\Delta \vdash B </math>; it follows from axiom ''p'' → (''q'' → ''p'') with substitution that <math>\Delta \vdash B \to (A \to B) </math> and hence by modus ponens that <math>\Delta \vdash A \to B </math>.

Now let us assume the induction hypothesis for proofs of length up to ''n'', and let <math>B</math> be a formula provable from <math>\Delta \cup \{A\}</math> with a proof of length ''n''+1. Then there are two possibilities:

#<math>B</math> is member of the set of formulas <math>\Delta \cup \{A\}</math>; in this case we proceed as for ''n''=1.
#<math>B</math> is arrived at by using modus ponens. Then there is a formula ''C'' such that <math>\Delta \cup \{A\}</math> proves <math>C</math> and <math>C \to B </math>, and modus ponens is then used to prove <math>B</math>. The proofs of <math>C</math> and <math>C \to B </math> are with at most ''n'' steps, and by the induction hypothesis we have <math>\Delta \vdash A \to C </math> and <math>\Delta \vdash A \to (C \to B) </math>. By the axiom (''p'' → (''q'' → ''r'')) → ((''p'' → ''q'') → (''p'' → ''r'')) with substitution it follows that  <math>\Delta \vdash (A \to (C \to B)) \to ((A \to C) \to (A \to B))</math>, and by using modus ponens twice we have <math>\Delta \vdash A \to B </math>.

Thus in all cases the theorem holds also for ''n''+1, and by induction the deduction theorem is proven.