Hilbert System - Metatheorems

Because Hilbert-style systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.

Some common metatheorems of this form are:

• The deduction theorem: if and only if .
• if and only if and .
• Contraposition: If then .
• Generalization: If and x does not occur free in any formula of then .