# Philosophy of Abstraction Logic

Cite as: https://doi.org/10.47757/pal.2
December 23rd, 2021
Abstract
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.

## Introduction

How can we do mathematics on a computer?
This question is bound to evoke a wide variety of responses. Many will ﬁnd the question somewhat silly and point out that a computer easily handles mathematics, for example via a calculator app. Others will question whether mathematics can be done on a computer at all, because mathematics is a social process happening within the mathematical community.
As has become abundantly clear in the last two decades, computers can support and facilitate social processes, for good and bad. This aspect of mathematics does not seem to be an unsurmountable obstacle to its computerisation. Attempts like the ProofPeer  project have been made to overcome this obstacle, but so far none of these attempts have been truly successful.
A central and maybe the most important aspect of mathematical activity is the formulation and proving of theorems. How can we do this on a computer, beyond just writing it up in TeX ?
In principle, this question has been answered. We can do it by using logic as a foundation of mathematics. Logic can be implemented via software (and/or hardware), and we can then use this logic to formulate and prove theorems. A large-scale example of this is the formal proof of the Kepler conjecture .

### What is Logic?

To allow the formulation of theorems, logic must provide a language in which to express these theorems. To make proofs of theorems possible, logic must clearly explain what a proof is, and how to certify that something is a proof of a given theorem.
There is no consensus on whether there is a single best logic to use as a foundation of mathematics. There are many different logics, and they differ in how (much) mathematics can be expressed in them. For example, the formal proof of the Kepler conjecture uses simply-typed higher-order logic (HOL) .
On one end of the spectrum one can ﬁnd the opinion that there cannot be a single best logic, and that the best we can do is to develop methods  which exploit commonalities among the plethora of logics.
On the other end of the spectrum there is the opinion, championed by Quine , that ﬁrst-order logic (FOL) is the proper foundation of mathematics. In Quine’s opinion, there is a more or less clear boundary between logic and mathematics, and other logics than FOL are not really logic, but simply mathematics dressed up as logic. He considers second-order logic (SOL) just as another way of formulating set theory, which in his opinion does not qualify as logic, but as mathematics.
Indeed, following Quine one can ask, what is the difference between logic and mathematics?
This article argues that the answer to this question is the key to understanding that there indeed is a best logic for serving as a foundation of mathematics.
The short answer is: There is a border between logic and mathematics, but it is not ﬁxed in one place, and it can be moved. Moving the border to the right incorporates more and more speciﬁc mathematics into the logic. Because there are many different mathematical theories that can potentially be turned into logics, moving the border to the right leads to a branching out into many different logics. On the other hand, moving the border to the left reverses the effect of branching out, and leads to a single logic at the root, which we call Abstraction Logic (AL).
AL is therefore the simplest of all logics that can serve as a foundation of mathematics. At the same time, it is also the most universal one, as all other logics to the right of it can be represented in it as mathematical theories. This is why we proclaim AL to be the best foundational logic.

## Calculator Logic

We have speculated earlier that many people will associate mathematics foremost with calculation.
Although this is of course a narrow view of mathematics, it is at the same time surprisingly general: Each term in the language of an AL can be viewed as a calculation, if one is prepared to understand the notion of calculation in a broad enough sense.
Consider the following simple logic which we will call Calculator Logic (CL). A term in CL is either a decimal literal denoting natural numbers, like $42$ or $0$, or an equality $a = b$, an addition $a + b$, a subtraction $a - b$, unary minus $-a$, a multiplication $a \times b$, or a division $a \div b$, where both $a$ and $b$ are terms. We use the usual rules of precedence, and brackets $(a)$ to override them.
The language of CL then consists of all of these terms. The theorems of CL are those terms of CL that evaluate to true. A proof of a theorem $A$ consists of evaluating $A$ and certifying that the result is true.
Therefore $300 - (42 + 8) \times 2 = -(1000 \div (-5))$ is certainly a theorem, and $0 = 1$ is not. The term $6 \times 7$ is not a theorem, because it evaluates to $42$ instead of true.
We deﬁne $x \div y$ to be the unique integer $z$ such that $x = y \times z$. If no such integer exists, or is not unique, then the result of a division will fail. This is the case for the expression $1 \div 0$, which fails, and is deﬁnitely not true. Therefore $1 \div 0$ is not a theorem. But what about $1 \div 0 = 0 \div 0$? Or $1 \div 0 = 7 \div 5$? And $8 \div 5 = 7 \div 5$? Are these theorems? Both the left-hand side and the right hand side of these equalities fail, and we decide that fail $=$ fail actually evaluates to true. Thus all three equalities are theorems in CL.
What about the term $(5 = 2 + 2) = 4$? Is that a theorem? No, it is not, because the left-hand side $(5 = 2 + 2)$ evaluates to false, and false is not equal to $4$.
We have been quite pragmatic about the results true, false and fail. We treated them as normal values that can occur during or as the result of a calculation. We could just as well expand the deﬁnition of CL terms by introducing dedicated terms for these values: $\top$ for true, $\bot$ for false, and $\Finv$ for fail. This would yield new theorems like $1 \div 0 = \Finv$ and $(5 = 2 + 2) = \bot$. It also allows terms like $2 + \top$. This is a term that does not seem to make much sense, so we decide that evaluating it fails and yields the theorem $2 + \top = \Finv$. Note that adding the terms $\top$, $\bot$ and $\Finv$ to CL does not create any issues that were not already inherent in our approach: $2 + (3 = 3)$ also fails.
CL is not an abstraction logic, as it does not feature variables, for example. But as we will see later , it can easily be embedded into an AL such that the terms of CL correspond to a subset of the terms of the AL, and such that a term in CL is a theorem if and only if the corresponding term in AL is a theorem.
Some will recoil with horror from CL as presented here. They will say, surely something like $2 + (3 = 3)$ should not be allowed to count as a term in the ﬁrst place? The situation bears obvious similarity with the division of programming language camps into proponents of dynamically typed programming languages like Lisp vs. proponents of statically typed programming languages like ML.
But there is a fundamental difference. While in programming languages static types serve as important safe guards against programming errors, in a logic there already is an ultimate safe guard and arbiter of truth: The theorem.
This obvious fact has been twisted in a rather ingenious way by declaring types to be the same as theorems . While this is certainly a viable way of approaching logic, it is by no means the only one, or even a very natural one, for that matter. Instead, using abstraction logic one can consider types as a useful mathematical theory , just like set theory, instead of hard-wiring types into the logic.

## Values, Operations, Operators

Abstraction logic presumes that all values we want to calculate with and reason about live in a single universe $\mathcal{U}$. This is the same assumption that ﬁrst-order logic makes. Unlike FOL, abstraction logic makes the additional assumption that there also is a value true in $\mathcal{U}$. Apart from this, AL makes no a-priori demands on $\mathcal{U}$.
The assumption that there is a single universe is an important reason why AL is conceptually so simple. Any value can in principle be combined with any other value without any a-priori restrictions. This is also what makes set theory so attractive, but unlike set theory, abstraction logic has no ontological presuppositions other than that $\mathcal{U}$ must contain true.
Values are combined via operations and operators.
An $n$-ary operation (of $\mathcal{U}$) is a function taking $n$ arguments where each argument is a value in $\mathcal{U}$, and returning a result that again is a value in $\mathcal{U}$.
An $n$-ary operator (of $\mathcal{U}$) is a function taking $n$ arguments where each argument is either a value or an $m$-ary operation, depending on the argument position; $m$ is ﬁxed for a given position. The result of applying an operator is still always a value.
We consider any value to also be an $0$-ary operation, and any $n$-ary operation to also be an $n$-ary operator. If we want to emphasise that an operation is not a value we call that operation proper. Similarly, we call an operator proper if it is not an operation.
Note that proper operations and operators are not part of the universe. There are simply too many of them for this to be the case if $\mathcal{U}$ contains more than one value, as we know due to Cantor’s theorem. Therefore all attempts to include all operations and/or all operators in the universe are doomed.
A most important difference between abstraction logic and ﬁrst-order logic is that while FOL only considers arbitrary operations (in the form of functions and relations), AL also allows the use of arbitrary operators. The only proper operators allowed in FOL are $\forall$ and $\exists$.

