Natural deduction is a type of forward reasoning proof system: the objective is to derive the conclusion of the argument, starting from its premises.
There are two ways of generating new conclusions in natural deduction: ?
- We either eliminate a connective from a formula in the proof to generate a new conclusion (via a connective elimination rule)
- We produce a new conclusion with a connective, by combining formulas in the proof (via a connective introduction rule)