502 – Propositional logic (2)

September 10, 2009

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 {S} is a set of formulas, and {A} and {B} are formulas, then {S\cup\{A\}\vdash B} if and only if {S\vdash A\rightarrow B.}

Read the rest of this entry »