Abstraction Logic

A New Foundation for Reasoning, Computing, and Understanding

Buy now on Amazon as an e-book or in print.
Or from Leanpub or Gumroad DRM-free with future updates included.

🆕 Abstraction Logic: A New Foundation
A Condensed Introduction to Abstraction Logic

🆕 Practal Flyweight
Flyweight Implementation of Abstraction Logic in TypeScript

🆕 Abstraction Logic Is All You Need
Abstraction Logic for Artificial Intelligence Theorem Proving (AITP)
Accepted for Theorem Proving and Machine Learning in the age of LLMs

Do you want a quick start?
Then check out this high-level introduction to abstraction logic, based on the book, presented as a series of five videos.

🔊 Do you want an even quicker start?
Then check out this podcast, automatically generated from the book by AI.

A Conversation with Graham Priest About Abstraction Logic
A conversation about abstraction logic with Claude representing Graham Priest.

Abstraction logic is a new logic combining exceptional simplicity with astonishing generality. It combines the best features of first-order logic and higher-order logic, while avoiding their respective drawbacks. It manages to do that because it is based on a simple understanding of the mathematical universe, its operations, and, in particular, its operators. Abstraction algebra encodes this understanding as a formal language, generalising abstract algebra. It is the right setting for the treatment of alpha equivalence. Abstraction logic then turns abstraction algebra into a logic by considering truth values as a partially ordered substructure of the mathematical universe. A key property of this logic is that formulas are merely terms. Among the presented proof systems are natural deduction, which is sound if truth values form a complete lattice, and sequent calculus, which is sound if truth values form a complete bi-Heyting algebra. By constructing the Rasiowa model, we prove that natural deduction is a complete proof system for abstraction logic.

The following material shows the evolution of Abstraction Logic. It is very much outdated.
For an introduction to Abstraction Logic, read Abstraction Logic: A New Foundation instead.

April 1, 2023 https://arxiv.org/abs/2304.00358 Logic is Algebra

Logic really is just algebra, given one uses the right kind of algebra, and the right kind of logic. The right kind of algebra is abstraction algebra, and the right kind of logic is abstraction logic.

February 5, 2023 https://practal.com/press/aair/1 Axioms Are Inference Rules

As it turns out, Abstraction Logic's axioms should be more general than initially thought. Instead of just terms, they should be inference rules.

July 13, 2022 https://arxiv.org/abs/2207.05610 Abstraction Logic: A New Foundation for (Computer) Mathematics

This was a submission to the CICM 2022 conference.

April 10, 2022 https://doi.org/10.47757/al.crete.1 Video: Abstraction Logic (UNILOG 2022)

This is a rerecording of a talk about Abstraction Logic at the UNILOG 2022 conference in Crete.

March 23, 2022 https://doi.org/10.47757/aal.1 Automating Abstraction Logic

We describe how to automate Abstraction Logic by translating it to the TPTP THF format.

December 21, 2021 (last revised December 23, 2021) https://doi.org/10.47757/pal.2 Philosophy of Abstraction Logic

Abstraction Logic has been introduced in a previous, rather technical article. In this article we take a step back and look at Abstraction Logic from a conceptual point of view. This will make it easier to appreciate the simplicity, elegance, and pragmatism of Abstraction Logic. We will argue that Abstraction Logic is the best logic for serving as a foundation of mathematics.

October 22, 2021 (last revised November 14, 2021) https://doi.org/10.47757/abstraction.logic.2 Abstraction Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of ﬁrst-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that ﬁrst-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between ﬁrst-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.