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?

  • $\begingroup$ generalization is not enough: there are somewhere axioms for quantifier. $\endgroup$ Feb 7 at 18:39
  • $\begingroup$ In addition, the theorem holds only with $\varphi$ closed. $\endgroup$ Feb 7 at 18:40
  • $\begingroup$ 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? $\endgroup$
    – Bram28
    Feb 7 at 18:45
  • $\begingroup$ @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. $\endgroup$
    – Josef K.
    Feb 7 at 19:54
  • $\begingroup$ @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? $\endgroup$
    – Josef K.
    Feb 7 at 19:56

1 Answer 1


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.




You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .