An interactive proof system for exploring combinatory logic, inspired by Raymond Smullyan’s book To Mock a Mockingbird. Instead of fully automating proofs, this tool allows users to manually construct logical deductions while automating tedious steps like variable substitution.
The system allows step-by-step proof construction, letting users perform logical transformations interactively. It includes partial support for first-order logic, specifically universal (∀) and existential (∃) quantifiers. Expressions can be rewritten by dragging and dropping terms, and users can define custom variable and expression names.
While solving combinatory logic puzzles manually, repetitive steps like term substitution and expression rewriting become tedious. This system helps by automating those mechanical processes while keeping users in control of the logical reasoning.
- For-all elimination: Apply universally quantified statements.
- For-all introduction: Prove a statement for an arbitrary term to generalize it.
- Exists elimination: Introduce a witness variable to remove an existential quantifier.
- Exists introduction: Deduce an existential statement from a concrete example.
- Rewriting: Replace sub-expressions using known equalities.
- Bound variable renaming: Change bound variable names safely.
-
For-all elimination
Drag an expression onto a universal quantifier to apply it:
-
Rewriting
Use a known equation to replace an expression:
-
Exists introduction
Introduce an existential quantifier:
You can try out the system here.
- Support for additional logical connectives:
⇒,∧,∨,¬ - Enhanced user interface (e.g. undo/redo, proof organization tools)