Proof Workspace
| # | Expression | Rule | Ref |
|---|
∴
Add premises in the sidebar, then start building your proof.
Use the rule buttons to derive new lines.
| # | Expression | Rule | Ref |
|---|
∴
Add premises in the sidebar, then start building your proof.
Use the rule buttons to derive new lines.
Formal logic is a cornerstone of mathematics, computer science, and philosophy, yet the tools for practicing natural deduction proofs are either desktop applications, academic software, or static PDF exercises. There is no polished, self-contained browser tool that lets you build Fitch-style proofs interactively with real-time validation. Fitch Prover fills that gap: a focused, zero-dependency proof builder that runs entirely in the browser.
Fitch Prover is an interactive natural deduction proof builder using the Fitch-style calculus for propositional logic. You define premises and a goal, then construct a formal proof line by line by applying inference rules. Each line you derive must cite the rule used and the line numbers it depends on. The tool validates your proof in real time, highlights errors, and provides hints when you're stuck. It supports all standard propositional rules including subproofs for conditional proof (→I), reductio ad absurdum (RAA), and excluded middle (∨E).
The proof is a tree of lines, each containing a proposition, a rule label, and references to supporting lines. The parser tokenizes each proposition, builds an abstract syntax tree (AST) using recursive descent parsing with standard operator precedence, and then the validation engine walks the proof top-down:
The hint engine searches for applicable rules to the current selection and suggests the next most productive line to add.
A → B, A). Click "+ Add" to add more.