Deduction Theorem - The Deduction Theorem in Predicate Logic

The Deduction Theorem in Predicate Logic

The deduction theorem is also valid in first-order logic in the following form:

• If T is a theory and F, G are formulas with F closed, and T∪{F}├G, then T├F→G.

Here, the symbol ├ means "is a syntactical consequence of." We indicate below how the proof of this deduction theorem differs from that of the deduction theorem in propositional calculus.

In the most common versions of the notion of formal proof, there are, in addition to the axiom schemes of propositional calculus (or the understanding that all tautologies of propositional calculus are to be taken as axiom schemes in their own right), quantifier axioms, and in addition to modus ponens, one additional rule of inference, known as the rule of generalization: "From K, infer ∀vK."

In order to convert a proof of G from T∪{F} to one of F→G from T, one deals with steps of the proof of G which are axioms or result from application of modus ponens in the same way as for proofs in propositional logic. Steps which result from application of the rule of generalization are dealt with via the following quantifier axiom (valid whenever the variable v is not free in formula H):

• (H→K)→(H→∀vK).

Since in our case F is assumed to be closed, we can take H to be F. This axiom allows one to deduce F→∀vK from F→K, which is just what is needed whenever the rule of generalization is applied to some K in the proof of G.