This is only the beginning of our journey into abstraction logic. The goal has always been to create a new foundation for reasoning, computing and understanding—one that aligns better with the way mathematics is practised than current standards such as first-order logic or type theory. So far things are looking good, but there is much work ahead, and much to explore. Let us conclude this chapter by briefly discussing a few important points. Mathematical Freedom. Abstraction logic does not limit your mathematical freedom in any way. You can discuss anything under the sun—or rather, anything possibly living in a mathematical universe. Your mathematical objects can mix and mingle as much as they like, but you can also introduce disciplined and conservative ways of constructing new mathematical objects. To manage your mathematical objects, you can introduce any abstraction you like. For example, it is easy to deal with undefinedness: mathematical objects such as Error can be introduced, different from false but logically equivalent. No static type system needs to be pacified for this to work; the mathematical expression of situations in which no error can occur remains unaffected and uncluttered. Both Logic and Logical Framework. This is because abstraction logic serves as both a logic and a logical framework. The logic has a clear and simple semantics. It is at the same time minimal yet so powerful that we can prove a completeness theorem for natural deduction without assuming any concrete abstractions. This might be particularly interesting for fields such as algebraic specification, which have invented notions such as institutions to cope with the sheer variety of different useful logics that have resisted a unifying foundation so far. It is possible that abstraction logic is that foundation that has been evasive for so long, making notions such as ‘logical framework’ obsolete. However, it is important to acknowledge that abstraction logic is the spiritual child of one such framework: Isabelle/Isar [26, 27, 28]. Isabelle is also both a logic and a framework, and therefore there are many parallels between Isabelle’s logic Pure [29], which is intuitionistic higher-order logic, and abstraction logic. The difference is that Pure is rooted in type theory and thus proof theory, offering only complicated semantic accounts [30] of its logic, while the meaning of abstraction logic is clear and simple. Hilbert-Style Natural Deduction. Abstraction logic unifies not only different kinds of logic but also different approaches to logic. It is a Hilbert-style system based on a few fixed inference rules and an arbitrary collection of axioms. But these axioms transcend the usual notion of an axiom, and are in fact also rules or even sequents. This means that natural deduction and also sequent calculus are integral to abstraction logic, unifying aspects of both model-theoretic and proof-theoretic approaches to logic. Paraconsistency. Paraconsistent logics seem at first to be at odds with abstraction logic, as there is only one value true representing truth in abstraction logic, the top element of the logical order. There are paraconsistent logics such as Graham Priest’s Logic of Paradox [25] which have multiple logical values designated as being true. Amine Chaieb pointed out early that this does not have to be a problem, as there can be a hard truth coexisting with other soft truth values. And indeed, this can be modelled in abstraction logic by using a logical order consisting of the ordinary two-valued Boolean algebra {true,false}, a universe {true, both, false}, and a logical mapping that assigns true to both true and both. Philosophical Considerations. The example of paraconsistency shows that supposedly high-brow aspects of logic turn out to be quite simple in abstraction logic. This is not a coincidence. Abstraction logic is based on a simple conceptualisation of the mathematical universe, its operations and operators. It is hard to imagine a simpler foundation that still respects Cantor’s theorem. But even to describe this simple foundation, we need to presuppose things like collections, to describe the mathematical universe, and functions, to describe operations and operators. Philosophically, our approach is Platonic. We can talk about basic concepts such as collections and functions without defining them because they are part of a mathematical reality we just tap into, rather than invent. While we reject paraconsistency and intuitionism from a philosophical point of view, they are perfectly valid and useful mathematical concepts that can be explained naturally within the framework of abstraction logic. Figure 3.15, Classifying Logics Along Two Dimensions: First-order logic has one mathematical universe and no general binders. Second-order logic has one mathematical universe and no general binders. Higher-order logic does not have one mathematical universe, but has general binders. Abstraction logic has both one mathematical universe, and general binders. Standard and Non-Standard. Another example of how abstraction logic crystallises difficult concepts is that of standard versus non-standard models. According to Hintikka [31], the distinction between standard and non-standard models was first explicitly formulated by Henkin in 1950, in the context of higher-order logic, and represented a watershed in the foundations of mathematics. In abstraction logic, valuation spaces are a simple concept that elegantly captures the essence of this distinction. They make it possible for natural deduction to be complete yet capable of expressing rules such as natural induction succinctly: A[0] x. A[x] ==> A[x+1] ------------------------ A[x] In standard models, the variable A varies over all possible unary operations on the mathematical universe, while in non-standard models which unary operations are covered depends on the valuation space of the model. First-Order and Higher-Order. Logics are usually classified according to their order, such as first-order, second-order or higher-order. First-order logic is the common standard, while second-order and especially higher-order logic have gained popularity due to their practical expressiveness [32] and adjacency to computer languages. First-order logic makes it possible to reason about the entire mathematical universe uniformly, and ZFC set theory takes advantage of that. Higher-order logic cannot do that, but needs to under-approximate the mathematical universe as a tower of typed slices owing to Cantor’s theorem (see Figure 1.2). The advantage of higher-order logic is its general mechanism of variable binding based on the lambda calculus. We call this feature general binders. First-order logic does not have general binders, but only two specific binding mechanisms, universal quantification and existential quantification. We can classify logics along these two dimensions, instead of their order, and Figure 3.15 shows the result. Interestingly, second-order logic is more like first-order logic than higher-order logic in that respect. Furthermore, the result tells us that abstraction logic combines the advantages of first-order logic and higher-order logic while avoiding their weaknesses by scoring in both dimensions. Note that abstraction logic does not achieve general binders via the lambda calculus, as this leads inevitably to a divided mathematical universe. Instead, abstraction logic embraces that operations and operators are not mathematical objects, but need to be represented through a separate mechanism, as illustrated in Figure 1.3. This fusion of a uniform mathematical universe with general binders is powerful, and can be confusing initially. When abstraction logic was first presented at the UNILOG 2022 conference in Crete, an audience member wondered how the formula '∀x. x' could ever mean anything sensible. Lemma 3.21 tells us that its meaning is false. The possibility of defining false like this has been noted as early as 1951 by Church [34], albeit Church let the quantifier range over booleans only. Much later in 2013 Kripke found it remarkable enough to exhibit it in a short note about Fregean first-order logic [33]. Unlike Church, and like us, Kripke lets the quantifier range over the entire universe, which he calls a Fregean domain. Relationship to Established Logics. We have given a self-contained presentation of abstraction logic. What remains to be done is to clarify its relationship to established logics. We have seen that axioms and inference rules for predicate logic (Figure 3.11) are easily encoded in abstraction logic (Figure 3.10), but we have not yet gone beyond acknowledging this surface-level similarity. For example, is our completeness result for natural deduction strong enough to imply the established completeness results for known logics when they are encoded in abstraction logic? Computer Algebra. The algebraic nature of abstraction logic seems particularly well-suited to finally allowing logic to make sizable inroads into computer algebra, which has resisted various such efforts based on conventional logics before. Automation. Much research has been done on automating theorem proving in first-order logic. Significant work has also been done on automating higher-order logic [35]. Automating higher-order logic is more difficult than automating first-order logic, much of which is due to the complications that lambda calculus and type systems bring. It seems that abstraction logic would make a great context in which to study automation, given that neither lambda calculus nor type systems are built into it, yet it integrates both first-order and higher-order aspects. Artificial Intelligence. Beyond conventional techniques for automation, AI has become a hot topic in machine-assisted proof [36]. Of particular interest is autoformalization [37], which means the process of translating informal mathematical prose into formal logic. Abstraction logic seems particularly well suited for autoformalization, as again, no type systems or towers of universes complicate the picture on the logical side.