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. (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 forall x: Calgary. However, the system also supports the rules used in the forall x: Cambridge remix.)

Create a new problem

Select if TFL or FOL syntax:

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

Conclusion:



Sample exercise sets

Instructions

TFL atomic sentences:
(single uppercase letters)
A, B, X, etc.
FOL atomic sentences:
(single uppercase letters other than A or E followed by
lowercase letters a–w without parentheses, or identities)
Pa, Fcdc, a = d, etc.
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