Skip to content
Free public beta until December 4, 2026: every course is open, no card needed. After that, the first chapter of each course stays free and full access is a one-time $39 ($19 for up to 100 founding members chosen for helpful feedback). Your progress is kept. How the beta works

natural deduction

A proof system with an introduction rule and an elimination rule for each connective.

Natural deduction is a style of proof system meant to mirror ordinary reasoning. Each connective has rules for introducing it and for using (eliminating) it, and assumptions are made and discharged inside subproofs. This course uses Fitch-style layout, with subproofs marked by indented bars.

Examples

  • ∧I, ∧E, →I, and →E are natural-deduction rules.

See also

formal proof introduction rule elimination rule
Read the full section →