[JFrusher]

Stacked on #4. Implements Phase 3 of ROADMAP.md.

• docs/spec/proofs.md: how each kind of justification is checked, proof structure, and the full rule catalogue.
• Logic core: α-equivalence, capture-avoiding substitution with β-reduction for property variables, instance matching, definition expansion.
• Truth tables decide unjustified propositional inferences and print a counterexample when one fails, e.g. C does not follow from P1, P2: counterexample A = false, B = true.
• Natural-deduction checker: scopes, citing closed subproofs, fresh-name conditions, strict box { } subproofs that only admit fully modalized formulas, and by rule as a one-step proof.
• The Aquinas example now has complete first-order proofs. Mutation-tested: five deliberate breakages are each caught with a specific message.
• 39 textbook exercises (propositional, first-order, identity, modal K/T/4/5, Barcan, definitions, λ-instantiation) plus misuse tests for the rules and proof structure.

Change from the plan: the checker already covers the full rule set (quantifiers, identity, S5, property variables). The Aquinas example needs quantifier rules to pass at all, and the substitution machinery is shared. Phase 5 now focuses on sort/type checking and the library formalizations. Recorded in the roadmap.

Also found and fixed in this phase:

• A subproof that opens with a nested subproof was wrongly rejected.
• Recursive definitions would make expansion loop forever; the validator now rejects them.

The parser fuzzer ran 206k inputs through the checker without crashes.

---

Generated by Claude Code

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 770718c5-fc21-4cc6-abe8-353546c83d46

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}