# Proof of the deduction theorem in first-order logic

I understand how to proof the deduction theorem $$(D): \Delta,\varphi\vdash\psi\Rightarrow\Delta\vdash\varphi\rightarrow\psi$$ with a set of propositions $$\Delta$$ and some propositions $$\varphi$$ and $$\psi$$ for propositional logic. If I understand correctly, it works via induction over the length of a proof n. Then we show that for n=1, $$\psi$$ must be either equal to $$\varphi$$, in which case the implication $$\varphi\rightarrow\psi$$ is trivially provable, or it is a member of $$\Delta$$ in which case we have $$\Delta\vdash\psi$$ and with the tautology $$\psi\rightarrow(\varphi\rightarrow\psi)$$ and MP we have $$\varphi\rightarrow\psi$$. Then we assume that for a proof of length n the above statement (D) holds true and conclude, that it must hold true for a proof of length n+1. We proceed as follows: $$\psi$$ must be reached via MP, so there is a proposition $$\phi$$, s.t. $$\phi\rightarrow\psi$$ and $$\phi$$ are proved from $$\Delta,\varphi$$ in a maximum of n steps. By our induction hypothesis we have $$\Delta\vdash\varphi\rightarrow\phi$$ and $$\Delta\vdash\varphi\rightarrow(\phi\rightarrow\psi)$$, so by the tautology $$(\varphi\rightarrow(\phi\rightarrow\psi)\rightarrow((\varphi\rightarrow\phi)\rightarrow(\varphi\rightarrow\psi))$$ using MP twice we have $$\Delta\vdash\varphi\rightarrow\psi$$ as desired.

Now as far as I understood proving (D) for predicate logic when using tautologies and tautological consequences everything is the same (assuming that $$\psi$$ is a sentence), we only have to consider one further step how to reach $$\psi$$ and that is generalization (I assume because specification can be somehow reduced?). But how does the reasoning work here exactly? I assume that (D) holds true for a proof of length n and have to show that it holds for a proof of length n+1. So let's assume we reach $$\psi$$ via generalization, that means that $$\psi=\forall{x}\psi'$$ and in our proof of length n we have the line $$\psi'$$ - how do I use the induction hypothesis here?

• generalization is not enough: there are somewhere axioms for quantifier. Feb 7 at 18:39
• In addition, the theorem holds only with $\varphi$ closed. Feb 7 at 18:40
• It seems like the reasoning for (D) in the first paragraph works no matter whether $\Delta$, $\phi$, and $\psi$ are statements from propositional logic or predicate logic ... I must be missing something? Feb 7 at 18:45
• @Bram28 I think it should, yes. If we treat all formulas that can be transformed into propositional tautologies via substitution as axioms, then the reasoning for reaching $\psi$ via MP should be the same. Feb 7 at 19:54
• @MauroALLEGRANZA I thought the requirement is that $\psi$ should be a sentence (t.i. closed) as I also wrote above? And concerning the axiom quantifiers you mean not only universal generalization, but also exist. gener., universal specification and exist. specification? Feb 7 at 19:56

The deduction theorem for predicate logic follows the same line of ideas as the deduction theorem for propositional calculus except for one restriction: The generalised variable in the consequent formula must not occur free in the antecedent formula.

For the systems that employ the axiom $$\forall x(A\rightarrow B)\rightarrow(\forall x A\rightarrow\forall x B)$$

the referred variable is already bound. For the systems that employ the axiom

$$\forall x(A\rightarrow B)\rightarrow(A\rightarrow\forall x B)$$

the restriction must be observed.

I shall go over the baseline of the relevant part of the proof without full annotation, since the steps are sufficiently clear.

Suppose $$\psi$$ is deduced by either

• modus ponens from two preceding formulas $$\psi_{j}$$ and $$\psi_{j}\rightarrow\psi$$, or
• generalisation from $$\psi_{j}$$.

The former prong of the fork is as in the familiar one of propositional calculus. We look into the latter prong. Hence, we have got $$\psi_{j}$$ for some $$j$$ in the sequence. Then,

$$\phi\rightarrow\psi_{j}$$ by induction hypothesis.

$$\forall x_{i}(\phi\rightarrow\psi_{j})$$ by generalisation where the variable $$x_{i}$$ does not occur free in $$\phi$$.

$$\forall x_{i}(\phi\rightarrow\psi_{j})\rightarrow(\phi\rightarrow\forall x_{i}\psi_{j})$$ by the axiom mentioned above.

$$\phi\rightarrow\forall x_{i}\psi_{j}$$ by modus ponens.

Therefore,

$$\Delta,\phi\vdash\psi\implies\Delta\vdash\phi\rightarrow\psi$$