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 the first public Practal preview. No installation, no backend, no accounts. Declare or define abstractions, state axioms, and work with checked theories — all in abstraction logic.
This first version is deliberately local and simple. AI integration, live file sync, and collaborative cloud features are planned for later.
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.
The current Practal Zero preview does not include AI integration or live file sync. The longer-term design is still file-centered: an AI agent should work on the same theory files as you, and every generated proof step should be checked in the same way as your own work.
This direction is promising because abstraction logic is designed to be explicit and regular. The goal is to make the barrier to entry for an AI as low as it is for a human.
For now, use Practal Zero as a standalone browser workspace with local browser storage and manual import/export.
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 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.
Practal is built in layers. The public release available now is Practal Zero, a free browser preview. Practal Code, editor integrations, AI-assisted workflows, and Practal Cloud are still under development.
The local kernel and tooling layer behind Practal. It is being used to build the current system, but it is not a public product or open-source release yet.
A browser-based Practal workspace with a structured block editor and checked theories. The first public preview is intentionally simple and local.
The future cloud platform for teams and institutions. Shared theory libraries, persistent workspaces, collaboration, and managed AI support 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.