502 – Propositional logic (2)

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