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.
No installation, no backend, no accounts. Declare or define abstractions, state axioms, and prove theorems — all in abstraction logic.
Practal is under active development. Practal Code and Practal Zero will launch here soon.
Practal doesn't lock AI into a chatbox. Instead, Practal Zero syncs with your local theory files. An AI agent like Claude Code works on the same files from the command line — reading your declarations, understanding your goals, and writing proof steps. The work of the AI is checked in the same way as yours is.
This works because abstraction logic is unusually AI-friendly, and therefore no large prior corpus of Practal theories is needed. The barrier to entry for an AI is as low as it is for a human.
Live file sync requires Chrome (File System Access API). Other browsers can use Practal Zero as a standalone editor with 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 Code is open source, and Practal Zero is free.
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.
Practal is built in layers. Practal Code is open source and free for anyone to use, embed and build on. Practal Zero is free to use. The cloud platform adds collaboration and scale.
The abstraction logic kernel. Processes theory files from the command line. Designed to be embedded in editors, CI pipelines, and AI agent workflows.
A browser-based proof assistant with a structured block editor. Syncs with local theory files so you can work alongside AI agents like Claude Code in real time.
A collaborative platform for teams and institutions. Shared theory libraries, persistent workspaces, and AI-assisted proving without local setup.
Papers, releases, notes, and project milestones.
Check back soon, or subscribe via RSS.
Practal is an independently funded project. The logic is open, Practal Code is open source, and Practal Zero is free. If you find the ideas compelling, you can support continued development through GitHub Sponsors. Every contribution helps move the work forward.