LFE: Proof Checker
This is modified version of Kevin Klement's proof editor and checker for Fitch-style natural deduction systems. The specific system used here is the one found in Jason Decker's Logic For Everyone: From Proof to Paradox.
Create a new problem
Select PL or QL syntax:Premises (separated with “;”):
Conclusion:
Proof:
Instructions
| PL atomic sentences: (single uppercase letters) | A, B, X, etc. |
| QL atomic sentences: (single uppercase letters other than A or E followed by lowercase letters a–w within parentheses (separated by commas), and identities) | P(a), F(c,d,c), 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 (QL only), you may use any of the symbols: | ∀x (∀x) Ax (Ax) ⋀x |
| For the existential quantifier (QL 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