## Abstraction and Shape

An abstraction is a name, intended to denote an operator. A signature is a collection of abstractions, where each abstraction is associated with a shape. A shape encodes both what kind of operator an abstraction can possibly denote, and how to interpret a term formed by applying the abstraction.
In general, a shape has the form $(m; p_0, \ldots, p_{n-1})$ where $m$ is the valence and $n$ the arity of the shape. The $p_i$ are subsets of $\{0, \ldots, m-1\}$. To avoid degenerate cases, we demand that the union of all $p_i$ must equal $\{0, \ldots, m-1\}$.
We say that the operator $o$ is compatible with the shape $(m; p_0, \ldots, p_{n-1})$ in all of these cases:
• The arity $n$ is zero (which implies $m = 0$, because we excluded degenerate shapes) and $o$ is a value.
• The valence $m$ is zero, the arity $n$ is non-zero, and $o$ is an $n$-ary operation. Note that $o$ is then necessarily a proper operation.
• The valence $m$ is non-zero (which implies $n > 0$) and $o$ is an $n$-ary operator, such that $o$ accepts in argument position $i$ a ${|{p_i}|}$-ary operation. Here ${|{p_i}|}$ is the size of $p_i$. Note that $o$ is then necessarily a proper operator.
In all other cases $o$ is not compatible with the shape.
Because degenerate shapes are excluded, a value is only compatible with shape $(0;)$, a unary operation must have shape $(0; \emptyset)$, a binary operation must have shape $(0; \emptyset, \emptyset)$, and a proper unary operator necessarily has shape $(1; \{0\})$.
An abstraction can only denote operators that are compatible with its shape.

## Syntax

We assume an inﬁnite pool $X$ of variables.
A term, relative to a given signature, is either a variable application or an abstraction application.
A variable application has the form $x[t_0, \ldots, t_{n-1}]$ where $x$ is a variable, and the $t_i$ are themselves terms. Instead of $x[]$ we usually just write $x$. We say that $x$ occurs with arity $n$.
An abstraction application has the form $(a\, x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ where $a$ is an abstraction belonging to the signature, $m$ is the valence of $a$, and $n$ is the arity of $a$. The $t_i$ are the terms to which the abstraction is being applied. The $x_j$ are distinct variables.
Often, instead of $(a.)$ we just write $a$, instead of $(a.\, s\, t)$ we write $s\, a\, t$ when appropriate, and instead of $(a.\, t)$ we might write $a\, t$ or $t\, a$, depending on whether we consider $a$ to be a preﬁx or postﬁx unary operator. In these cases we might disambiguate via brackets $(\ldots)$ and the usual assumptions about associativity and precedence.
We consider the arity with which a variable occurs to be an implicit part of the variable name. This means that the two occurrences of the variable $x$ in $x[x]$ actually refer to two different variables. We could emphasise this by writing $x^1[x^0]$ instead, but we choose the simpler syntax, as no ambiguities can arise. Because of this convention, we do not need to distinguish between wellformed terms and non-wellformed terms. As long as abstraction applications use the correct arity and valence according to the signature, all terms are automatically wellformed.

## Logic

A logic signature is a signature $\mathfrak{S}$ that contains at least three abstractions:
• The abstraction $\top$, intended to denote a value.
• The abstraction $⇒$, intended to denote a binary operation.
• The abstraction $\forall$, intended to denote a proper unary operator.
An abstraction logic is a logic signature $\mathfrak{S}$ together with a list ${\mathbb{A}}$ of terms called axioms.
Obviously, $\top$ represents the value true, $⇒$ is implication, and $\forall$ stands for universal quantiﬁcation.
A signature $\mathfrak{S}'$ extends a signature $\mathfrak{S}$ if every abstraction of $\mathfrak{S}$ is also an abstraction of $\mathfrak{S}'$, and has the same shape in both $\mathfrak{S}$ and $\mathfrak{S}'$.
An abstraction logic ${\mathcal{L}}'$ extends an abstraction logic ${\mathcal{L}}$ if the signature of ${\mathcal{L}}'$ extends the signature of ${\mathcal{L}}$, and if every axiom of ${\mathcal{L}}$ is also an axiom of ${\mathcal{L}}'$ (modulo $\alpha$-equivalence ).

## Several Abstraction Logics

Deduction Logic ${\mathcal{L}}_D$ has signature $\mathfrak{S}_D$ consisting of the minimally required three abstractions, and the following axioms ${\mathbb{A}}_D$:
1. $⊤$
2. $A ⇒ (B ⇒ A)$
3. $(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))$
4. $(∀ x.\,A[x]) ⇒ A[x]$
5. $(∀ x.\,A ⇒ B[x]) ⇒ (A ⇒ (∀ x.\, B[x]))$
The relevance of ${\mathcal{L}}_D$ is founded in the Deduction Theorem .
Axioms 2 to 5 might surprise despite their familiar form, because one would expect them to apply only to truth values, not every value in the entire universe. But because abstraction logic has only a single universe $\mathcal{U}$, every value must also be considered to be a truth value, because for any term $t$ one can ask the question: Is $t$ true?
Deduction Logic with Equality ${\mathcal{L}}_E$ extends ${\mathcal{L}}_D$. It has signature $\mathfrak{S}_E$ which extends $\mathfrak{S}_D$ by adding the equality abstraction $=$. It has axioms ${\mathbb{A}}_E$, adding the following axioms to ${\mathbb{A}}_D$:
1. $x = x$
2. $x = y ⇒ (A[x] ⇒ A[y])$
3. $A ⇒ (A = ⊤)$
${\mathcal{L}}_E$ is arguably the most important abstraction logic from a theoretical point of view. We will show that every abstraction logic extending ${\mathcal{L}}_E$ is complete .
Deduction Logic with Equality and Falsity ${\mathcal{L}}_F$ extends ${\mathcal{L}}_E$. Its signature $\mathfrak{S}_F$ extends $\mathfrak{S}_E$ by adding $\bot$, denoting false, logical negation $¬$, and inequality $≠$. Its axioms ${\mathbb{A}}_F$ add the following axioms to ${\mathbb{A}}_E$:
1. $⊥ = (∀ x.\, x)$
2. $¬ A = (A ⇒ ⊥)$
3. $(x ≠ y) = ¬(x = y)$
The possibility of deﬁning $\bot$ like this has been noted as early as 1951 by Church , albeit Church let the quantiﬁer range over booleans only. Much later in 2013 Kripke found it remarkable enough to exhibit it in a short note about Fregean Quantiﬁcation Theory . Unlike Church, and like us, Kripke lets the quantiﬁer range over the entire universe, which he calls a Fregean domain.
Intuitionistic Logic ${\mathcal{L}}_I$ extends ${\mathcal{L}}_F$. Its signature $\mathfrak{S}_I$ adds abstractions to $\mathfrak{S}_F$ for conjunction $∧$, disjunction $∨$, equivalence $\Leftrightarrow$ and existential quantiﬁcation $∃$. Its axioms ${\mathbb{A}}_I$ are obtained by adding the following axioms to ${\mathbb{A}}_F$:
1. $(A ∧ B) ⇒ A$
2. $(A ∧ B) ⇒ B$
3. $A ⇒ (B ⇒ (A ∧ B))$
4. $A ⇒ (A ∨ B)$
5. $B ⇒ (A ∨ B)$
6. $(A ∨ B) ⇒ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ C))$
7. $(A \Leftrightarrow B) = ((A ⇒ B) ∧ (B ⇒ A))$
8. $A[x] ⇒ (∃ x.\, A[x])$
9. $(∃ x.\, A[x]) ⇒ ((∀ x.\, A[x] ⇒ B) ⇒ B)$
Classical Logic ${\mathcal{L}}_K$ extends ${\mathcal{L}}_I$ with the law of the excluded middle:
1. $A ∨ ¬ A$

