Abstraction Logic

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.

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

This was a submission to the CICM 2022 conference.

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

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

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.

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-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.