# 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:

### 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.