Proofs

Write Fitch-style natural deduction proofs, checked line by line, with hints when you're stuck.

Argument to prove

Premises separated by commas, then ∴ and the goal, as in P → Q, P ∴ Q. To prove a theorem, start with ∴.

Allow derived rules

DS, MT, DNE, LEM and DeM, as in forall x.

Suggest rules while typing

Off hides the list while you type. The Choose a rule button and Ctrl+Space still show it.

Tab opens a subproof and Shift+Tab closes it. Press Esc, then Tab, to leave a field.