Natural Deduction Proof Generator & Checker

This is a proof generator and checker for the Fitch-style natural deduction system found in forall x: Calgary. It is based on the Open Logic Project proof checker. More information can be found in the ND-Prover repository.

Basic deduction rules for TFL
R — Reiteration
R — Reiteration (1)
∧I — Conjunction introduction
∧I — Conjunction introduction (1)
∧E — Conjunction elimination
∧E — Conjunction elimination (1)
∧E — Conjunction elimination (2)
∨I — Disjunction introduction
∨I — Disjunction introduction (1)
∨I — Disjunction introduction (2)
∨E — Disjunction elimination
∨E — Disjunction elimination (1)
→I — Conditional introduction
→I — Conditional introduction (1)
→E — Conditional elimination
→E — Conditional elimination (1)
↔I — Biconditional introduction
↔I — Biconditional introduction (1)
↔E — Biconditional elimination
↔E — Biconditional elimination (1)
↔E — Biconditional elimination (2)
¬I — Negation introduction
¬I — Negation introduction (1)
¬E — Negation elimination
¬E — Negation elimination (1)
X — Explosion
X — Explosion (1)
IP — Indirect proof
IP — Indirect proof (1)
Derived rules for TFL
DS — Disjunctive syllogism
DS — Disjunctive syllogism (1)
DS — Disjunctive syllogism (2)
MT — Modus tollens
MT — Modus tollens (1)
DNE — Double-negation elimination
DNE — Double-negation elimination (1)
LEM — Law of excluded middle
LEM — Law of excluded middle (1)
DeM — De Morgan's laws
DeM — De Morgan's laws (1)
DeM — De Morgan's laws (2)
DeM — De Morgan's laws (3)
DeM — De Morgan's laws (4)
Basic deduction rules for FOL
∀I — Universal introduction
∀I — Universal introduction (1)
∀E — Universal elimination
∀E — Universal elimination (1)
∃I — Existential introduction
∃I — Existential introduction (1)
∃E — Existential elimination
∃E — Existential elimination (1)
=I — Identity introduction
=I — Identity introduction (1)
=E — Identity elimination
=E — Identity elimination (1)
=E — Identity elimination (2)
Derived rules for FOL
CQ — Conversion of quantifiers
CQ — Conversion of quantifiers (1)
CQ — Conversion of quantifiers (2)
CQ — Conversion of quantifiers (3)
CQ — Conversion of quantifiers (4)
Basic deduction rules for ML
☐I — Box introduction
☐I — Box introduction (1)
☐E — Box elimination
☐E — Box elimination (1)
Def◇ — Definition of diamond
Def◇ — Definition of diamond (1)
Def◇ — Definition of diamond (2)
RT — Rule for System T
RT — Rule for System T (1)
R4 — Rule for System S4
R4 — Rule for System S4 (1)
R5 — Rule for System S5
R5 — Rule for System S5 (1)
Derived rules for ML
MC — Modal conversion
MC — Modal conversion (1)
MC — Modal conversion (2)
MC — Modal conversion (3)
MC — Modal conversion (4)
Derived rules for FOML
BF — Barcan formula
BF — Barcan formula (1)
CBF — Converse Barcan formula
CBF — Converse Barcan formula (1)