## Calculator Logic as an AL

Let us explore how Calculator Logic can be represented as an AL. Our starting point is ${\mathcal{L}}_K$. We follow an axiomatisation of arithmetic  described by Wang.

### Primitive Abstractions

Here is the list of primitive CL abstractions we add:
$\begin{array}{c|c} {\includegraphics[height=0.5em]{344FBFC4-5DC4-47C7-9682-7F00BE54FCD6}} & {\includegraphics[height=0.5em]{874C7733-3CF7-47F8-9E3F-E5A3B4826256}} \\\hline 0 & {\includegraphics[height=0.5em]{CCCE03B1-F6B6-40F9-84CF-6954E1F30F52}} \\ 1 & {\includegraphics[height=0.5em]{19960BAC-46F8-4FC2-82A5-5C054EFD6B8C}} \\ x + y & {\includegraphics[height=0.5em]{89F41138-F4FB-41B0-BC48-70B32CCE65FC}} \\ x - y & {\includegraphics[height=0.5em]{ED8BF189-550D-4C67-BF0F-F32403E3962D}} \\ - x & {\includegraphics[height=0.5em]{1313AF99-D435-4C25-AB7D-B285F94D338F}} \\ x \times y & {\includegraphics[height=0.5em]{CFFF785E-DE4F-4C5A-8A5F-0FA12C817CDC}} \\ x \div y & {\includegraphics[height=0.5em]{C0474A45-113E-45F5-9C40-7EB2A6E0D7BD}} \\ (\text{Num}.\, x) & x\ {\includegraphics[height=0.5em]{98184A52-C7C8-4940-9296-77299396D831}} \\ (\text{Pos}.\, x) & x\ {\includegraphics[height=0.5em]{BA33B9F3-5B96-4605-936F-DF5D0EB80FEC}} \\ \end{array}$
Note that as long as abstractions have different arities and/or valence, as subtraction and minus do, they can share the same symbol and still be told apart. Just as we do for variables, we treat valence and arity of an abstraction as part of its name.

### Deﬁnitions

