forall x proof builder and checker

This is a demo of a proof checker for the deductive systems found in the book forall x: an Introduction to Formal Logic, by P.D. Magnus, based in particular on the Calgary remix, which has changes due to Tim Button, J. Robert Loftis, Aaron Thomas Bolduc and Richard Zach.

The proof builder/checker therefore matches the remix proof system, which differs a little from the original.

At the moment, this is just a test demo, but may become something more down the road.

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.

For a summary of the rules used in this system, see this summary document.

Sample exercise sets

Create an arbitrary problem below


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

Conclusion: