more from David Bostock

Single Idea 13754

[catalogued under 5. Theory of Logic / H. Proof Systems / 4. Natural Deduction]

Full Idea

Natural deduction adopts for → as rules the Deduction Theorem and Modus Ponens, here called →I and →E. If ψ follows φ in the proof, we can write φ→ψ (→I). φ and φ→ψ permit ψ (→E).

Clarification

'I' means introduction, and 'E' means elimination

Gist of Idea

Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E)

Source

David Bostock (Intermediate Logic [1997], 6.2)

Book Reference

Bostock,David: 'Intermediate Logic' [OUP 1997], p.248


A Reaction

Natural deduction has this neat and appealing way of formally introducing or eliminating each connective, so that you know where you are, and you know what each one means.

Related Idea

Idea 13755 Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it [Bostock]