We add derived CL abstractions via deﬁnitions  of the form $A ≝ B$, where $A$ is an application of an abstraction $a$. This introduces $a$ as an abstraction, and adds $A = B$ to the list of axioms. The shape of $a$ will be obvious from the structure of $A$.
$\begin{array}{rcl} (\text{Num}.\, x\, y) & ≝ & (\text{Num}.\, {x}) ∧ (\text{Num}.\, {y}) \\ (\text{Num}.\, x\,y\, z) & ≝ & (\text{Num}.\, {x}) ∧ (\text{Num}.\, {y}) ∧ (\text{Num}.\, {z})\\ (\operatorname{closed} x.\, D[x]\, F[x]) & ≝ & (\forall x.\, D[x] ⇒ D[F[x]]) \\ (\operatorname{closed} x \,y.\, D[x]\, F[x, y]) & ≝ & (\forall x\, y.\, D[x] ∧ D[y] ⇒ D[F[x, y]]) \\ (\operatorname{comm} x \,y.\, F[x, y]) & ≝ & (\forall x\, y.\, (\text{Num}.\, x\, y) ⇒ F[x, y] = F[y, x]) \\ (\operatorname{assoc} x \,y.\, F[x, y]) & ≝ & (\forall x\, y\, z.\, (\text{Num}.\, x\,y\, z) ⇒ \\ & & \phantom{(\forall}F[x, F[y, z]] = F[F[x, y], z]) \\ (\operatorname{distr} x \,y.\, F[x, y]\, G[x, y]) & ≝ & (\forall x\, y\, z.\, (\text{Num}.\, x\,y\, z) ⇒ \\ & & \phantom{(\forall}F[G[x, y], G[x, z]] = G[x, F[y, z]]) \\ (\operatorname{right-neutral} x\,y.\, F[x,y]\, e) & ≝ & (\text{Num}.\, e)\ ∧ \\ & & (\forall x.\, (\text{Num}.\, x) ⇒ F[x, e] = x) \\ (\text{either-or}.\, A\, B\, C) & ≝ & (A ∨ B ∨ C)\, ∧ \\ & & ¬(A ∧ B) ∧ ¬(A ∧ C) ∧ ¬(B ∧ C) \end{array}$

### Literals

The purpose of the following deﬁnitions is to support decimal literals of integers: $\begin{array}{rcl} 2 & ≝ & 1 + 1 \\ 3 & ≝ & 2 + 1 \\ 4 & ≝ & 3 + 1 \\ 5 & ≝ & 4 + 1 \\ 6 & ≝ & 5 + 1 \\ 7 & ≝ & 6 + 1 \\ 8 & ≝ & 7 + 1 \\ 9 & ≝ & 8 + 1 \\ (\text{dec}.\, x\, y) & ≝ & (9 + 1) \times x + y \end{array}$ E.g. the literal $57104$ can then be understood as syntactic sugar for $(\text{dec}.\, {(\text{dec}.\, {(\text{dec}.\, {(\text{dec}.\, 5\, 7)}\, 1)}\, 0)}\, 4)$

### Axioms

The remaining axioms of CL are:
• $(\operatorname{right-neutral}\, x\, y.\, (x + y)\, 0)$
• $(\operatorname{right-neutral}\, x\, y.\, (x \times y)\, 1)$
• $(\operatorname{closed}\,x\,y.\, (\text{Num}.\, x)\, (x + y))$
• $(\operatorname{closed}\,x\,y.\, (\text{Num}.\, x)\, (x \times y))$
• $(\operatorname{closed}\,x.\, (\text{Num}.\, x)\, (- x))$
• $(\operatorname{comm}\, x\, y.\, x + y)$
• $(\operatorname{assoc}\, x\, y.\, x + y)$
• $(\operatorname{comm}\, x\, y.\, x \times y)$
• $(\operatorname{assoc}\, x\, y.\, x \times y)$
• $(\operatorname{distr}\, x\, y.\, (x + y)\, (x \times y))$
• $(\text{Num}.\, x\, y) ⇒ x - y = x + (-y)$
• $(\text{Num}.\, x\,y\, z)⇒ y ≠ 0 ⇒ (x \div y = z) = (x = z \times y)$
• $(\text{Num}.\, x) ⇒ x - x = 0$
• $(\text{Num}.\, x\,y\, z) ⇒ z ≠ 0 ⇒ z \times x = z \times y ⇒ x = y$
• $(\operatorname{closed}\,x\,y.\, (\text{Pos}.\, x)\, (x + y))$
• $(\operatorname{closed}\,x\,y.\, (\text{Pos}.\, x)\, (x \times y))$
• $(\text{Num}.\, x) ⇒ (\text{either-or}.\, (\text{Pos}.\, x)\, (x = 0)\, (\text{Pos}.\, {-x}))$
• $A ⇒ (\forall x.\, A[x] ⇒ A[x + 1]) ⇒ (\text{Pos}.\, x) ⇒ A[x]$
The last axiom is the axiom of induction. It can be represented in AL effortlessly.

### Undeﬁnedness

The axioms we have introduced so far cover the standard behaviour of arithmetic, but do not say anything about terms like $2 + \top$ or $1 \div 0$. This can be an advantage, because it means the theorems proven for this abstraction logic are applicable in more contexts. For example, there might be a context in which we would want $1 \div 0 = \infty$ to hold. Or maybe we would prefer to leave division by zero mostly unspeciﬁed except for requiring $(\text{Num}.\, x) ⇒ (\text{Num}.\, {x \div 0})$. Therefore, we might want to leave terms like this undeﬁned on purpose.
The disadvantage of undeﬁned terms is that we cannot use theorems to prove that they are undeﬁned; this is because they are undeﬁned, and we cannot say much about them. This is where type systems shine: many undeﬁned terms are automatically rejected because type checking has proven that the term is illtyped.
To emulate this feature of type systems, we would like to be able to prove a theorem of the form “$t$ is undeﬁned”. We cannot really do that, as explained before. But we can arrange things so that we can prove a theorem of the form “$t$ is an error”. Simplifying further, we decide that there is a single error fail, which we denote by $\Finv$. We can then show that $t$ fails by proving the theorem $t = \Finv$.
We introduce the following tools to deal with errors:
• Abstraction “$\Finv$” is added, denoting a value.
• $(\operatorname{domain-bound} x.\, D[x]\, F[x]) ≝ (\forall x.\, ¬ D[x] ⇒ F[x] = \Finv)$
• $(\operatorname{domain-bound} x\, y.\, D[x]\, F[x, y]) ≝ (\forall x\, y.\, ¬ (D[x] ∧ D[y]) ⇒ F[x, y] = \Finv)$
• $(\exists_1 x.\, A[x]) ≝ (∃ x.\, A[x] ∧ (\forall y.\, A[y] ⇒ x = y))$
• Abstraction “$\operatorname{the}$” is added, denoting a proper unary operator.
• $(\exists_1 x.\, A[x]) ⇒ A[x] ⇒ (\operatorname{the} x.\, A[x]) = x$
• $¬ (\exists_1 x.\, A[x]) ⇒ (\operatorname{the} x.\, A[x]) = \Finv$
With these, we make the following changes to CL:
• $(\text{either-or}.\ ((x = \top) ∨ (x = \bot))\, (\text{Num}.\, x) \,(x = \Finv))$
• $(\operatorname{domain-bound} x\, y.\, (\text{Num}.\, x)\, (x + y))$
• $(\operatorname{domain-bound} x.\, (\text{Num}.\, x)\, (- x))$
• $(\operatorname{domain-bound} x\, y.\, (\text{Num}.\, x)\, (x \times y))$
• We drop the previous axiom governing division.
• $x \div y = (\operatorname{the} z.\, (x = z \times y))$
This says that the only values in the universe are booleans, numbers, and fail. Furthermore, all arithmetical operations fail if not applied to numbers. Division fails if it is not uniquely determined.
Farmer proposes a traditional approach to undeﬁnedness  as a basis for formalising undeﬁnedness. He mentions that undeﬁned could be modelled as a third truth value besides $\top$ and $\bot$, but warns that
[...] it is very unusual in mathematical practice to use truth values beyond true and false. Moreover, the presence of a third truth value makes the logic more complicated to use and implement.
Our approach to undeﬁnedness resolves these issues. There is a third value $\Finv$ with $\Finv ≠ \top$ and $\Finv ≠ \bot$, but logically, it is the same as $\bot$, because we can prove $\Finv \Leftrightarrow \bot$. Furthermore, there is no need to change the implementation of the logic at all, as all we needed were a few additional abstractions and axioms.

## Semantics

A valuation $\nu$ in $\mathcal{U}$ is a function that assigns to each variable $x$ in $X$ occurring with arity $n$ an $n$-ary operation $\nu(x, n)$ of $\mathcal{U}$. Given a valuation $\nu$ in $\mathcal{U}$, distinct variables $x_0, \ldots, x_{k-1}$ and values $u_0, \ldots, u_{k-1}$ in $\mathcal{U}$, we deﬁne an updated valuation via $\nu[x_0 \coloneqq u_0, \ldots, x_{k-1} \coloneqq u_{k-1}](y, n) = \begin{cases}u_i & \text{for}\ y = x_i\ \text{and}\ n = 0 \\ \nu(y, n) & \text{otherwise}\end{cases}$
An abstraction algebra is a universe $\mathcal{U}$ together with a signature $\mathfrak{S}$ and an interpretation $I(a)$ of each abstraction $a$ in $\mathfrak{S}$ as an operator of $\mathcal{U}$ compatible with the shape of $a$. We say that $a$ denotes $I(a)$ (in the given abstraction algebra).
Abstraction algebras are a generalisation of what Rasiowa calls abstract algebras . An abstract algebra is an abstraction algebra that only contains abstractions with zero valence. Rasiowa uses abstract algebras as models for propositional calculi, i.e. to provide an algebraic semantics for propositional logics. We take this a step further and use abstraction algebras to provide models for abstraction logics.
Given such an abstraction algebra, and a valuation $\nu$ in $\mathcal{U}$, every term $t$ denotes a value $\llbracket t \rrbracket$ in the universe $\mathcal{U}$. The calculation of this value is straightforward, and recurses over the structure of $t$:
• If $t = x$ where $x$ is a variable, then $\llbracket t \rrbracket = \nu(x, 0)$.
• If $t = x[t_0, \ldots, t_{n-1}]$ is a variable application with $n > 0$, then $\llbracket t \rrbracket = f(u_0, \ldots, u_{n-1})$ where $f = \nu(x, n)$ is the $n$-ary operation assigned to $x$ via the valuation $\nu$, and $u_i$ is the value of $t_i$ with respect to $\nu$.
• If $t = (a.)$ then $\llbracket t \rrbracket = u$, where $a$ denotes the value $u$.
• If $t = (a.\, t_0 \ldots t_{n-1})$ for $n > 0$, then $\llbracket t \rrbracket = f(u_0, \ldots, u_{n-1})$ where $a$ denotes the $n$-ary operation $f$, and $u_i$ is the value of $t_i$ with respect to $\nu$.
• Assume $t = (a\, x_0\ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ for $m > 0$, and let the shape of $a$ be $(m; p_0, \ldots, p_{n-1})$. Let $F$ be the $n$-ary operator denoted by $a$. We deﬁne the arguments $r_i$ to which we will apply $F$ as follows. If $p_i = \emptyset$, then $r_i$ is the value denoted by $t_i$ with respect to $\nu$. If $p_i = \{j_0, \ldots, j_{k-1}\}$ for ${|{p_i}|} = k > 0$, then the abstraction $a$ binds the variables $x_{j_0}, \ldots, x_{j_{k-1}}$ occurring with arity $0$ in $t_i$. Thus $r_i$ is the $k$-ary operation which maps $k$ values $u_0, \ldots, u_{k-1}$ to the value denoted by $t_i$ with respect to the valuation $\nu[x_{j_0} \coloneqq u_0, \ldots, x_{j_{k-1}} \coloneqq u_{k-1}]$. Then $\llbracket t \rrbracket = F(r_0, \ldots, r_{n-1})$
Two terms $s$ and $t$ are called $\alpha$-equivalent with respect to a given signature $\mathfrak{S}$ iff for all abstraction algebras $\mathfrak{A}$ with this signature, and all valuations in (the universe of) $\mathfrak{A}$, $s$ and $t$ denote the same value. It can easily be checked whether two terms are $\alpha$-equivalent by ﬁrst computing their de Bruijn representations, and then checking if the two representations are identical. A proof of this can be found in the original AL report  under the moniker “equivalence of $\alpha$-equivalence and semantical equivalence”.
A variable $x$ occurs free with arity $n$ in a term $t$ if there is an occurrence of $x$ with arity $n$ in $t$ that is not bound by any surrounding abstraction. Because abstractions bind only variables of arity $0$, any occurrence of $x$ in $t$ with arity $n > 0$ is free.
It is clear that the value of $t$ depends only on the assignments in the valuation to those variables $x$ which are free in $t$. Therefore the value of a closed term $t$, i.e. a term without any free variables, does not depend on the valuation at all, but only on the abstraction algebra in which the calculation takes place.

## Substitution

An $n$-ary template has the form $[x_0 \ldots x_{n-1}.\, t]$, where the $x_i$ are distinct variables and $t$ is a term. The template binds all free occurrences of $x_i$ in $t$ of arity $0$. A $0$-ary template $[.\, t]$ is usually just written $t$.
A substitution $\sigma$ is a function deﬁned on a domain $D$ that maps a variable $x$, given an arity $n$ such that $(x, n)$ belongs to $D$, to an $n$-ary template $\sigma(x, n)$.
The purpose of a substitution $\sigma$ is to be applied to a term $t$, yielding another term ${t} / {\sigma}$ as the result of the substitution. This is done by determining those free occurrences of $x$ in $t$ of arity $n$ that are in $\sigma$’s domain, and replacing them with $\sigma(x, n)$. This means that expressions of the form $[x_0 \ldots x_{n-1}.\, t][s_0, \ldots, s_{n-1}]$ must be resolved to actual terms when replacing variables occurring with non-zero arity. This can in turn be done by applying to $t$ the substitution that maps $x_i$ to $s_i$.
The usual caveats of substitution in the presence of bound variables apply. For example, assume $\sigma$ maps $x$ to $y$. Then applying $\sigma$ to $(a\, y.\, (b.\, x\, y))$ by performing a direct replacement of $x$ with $y$ would yield $(a\, y.\, (b.\, y\, y))$. This is not what we want, as can be seen as follows. Note ﬁrst that $(a\, y.\, (b.\, x\, y))$ is $\alpha$-equivalent to $(a\, z.\, (b.\, x\, z))$, i.e. the meaning of those two terms is the same in all abstraction algebras with respect to all valuations. Therefore it should not matter to which of the two terms we apply the substitution to, the results should be the same, or at least $\alpha$-equivalent. But applying $\sigma$ to the second term (again via direct replacement) yields $(a\, z.\, (b.\, y\, z))$, which is not $\alpha$-equivalent to $(a\, y.\, (b.\, y\, y))$.
These issues can be dealt with by deﬁning substitution via de Bruijn terms instead of terms. The details of this have been worked out in the original AL report . For our purposes here we will just note that we can deal with these issues by renaming bound variables appropriately before performing replacement to avoid clashes between free and bound variables. Also note that there is no canonical result of applying a substitution, but that the result is determined only up to $\alpha$-equivalence.

### Substitution as Valuation

The main property of substitution is that, given a background valuation $\nu$, we can turn any substitution $\sigma$ into a valuation $\nu_\sigma$. The role of the background valuation is to provide meaning for free variables that are either not in the domain of $\sigma$, or free in some template of $\sigma$.
The valuation $\nu_\sigma$ has the property that for any term $t$ $\llbracket {t} \rrbracket_\sigma = \llbracket {{t} / {\sigma}} \rrbracket$ holds. Here $\llbracket {\cdot} \rrbracket$ denotes evaluation with respect to $\nu$, and $\llbracket {\cdot} \rrbracket_\sigma$ calculates the value with respect to $\nu_\sigma$.
We deﬁne $\nu_\sigma$ as follows for a variable $x$ occurring with arity $n$:
• If $n = 0$, then $\nu_\sigma(x, n) = \llbracket {{x} / {\sigma}} \rrbracket$.
• If $n > 0$, then for any values $u_0, \ldots, u_{n-1}$ we deﬁne $\nu_\sigma(x, n)(u_0, \ldots, u_{n-1}) = \llbracket {t} \rrbracket_{y \coloneqq u}$ where $\sigma(x, n) = [y_0 \ldots y_{n-1}.\, t]$, and $\llbracket {\cdot} \rrbracket_{y \coloneqq u}$ evaluates with respect to the valuation $\nu[y_0 \coloneqq u_0, \ldots, y_{n-1} \coloneqq u_{n-1}]$.
Further details and a proof of above property using de Bruijn terms can be found in the original AL report .

## Models

What is the meaning of an abstraction logic? Terms have been given meaning relative to an abstraction algebra and a valuation earlier . Correspondingly, a model of an abstraction logic ${\mathcal{L}}$ with signature $\mathfrak{S}$ and axioms ${\mathbb{A}}$ is almost an abstraction algebra ${\mathfrak{A}}$ with the same logic signature $\mathfrak{S}$, a universe $\mathcal{U}$, and an interpretation $I$, such that we have for all valuations $\nu$ in $\mathcal{U}$ and all axioms $a$ in ${\mathbb{A}}$ $\llbracket {a} \rrbracket = I(\top)$ There are two important modiﬁcations to be made before arriving at the actual deﬁnition of a model:
1. We are not interested in all possible abstraction algebras as models, but only in those that are logic algebras.
2. We are not interested in testing the axioms with all possible valuations, but only with those that belong to a space of valuations depending on the model itself.
To address the ﬁrst point, we deﬁne a logic algebra to be an abstraction algebra with logic signature $\mathfrak{S}$ such that $⇒$ and $\forall$ have denotations satisfying the following minimum requirements:
• $I(⇒)(I(\top), u) = I(\top)$ implies $u = I(\top)$ for all values $u$ in $\mathcal{U}$.
• Let $f$ be any unary operation of $\mathcal{U}$ such that $f(u) = I(\top)$ for all values $u$ in $\mathcal{U}$. Then $I(\forall)(f) = I(\top)$.
To address the second point, we deﬁne a valuation space $\mathcal{V}$ of an abstraction algebra ${\mathfrak{A}}$ to be a collection of valuations in the universe of ${\mathfrak{A}}$ such that:
• $\mathcal{V}$ is not empty.
• If $\nu$ is a valuation belonging to $\mathcal{V}$, $u$ is a value in the universe of ${\mathfrak{A}}$, and $x$ is a variable in $X$, then $\nu[x \coloneqq u]$ also belongs to $\mathcal{V}$.
• If $\nu$ is a valuation belonging to $\mathcal{V}$, and if $\sigma$ is a substitution with respect to the signature of ${\mathfrak{A}}$, then $\nu_\sigma$ also belongs to $\mathcal{V}$.
These requirements for $\mathcal{V}$ will turn out to be just strong enough to show soundness  of any abstraction logic, and weak enough to prove completeness  for any abstraction logic extending ${\mathcal{L}}_E$.
A model of an abstraction logic ${\mathcal{L}}$ is then a pair $({\mathfrak{A}}, \mathcal{V})$ such that ${\mathfrak{A}}$ is a logic algebra with the same signature as ${\mathcal{L}}$, and $\mathcal{V}$ is a valuation space of ${\mathfrak{A}}$, such that $\llbracket {a} \rrbracket = I(\top)$ for all valuations $\nu$ in $\mathcal{V}$ and all axioms $a$ in ${\mathbb{A}}$.
A model is called degenerate if the universe of ${\mathfrak{A}}$ consists of a single element. Note that every abstraction logic has a degenerate model.
If every model of ${\mathcal{L}}$ is also a model of the logic with the same signature as ${\mathcal{L}}$ and the single axiom $t$, then we say that $t$ is valid in ${\mathcal{L}}$ and write ${\mathcal{L}} ⊨ t$

## Proofs

Given a logic ${\mathcal{L}}$ with signature $\mathfrak{S}$ and axioms ${\mathbb{A}}$, a proof in ${\mathcal{L}}$ of a term $t$ is one of the following:
1. An axiom invocation $\operatorname{AX}(t)$ such that $t$ is an axiom in ${\mathbb{A}}$.
2. An application of substitution $\operatorname{SUBST}(t, \sigma, p_s)$ where
• $p_s$ is proof of $s$ in ${\mathcal{L}}$
• $\sigma$ is a substitution
• $t$ and ${s} / {\sigma}$ are $\alpha$-equivalent
3. An application of modus ponens $\operatorname{MP}(t, p_h, p_g)$ such that
• $p_h$ is a proof of $h$ in ${\mathcal{L}}$
• $p_g$ is a proof of $g$ in ${\mathcal{L}}$
• $g$ is identical to $h ⇒ t$
4. Introduction of the universal quantiﬁer $\operatorname{ALL}(t, x, p_s)$ where
• $x$ is a variable
• $p_s$ is a proof of $s$ in ${\mathcal{L}}$
• $t$ is identical to $(\forall x.\, s)$
If there exists a proof of $t$ in ${\mathcal{L}}$, we say that $t$ is a theorem of ${\mathcal{L}}$ and write ${\mathcal{L}} ⊢ t$

## The Deduction Theorem

The Deduction Theorem for abstraction logic is that any proof of $A$ in a logic ${\mathcal{L}}^+$ with axioms ${\mathbb{A}}$ and the additional axiom $\phi$ can be translated into a proof of $\phi' ⇒ A$ in the logic ${\mathcal{L}}$ with the same signature, but only axioms ${\mathbb{A}}$, as long as ${\mathcal{L}}$ extends ${\mathcal{L}}_D$.
Here $\phi'$ is the universal closure of $\phi$, i.e. $\phi' = ∀ x_0. ∀ x_1. \ldots ∀ x_{n-1}.\, \phi$ where the $x_i$ are the distinct free variables of $\phi$. Note that this implies that $\phi$ cannot contain free variables of non-zero arity for the Deduction Theorem to apply without any further conditions.
The proof of the Deduction Theorem is simply by recursing over the structure of the original proof and translating it step by step.
A special case of a stronger version of the Deduction Theorem is ${\mathcal{L}}_D ⊢ A ⇒ A$ We can prove this directly: Substituting $A$ for $C$ in Axiom 3  and then applying modus ponens using Axiom 2  yields the theorem $(A ⇒ B) ⇒ (A ⇒ A)$. Substituting $B ⇒ A$ for $B$ and applying modus ponens using Axiom 2  again, we obtain the theorem $A ⇒ A$.
In a system for machine-assisted theorem proving like Practal  it makes sense to bake in native support for ${\mathcal{L}}_D$ so that moving theorems from ${\mathcal{L}}^+$ to ${\mathcal{L}}$ doesn’t necessarily involve the actual translation of proofs.

## Soundness

Abstraction logic is sound, i.e. every theorem of ${\mathcal{L}}$ is also valid in ${\mathcal{L}}$: ${\mathcal{L}} ⊢ t \quad\text{implies}\quad {\mathcal{L}} ⊨ t$ We show by induction over $p$ that if $p$ is a proof of $t$ in ${\mathcal{L}}$, then $t$ is valid in ${\mathcal{L}}$:
• Assume $p = \operatorname{AX}(t)$. Then $t$ is an axiom and is therefore valid.
• Assume $p = \operatorname{SUBST}(t, \sigma, p_s)$. Then $p_s$ is a proof of $s$, and therefore $s$ is valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Then $\llbracket t \rrbracket = \llbracket {s / {\sigma}} \rrbracket = {\llbracket s \rrbracket}_\sigma$ Because $\nu_\sigma$ is in $\mathcal{V}$ as well, and $s$ is valid, ${\llbracket s \rrbracket}_\sigma = I(⊤)$ Together this yields $\llbracket t \rrbracket = {\llbracket s \rrbracket}_\sigma = I(⊤)$.
• Assume $p = \operatorname{MP}(t, p_h, p_g)$. Then $p_h$ is a proof of $h$, and $p_g$ is a proof of $g$, and therefore both $h$ and $g$ are valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Then $\llbracket h \rrbracket = I(⊤)$ and $I(⊤) = \llbracket g \rrbracket = \llbracket {h ⇒ t} \rrbracket = I(\text{⇒})(\llbracket h \rrbracket, \llbracket t \rrbracket) = I(\text{⇒})(I(⊤), \llbracket t \rrbracket)$ This implies $\llbracket t \rrbracket = I(⊤)$.
• Assume $p = \operatorname{ALL}(t, x, p_s)$. Then $p_s$ is a proof of $s$, and therefore $s$ is valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Let $\mathcal{U}$ be the universe of ${\mathfrak{A}}$. Then $\llbracket t \rrbracket = \llbracket {(\text{∀} x.\, s)} \rrbracket = I(\text{∀})(f)$ Here $f$ is a unary operation of $\mathcal{U}$ where $f(u) = {\llbracket s \rrbracket}_{x \coloneqq u}$ for all values $u$ in $\mathcal{U}$. Because $\nu[x \coloneqq u]$ also belongs to $\mathcal{V}$ and $s$ is valid, we have ${\llbracket s \rrbracket}_{x \coloneqq u} = I(⊤)$ and therefore $f(u) = I(⊤)$ for all $u$. This implies $\llbracket t \rrbracket = I(\text{∀})(f) = I(⊤)$.

## Completeness

An abstraction logic ${\mathcal{L}}$ is called complete if every valid term is also a theorem: ${\mathcal{L}} ⊨ t \quad \text{implies}\quad {\mathcal{L}} ⊢ t$
If ${\mathcal{L}}$ extends ${\mathcal{L}}_E$, then ${\mathcal{L}}$ is complete.
To prove this, we construct the Rasiowa Model $(\mathfrak{R}, \mathcal{V})$ of ${\mathcal{L}}$, which is a model for ${\mathcal{L}}$. The construction relies heavily on the fact that ${\mathcal{L}}$ extends ${\mathcal{L}}_E$. The universe of the Rasiowa Model consists of equivalence classes of terms, where two terms $s$ and $t$ are called equivalent if $s = t$ is a theorem of ${\mathcal{L}}$. This is a variation of a standard approach to prove completeness, originally due to Lindenbaum and Tarski. We write ${[t]_{\mathfrak{R}}}$ for the equivalence class to which a term $t$ belongs. The details of the construction can be found in the original AL paper  (the Rasiowa Model is called Rasiowa Abstraction Algebra there, which is a misnomer). In the construction we make essential use of the fact that $\mathcal{V}$ does not need to be the class of all valuations, but can be custom tailored as long as we can guarantee that $\mathcal{V}$ has the properties required of a valuation space.
Most importantly, there exists a valuation in $\mathcal{V}$ with $\llbracket {t} \rrbracket = {[{t}]_{\mathfrak{R}}}$ for any term $t$, where $\llbracket {\cdot} \rrbracket$ evaluates with respect to that valuation. Furthermore, for the interpretation $I$ of $\mathfrak{R}$ we have $I(\top) = {[{\top}]_{\mathfrak{R}}}$
From this we can see immediately that ${\mathcal{L}}$ is complete. Because assume that $t$ is valid. Then ${[t]_{\mathfrak{R}}} = \llbracket t \rrbracket = I(\top) = {[{\top}]_{\mathfrak{R}}}$ which shows that $t = \top$ is a theorem of ${\mathcal{L}}$, and thus $t$ is a theorem as well.

## Consistency

An abstraction logic ${\mathcal{L}}$ is called inconsistent if all terms are also theorems, and consequently consistent if there is at least one term which is not a theorem.
If ${\mathcal{L}}$ is an extension of a deduction logic ${\mathcal{L}}_D$, then inconsistency of ${\mathcal{L}}$ is equivalent to ${\mathcal{L}} ⊢ ∀ x.\, x$ This is easy to see. Assume $∀ x.\,x$ is a theorem in ${\mathcal{L}}$. Substituting $[x.\, x]$ for $A$ in Axiom 4  of ${\mathcal{L}}_D$ and applying modus ponens, it follows that $x$ is a theorem. Substituting any term $t$ for $x$ shows that $t$ is a theorem.
If an abstraction logic ${\mathcal{L}}$ is inconsistent, then all models of ${\mathcal{L}}$ are degenerate. Assume ${\mathcal{L}}$ is inconsistent. It follows that $x$ is a theorem for any variable $x$ of arity zero. That means that $x$ is valid in any model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. In particular, for any valuation $\nu$ in $\mathcal{V}$ we have $\llbracket x \rrbracket = I(⊤)$. There is such $\nu$ because $\mathcal{V}$ is non-empty. For any value $u$ in the universe $\mathcal{U}$ of ${\mathfrak{A}}$ the valuation $\nu[x \coloneqq u]$ is in $\mathcal{V}$ as well, and therefore $u = \llbracket {x} \rrbracket_{x \coloneqq u} = I(⊤)$. That means $\mathcal{U}$ consists only of $I(⊤)$, thus any model of ${\mathcal{L}}$ is degenerate.
What about the other direction? If every model of an abstraction logic ${\mathcal{L}}$ is degenerate, then $\llbracket t \rrbracket = I(⊤)$ holds for any term $t$ with respect to any valuation. Therefore ${\mathcal{L}} ⊨ t$ But is $t$ then a theorem of ${\mathcal{L}}$? We have seen that this is indeed the case if ${\mathcal{L}}$ extends ${\mathcal{L}}_E$, because then ${\mathcal{L}}$ is complete .
Therefore, if ${\mathcal{L}}$ extends ${\mathcal{L}}_E$, then inconsistency of an abstraction logic ${\mathcal{L}}$ is equivalent to all of its models being degenerate.
It is thus straightforward to see that ${\mathcal{L}}_K$ is consistent. As a model, use a two-element Boolean Algebra  extended in the obvious way with operators denoting $\forall$ and $\exists$. The axioms of ${\mathcal{L}}_K$ can then be checked by simply exhausting all possibilities.

## Deﬁnitions

A head $h$ for an abstraction $a$ is an abstraction application of the form $(a\, x_0\ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ such that:
• Each term $t_i$ has the form $F_i[x_{j_0}, \ldots, x_{j_{k-1}}]$ where the $x_{j_0}, \ldots, x_{j_{k-1}}$ are distinct variables bound by $a$.
• All $F_i$ are distinct free variables of $h$.
The shape of $a$ can easily be determined from a head for $a$. It must be $(m; p_0, \ldots, p_{n-1})$, where $p_i = \{{j_0}, \ldots, {j_{k-1}}\}$ given the above form of $t_i$.
Given a logic ${\mathcal{L}}$ extending ${\mathcal{L}}_E$, a deﬁnition has the form $h ≝ t$ where $h$ is a head for an abstraction $a$ not contained in ${\mathcal{L}}$, and $t$ is a term of ${\mathcal{L}}$ such that all of $t$’s free variables are also free variables of $h$.
A deﬁnition results in a logic ${\mathcal{L}}'$ which is an extension of ${\mathcal{L}}$. The signature of ${\mathcal{L}}'$ is that of ${\mathcal{L}}$ extended by the abstraction $a$. The axioms of ${\mathcal{L}}'$ are the axioms of ${\mathcal{L}}$ plus the axiom $h = t$.
Furthermore, ${\mathcal{L}}'$ is a conservative extension of ${\mathcal{L}}$, i.e. ${\mathcal{L}}'$ is not only an extension of ${\mathcal{L}}$, but if $t$ is a term of ${\mathcal{L}}$, then $t$ is a theorem of ${\mathcal{L}}$ iff $t$ is a theorem of ${\mathcal{L}}'$. This is straightforward to prove by induction over the structure of proofs, and considering the more general statement that $t'$ is a theorem of ${\mathcal{L}}$ iff $t$ is a theorem of ${\mathcal{L}}'$. Here $t'$ results from $t$ by rewriting away all occurrences of $a$ using the equation $h = t$.
Therefore if ${\mathcal{L}}'$ is inconsistent, then ${\mathcal{L}}$ is inconsistent as well, because $\forall x.\, x$ is a term of ${\mathcal{L}}$. Consequently, ${\mathcal{L}}$ is consistent iff ${\mathcal{L}}'$ is consistent.
We can also allow conditional deﬁnitions of the form $c ⇒ h ≝ t$ by considering this as an abbreviation for $h ≝ (\text{if}.\, c\, t)$ where the abstraction “$\text{if}$” is governed by the single axiom $(\text{if}.\, \top\, x) = x$, which is assumed to be already contained in ${\mathcal{L}}$. This allows us to derive $c ⇒ h = t$ in ${\mathcal{L}}'$.

## Rasiowa’s Algebraic Approach

Abstraction logic was born out of the desire to ﬁnd solid logical foundations for Practical Types . Discussions on the Lean Zulip chat with Mario Carneiro and others left me convinced that while Practical Types were basically the right approach, in order to make a convincing case I needed to be able to explain the logical foundations with a level of detail that I was not able to at that moment.
During my search for logical foundations for Practical Types, I came across the work of . The algebraic approach to logic  as Rasiowa applied it to propositional logic made immediate sense to me. Rasiowa chose to generalise this approach to predicate logic by following Mostowski and interpreting quantiﬁers as least upper bounds and greatest lower bounds. To me, that does not seem to be the proper way to generalise Rasiowa’s approach. Instead, I believe abstraction logic is. Just like Rasiowa restricts her models by restricting abstract algebras to implicative algebras to ensure that implication satisﬁes modus ponens, AL meets minimal requirements of implication and universal quantiﬁcation by restricting abstraction algebras to logic algebras.
Why did Rasiowa miss this generalisation, which now seems obvious with hindsight? The reason may simply be that operators were not part of her normal toolbox, while working with higher-order functions is standard in both programming and mechanised theorem proving today. Another possible reason is that working with a Fregean domain  might have felt alien to her. But on the other hand, her models for propositional logic are topological spaces, and it must have felt somewhat of a waste of space to ﬁll them just with mere truth values. As we can see now, these spaces can represent whole universes.
Our approach seems to be conceptually simpler and less involved than Rasiowa’s approach to predicate logics. An important indicator for this is how simple, elegant and without any need to exclude special cases our completeness proof for abstraction logic is (once the Rasiowa Model is constructed). Completeness holds for all abstraction logics from ${\mathcal{L}}_E$ on, including intuitionistic abstraction logic, classical abstraction logic, and all logics in between and beyond. On the other hand, completeness for predicate logics based on Rasiowa’s approach is in general complicated territory . Ono concludes his paper  from 1995 on the completeness of predicate logics with respect to algebraic semantics with the words
[...] there seems to be a big difference between instantiations in logic and in algebra. In other words, though usually we interpret quantiﬁers as inﬁnite joins and meets in algebraic semantics, i.e., we deal with quantiﬁers like inﬁnite disjunctions and conjunctions, this will be not always appropriate. So, one of the most important questions in the study of algebraic semantics for predicate logics would be how to give an appropriate interpretation of quantiﬁers, in other words, how to extend algebraic semantics.
It seems that abstraction logic just might be this extension of algebraic semantics that Ono was looking for.

## Propositional Logic

Given that AL is a generalisation of algebraic semantics for propositional logics, we can formulate all propositional logics from Rasiowa’s book  as ALs. As an example, we do this for positive implicative logic.
There is a caveat though: $\top$ and $\forall$ are part of any AL by deﬁnition, but these abstractions are not present in positive implicative logic. We will not be bothered by this, and just assume the following two axioms:
• $\top$
• $(\forall x.\, F[x])$
The ﬁrst axiom is obvious. The second axiom effectively renders $\forall$ a complicated way of writing $\top$.
The remaining axioms of positive implicative logic are:
• $A ⇒ (B ⇒ A)$
• $(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))$
The semantics of this AL is identical to the semantics given by Rasiowa. Rasiowa shows that this logic is both complete and consistent.
Another approach is to deﬁne propositional logic as an abstraction logic such that the universe only consists of propositions. Starting from ${\mathcal{L}}_I$ or ${\mathcal{L}}_K$, we add the axiom $(A \Leftrightarrow B) ⇒ (A = B)$ and obtain intuitionistic propositional AL ${\mathcal{L}}_{IP}$ or classical propositional AL ${\mathcal{L}}_{KP}$, respectively. Completeness follows from both ${\mathcal{L}}_{IP}$ and ${\mathcal{L}}_{KP}$ extending ${\mathcal{L}}_E$. Consistency can be conﬁrmed as before for ${\mathcal{L}}_K$ .

## Paraconsistent Logic

AL will be hard-pressed to implement any paraconsistent logic, as AL assumes there being only a single value representing true. This is at odds with Priest’s 3-valued Logic of Paradox , for example, which has an additional value paradoxical which is also “true”. In particular, any AL extending ${\mathcal{L}}_F$ has the principle of explosion as a theorem: $A ⇒ ((¬ A) ⇒ B)$ It should be possible to adapt abstraction logic to allow multiple different values all representing “true”. But as no paraconsistent logic provides a widely accepted foundation of mathematics, there seems no need to accommodate paraconsistency at this point.

## First-Order Logic

To represent ﬁrst-order logic (FOL) as an abstraction logic, we should be able to use the same method as for Calculator Logic . But instead of just numbers “$\text{Num}$”, we embed an entire FOL-universe “${\includegraphics[height=0.5em]{FBED8125-6F35-4327-9066-6D87A363FBCD}}$” in our AL-universe $\mathcal{U}$. As for Calculator Logic, we build FOL on top of ${\mathcal{L}}_K$, and we model undeﬁnedness  via $\Finv$. FOL operators would be deﬁned in such a way that illformed FOL formulas evaluate to $\Finv$. We will not ﬂesh out this construction in detail at this point, but leave this for another time.

## The Best Logic?

I hope a picture is forming by now why I believe Abstraction Logic to be the best logic. It is doubtful that this claim can ever be proven. But it doesn’t need to be. I mean best logic in a very practical sense, and therefore if the claim is indeed true, Abstraction Logic should be able to form the basis of a theorem proving system which surpasses other systems based on just FOL, set theory, HOL, or dependent types. In fact, it should be able to accommodate all of these foundations, as they all should be axiomatisable in Abstraction Logic.
So, let’s build Practal and see!

## References

Steven Obua, Jacques Fleuriot, Phil Scott, David Aspinall. (2014). ProofPeer: Collaborative Theorem Proving, https://arxiv.org/abs/1404.6186.
Donald E. Knuth. (1986). The TeXbook, Addison-Wesley.
Thomas Hales et al. (2017). A Formal Proof of the Kepler Conjecture, https://doi.org/10.1017/fmp.2017.1.
Alonzo Church. (1940). A formulation of the simple theory of types, https://doi.org/10.2307/2266170.
Florian Rabe. (2015). The Future of Logic: Foundation-Independence, https://doi.org/10.1007/s11787-015-0132-x.
W. V. Quine. (1986). Philosophy of Logic, https://doi.org/10.2307/j.ctvk12scx.
Steven Obua. (2021). Abstraction Logic, https://doi.org/10.47757/abstraction.logic.2.
Philip Wadler. (2015). Propositions as types, https://doi.org/10.1145/2699407.
Steven Obua. (2021). Practical Types, https://doi.org/10.47757/practical.types.1.
Alonzo Church. (1951). A formulation of the logic of sense and denotation, https://archive.org/details/structuremethodm0000henl.
Saul A. Kripke. (2013). Fregean Quantification Theory, https://doi.org/10.1007/s10992-013-9299-x.
Hao Wang. (1957). The Axiomatization of Arithmetic, https://doi.org/10.2307/2964176.
William M. Farmer. (2004). Formalizing Undefinedness Arising in Calculus, https://doi.org/10.1007/978-3-540-25984-8_35.
Helena Rasiowa. (1974). An algebraic approach to non-classical logics, https://doi.org/10.1016/s0049-237x(09)x7004-7.
Steven Obua. (2021). Practal — Practical Logic: A Bicycle for Your Mathematical Mind, https://doi.org/10.47757/practal.1.
Paul Halmos, Steven Givant. (2009). Introduction to Boolean Algebras, https://doi.org/10.1007/978-0-387-68436-9.
Petr Cintula, Carles Noguera. (2015). A Henkin-Style Proof of Completeness for First-Order Algebraizable Logics, https://doi.org/10.1017/jsl.2014.19.
Hiroakira Ono. (1995). Algebraic semantics for predicate logics and their completeness, https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/0927-7.pdf.
Graham Priest. (1979). The Logic of Paradox, https://doi.org/10.1007/BF00258428.