Natural Deduction Proof Generator & Checker

This is a proof generator and checker for the Fitch-style natural deduction system found in forall x: Calgary. You can work through exercises from the textbook or experiment with arguments of your own. If you get stuck, you can request hints to help you complete your proof one step at a time. For the source code and further details, see 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)
  • c must not occur in any premise or undischarged assumption before line m
∀E — Universal elimination
∀E — Universal elimination (1)
∃I — Existential introduction
∃I — Existential introduction (1)
∃E — Existential elimination
∃E — Existential elimination (1)
  • c must not occur in any premise or undischarged assumption before line i
  • c must not occur in ∃x A(...x...x...)
  • c must not occur in B
=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)

No line or subproof above line m may be cited by any rule within the strict subproof begun at line m unless the rule explicitly allows it.

☐E — Box elimination
☐E — Box elimination (1)

☐E can only be applied if line m (containing ☐A) lies outside of the strict subproof in which line n falls, and this strict subproof is not itself part of a strict subproof not containing m.

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)

The line n on which rule RT is applied must not lie in a strict subproof that begins after line m.

R4 — Rule for System S4
R4 — Rule for System S4 (1)

R4 can only be applied if line m (containing ☐A) lies outside of the strict subproof in which line n falls, and this strict subproof is not itself part of a strict subproof not containing m.

R5 — Rule for System S5
R5 — Rule for System S5 (1)

R5 can only be applied if line m (containing ¬☐A) lies outside of the strict subproof in which line n falls, and this strict subproof is not itself part of a strict subproof not containing m.

Derived rules for ML
MC — Modal conversion
MC — Modal conversion (1)
MC — Modal conversion (2)
MC — Modal conversion (3)
MC — Modal conversion (4)
Basic deduction rules for QML
∀I — Universal introduction
∀I — Universal introduction (1)
  • c must not occur in any citable premise or undischarged assumption before line m
  • If used inside a strict subproof, c must not occur in any line imported into the strict subproof (i.e. any line justified by the rules ☐E, R4, or R5)
∃E — Existential elimination
∃E — Existential elimination (1)
  • c must not occur in any citable premise or undischarged assumption before line i
  • c must not occur in ∃x A(...x...x...)
  • c must not occur in B
  • If used inside a strict subproof, c must not occur in any line imported into the strict subproof (i.e. any line justified by the rules ☐E, R4, or R5)
BF — Barcan formula
BF — Barcan formula (1)
ND — Necessity of distinctness
ND — Necessity of distinctness (1)
Derived rules for QML
CBF — Converse Barcan formula
CBF — Converse Barcan formula (1)
NI — Necessity of identity
NI — Necessity of identity (1)