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