Visualizing Proof Theory & Gentzen’s Hauptsatz

Toy Hauptsatz is an interactive, client-side logic engine that visualizes classical propositional logic proofs. It parses formulas into Lisp S-expressions, runs an automated forward-chaining deduction search via a priority queue, and generates step-by-step natural deduction trees. Under the hood, it demonstrates the structural subformula property guaranteed by Gerhard Gentzen’s Cut Elimination Theorem (Hauptsatz), illustrating how proof search spaces are strictly bounded to prevent infinite lemma guessing.