Natural deduction proof checker

This is a proof checker for the Fitch-style natural deduction system found in forall x: An Introduction to Formal Logic. It is a slightly modified version of this proof checker. I have modified the names for the rules in the original text of forall x, and have therefore updated the code for the proof checker to match.

Create a new problem

Select if SL or PL syntax:

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

Conclusion:



Sample exercise sets

Instructions

SL atomic sentences:
(single uppercase letters)
A, B, X, etc.
PL atomic sentences:
(single uppercase letters other than A or E followed by
lowercase letters a–w without parentheses)
Pa, Fcdc, 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 SL only: =)
For the conditional you may use any of the symbols: → ⇒ ⊃ -> >
For the universal quantifier (PL only), you may use any of the symbols: ∀x (∀x) Ax (Ax) (x) ⋀x
For the existential quantifier (PL 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