I now proceed to present a series of results whose overall goal is to make the handling of formal proofs more efficient and natural. These results formalize different methods of reasoning commonly used in practice. A second goal in presenting these results is in preparing the way for the proof of the completeness theorem.
Theorem 7 (The deduction theorem) If
is a set of formulas, and
and
are formulas, then
if and only if
![]()