Abstraction logic unifies the single mathematical universe of first-order logic with the general variable binding of higher-order logics — yielding a complete logic with elementary semantics. Practal is the proof assistant that brings it to life.
Practal Zero is a theorem proving system for abstraction logic. Open it directly in your browser without any installation. There is no backend and no account.
Zero starts with a small introduction document so the workspace opens quickly. Larger example theories are available as a separate download for import/export experiments.
Zero can also be installed on your desktop (as a PWA, progressive web app). This works best with Chrome, but also with Safari on newer versions of macOS.
Traditional logics force a choice. First-order logic gives you a single universe of mathematical objects but no way to bind variables beyond simple quantification. Higher-order logics give you general variable binding but split the universe into an infinite tower of types. Abstraction logic refuses the trade-off.
| Logic | Single Universe | General Binders |
|---|---|---|
| First-Order | Yes | No |
| Second-Order | No | No |
| Higher-Order | No | Yes |
| Abstraction | Yes | Yes |
The key insight is that just like in first-order logic, but unlike in higher-order logic, operations need not be mathematical objects. An operation takes values from the universe and returns a value. Crucially, an operator takes operations and returns a value. This avoids inconsistency by sidestepping Cantor's theorem without sacrificing expressiveness. The resulting semantics is elementary and based on abstraction algebras with a logical order and a valuation space.
Classical, intuitionistic, modal, paraconsistent and quantum logics; lambda calculus; dependent type theory; algebraic effects — these are all expressible as abstraction logics.
Every abstraction logic based only on pure deduction is complete with respect to general models, and even with respect to classical models.
The syntax and semantics of abstraction logic are simple and elementary. This gives working with it a similar feel as computer algebra.
The logic is open and welcomes scrutiny. Practal Zero runs locally and is free to use, and deeper local tooling is being prepared.
In abstraction logic, you don't switch systems to work with a different logic. Abstraction logic can adapt to many different logical paradigms and fits many mathematical situations. You declare or define abstractions, state axioms as needed, and reason within the resulting theory. There is no distinction between logical and mathematical constants, everything is just an abstraction.
The larger example library is available as a ZIP instead of being loaded into every fresh Practal Zero workspace. Import it when you want to explore substantial theories or try Zero's import/export workflow.
The public release available now is Practal Zero, a free theorem proving system that runs locally in your browser.
The local kernel and tooling layer behind Practal. It is being used to build the current system, but it is not a public product yet.
A theorem proving system with a structured block editor and checked theories. Run it locally in your browser, or install it as a desktop progressive web app.
The future cloud platform for teams and institutions. Shared theory libraries, persistent workspaces, collaboration, and team administration belong here later.
Latest work and blog posts. Check back soon, or subscribe via RSS.
Practal is an independently funded project. The logic is open, and Practal Zero is free to use. If you find the ideas compelling, you can support continued development through GitHub Sponsors. Every contribution helps move the work forward.