2 Propositional natural deduction
We begin the study of natural deduction by looking at the rules governing the connectives AND and IMP which are intended to be read "and" and "if...then" respectively. After reading the first three sections, make sure you understand the sample proofs using these two connectives, as they require the concepts fundamental to all proofs in the natural deductive style.
We then add the remaining connectives NOT and OR with the introduction and elimination rules governing them. This will complete the deductive account of propositional logic. Work through all of the proofs in this chapter and make sure you understand them. It is important to become fluent in using the natural deduction system at the propositional level before proceeding to any more advanced parts of logic.
The exercises in this chapter are best approached using the proof editing tool provided.
 Conjunction Natural deduction rules ANDI and ANDE
 Implication The rules IMPI and IMPE; discharging assumptions
 Counting assumptions Theorems, weakening and contraction
 Examples Proofs using conjunction and implication
 Negation Natural deduction rules NOTI and NOTE; using RAA instead
 Extra (math) RAA is equivalent to NOTI and NOTE
 Disjunction Natural deduction rules ORI and ORE
 Examples Proofs using negation and disjunction

Propositional proof exercises Sample problems with solutions