Logic Tools

Free software for learning symbolic logic, written to accompany How Logic Works but usable with any course that teaches natural deduction in the Lemmon style. Nothing to install, no account, no charge.

Open the tools →

Check a proof you wrote by hand

Photograph a completed proof with your phone and the page is transcribed and checked. You see the transcription beside the photograph and correct it before anything is judged, so a misreading costs you an edit rather than a wrong answer.

Check a proof you type

Enter a derivation line by line and every line is checked against the rules: the dependencies, the citations, and the rule itself. When a line fails you are told which requirement it missed, not merely that something is wrong.

Sentences, truth tables and models

For instructors

The proof checker implements the twenty-one rules of How Logic Works exactly as the book states them, including the dependency bookkeeping that most software omits. It is deliberately strict about citation order and about blank dependency cells, because those are where students’ mistakes actually live.

Students need no account and submit nothing to me; the tools run in the browser against a small server and keep no record of what is checked. You are welcome to link to any of these pages from a syllabus.

The whole suite is open source and written in Haskell. If your course uses a different rule set, the checker is small enough to adapt.

There is also a translator between Lemmon-style and Fitch-style proofs, and a short paper on the theory behind it. Translation in one direction turns out to be entirely routine and in the other not, and the reason is worth knowing: a Lemmon line records exactly what it depends on, while a Fitch line’s dependencies are merely bounded by the subproofs around it. If you teach one notation and your colleagues teach the other, the paper says precisely what survives the crossing.