Metalogical properties of logic systems
Logic and Metalogic

Deductibility is the property of a logical system that expresses the passage from deduction (a syntactic consequence of a metalogical nature) to implication (of a logical nature).

A deduction theorem is a metatheorem that justifies the use of proof conditionals in logical systems that lack explicit ad hoc inference rules.

This considerably simplifies the construction of demonstrations.

Establishing the deduction theorem is necessary to prove the completeness theorem.