Natural deduction proof editor and checker

This is a demo of a proof checker for Fitch-style natural deduction systems found in many popular introductory logic textbooks. The specific system used here is the one found in forall x: Calgary Remix. (Although based on forall x: an Introduction to Formal Logic, the proof system in that original version differs from the one used here and in the Calgary Remix. However, the system also supports the rules used in the forall x: Cambridge remix.)

Create a new problem


Premises (separate with “,” or “;”):

Conclusion:



Sample exercise sets

Instructions

For negation you may use any of the symbols: ¬ ~ ∼ - −
For conjunction you may use any of the symbols: ∧ ^ & . · *
For disjunction you may use any of the symbols: ∨ v
For the biconditional you may use any of the symbols: ↔ ≡ <-> <> (or in TFL only: =)
For the conditional you may use any of the symbols: → ⇒ ⊃ -> >
For the universal quantifier (FOL only), you may use any of the symbols: ∀x (∀x) Ax (Ax) (x) ⋀x
For the existential quantifier (FOL only), you may use any of the symbols: ∃x (∃x) Ex (Ex) ⋁x
For a contradiction you may use any of the symbols: ⊥ XX #

The following buttons do the following things:

×= delete this line
|+= add a line below this one
||+= add a new subproof below this line
<+= add a new line below this subproof to the parent subproof
<|+= add a new subproof below this subproof to the parent subproof

Apart from premises and assumptions, each line has a cell immediately to its right for entering the justifcation. Click on it to enter the justification as, e.g. “&I 1,2”.

Hopefully it is otherwise more or less obvious how to use it.

Rules

Basic rules
Derived rules
Rules for Cambridge