Paperweight implementation of abstraction logic in TypeScript for experimenting with abstraction logic in practice.
See the paper at https://doi.org/10.5281/zenodo.18717799. Paperweight is described in Section 3.7.
Automation is currently non-existent, but using Claude Code and/or Codex you can already partially remedy that and turn it into an actual interactive theorem proving assistant (make it read the paper first). That is how many of the theories below have been created.
To install, run npm install.
You can run each theory, for example: npm run Implication.
- Example-6
- Example-13
- Implication
- Pure-Equality
- Equality
- Negation
- Universal
- Positive-Logic
- Minimal-Logic
- Intuitionistic-Predicate-Logic
- Classical-Predicate-Logic
- Peano
- Peano-Recursion
- Peano-Theorems
- Dependent-Types
- Lambda-Calculus
- Inconsistent-Lambda-Calculus
- Category-Theory
- Paraconsistent-Logic
- S4
- Kripke-S4
- Quantum
- Algebraic-Effects