Abstraction Logic

Cite as: https://doi.org/10.47757/abstraction.logic.2

November 14th, 2021

Abstract

Abstraction Logic is introduced as a foundation for Practical Types [1] and Practal [2]. 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.

Introduction

The goal of Practical Types [1] is to provide a foundation for formal machine-assisted reasoning that anyone would ﬁnd empowering who is interested in rigorous thinking and design. This paper provides a foundation on which Practical Types will be built as a particular class of abstraction logics.

Like ﬁrst-order logic, abstraction logic has a single universe of discourse, i.e. it is one-sorted. It goes even further than ordinary ﬁrst-order logic in that truth values are part of this universe, i.e. the universe forms a Fregean domain [3].

Like higher-order logic and type theory, abstraction logic provides built-in support for variable binding constructs. But variable binding is not achieved indirectly via a function sort or type; instead it is directly modelled via shape speciﬁcations for (possibly) variable binding constructs called abstractions. Abstractions are simply the constants of abstraction logic. As a consequence

\alpha

-equivalence of terms is a central concept in abstraction logic, but

\beta/\eta

-conversion do not play any role at this level.

Free variables can depend on parameters. Thus where ﬁrst-order logic needs axiom schemata consisting of inﬁnitely many axioms, abstraction logic can express the same with a single axiom, just like higher-order logic. This is illustrated multiple times when we present several concrete abstraction logics →.

Although abstraction logic started out as an investigation into the logic of Practical Types, it will be important for the design of Practal [2] in its own right. The relationship between Practal, Practical Types and abstraction logic is similar to the relationship between the Isabelle System [4] and its logics HOL and Pure. Locales [5] are an important mechanism for modular reasoning in Isabelle built on top of Pure. Because abstraction logic is simpler than type theory, but at the same time more versatile, the same should be true for an abstraction logic mechanism for modular reasoning inspired by locales.

The relationship between Practical Types and abstraction logic can also be compared to the relationship between set theory and ﬁrst-order logic. Similarly, abstraction logic is not limited to Practical Types, it can provide a foundation for many applications where currently ﬁrst-order logic is used. Furthermore, abstraction logic can be applied in places where previously higher-order logic was needed, as in the realm of interactive theorem proving.

Overview. We ﬁrst list some notation →. Then abstraction algebras → are introduced. Then the syntax → and semantics → of terms representing values in abstraction algebras is presented. De Bruijn terms → for abstraction syntax are deﬁned next, and the treatment of $\alpha$ -equivalence → is based on them. After introducing substitution →, we show that de Bruijn terms form an abstraction algebra themselves →, and use this fact to show the fundamental role that

\alpha

-equivalence plays. Finally abstraction logic → itself is introduced, and our notion of proof → is shown to be sound →. Several examples → of abstraction logics are presented. We discuss consistency → in the context of abstraction logic. We construct the Rasiowa Abstraction Algebra → of any abstraction logic

{\mathcal{L}}

that extends Deduction Logic with Equality →, and use it to prove completeness → of any such

{\mathcal{L}}

, including intuitionistic and classical abstraction logic. We conclude by brieﬂy discussing matching and uniﬁcation → of abstraction syntax terms.

Preliminaries

Let’s ﬁx some general notation ﬁrst:

$\mathbb{N}$ is the set of natural numbers starting from $0$ .
We write ${\overline{{n}}}$ for $\{0,\ldots,n-1\}$ , in particular ${\overline{{0}}} = \emptyset$ .
We write ${\langle {i_0, \ldots, i_{n-1}} \rangle}$ where $i_0 < i_1 < \ldots < i_{n-1}$ for the set $\{{i_0, \ldots, i_{n-1}}\}$ .
We write ${U \rightarrow V}$ for the set of functions from set $U$ to set $V$ .
We write ${U ↪ V}$ for the set of partial functions from set $U$ to set $V$ .
The function $\operatorname{id}_{U} : {U \rightarrow U}$ denotes the identity on $U$ .
We write $U \times V$ for the cartesian product of the sets $U$ and $V$ .
We deﬁne $U^n$ for $n \in \mathbb{N}$ , $n \geq 1$ via $U^1 = U$ and $U^{m+1} = U^m \times U$ for $m \geq 1$ .
We write ${|p|}$ for the size of the ﬁnite set $p$ .
For $f : {U \rightarrow V}$ , distinct ${x_0, \ldots, x_{n-1}}$ , and arbitrary ${v_0, \ldots, v_{n-1}}$ in $V$ , we write $f[x_0 \coloneqq v_0, \ldots, x_{n-1} \coloneqq v_{n-1}]$ for the function $g : {{U \cup \{{x_0, \ldots, x_{n-1}}\}} \rightarrow V}$ deﬁned via $g(u) = \begin{cases} v_i & \text{if}\ u = x_i \\ f(u) & \text{if}\ u \notin \{{x_0, \ldots, x_{n-1}}\} \end{cases}$
Instead of $f[x_{i_0} \coloneqq v[i_0], \ldots, x_{i_{n-1}} \coloneqq v[i_{n-1}]]$ we also write $f[\overline{x_p \coloneqq v[p]}]$ where $p = {\langle {i_0, \ldots, i_{n-1}} \rangle}$ and $v[x]$ stands for an arbitrary expression depending on $x$ .

Algebra

A shape

\sigma

prescribes a number

m

of binders and a number

n

of parameters. Furthermore it assigns to each parameter the set of binders it depends on. A shape is therefore written as

(m; p_0, \ldots, p_{n-1})

where

m, n \in \mathbb{N}

, and each

p_i

is a subset of

{\overline{{m}}}

. Furthermore we require that there are no superﬂuous binders:

\bigcup_{i=0}^{n-1} p_i = {\overline{{m}}}

We call

m

the valence of the shape, and

n

its arity. Above condition implies that a shape with arity

0

necessarily has valence

0

. It also implies that for a unary shape its sole parameter will depend on all binders.

An abstraction signature

\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1})

is a list of

k

different abstractions

a_i

, where each abstraction

a_i

is associated with its shape

\sigma_i

An abstraction algebra

{\mathfrak{A}} = (U; I; \mathfrak{S})

is a non-empty set

U

together with an abstraction signature

\mathfrak{S}

and an interpretation

I

which interprets an abstraction

a_i

as an element

I(a_i)

of the set

{\Lambda_{U}({\sigma_i})}

. The set

{\Lambda_{U}({\sigma_i})}

will be deﬁned shortly.

Examples of abstractions and their shapes are:

Equality $x = y$ has two parameters $x$ and $y$ and no binders. The shape of equality is therefore ${\sigma_{=}} = (0; \{\}, \{\})$ .
Universal quantiﬁcation $\forall x.\, P[x]$ has one binder $x$ and one parameter $P$ , which depends on $x$ . The shape of universal quantiﬁcation is ${\sigma_{{\forall}}} = (1; \{0\})$ .
Function abstraction $\lambda x : T.\, A[x]$ has one binder $x$ and two parameters $T$ and $A$ . The parameter $T$ does not depend on $x$ , but $A$ does. The shape of function abstraction is therefore ${\sigma_{{\lambda}}} = (1; \{\}, \{0\})$ .

We require an abstraction

a

of shape

\sigma

to be an element of

{\Lambda_{U}({\sigma})}

. We deﬁne

{\Lambda_{U}({\sigma})}

for

\sigma = (m; {p_0, \ldots, p_{n-1}})

as follows:

{\Lambda_{U}({\sigma})} = \begin{cases} U & \text{if}\ n = 0\\ {{{\mathcal{F}_{m}^{{p_0}}(U)} \times \ldots \times {\mathcal{F}_{m}^{{p_{n-1}}}(U)}} \rightarrow U} & \text{if}\ n \geq 1 \end{cases}

Here, for

m \geq 1

and

p \subseteq {\overline{{m}}}

, we deﬁne

{\mathcal{F}_{m}^{p}(U)}

as follows:

{\mathcal{F}_{m}^{p}(U)} = \begin{cases} U & \text{if}\ p = \emptyset\\ \{\, f \circ {\pi_m^p(U)} \,\mid\, f \in {{U^{{|p|}}} \rightarrow U} \} \subseteq {{U^m} \rightarrow U} & \text{if}\ p \neq \emptyset \end{cases}

The projections

{\pi_m^p(U)} : {{U^m} \rightarrow {U^{|{p}|}}}

are deﬁned for

p = {\langle {i_0, \ldots, i_{n-1}} \rangle}

via

(u_0, \ldots, u_{m-1}) \mapsto (u_{i_0}, \ldots, u_{i_{n-1}})

In particular, if the valence of

\sigma

0

and its arity

n

, then

{\Lambda_{U}({\sigma})} = \begin{cases} U & \text{if}\ n = 0\\ {{U^n} \rightarrow U} & \text{if}\ n \neq 0 \end{cases}

Note that an abstract algebra as described by Rasiowa [6] (see also [7], [8] →) is thus simply an abstraction algebra where all abstractions have zero valence.

If the valence of

\sigma

1

, then

{\Lambda_{U}({\sigma})} = {{{\mathcal{F}_{1}^{{p_0}}(U)} \times \ldots \times {\mathcal{F}_{1}^{{p_{n-1}}}(U)}} \rightarrow U}

, where

{\mathcal{F}_{1}^{{p_i}}(U)}

is either

U

{U \rightarrow U}

, depending on whether

p_i = \emptyset

p_i = \{0\}

, respectively.

Continuing our previous examples, we can now say the following:

The interpretation of $=$ is a function in ${{U \times U} \rightarrow U}$ .
The interpretation of $\forall$ is a function in ${{({U \rightarrow U})} \rightarrow U}$ .
The interpretation of $\lambda$ is a function in ${{U \times ({U \rightarrow U})} \rightarrow U}$ .

Bounded universal quantiﬁcation

\forall x : T.\, P[x]

has shape

(1; \{\}, \{0\})

, and is therefore interpreted as an element of

{{U \times ({U \rightarrow U})} \rightarrow U}

Another example is deﬁned by

\operatorname{funeq} x.\, T\, f[x]\, g[x] ≝ \forall x : T.\, f[x] = g[x]

The shape of

\operatorname{funeq}

(1; \{\}, \{0\}, \{0\})

, and therefore

\operatorname{funeq} : {{U \times ({U \rightarrow U}) \times ({U \rightarrow U})} \rightarrow U}

Syntax

Given an abstraction signature

\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1})

and a set of variables

X

, we deﬁne the set

{\mathcal{T}_{{X}}({\mathfrak{S}})}

of terms over

\mathfrak{S}

. We require variables and abstractions not to overlap, of course, i.e.

a_i \notin X

for all

i \in {\overline{{k}}}

. We also require each variable

x\in X

to be associated with a ﬁxed arity

{x_{\operatorname{arity}}} \in \mathbb{N}

The set

{\mathcal{T}_{{X}}({\mathfrak{S}})}

of terms is then deﬁned inductively as follows:

Given a variable $x$ and terms ${t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}$ , $x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ is a term. We also write just $x$ instead of $x[\,]$ .
Given an abstraction $a$ of valence $m$ and arity $n$ , terms ${t_0, \ldots, t_{n-1}}$ , and distinct variables ${x_0, \ldots, x_{m-1}}$ such that ${{(x_i)}_{\operatorname{arity}}} = 0$ for all $i \in {\overline{m}}$ , $(a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ is also a term.

Note that with this deﬁnition all terms in

{\mathcal{T}_{{X}}({\mathfrak{S}})}

are wellformed, although the deﬁnition makes only use of the valence and arity of an abstraction instead of its full shape. Of course, the full shape is important: it is needed to determine the free variables

{\operatorname{Free}({t})}

of a term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

. We deﬁne

{\operatorname{Free}(t)}

recursively, following the inductive deﬁnition of

{\mathcal{T}_{{X}}({\mathfrak{S}})}

\begin{array}{lcl} {\operatorname{Free}({x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]})} & = & \{x\} \cup {\operatorname{Free}({t_0})} \cup \ldots \cup {\operatorname{Free}({t_{{x_{\operatorname{arity}}} - 1}})} \\[0.2cm] {\operatorname{Free}({(a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})})} & = & \phantom{\cup\ }({\operatorname{Free}({t_0})} \setminus \{x_{i_{0, 0}}, \ldots, x_{i_{0, {|{p_0}|} - 1}}\}) \\ & &\cup\ ({\operatorname{Free}({t_1})} \setminus \{x_{i_{1, 0}}, \ldots, x_{i_{1, {|{p_1}|} - 1}}\}) \\ & & \vdots \\ & &\cup\ ({\operatorname{Free}({t_{n-1}})} \setminus \{x_{i_{n-1, 0}}, \ldots, x_{i_{n-1, {|{p_{n-1}}|} - 1}}\}) \\ & & \text{where}\ {\sigma_{a}} = (m; {p_0, \ldots, p_{n-1}}) \\ & & \text{and}\ p_j = \langle i_{j, 0}, \ldots, i_{j, {|{p_j}|} - 1} \rangle \ \forall j \in {\overline{{n}}} \end{array}

In case of

{\operatorname{Free}(t)} = \emptyset

, the term

t

is called closed.

The following table examines our previous examples in terms of abstraction syntax:

\begin{array}{c|c|c} {\includegraphics[height=0.5em]{FF6AAFAC-BADB-41C3-ADC7-A1AAD402ED58}} & {\includegraphics[height=0.5em]{87C1D531-C2C1-42AF-9E21-8F87031148D8}} & {\includegraphics[height=0.5em]{49711145-C51A-4355-920C-D2354871B67C}} \\\hline x = y & (= .\, x\ y) & x, y \\ \forall x.\, P[x] & (\forall x.\, P[x]) & P \\ \lambda x : T.\, A[x] & (\lambda x .\, T\, A[x]) & T, A \\ \forall x : T.\, P[x] & (\forall x.\, T\, P[x]) & T, P \\ \operatorname{funeq} x.\, T\, f[x]\, g[x] & (\operatorname{funeq} x.\, T\, f[x]\, g[x]) & T, f, g\\ \forall x : T.\, f[x] = g[x] & (\forall x.\, T\, (= .\, f[x]\, g[x])) & T, f, g \end{array}

Note that

x

is a free variable of the expression

\lambda x : x.\ x

Although the variable

x

is bound in the second parameter of

\lambda

, it occurs free in the ﬁrst parameter of

\lambda

, and is therefore a free variable of the entire expression.

Semantics

Given a set

F

of variables, and a set

U

, a valuation

\nu

F

U

is a mapping that assigns to each

x \in F

with

{x_{\operatorname{arity}}} = 0

an element

\nu(x) \in U

, and to each

x \in F

with

{x_{\operatorname{arity}}} \geq 1

a function

\nu(x) \in {{U^{{x_{\operatorname{arity}}}}} \rightarrow U}

. We denote the set of valuations of

F

U

{\includegraphics[height=0.5em]{4C074B62-3A5B-434A-99AE-50F05AE46B36}}(F, U)

Let

\mathfrak{S}

be an abstraction signature, and

{\mathfrak{A}} = (U; I; \mathfrak{S})

an abstraction algebra with signature

\mathfrak{S}

. Given a term

t \in {\mathcal{T}_{X}({\mathfrak{S}})}

, any valuation

\nu

{\operatorname{Free}(t)}

U

determines an element

{\nu}\llbracket{t}\rrbracket \in U

, recursively deﬁned as follows:

If $t = x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ , then $x \in {\operatorname{Free}(t)}$ , and ${\operatorname{Free}({t_i})} \subseteq {\operatorname{Free}(t)}$ for all $i \in {\overline{{{x_{\operatorname{arity}}}}}}$ . Thus we set ${\nu}\llbracket{t}\rrbracket = \begin{cases} \nu(x) & \text{if}\ {x_{\operatorname{arity}}} = 0\\ \nu(x)\left({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{{x_{\operatorname{arity}}} - 1}}}\rrbracket\right) & \text{if}\ {x_{\operatorname{arity}}} \geq 1 \end{cases}$
If $t = (a.\, t_0 \ldots t_{n-1})$ for an abstraction $a$ with zero valence and arity $n$ , we set ${\nu}\llbracket{t}\rrbracket = \begin{cases} I(a) & \text{if}\ n = 0\\ I(a)\left({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n - 1}}}\rrbracket\right) & \text{if}\ n \geq 1 \end{cases}$
Assume now $t = (a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ for an abstraction $a$ with valence $m \geq 1$ and arity $n \geq 1$ , and of shape ${\sigma_{{a}}} = (m; {p_0, \ldots, p_{n-1}})$ . Let us consider a ﬁxed $i \in {\overline{{n}}}$ , and let $p_i = {\langle {j_0, \ldots, j_{k-1}} \rangle} \subseteq {\overline{m}}$ . We have ${\operatorname{Free}({t_i})} \subseteq {\operatorname{Free}(t)} \cup \{x_{j_0}, \ldots, x_{j_{k-1}}\}$ Therefore, for any $({u_0, \ldots, u_{m-1}}) \in U^m$ , the valuation $\mu_i = \nu[x_{j_0} \coloneqq u_{j_0}, \ldots, x_{j_{k-1}} \coloneqq u_{j_{k-1}}]$ determines a value ${\mu_i}\llbracket{{t_i}}\rrbracket \in U$ . Deﬁning $f_i : {{U^m} \rightarrow U}$ by $f_i : ({u_0, \ldots, u_{m-1}}) \mapsto {\mu_i}\llbracket{{t_i}}\rrbracket$ it is obvious that $f_i \in {\mathcal{F}_{m}^{{p_i}}(U)}$ . Consequently, we set ${\nu}\llbracket{t}\rrbracket = I(a)\left({f_0, \ldots, f_{n-1}}\right)$

t

is a closed term, then

{\nu}\llbracket{t}\rrbracket

is independent of the choice of the valuation

\nu

U

, and we can therefore deﬁne

{{\llbracket t \rrbracket}_{{\mathfrak{A}}}} = {\nu}\llbracket{t}\rrbracket

De Bruijn Terms

Terms

{\mathcal{T}_{{X}}({\mathfrak{S}})}

provide an adequate user interface for humans, but are awkward to handle from a technical point of view. This becomes apparent when formulating more complex operations on terms, like substitution. One reason for this awkwardness is the potential of clashes between bound variables and free variables. Another reason is that two terms which are semantically equivalent, like

(a\, x.\, x)

and

(a\, y.\, y)

, can nevertheless be syntactically different because of different choices for the names of bound variables.

In actual software implementations of logic, a common approach to deal with this problem is called locally nameless [9]. The following deﬁnitions are inspired by this approach. We ﬁrst deﬁne de Bruijn preterms

{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

For any $n \in \mathbb{N}$ , $\uparrow\hspace{-0.15em}{{n}}$ is a de Bruijn preterm. We implicitly assume everywhere that $\uparrow\hspace{-0.15em}{{n}} \notin X$ . Given a set $N \subset \mathbb{N}$ we write $\uparrow\hspace{-0.15em}{{N}}$ for the set $\{\uparrow\hspace{-0.15em}{{n}} \mid n \in N\}$ .
Given a variable $x \in X$ and de Bruijn preterms ${t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}$ , $x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ is a de Bruijn preterm. We also write just $x$ instead of $x[\,]$ .
Given an abstraction $a$ of arity $n$ , and de Bruijn preterms ${t_0, \ldots, t_{n-1}}$ , $(a\,t_0 \ldots t_{n-1})$ is also a de Bruijn preterm.

The idea is that a term like

(a\, x\, y.\, (b.\, x\, y)\, (c\, x.\, x\, y))

corresponds to the de Bruijn term

(a\, (b\, \uparrow\hspace{-0.15em}{{0}}\, \uparrow\hspace{-0.15em}{{1}})\, (c\, \uparrow\hspace{-0.15em}{{0}}\, \uparrow\hspace{-0.15em}{{2}}))

This correspondence is made precise by the mapping

\alpha : {{{\mathcal{T}_{{X}}({\mathfrak{S}})}} \rightarrow {{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}}}

Let

X_0 = \{x \in X \mid {{x}_{\operatorname{arity}}} = 0\}

. To deﬁne

\alpha

, we ﬁrst deﬁne a function

\alpha' : {{{\mathcal{T}_{{X}}({\mathfrak{S}})} \times ({{X_0} ↪ {\mathbb{N}}})} \rightarrow {{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}}}

which keeps track of the current mapping of bound variables to de Bruijn indices:

\begin{array}{rcl} \alpha'(x[{t_0, \ldots, t_{n-1}}], \eta) & = & x[\alpha'(t_0, \eta), \ldots, \alpha'(t_{n - 1}, \eta)] \\ & & \text{if}\ \eta\ \text{is undefined at}\ x \\[0.5em] \alpha'(x, \eta) & = & \uparrow\hspace{-0.15em}{{\eta(x)}} \\ & & \text{if}\ \eta\ \text{is defined at}\ x\\[0.5em] \alpha'((a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1}), \eta) & = & (a\, t'_0 \ldots t'_{n-1}) \\ \text{where the shape of}\ a &=& (m; {p_0, \ldots, p_{n-1}}) \\ \text{and for all }\ i \in {\overline{{n}}},\ t'_i & = & \alpha'(t_i, (\eta + m)[\overline{x_{p_i} \coloneqq p_i}]) \end{array}

For any partial function

f : {U ↪ {\mathbb{N}}}

and any

m \in \mathbb{N}

we deﬁne

f' = f + m

in the obvious way such that

f'(u) = f(u) + m

holds if

f

is deﬁned at

u \in U

Then we can deﬁne

\alpha

\alpha(t) = \alpha'(t, \emptyset)

Of particular interest are those elements of

{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

that are in the image of

\alpha

. We are also interested in (part of) the image of

\alpha'

\begin{array}{rcl} {\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} & = & \left\{ \alpha'(t, \eta) \mid (t, \eta) \in {\mathcal{T}_{{X}}({\mathfrak{S}})} \times ({{X_0} ↪ {{\overline{h}}}}) \right\} \\[0.5em] {\mathcal{B}_{{X}}({\mathfrak{S}})} & = & \bigcup_{h = 0}^\infty\, {\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} \end{array}

The image of

\alpha

therefore is

{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

. We call

{\mathcal{B}_{{X}}({\mathfrak{S}})}

the set of de Bruijn terms, and

{\mathcal{B}_{{X}}^{h}({\mathfrak{S}})}

is the set of de Bruijn terms with at most

h

holes.

Instead of deﬁning de Bruijn terms indirectly via

\alpha'

, it is easy to carve them out of de Bruijn preterms in a more direct fashion. For that we need the notion of free atoms

{\operatorname{FreeAtoms}(t)}

of a de Bruijn preterm

t \in {\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

\begin{array}{rcl} {\operatorname{FreeAtoms}(t)} & = & {\operatorname{FreeAtoms}_{0}(t)} \\[0.5em] {\operatorname{FreeAtoms}_{l}({\uparrow\hspace{-0.15em}{n}})} & = & \begin{cases} \emptyset & \text{if}\ n < l\\ \{n - l\} & \text{if}\ n \geq l \end{cases}\\[1.5em] {\operatorname{FreeAtoms}_{l}({x[{t_0, \ldots, t_{n-1}}]})} & = & \{x\} \cup \bigcup_{i=0}^{n-1} {\operatorname{FreeAtoms}_{l}({t_i})} \\[0.8em] {\operatorname{FreeAtoms}_{l}({(a\,t_0\ldots t_{n-1})})} & = & \bigcup_{i=0}^{n-1} {\operatorname{FreeAtoms}_{{l + m}}({t_i})} \\ & & \text{where}\ m\ \text{is the valence of}\ a \end{array}

De Bruijn terms

{\mathcal{B}_{{X}}({\mathfrak{S}})}

are then those de Bruijn preterms

t

such that for every subpreterm of

t

of the form

(a\,t_0 \ldots t_{n-1})

the inclusion

{\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}}

holds for all

i \in {\overline{n}}

. Here the shape of

a

(m; {p_0, \ldots, p_{n-1}})

Note that an immediate consequence of this characterisation is that every subterm of a de Bruijn term is also a de Bruijn term.

Furthermore, note that

{\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} = \left\{ t \in {\mathcal{B}_{{X}}({\mathfrak{S}})} \mid {\operatorname{FreeAtoms}(t)}\,\cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq\, \uparrow\hspace{-0.15em}{{{\overline{h}}}} \right\}

$\alpha$ -Equivalence

We say that two terms

s

and

t

{\mathcal{T}_{{X}}({\mathfrak{S}})}

are $\alpha$ -equivalent iff

\alpha(s) = \alpha(t)

The importance of

\alpha

-equivalence stems from the fact that it is the same as semantical equivalence. We call

s

and

t

{\mathcal{T}_{{X}}({\mathfrak{S}})}

semantically equivalent iff for any abstraction algebra

(U; I; \mathfrak{S})

, and for any valuation

\nu \in {\includegraphics[height=0.5em]{F47FEC58-3FC9-437D-8276-F73D733DA708}}({X}, U)

, we have

\nu(s) = \nu(t)

We ﬁrst show that

\alpha

-equivalence implies semantical equivalence.

To this end, we deﬁne valuations also on de Bruijn terms. Given a set

F

of variables and a subset

N

\mathbb{N}

, a de Bruijn valuation

\nu

F\, \cup \uparrow\hspace{-0.15em}{{N}}

U

is a mapping such that

\nu

is a valuation of

F

U

, and additionally,

\nu

assigns to each

\uparrow\hspace{-0.15em}{{n}}

an element

\nu(\uparrow\hspace{-0.15em}{{n}}) \in U

for all

n \in N

Any valuation

\nu

{\operatorname{FreeAtoms}({t})}

U

determines an element

{\nu}\llbracket{t}\rrbracket \in U

\begin{array}{rcl} {\nu}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket & = & \nu(\uparrow\hspace{-0.15em}{n}) \\[0.5em] {\nu}\llbracket{{x[{t_0, \ldots, t_{n-1}}]}}\rrbracket & = & \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)\\[0.5em] {\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket & = & I(a)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)\\ & & \text{if the valence of}\ a\ \text{is}\ 0 \\[0.5em] {\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket & = & I'(a)(f_0, \ldots, f_{n-1})\\ & & \text{if the valence of}\ a\ \text{is}\ m \geq 1 \\ \text{where}\ f_i({u_0, \ldots, u_{m-1}})& = & {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket\\ & & \text{for all}\ ({u_0, \ldots, u_{m-1}}) \in U^m \end{array}

Here

I'

is a slight modiﬁcation of the interpretation

I

in that where

I(a)

expects an element

e \in U

as one of its arguments,

I'(a)

will accept a constant function

({u_0, \ldots, u_{m-1}}) \mapsto e

instead. Otherwise,

I'

and

I

are identical.

The valuation

\uparrow^{m}\hspace{-0.15em}({\nu})

is derived from

\nu

via

\begin{array}{rcll} \uparrow^{m}\hspace{-0.15em}({\nu})(x) & = & \nu(x) & \text{where}\ x \in X \\ \uparrow^{m}\hspace{-0.15em}({\nu})(\uparrow\hspace{-0.15em}{{(m + n)}}) & = & \nu(\uparrow\hspace{-0.15em}{n}) & \text{where}\ n \in \mathbb{N} \end{array}

In the above the left hand sides are deﬁned iff the right hand sides are deﬁned.

It is not immediately obvious that

{\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket

is well-deﬁned, because in order to be able to apply

I'(a)

({f_0, \ldots, f_{n-1}})

, the

f_i

cannot be just any functions in

{{U^m} \rightarrow U}

. Assuming that the shape of

a

(m; {p_0, \ldots, p_{n-1}})

, if

p_i = \emptyset

f_i

must be a constant function, and for

p_i \neq \emptyset

f_i

needs to be in

{\mathcal{F}_{m}^{{p_i}}(U)}

. But this is easily seen to be the case, given that

{\nu'}\llbracket{t}\rrbracket \neq {\nu}\llbracket{t}\rrbracket

only holds if

\nu'

and

\nu

have a different assignment for some

q \in {\operatorname{FreeAtoms}(t)}

, and according to our earlier observation →,

{\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}}

Given a valuation

\nu \in {\includegraphics[height=0.5em]{B2734E0C-053C-4DC9-A5E3-B9B30088182A}}({X}, U)

, together with an injective function

\eta : {{X_0} ↪ {\mathbb{N}}}

, the corresponding de Bruijn valuation

\nu_\eta

is deﬁned as

\begin{array}{rcll} \nu_\eta(x) & = & \nu(x) & \text{where}\ x \in X \\ \nu_\eta(\uparrow\hspace{-0.15em}{n}) & = & \nu(x) & \text{where}\ \eta(x) = n \end{array}

We prove that for any term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

, any valuation

\nu \in {\includegraphics[height=0.5em]{A67B38AA-0E23-4CC7-8340-BB13C8F095C9}}({X}, U)

, and any injective

\eta : {{X_0} ↪ {\mathbb{N}}}

, we have

{\nu_\eta}\llbracket{{\alpha'(t, \eta)}}\rrbracket = {\nu}\llbracket{t}\rrbracket\quad

The proof is by induction over

t

Assume $t = x[{t_0, \ldots, t_{n-1}}]$ . Then ${\nu}\llbracket{t}\rrbracket = \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)$ .
- If $\eta$ is undeﬁned at $x$ then $t' = \alpha'(t, \eta) = x[\alpha'(t_0, \eta), \ldots, \alpha'(t_{n - 1}, \eta)]$ and furthermore, $\begin{array}{rcl} {\nu_\eta}\llbracket{{t'}}\rrbracket & = & \nu(x)({\nu_\eta}\llbracket{{\alpha'(t_0, \eta)}}\rrbracket, \ldots, {\nu_\eta}\llbracket{{\alpha'(t_{n - 1}, \eta)}}\rrbracket) \\ & = & \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket) \\ & = & {\nu}\llbracket{t}\rrbracket \end{array}$
- If $\eta$ is deﬁned at $x$ then $n = 0$ and $t' = \alpha'(t, \eta) =\, \uparrow\hspace{-0.15em}{{\eta(x)}}$ . Thus ${\nu_\eta}\llbracket{{t'}}\rrbracket = \nu_\eta(\uparrow\hspace{-0.15em}{{\eta(x)}}) = \nu(x) = {\nu}\llbracket{t}\rrbracket$
Assume $t = (a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ , and that the shape of $a$ is $(m; {p_0, \ldots, p_{n-1}})$ . Then ${\nu}\llbracket{t}\rrbracket = I'(a)(f_0, \ldots, f_{n-1})$ , where $f_i(u_0, \ldots, u_{m-1}) = {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]}\llbracket{{t_i}}\rrbracket$ Here $I'$ denotes the same interpretation modiﬁcation as before →.

On the other hand, $t' = \alpha'(t, \eta) = (a\, t'_0 \ldots t'_{n-1})$ , where $t'_i = \alpha'(t_i, (\eta + m)[\overline{x_{p_i} \coloneqq p_i}])$ Then ${\nu_\eta}\llbracket{{t'}}\rrbracket = {\nu_\eta}\llbracket{{(a\, t'_0 \ldots t'_{n-1})}}\rrbracket = I'(a)(f'_0, \ldots, f'_{n-1})$ where $f'_i(u_0, \ldots, u_{n-1}) =\, {\uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t'_i}}\rrbracket$ It remains to show that $f_i = f'_i$ holds for all $i \in {\overline{n}}$ .

Let $\xi = (\eta + m)[\overline{x_{p_i} \coloneqq p_i}]$ . Clearly, $\xi$ is injective. Then ${\mu_\xi}\llbracket{{t'_i}}\rrbracket = {\mu_\xi}\llbracket{{\alpha'(t_i, \xi)}}\rrbracket = {\mu}\llbracket{{t_i}}\rrbracket$ holds for any valuation $\mu : {{X} \rightarrow U}$ , in particular $\mu = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}]$ . Thus $\begin{array}{rcl} f_i({u_0, \ldots, u_{n-1}}) & = & {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]}\llbracket{{t_i}}\rrbracket \\ & = & {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]_\xi}\llbracket{{t'_i}}\rrbracket\\ & = & {\uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t'_i}}\rrbracket\\ & = & f'_i({u_0, \ldots, u_{n-1}}) \end{array}$ if we can show $L(q) = R(q)$ for all $q \in {\operatorname{FreeAtoms}({t'_i})}$ , where $\begin{array}{rcl} L & = & \nu[\overline{x_{p_i} \coloneqq u_{p_i}}]_\xi \\[0.5em] \text{and}\quad R & = & \, \uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}] \end{array}$

We show this by case distinction:
- Assume $x \in X$ . We can furthermore assume $x \neq x_k$ for all $k \in p_i$ , because $x_k \notin {\operatorname{FreeAtoms}({t'_i})}$ . Then $L(x) = \nu(x) = R(x)$ .
- Assume $i \in {\overline{{m}}}$ . We can assume $i \in p_i$ , because otherwise $\uparrow\hspace{-0.15em}{i} \notin {\operatorname{FreeAtoms}({t'_i})}$ . Then $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x)$ where $\xi(x) = i$ , which implies $x = x_i$ . Thus $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x_i) = u_i = R(\uparrow\hspace{-0.15em}{i})$ .
- Assume $i \in \mathbb{N} \setminus {\overline{{m}}}$ . Then $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x)$ where $\xi(x) = i$ , which implies $(\eta + m)(x) = i$ , and thus $\eta(x) = i - m$ and $x \neq x_k$ for all $k \in p_i$ . Thus $L(\uparrow\hspace{-0.15em}{i}) = \nu(x)$ where $\eta(x) = i - m$ . On the other hand, $R(\uparrow\hspace{-0.15em}{i}) =\, \uparrow^{m}\hspace{-0.15em}({\nu_\eta})(\uparrow\hspace{-0.15em}{i}) = \nu_\eta(\uparrow\hspace{-0.15em}{(}i - m)) = \nu(y)$ where $\eta(y) = i - m$ . From the injectivity of $\eta$ it follows that $L(\uparrow\hspace{-0.15em}{i}) = \nu(y) = R(\uparrow\hspace{-0.15em}{i})$ .

In particular, for

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

and

\nu \in {\includegraphics[height=0.5em]{070CF6F8-5A9F-4A22-8ACD-F5F6EFC19D5E}}({X}, U)

{\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket

An immediate consequence is that

\alpha

-equivalence implies semantical equivalence: Let

s

and

t

\alpha

-equivalent terms in

{\mathcal{T}_{{X}}({\mathfrak{S}})}

, i.e.

\alpha(s) = \alpha(t)

. Then for all valuations

\nu \in {\includegraphics[height=0.5em]{B9B27D46-49AE-4423-B5C6-F1730BE3FB1A}}({X}, U)

, we have

{\nu}\llbracket{s}\rrbracket = {\nu}\llbracket{{\alpha(s)}}\rrbracket = {\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket

Substitution

Before showing that semantical equivalence implies

\alpha

-equivalence in the next section →, we will ﬁrst consider how to perform substitution of (some of) the free atoms in a de Bruijn term.

A substitution is a function

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

with domain

D \subseteq X\, \cup \uparrow\hspace{-0.15em}{{\mathbb{N}}}

. Application

t / {\sigma}

of a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

to a de Bruijn term

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

is recursively deﬁned as follows:

\begin{array}{rcll} {\uparrow\hspace{-0.15em}{n}} / {\sigma} & = & \sigma(\uparrow\hspace{-0.15em}{n}) \\ & & \text{if}\ \uparrow\hspace{-0.15em}{n}\ \text{is in the domain of}\ \sigma \\[0.5em] {\uparrow\hspace{-0.15em}{n}} / {\sigma} & = & \uparrow\hspace{-0.15em}{n} \\ & & \text{if}\ \uparrow\hspace{-0.15em}{n}\ \text{is not in the domain of}\ \sigma \\[0.5em] {x[{t_0, \ldots, t_{n-1}}]} / {\sigma} & = & ({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq t'_0, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq t'_{n-1}]}) - n \\ & & \text{if}\ x\ \text{is in the domain of}\ \sigma;\\ & & \text{here}\ \emptyset\ \text{denotes the empty substitution}, \\ & & \text{and}\ t'_i = ({t_i} / {\sigma}) + n \\[0.5em] {x[{t_0, \ldots, t_{n-1}}]} / {\sigma} & = & x[{t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}] \\ & & \text{if}\ x\ \text{is not in the domain of}\ \sigma \\[0.5em] {(a\, t_0 \ldots t_{n-1})} / {\sigma} & = & (a\, t'_0 \ldots t'_{n-1})\ \text{where}\ t'_i =\, {t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})},\\ & & \text{given the valence of}\ a\ \text{is}\ m \end{array}

In the above deﬁnition we used the expression

t + z

for

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

and

z \in \mathbb{Z}

. This expression is only deﬁned if for all

\uparrow\hspace{-0.15em}{n} \in {\operatorname{FreeAtoms}(t)}

, we have

n + z \geq 0

. Then:

\begin{array}{rcll} t + z & = & t +_0 z &\\ \uparrow\hspace{-0.15em}{n} +_l z & = & \uparrow\hspace{-0.15em}{n} & \text{if}\ n < l \\ \uparrow\hspace{-0.15em}{n} +_l z & = & \uparrow\hspace{-0.15em}{{(n + z)}} & \text{if}\ n \geq l \\ x[{t_0, \ldots, t_{n-1}}] +_l z & = & x[t_0 +_l z, \ldots, t_{n-1} +_l z] \\ (a\, t_0 \ldots t_{n-1}) +_l z & = & (a\, (t_0 +_{l + m} z) \ldots (t_{n-1} +_{l + m} z)) \\ & & \text{where the valence of}\ a\ \text{is}\ m \end{array}

Furthermore, we deﬁne

\uparrow^{m}\hspace{-0.15em}({\sigma})

for a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

and

m \in \mathbb{N}

\begin{array}{rcll} \uparrow^{m}\hspace{-0.15em}({\sigma}) (x) & = & \sigma(x) +_{{x_{\operatorname{arity}}}} m & \text{for}\ x \in X \cap D \\ \uparrow^{m}\hspace{-0.15em}({\sigma}) (\uparrow\hspace{-0.15em}{{(m + n)}}) & = & \sigma(\uparrow\hspace{-0.15em}{n}) + m & \text{for} \uparrow\hspace{-0.15em}{n} \in D \end{array}

Then

\uparrow^{m}\hspace{-0.15em}({\sigma})

is a substitution with domain

(X \cap D) \cup \{\uparrow\hspace{-0.15em}{{(m + n)}} \mid\, \uparrow\hspace{-0.15em}{n} \in D\}

We deﬁne the free atoms of a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

\begin{array}{rcl} {\operatorname{FreeAtoms}({\sigma})} & = & \bigcup_{\uparrow n \in D} {\operatorname{FreeAtoms}({\sigma(\uparrow\hspace{-0.15em}{n})})} \\ & \cup & \bigcup_{x \in D \cap X} \{q - {{x}_{\operatorname{arity}}} \mid q \in {\operatorname{FreeAtoms}({\sigma(x)})} \setminus {\overline{{{{x}_{\operatorname{arity}}}}}})\} \end{array}

We call a substitution

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

regular if

{\operatorname{FreeAtoms}({\sigma})} \subseteq X

For regular

\sigma

we have

\sigma(x) \in {\mathcal{B}_{{X}}^{{{x_{\operatorname{arity}}}}}({\mathfrak{S}})}

for all

x \in D \cap X

and

\sigma(\uparrow\hspace{-0.15em}{n}) \in {\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

for all

\uparrow\hspace{-0.15em}{n} \in D

Note that if

\sigma

is regular, then

\uparrow^{m}\hspace{-0.15em}({\sigma})

is regular, too.

Given a de Bruijn valuation

\nu

F

U

, any regular substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

with

{\operatorname{FreeAtoms}({\sigma})} \subseteq F

induces a de Bruijn valuation

\nu_\sigma

F \cup D

U

via

\begin{array}{rcl} \nu_\sigma(q) & = & \nu(q) \\ & & \text{if}\ q \in F \setminus D \\[0.5em] \nu_\sigma(\uparrow\hspace{-0.15em}{n}) & = & {\nu}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{n})}}\rrbracket\\ & & \text{if}\ \uparrow\hspace{-0.15em}{n} \in D \\[0.5em] \nu_\sigma(x) & = & {\nu}\llbracket{{\sigma(x)}}\rrbracket\\ & & \text{if}\ x \in D \cap X_0 \\[0.5em] \nu_\sigma(x) & = & ({u_0, \ldots, u_{n-1}}) \mapsto\, {\nu[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq u_{n-1}]}\llbracket{{\sigma(x)}}\rrbracket \\ & & \text{if}\ x \in D \cap X \ \text{and where}\ {x_{\operatorname{arity}}} = n > 0 \end{array}

The following holds for any

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

with

{\operatorname{FreeAtoms}(t)} \subseteq F \cup D

{\nu}\llbracket{{t / {\sigma}}}\rrbracket = {\nu_\sigma}\llbracket{t}\rrbracket

We prove this by induction on

t

Assume $t =\, \uparrow\hspace{-0.15em}{n}$ . If $\uparrow\hspace{-0.15em}{n} \in F \setminus D$ , then ${\nu_\sigma}\llbracket{t}\rrbracket = {\nu_\sigma}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket = \nu(\uparrow\hspace{-0.15em}{n}) = {\nu}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket = {\nu}\llbracket{{{\uparrow\hspace{-0.15em}{n}} / {\sigma}}}\rrbracket = {\nu}\llbracket{{t / {\sigma}}}\rrbracket$ If $\uparrow\hspace{-0.15em}{n} \in D$ , then ${\nu_\sigma}\llbracket{t}\rrbracket = {\nu_\sigma}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket = {\nu}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{n})}}\rrbracket = {\nu}\llbracket{{{\uparrow\hspace{-0.15em}{n}} / {\sigma}}}\rrbracket = {\nu}\llbracket{{t / {\sigma}}}\rrbracket$
Assume $t = x \in X_0$ . If $x \in F \setminus D$ , then ${\nu_\sigma}\llbracket{t}\rrbracket = {\nu_\sigma}\llbracket{{x}}\rrbracket = \nu(x) = {\nu}\llbracket{x}\rrbracket = {\nu}\llbracket{{{x} / {\sigma}}}\rrbracket = {\nu}\llbracket{{t / {\sigma}}}\rrbracket$ If $x \in D$ , then ${\nu_\sigma}\llbracket{t}\rrbracket = {\nu_\sigma}\llbracket{{x}}\rrbracket = {\nu}\llbracket{{\sigma(x)}}\rrbracket = {\nu}\llbracket{{{x} / {\sigma}}}\rrbracket = {\nu}\llbracket{{t / {\sigma}}}\rrbracket$
Assume $t = x[{t_0, \ldots, t_{n-1}}]$ for $n > 0$ . If $x \in F \setminus D$ , then $\begin{array}{l} {\nu_\sigma}\llbracket{t}\rrbracket \\ \quad = {\nu_\sigma}\llbracket{{x[{t_0, \ldots, t_{n-1}}]}}\rrbracket \\ \quad = \nu_\sigma(x)({\nu_\sigma}\llbracket{{t_0}}\rrbracket, \ldots, {\nu_\sigma}\llbracket{{t_{n-1}}}\rrbracket) \\ \quad = \nu(x)({\nu}\llbracket{{{t_0} / {\sigma}}}\rrbracket, \ldots, {\nu}\llbracket{{{t_{n-1}} / {\sigma}}}\rrbracket) \\ \quad = {\nu}\llbracket{{x[{t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}]}}\rrbracket \\ \quad = {\nu}\llbracket{{{x[{t_0, \ldots, t_{n-1}}]} / {\sigma}}}\rrbracket \\ \quad = {\nu}\llbracket{{t / {\sigma}}}\rrbracket \end{array}$ If $x \in D$ , then $\begin{array}{l} {\nu_\sigma}\llbracket{t}\rrbracket \\ \quad = {\nu_\sigma}\llbracket{{x[{t_0, \ldots, t_{n-1}}]}}\rrbracket \\ \quad = \nu_\sigma(x)({\nu_\sigma}\llbracket{{t_0}}\rrbracket, \ldots, {\nu_\sigma}\llbracket{{t_{n-1}}}\rrbracket) \\[0.3em] \quad = {\nu[\uparrow\hspace{-0.15em}{0} \coloneqq {{\nu}\llbracket{{{t_0} / {\sigma}}}\rrbracket}, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq {{\nu}\llbracket{{{t_{n-1}} / {\sigma}}}\rrbracket}]}\llbracket{{\sigma(x)}}\rrbracket \\[0.3em] \quad = {\nu}\llbracket{{({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq {({t_0} / {\sigma})}, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq ({t_{n-1}} / {\sigma})])}}}\rrbracket\\[0.3em] \quad = {\nu}\llbracket{{{x[{t_0, \ldots, t_{n-1}}]} / {\sigma}}}\rrbracket \\[0.3em] \quad = {\nu}\llbracket{{t / {\sigma}}}\rrbracket \end{array}$
Assume $t = (a\, t_0 \ldots t_{n-1})$ where the valence of $a$ is $m$ . Then $\begin{array}{l} {\nu_\sigma}\llbracket{t}\rrbracket \\ \quad = {\nu_\sigma}\llbracket{{(a\, t_0 \ldots t_{n-1})}}\rrbracket \\ \quad = I'(a)({f_0, \ldots, f_{n-1}}) \\ \text{where}\ f_i({u_0, \ldots, u_{m-1}}) =\, {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket\\ \quad = I'(a)({g_0, \ldots, g_{n-1}}) \\ \text{where}\ g_i({u_0, \ldots, u_{m-1}}) =\, {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{({t_{i}} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})}}\rrbracket \\ \quad = {\nu}\llbracket{{(a\, {({t_0} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})} \ldots {({t_{n-1}} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})})}}\rrbracket \\ \quad = {\nu}\llbracket{{{(a\, t_0 \ldots t_{n-1})} / {\sigma}}}\rrbracket \\ \quad = {\nu}\llbracket{{{t} / {\sigma}}}\rrbracket \\ \end{array}$

We need to show $f_i({u_0, \ldots, u_{m-1}}) = g_i({u_0, \ldots, u_{m-1}})$ : $\begin{array}{l} g_i({u_0, \ldots, u_{m-1}}) \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{({t_{i}} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})}}\rrbracket \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}\llbracket{{t_i}}\rrbracket \\ \quad = {\zeta}\llbracket{{t_i}}\rrbracket \quad \text{where}\ \zeta = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}\\ \quad = {\xi}\llbracket{{t_i}}\rrbracket \quad \text{where}\ \xi = {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket \\ \quad = f_i({u_0, \ldots, u_{m-1}}) \end{array}$

Finally, we need to prove that the two valuations $\zeta$ and $\xi$ are the same for $t_i$ . We do this by case analysis of $q \in {\operatorname{FreeAtoms}({t_i})}$ in the equation $\zeta(q) = \xi(q)$ :
- Assume $q = x \in X$ and $x \in F \setminus D$ . Then $\zeta(x) = \nu(x) = \nu_\sigma(x) = \xi(x)$
- Assume $q = x \in X_0$ and $x \in D$ . Then $\begin{array}{l} \zeta(x) \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])}\llbracket{{{\uparrow^{m}\hspace{-0.15em}({\sigma})}(x)}}\rrbracket\\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])}\llbracket{{\sigma(x) + m}}\rrbracket \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu}))}\llbracket{{\sigma(x) + m}}\rrbracket \\ \quad = {\nu}\llbracket{{\sigma(x)}}\rrbracket = \nu_\sigma(x) = \xi(x) \end{array}$
- Assume $q = x \in X \setminus X_0$ and $x \in D$ . Let $r = {x_{\operatorname{arity}}}$ . Then $\begin{array}{l} \zeta(x)({w_0, \ldots, w_{r-1}}) \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}(x)({w_0, \ldots, w_{r-1}}) \\ \quad = {\rho[\uparrow\hspace{-0.15em}{0} \coloneqq w_0, \ldots, \uparrow\hspace{-0.15em}{{(r-1)}} \coloneqq w_{r-1}]}\llbracket{{\uparrow^{m}\hspace{-0.15em}({\sigma})(x)}}\rrbracket \\ \quad \quad \text{where}\ \rho =\, \uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}] \\ \quad = {\rho[\uparrow\hspace{-0.15em}{0} \coloneqq w_0, \ldots, \uparrow\hspace{-0.15em}{{(r-1)}} \coloneqq w_{r-1}]}\llbracket{{\sigma(x) +_r m}}\rrbracket \\ \quad = {\rho[\uparrow\hspace{-0.15em}{0} \coloneqq w_0, \ldots, \uparrow\hspace{-0.15em}{{(r-1)}} \coloneqq w_{r-1}]}\llbracket{{\sigma(x)}}\rrbracket \\ \quad = {\nu[\uparrow\hspace{-0.15em}{0} \coloneqq w_0, \ldots, \uparrow\hspace{-0.15em}{{(r-1)}} \coloneqq w_{r-1}]}\llbracket{{\sigma(x)}}\rrbracket \\ \quad = \nu_\sigma(x)({w_0, \ldots, w_{r-1}}) \\ \quad = (\uparrow^{m}\hspace{-0.15em}({\nu_\sigma}))(x)({w_0, \ldots, w_{r-1}})\\ \quad = \xi(x)({w_0, \ldots, w_{r-1}}) \end{array}$ Note that the regularity of $\sigma$ is of crucial importance for this case.
- Assume $q =\, \uparrow\hspace{-0.15em}{k}$ for $k < m$ . Then $\begin{array}{l} \zeta(\uparrow\hspace{-0.15em}{k}) \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}(\uparrow\hspace{-0.15em}{k}) \\ \quad = (\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])(\uparrow\hspace{-0.15em}{k}) \\ \quad = u_k \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}(\uparrow\hspace{-0.15em}{k}) \\ \quad = \xi(\uparrow\hspace{-0.15em}{k}) \end{array}$
- Assume $q =\, \uparrow\hspace{-0.15em}{k}$ for $k \geq m$ . Because of $\uparrow\hspace{-0.15em}{k} \in {\operatorname{FreeAtoms}({t_i})}$ we know $\uparrow\hspace{-0.15em}{{(k - m)}} \in F \cup D$
  
  For $\uparrow\hspace{-0.15em}{{(k - m)}} \in D$ follows: $\begin{array}{l} \zeta(\uparrow\hspace{-0.15em}{k}) \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}(\uparrow\hspace{-0.15em}{k}) \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{\uparrow^{m}\hspace{-0.15em}({\sigma})(\uparrow\hspace{-0.15em}{k})}}\rrbracket \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{{(k-m)}}) + m}}\rrbracket \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu})}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{{(k-m)}}) + m}}\rrbracket \\ \quad = {\nu}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{{(k - m)}})}}\rrbracket\\ \quad = \nu_\sigma(\uparrow\hspace{-0.15em}{{(k - m)}}) \\ \quad =\, \uparrow^{m}\hspace{-0.15em}({\nu_\sigma})(\uparrow\hspace{-0.15em}{k})\\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}(\uparrow\hspace{-0.15em}{k}) \\ \quad = \xi(\uparrow\hspace{-0.15em}{k}) \end{array}$
  
  For $\uparrow\hspace{-0.15em}{{(k - m)}} \in F \setminus D$ follows: $\begin{array}{l} \zeta(\uparrow\hspace{-0.15em}{k}) \\ \quad = {(\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}])_{\uparrow^{m}\hspace{-0.15em}({\sigma})}}(\uparrow\hspace{-0.15em}{k}) \\ \quad =\, \uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}](\uparrow\hspace{-0.15em}{k}) \\ \quad = \uparrow^{m}\hspace{-0.15em}({\nu})(\uparrow\hspace{-0.15em}{k}) \\ \quad = \nu(\uparrow\hspace{-0.15em}{{(k - m)}}) \\ \quad = \nu_\sigma(\uparrow\hspace{-0.15em}{{(k - m)}}) \\ \quad =\, \uparrow^{m}\hspace{-0.15em}({\nu_\sigma})(\uparrow\hspace{-0.15em}{k})\\ \quad = {\uparrow^{m}\hspace{-0.15em}({\nu_\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}(\uparrow\hspace{-0.15em}{k}) \\ \quad = \xi(\uparrow\hspace{-0.15em}{k}) \end{array}$

De Bruijn Abstraction Algebra

Given an abstraction signature

\mathfrak{S}

and a set of variables

X

, we deﬁne an abstraction algebra

\mathfrak{B}_{{X}}({\mathfrak{S}}) = (U; I; \mathfrak{S})

such that

\begin{array}{rcl} U & = & {\mathcal{B}_{{X}}({\mathfrak{S}})} \uplus \{\star\} \end{array}

The symbol

\star

represents an undeﬁned value.

To deﬁne the interpretation

I

, let us ﬁrst deﬁne functions

\Psi_h : {{{\mathcal{B}_{{X}}({\mathfrak{S}})}} \rightarrow {({{U^h} \rightarrow U})}}

for

h \in \mathbb{N}

and

h > 0

via

\begin{array}{rcl} \Psi_h(t)({u_0, \ldots, u_{h-1}}) & = &(t / {\emptyset[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0} + h, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}} + h]}) - h\\ & & \text{where}\ \uparrow\hspace{-0.15em}{{{\overline{h}}}} \cap {\operatorname{FreeAtoms}(t)} =\, \uparrow\hspace{-0.15em}{{{\langle {j_0, \ldots, j_{l-1}} \rangle}}} \\ & & \text{and where}\ u_i \neq \star \ \text{for all}\, i \in {\langle {j_0, \ldots, j_{l-1}} \rangle} \\[0.5em] \Psi_h(t)({u_0, \ldots, u_{h-1}}) & = & \star \\ & & \text{if}\ u_i = \star \ \text{for some}\ \uparrow\hspace{-0.15em}{i} \in\, \uparrow\hspace{-0.15em}{{{\overline{h}}}} \cap {\operatorname{FreeAtoms}(t)} \end{array}

It is easy to see that

\Psi_h

is injective: Assume

s, t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

and

s \neq t

. Then

s

and

t

must differ at some topmost position. If both

s

and

t

contain in that position only abstractions, variables, or de Bruijn indices not corresponding to one of the

h

function arguments, then this difference will survive the substitution. If only one of them contains a function argument de Bruijn index, then just vary the corresponding argument to produce a difference. If both contain function argument de Bruijn indices, then the indices must be different, so just pass different arguments for those two indices to produce a difference.

Assume now

a

is an abstraction of shape

(m; {p_0, \ldots, p_{n-1}})

. What is

I(a)

If $n = 0$ , then $I(a) = a$ .
If $m = 0$ and $n > 0$ , then $I(a) = ({u_0, \ldots, u_{n-1}}) \mapsto \begin{cases} (a\, u_0 \ldots u_{n-1}) & \text{if}\ u_i \neq \star \ \text{for all}\ i \in {\overline{n}} \\ \star & \text{if}\ u_i = \star \ \text{for some}\ i \in {\overline{n}} \end{cases}$
If $m > 0$ (and therefore also $n > 0$ ), then $I(a) = ({f_0, \ldots, f_{n-1}}) \mapsto \begin{cases} (a\, t_0 \ldots t_{n-1}) & \text{if}\ t_i \neq \star \ \text{for all}\ i \in {\overline{n}} \\ \star & \text{if}\ t_i = \star \ \text{for some}\ i \in {\overline{n}} \end{cases}$ Here $t_i$ is the result of trying to convert $f_i \in {\mathcal{F}_{m}^{{p_i}}(U)}$ into an element of ${\mathcal{B}_{{X}}({\mathfrak{S}})}$ such that ${\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq p_i$ . If the conversion fails, we have $t_i = \star$ .
- If $p_i = \emptyset$ , then $f_i \in U$ , and therefore we set $t_i = f_i$ .
- If $p_i \neq \emptyset$ , then $f_i \in {{U^m} \rightarrow U}$ . There is at most one $s$ such that $\Psi_m(s) = f_i$ . If such an $s$ exists, we set $t_i = s$ , otherwise we set $t_i = \star$ . Note that if $s$ exists, then necessarily ${\operatorname{FreeAtoms}({s})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq p_i$ , because otherwise $\Psi_m(s) \notin {\mathcal{F}_{m}^{{p_i}}(U)}$ .

We call

\mathfrak{B}_{{X}}({\mathfrak{S}})

the de Bruijn Abstraction Algebra for

\mathfrak{S}

and

X

There is a straightforward relationship between valuation in

\mathfrak{B}_{{X}}({\mathfrak{S}})

and substitution. To state this relationship we need the notion of strict valuation. This is a valuation

\nu : {D \rightarrow U}

such that for all

x \in D \cap X

with

{{x}_{\operatorname{arity}}} > 0

\nu(x)({u_0, \ldots, u_{{{{x}_{\operatorname{arity}}}}-1}}) = \star \quad\text{if}\ u_i = \star\ \text{for some}\ i \in {\overline{{{{x}_{\operatorname{arity}}}}}}

We need strict valuations because they possess the following property. Given a term

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

with

{\operatorname{FreeAtoms}(t)} \subseteq D

, then

{\nu}\llbracket{t}\rrbracket = \star \quad \text{if}\ \nu(q) = \star\ \text{for some}\ q \in {\operatorname{FreeAtoms}(t)}

We prove this by induction over

t

Let $t =\, \uparrow\hspace{-0.15em}{n}$ . Then $\uparrow\hspace{-0.15em}{n}$ is the only free atom in $t$ , and thus ${\nu}\llbracket{t}\rrbracket = \nu(\uparrow\hspace{-0.15em}{n}) = \star$ .
Let $t = x \in X_0$ . Then $x$ is the only free atom in $t$ , and thus ${\nu}\llbracket{t}\rrbracket = \nu(x) = \star$ .
Let $t = x[{t_0, \ldots, t_{n-1}}]$ with $n > 0$ . We have ${\nu}\llbracket{t}\rrbracket = \nu(x)(\nu(t_0), \ldots, \nu(t_{n-1}))$ . Because $\nu(x)$ is a function, it cannot be that $\nu(x) = \star$ , and thus at least one of the $t_i$ , say $t_0$ , must contain the free atom $q$ with $\nu(q) = \star$ . Thus $\nu(t_0) = \star$ . From the strictness of $\nu$ follows ${\nu}\llbracket{t}\rrbracket = \nu(x)(\nu(t_0), \nu(t_1), \ldots, \nu(t_{n-1})) = \nu(x)(\star, \nu(t_1), \ldots, \nu(t_{n-1})) = \star$
Let $t = (a\,t_0 \ldots t_{n-1})$ where the valence of $t$ is zero. Again, we assume that $t_0$ contains the free atom $q$ with $\nu(q) = \star$ . Then ${\nu}\llbracket{{t_0}}\rrbracket = \star$ and ${\nu}\llbracket{t}\rrbracket = I(a)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket) = I(a)(\star, \ldots) = \star$
Let $t = (a\,t_0 \ldots t_{n-1})$ where the valence of $t$ is $m > 0$ . We can assume that $t_0$ contains a free atom $q'$ such that ${\uparrow^{m}\hspace{-0.15em}({\nu})}\llbracket{{q'}}\rrbracket = \star$ and $q \notin\, \uparrow\hspace{-0.15em}{{{\overline{m}}}}$ . Then ${\nu}\llbracket{t}\rrbracket = I'(a)({f_0, \ldots, f_{n-1}})$ where $f_i({u_0, \ldots, u_{m-1}}) = {\nu_i}\llbracket{{t_i}}\rrbracket$ and $\nu_i =\, \uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]$ The valuations $\nu_i$ are strict, because $\nu$ is strict, and furthermore $\nu_i(q') = \star$ . Thus ${\nu_0}\llbracket{{t_0}}\rrbracket = \star$ , and therefore $f_0$ is a function with constant value $\star$ . Thus ${\nu}\llbracket{t}\rrbracket = I'(a)(f_0, \ldots) = \star$

Given a substitution

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

, we can view it as a de Bruijn valuation

\sigma'

D

U

as follows:

\begin{array}{rcll} \sigma'(\uparrow\hspace{-0.15em}{n}) & = & \sigma(\uparrow\hspace{-0.15em}{n}) & \text{if}\ \uparrow\hspace{-0.15em}{n} \in D\\ \sigma'(x) & = & \sigma(x) & \text{if}\ x \in X_0 \cap D \\ \sigma'(x) & = & \Psi_{{x_{\operatorname{arity}}}}(\sigma(x)) & \text{if}\ x \in X \cap D\ \text{and}\ {x_{\operatorname{arity}}} > 0 \end{array}

We call

\sigma

a strict substitution if

\sigma'

is a strict valuation. An equivalent characterisation of a strict substitution

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

is that for all

x \in D \cap X

{\operatorname{FreeAtoms}({\sigma(x)})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{{{x_{\operatorname{arity}}}}}}}} =\, \uparrow\hspace{-0.15em}{{{\overline{{{x_{\operatorname{arity}}}}}}}}

Applying a strict substitution

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

to a term

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

with

{\operatorname{FreeAtoms}(t)} \subseteq D

is the same as applying the valuation

\sigma'

t

{\sigma'}\llbracket{t}\rrbracket = t / {\sigma}

We prove this by induction over

t

Assume $t = x$ where $x \in X_0$ . Then $x \in {\operatorname{FreeAtoms}(x)} \subseteq D$ and ${\sigma'}\llbracket{x}\rrbracket = \sigma(x) = x / {\sigma}$
Assume $t = x[{t_0, \ldots, t_{n-1}}]$ and $n > 0$ . Then $x \in {\operatorname{FreeAtoms}(x)} \subseteq D$ and $\begin{array}{rcl} {\sigma'}\llbracket{t}\rrbracket & = & \sigma'(x)({\sigma'}\llbracket{{t_0}}\rrbracket, \ldots, {\sigma'}\llbracket{{t_{n-1}}}\rrbracket)\\ & = & \sigma'(x)({t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}) \\ & = & \Psi_n(\sigma(x))({t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}) \\ & = & ({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq ({t_{j_0}} / {\sigma}) + n, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq ({t_{j_{l-1}}} / {\sigma}) + n]}) - n \\ & & \text{where}\ \uparrow\hspace{-0.15em}{{{\langle {j_0, \ldots, j_{l-1}} \rangle}}} = {\operatorname{FreeAtoms}({\sigma(x)})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{n}}}} \\ & = & ({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq ({t_0} / {\sigma}) + n, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq ({t_{n-1}} / {\sigma}) + n]}) - n \\ & = & {(x[{t_0, \ldots, t_{n-1}}])} / {\sigma} \\ & = & t / {\sigma} \end{array}$
Assume $t =\, \uparrow\hspace{-0.15em}{n}$ . Then $\uparrow\hspace{-0.15em}{n} \in {\operatorname{FreeAtoms}(t)} \subseteq D$ and ${\sigma'}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket = \sigma'(\uparrow\hspace{-0.15em}{n}) = \sigma(\uparrow\hspace{-0.15em}{n}) = {\uparrow\hspace{-0.15em}{n}} / {\sigma}$
Assume $t = (a\, t_0 \ldots t_{n-1})$ where the valence of $a$ is $0$ . Then $\begin{array}{rcl} {\sigma'}\llbracket{t}\rrbracket & = & {\sigma'}\llbracket{{(a\, t_0 \ldots t_{n-1})}}\rrbracket \\ & = & I(a)({\sigma'}\llbracket{{t_0}}\rrbracket, \ldots, {\sigma'}\llbracket{{t_{n-1}}}\rrbracket) \\ & = & I(a)({t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}) \\ & = & (a\, {t_0} / {\sigma} \ldots {t_{n-1}} / {\sigma}) \\ & = & {(a\, t_0 \ldots t_{n-1})} / {\sigma} \\ & = & t / {\sigma} \end{array}$
Assume $t = (a\, t_0 \ldots t_{n-1})$ where the shape of $a$ is $(m; {p_0, \ldots, p_{n-1}})$ and $m> 0$ : $\begin{array}{rcl} {\sigma'}\llbracket{t}\rrbracket & = & {\sigma'}\llbracket{{(a\, t_0 \ldots t_{n-1})}}\rrbracket \\ & = & I'(a)({f_0, \ldots, f_{n-1}}) \\ & = & (a\, s_0 \ldots s_{n-1}) \\ & \overset{(*)}{=} & (a\, t'_0 \ldots t'_{n-1}) \\ & = & {(a\, t_0 \ldots t_{n-1})} / {\sigma} \\ & = & t / {\sigma} \end{array}$ Here we have $\begin{array}{rcl} f_i({u_0, \ldots, u_{m-1}}) & = & {\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket \\ \Psi_m(s_i) & = & f_i\quad\text{if}\ s\ \text{exists with}\ \Psi_m(s) = f_i \\ t'_i & = & {t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})} \end{array}$ We need to show $(*)$ , i.e. $s_i = t'_i$ for all $i \in {\overline{n}}$ . This is true if $\Psi_m(t'_i) = f_i$ .

Let ${\langle {j_0, \ldots, j_{l-1}} \rangle} = {\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}}$ . Note that then also ${\langle {j_0, \ldots, j_{l-1}} \rangle} = {\operatorname{FreeAtoms}({t'_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}}$ .
- Assume $u_k \in U \setminus \{\star\}$ for all $k \in {\langle {j_0, \ldots, j_{l-1}} \rangle}$ . Then $\begin{array}{l} \Psi_m(t'_i)(u_0, \ldots, u_{m-1}) \\ \quad = ({t'_i} / {\emptyset[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0} + m, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}} + m]}) - m \\ \quad = ({({t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})} / {\emptyset[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0} + m, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}} + m]}) - m \\ \quad = {t_i} / {\rho} \\ \quad = {\rho'}\llbracket{{t_i}}\rrbracket \\ \quad \overset{(**)} = {\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}]}\llbracket{{t_i}}\rrbracket \\ \quad = {\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket \\ \quad = f_i({u_0, \ldots, u_{m-1}}) \end{array}$ Here we deﬁne the substitution $\rho$ by $\begin{array}{rcll} \rho(x) & = & \sigma(x) & \text{for}\ x \in X \cap D \\ \rho(\uparrow\hspace{-0.15em}{{(m + n)}}) & = & \sigma(\uparrow\hspace{-0.15em}{n}) & \text{for}\ \uparrow\hspace{-0.15em}{n} \in D \\ \rho(\uparrow\hspace{-0.15em}{k}) & = & u_k & \text{for}\ k \in {\langle {j_0, \ldots, j_{l-1}} \rangle} \end{array}$ We still need to show $(**)$ , i.e. $\rho'(q) = (\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}])(q)$ for all $q \in {\operatorname{FreeAtoms}({t_i})}$ :
  - Assume $q = x$ for $x \in X_0 \cap D$ . Then $\begin{array}{l} \rho'(x) = \rho(x) = \sigma(x) \\ \quad = \sigma'(x) = (\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}])(x) \end{array}$
  - Assume $q = x$ for $x \in (X \setminus X_0) \cap D$ . Then $\begin{array}{l} \rho'(x) = \Psi_{{x_{\operatorname{arity}}}}(\rho(x)) = \Psi_{{x_{\operatorname{arity}}}}(\sigma(x)) = \sigma'(x) \\ \quad = (\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}])(x) \end{array}$
  - Assume $q =\, \uparrow\hspace{-0.15em}{k}$ for $k \in {\langle {j_0, \ldots, j_{l-1}} \rangle}$ . Then $\begin{array}{l} \rho'(\uparrow\hspace{-0.15em}{k}) = \rho(\uparrow\hspace{-0.15em}{k}) = u_k \\ \quad = (\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}])(\uparrow\hspace{-0.15em}{k}) \end{array}$
  - Assume $q = \, \uparrow\hspace{-0.15em}{{(m+n)}}$ for $\uparrow\hspace{-0.15em}{n} \in D$ . Then $\begin{array}{l} \rho'(\uparrow\hspace{-0.15em}{{(m+n)}}) = \rho(\uparrow\hspace{-0.15em}{{(m+n)}}) = \sigma(\uparrow\hspace{-0.15em}{n})\\ \quad = \sigma'(\uparrow\hspace{-0.15em}{n})\\ \quad = (\uparrow^{m}\hspace{-0.15em}({\sigma'}))(\uparrow\hspace{-0.15em}{{(m + n)}}) \\ \quad = (\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{{j_0}} \coloneqq u_{j_0}, \ldots, \uparrow\hspace{-0.15em}{{j_{l-1}}} \coloneqq u_{j_{l-1}}])(\uparrow\hspace{-0.15em}{{(m + n)}}) \end{array}$
- Assume $u_k \in U$ for all $k \in {\overline{m}}$ and $u_h = \star$ for some $h \in {\langle {j_0, \ldots, j_{l-1}} \rangle}$ . Then $\begin{array}{l} \Psi_m(t'_i)(u_0, \ldots, u_{m-1}) \\ \quad = \star \\ \quad \overset{(***)} = {\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket \\ \quad = f_i({u_0, \ldots, u_{m-1}}) \end{array}$ Equation $(***)$ follows because for $\nu =\, \uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]$ we know that $\nu$ is strict and $\nu(\uparrow\hspace{-0.15em}{h}) = u_h = \star$ and $\uparrow\hspace{-0.15em}{h} \in {\operatorname{FreeAtoms}({t_i})}$ .

Consider now the strict substitution

\iota : {X \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

deﬁned by

\begin{array}{rcll} \iota(x) & = & x & \text{if}\ x \in X_0 \\ \iota(x) & = & x[\uparrow\hspace{-0.15em}{0}, \ldots, \uparrow\hspace{-0.15em}{{({{x}_{\operatorname{arity}}}-1)}}] & \text{if}\ x \in X \setminus X_0 \end{array}

Obviously

t / {\iota} = t

holds for all

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

, and thus also

{\iota'}\llbracket{t}\rrbracket = t / {\iota} = t

We call

\iota

the canonical substitution.

Assume two terms

s, t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

which are semantically equivalent. Then

\alpha(s) = {\iota'}\llbracket{{\alpha(s)}}\rrbracket = {\iota'}\llbracket{{s}}\rrbracket = {\iota'}\llbracket{{t}}\rrbracket = {\iota'}\llbracket{{\alpha(t)}}\rrbracket = \alpha(t)

and therefore

s

and

t

are

\alpha

-equivalent.

Thus semantical equivalence implies

\alpha

-equivalence. Together with our previous result that

\alpha

-equivalence implies semantical equivalence this means that semantical equivalence and

\alpha

-equivalence are equivalent.

Logic

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}'

A logic algebra is a tuple

\mathfrak{L} = (U; X; V; I; \mathfrak{S})

such that

$(U; I; \mathfrak{S})$ is an abstraction algebra.
$X$ is a set of variables, and $V$ is a non-empty subset of ${\includegraphics[height=0.5em]{5FA0A1F7-27C7-47B5-8076-B55802A33E1D}}({X}, U)$ such that:
- If $v \in V$ , $x \in X_0$ , $u \in U$ , then $v[x \coloneqq u] \in V$
- If $v \in V$ and $\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}$ is a regular substitution with $D \subseteq X$ , then $v_\sigma \in V$
$\mathfrak{S}$ is an extension of the signature ${\mathfrak{S}_0}$ , where ${\mathfrak{S}_0} = \left( \begin{array}{ccl} ⊤ & : & (0;) \\ ⇒ & : & (0; \{\}, \{\}) \\ ∀ & : & (1; \{0\}) \end{array} \right)$
$I(⇒)(I(⊤), b) = I(⊤)$ implies $b = I(⊤)$ for all $b \in U$ .
For all $f : {U \rightarrow U}$ , if $f(u) = I(⊤)$ for all $u \in U$ , then $I(∀)(f) = I(⊤)$ .

A logic algebra is called degenerate if

U

consists of a single element.

An abstraction logic

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

is a signature

\mathfrak{S}

together with a set of variables

X

and a set of axioms

{\mathbb{A}}

such that

$\mathfrak{S}$ is an extension of the signature ${\mathfrak{S}_0}$ .
$X$ is a set of variables with associated arities, such that both $X$ and $X_0$ are countably inﬁnite.
${\mathbb{A}}$ is a subset of ${\mathcal{T}_{{X}}({\mathfrak{S}})}$ .

An abstraction logic

{\mathcal{L}}' = (\mathfrak{S}'; X'; {\mathbb{A}}')

is called an extension of

{\mathcal{L}}

\mathfrak{S}'

is an extension of

\mathfrak{S}

and

X \subseteq X'

and

{\mathbb{A}} \subseteq {\mathbb{A}}'

We say that a logic algebra

(U; X; V; I; \mathfrak{S})

is a model for the term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

if for every valuation

\nu \in V

we have

{\nu}\llbracket{t}\rrbracket = I(⊤)

We furthermore say that a logic algebra is a model for the logic

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

if it is a model for all axioms

a \in {\mathbb{A}} \subseteq {\mathcal{T}_{{X}}({\mathfrak{S}})}

. Note that any abstraction algebra with

{|U|} = 1

and signature

\mathfrak{S}

induces a model for

{\mathcal{L}}

If every model of

{\mathcal{L}}

is also a model of

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

, then we say that

t

is valid in

{\mathcal{L}}

{\mathcal{L}} ⊨ t

Proofs

Given a logic

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

, a proof in

{\mathcal{L}}

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

is one of the following:

An axiom: $\operatorname{AX}(t)$ such that $t \in {\mathbb{A}}$ .
An application of substitution: $\operatorname{SUBST}(t, \sigma, p_s)$ where
- $p_s$ is proof of $s$ in ${\mathcal{L}}$
- $\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}$ is a regular substitution and $D \subseteq X$
- $\alpha(t) = {\alpha(s)} / {\sigma}$
A use 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 = (\text{⇒}.\, h\, t)$
Introduction of the universal quantiﬁer: $\operatorname{ALL}(t, x, p_s)$ where
- $x \in X_0$
- $p_s$ is a proof of $s$ in ${\mathcal{L}}$
- $t = (\text{∀} x.\, s)$

If there exists a proof of

t

{\mathcal{L}}

, we say that

t

is a theorem of

{\mathcal{L}}

{\mathcal{L}} ⊢ t

Soundness

Abstraction logic is sound, i.e. every theorem of

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

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

{\mathcal{L}}

, then

t

is valid in

{\mathcal{L}}

Assume $p = \operatorname{AX}(t)$ . Then $t \in {\mathbb{A}}$ 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 \in V$ for some logic algebra $(U; X; V; I;\mathfrak{S})$ . Then ${\nu}\llbracket{t}\rrbracket = {\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{{{\alpha(s)} / {\sigma}}}\rrbracket = {\nu_\sigma}\llbracket{{\alpha(s)}}\rrbracket$ Because $\nu_\sigma \in V$ , and $s$ is valid, ${\nu_\sigma}\llbracket{{\alpha(s)}}\rrbracket = {\nu_\sigma}\llbracket{s}\rrbracket = I(⊤)$ Together this yields ${\nu}\llbracket{t}\rrbracket = {\nu_\sigma}\llbracket{{\alpha(s)}}\rrbracket = 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 \in V$ for some logic algebra $(U; X; V; I;\mathfrak{S})$ . Then ${\nu}\llbracket{h}\rrbracket = I(⊤)$ and $I(⊤) = {\nu}\llbracket{g}\rrbracket = {\nu}\llbracket{{(\text{⇒}.\, h\, t)}}\rrbracket = I(\text{⇒})({\nu}\llbracket{h}\rrbracket, {\nu}\llbracket{t}\rrbracket) = I(\text{⇒})(I(⊤), {\nu}\llbracket{t}\rrbracket)$ This implies ${\nu}\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 \in V$ for some logic algebra $(U; X; V; I;\mathfrak{S})$ . Then ${\nu}\llbracket{t}\rrbracket = {\nu}\llbracket{{(\text{∀} x.\, s)}}\rrbracket = I(\text{∀})(f)$ Here $f: {U \rightarrow U}$ where $f(u) = {\nu[x \coloneqq u]}\llbracket{s}\rrbracket$ for all $u \in U$ . Because $\nu[x \coloneqq u] \in V$ and $s$ is valid, we have ${\nu[x \coloneqq u]}\llbracket{s}\rrbracket = I(⊤)$ and therefore $f(u) = I(⊤)$ for all $u$ . This implies ${\nu}\llbracket{t}\rrbracket = I(\text{∀})(f) = I(⊤)$

Several Abstraction Logics

In this section several abstraction logics of practical interest are introduced. We use convenient concrete syntax instead of pure abstraction syntax to present their axioms.

Deduction Logic

{\mathcal{L}}_D

has signature

\mathfrak{S}_D = {\mathfrak{S}_0}

and the following axioms

{\mathbb{A}}_D

$⊤$
$A ⇒ A$
$A ⇒ (B ⇒ A)$
$(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))$
$(∀ x.\,A[x]) ⇒ A[x]$
$(∀ x.\,A ⇒ B[x]) ⇒ (A ⇒ ∀ x.\, B[x])$

Axiom 1 might surprise, because one would expect it to apply only to truth values, not the entire universe. But because abstraction logic has only a single universe of discourse, every value must also be considered to be a truth value, because for any term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

one can ask the question: Is

t

true?

Using these axioms one can prove the following deduction theorem: Any proof of

A

{\mathcal{L}}^+ = (\mathfrak{S}, X, {\mathbb{A}} \cup \{\phi\})

can be translated into a proof of

\phi' ⇒ A

in the logic

{\mathcal{L}} = (\mathfrak{S}, X, {\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

{\operatorname{Free}({\phi})} = \{x_0, \ldots, x_{n-1}\}

In a system for machine-assisted theorem proving like Practal [2] it makes sense to bake in native support for

{\mathcal{L}}_D

so that moving theorems from

{\mathcal{L}}^+

{\mathcal{L}}

doesn’t necessarily involve the actual translation of proofs.

Deduction Logic with Equality

{\mathcal{L}}_E

extends

{\mathcal{L}}_D

by adding the equality abstraction

=

such that

\mathfrak{S}_E = \mathfrak{S}_D + \left(\begin{array}{ccl} = & : & (0; \emptyset, \emptyset)\end{array}\right)

It has axioms

{\mathbb{A}}_E

, adding the following axioms to

{\mathbb{A}}_D

$x = x$
$x = y ⇒ (A[x] ⇒ A[y])$
$A ⇒ (A = ⊤)$

Note that

(A = ⊤) ⇒ A

is then also a theorem in

{\mathcal{L}}_E

Deduction Logic with Equality and Falsity

{\mathcal{L}}_F

extends

{\mathcal{L}}_E

with falsity

⊥

and negation

¬

\mathfrak{S}_F = \mathfrak{S}_E + \left( \begin{array}{ccl} ⊥ & : & (0;)\\ ¬ & : & (0; \emptyset)\\ \end{array} \right)

Its set of axioms

{\mathbb{A}}_F

is obtained by adding the following axioms to

{\mathbb{A}}_E

$⊥ = (∀ x.\, x)$
$¬ A = (A ⇒ ⊥)$

Note that all of the following are theorems of

{\mathcal{L}}_F

$⊤ = ¬ ⊥$
$⊥ ⇒ A$
$A ⇒ (¬ A ⇒ ⊥)$

In particular,

{\mathcal{L}}_F

is certainly not paraconsistent as the principle of explosion

A ⇒ (¬ A ⇒ B)

is a theorem.

Axioms 9 and 10 are actually deﬁnitions. That means that

{\mathcal{L}}_F

does not add anything new to

{\mathcal{L}}_E

really: Falsity and negation are already present in

{\mathcal{L}}_E

, albeit in disguise.

Intuitionistic Logic

{\mathcal{L}}_I

extends

{\mathcal{L}}_F

by adding abstractions for conjunction

∧

, disjunction

∨

, equivalence

\Leftrightarrow

and existential quantiﬁcation

∃

such that

\mathfrak{S}_I = \mathfrak{S}_F + \left( \begin{array}{ccl} ∧ & : & (0; \emptyset, \emptyset)\\ ∨ & : & (0; \emptyset, \emptyset)\\ \Leftrightarrow & : & (0; \emptyset, \emptyset)\\ ∃ & : & (1; \{0\})\\ \end{array} \right)

Its set of axioms

{\mathbb{A}}_I

is obtained by adding the following axioms to

{\mathbb{A}}_F

$(A ∧ B) ⇒ A$
$(A ∧ B) ⇒ B$
$A ⇒ (B ⇒ (A ∧ B))$
$A ⇒ (A ∨ B)$
$B ⇒ (A ∨ B)$
$(A ∨ B) ⇒ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ C))$
$(A \Leftrightarrow B) = ((A ⇒ B) ∧ (B ⇒ A))$
$A[x] ⇒ ∃ x.\, A[x]$
$(∃ x.\, A[x]) ⇒ ((∀ x.\, A[x] ⇒ B) ⇒ B)$

Note that

A \Leftrightarrow (A = ⊤)

and

A \Leftrightarrow (A \Leftrightarrow ⊤)

and

¬ A \Leftrightarrow (A \Leftrightarrow ⊥)

are all theorems of

{\mathcal{L}}_I

, but

¬ A \Leftrightarrow (A = ⊥)

is not.

Classical Logic

{\mathcal{L}}_K

extends

{\mathcal{L}}_I

with the law of the excluded middle:

$A ∨ ¬ A$

Note that

(A \Leftrightarrow ⊤) ∨ (A \Leftrightarrow ⊥)

is thus a theorem in

{\mathcal{L}}_K

The class of abstraction logics Practical Types

{\mathcal{L}}_ℙ

will be designed as extensions of

{\mathcal{L}}_K

With proper support for modular reasoning and axiom tracking, it should be possible to mix different logics, so that statements like the following become provable: Theorem

\phi

{\mathcal{L}}_ℙ

has a proof in

{\mathcal{L}}_I

assuming hypotheses

\psi_0, \ldots, \psi_{n-1}

which have been proven in

{\mathcal{L}}_ℙ

Locales [5] are a mechanism for modular reasoning in Isabelle [4]. A locale corresponds in Practal just to a particular abstraction logic. So supporting locales comes down to supporting the simultaneous use of different abstraction logics, and to facilitate the transfer of theorems between them. In principle such a transfer should always construct a proof in the target logic from a proof in the source logic. In practice less expensive methods and short cuts can be used if such a proof replay is guaranteed to be possible in principle.

Consistency

An abstraction logic

{\mathcal{L}}

is called inconsistent if

{\mathcal{L}} ⊢ ∀ x.\, x

and consistent if it is not inconsistent.

If an abstraction logic

{\mathcal{L}}

is inconsistent and an extension of a deduction logic

{\mathcal{L}}_D

, then all models of

{\mathcal{L}}

are degenerate. This is easy to see. Assume

{\mathcal{L}}

is inconsistent. Then

∀ x.\,x

is a theorem in

{\mathcal{L}}

. Using axiom 4 of

{\mathcal{L}}_D

for

A[x] = x

and modus ponens it follows that

x

is a theorem. That means that

x

is valid in any model

(U; X; V; I; \mathfrak{S})

{\mathcal{L}}

. In particular, for any valuation

\nu \in V

we have

{\nu}\llbracket{x}\rrbracket = I(⊤)

. For any

u \in U

we can deﬁne a valuation

\nu_u \in V

such that

\nu_u(x) = u

. Then

u = \nu_u(x) = {\nu_u}\llbracket{x}\rrbracket = I(⊤)

. That means

U = \{I(⊤)\}

, thus any model of

{\mathcal{L}}

is degenerate.

What about the other direction? If every model

{\mathfrak{A}}

of an abstraction logic

{\mathcal{L}}

is degenerate, then

{{\llbracket {∀ x.\, x} \rrbracket}_{{\mathfrak{A}}}} = I(⊤)

holds. Therefore

{\mathcal{L}} ⊨ ∀ x.\, x

But is

∀ x.\, x

then a theorem of

{\mathcal{L}}

? We will see soon → that this is indeed the case if

{\mathcal{L}}

extends

{\mathcal{L}}_E

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.

Rasiowa Abstraction Algebra

Helena Rasiowa [10] proved completeness of intuitionistic predicate logic using algebraic methods, and furthermore gave a detailed description of her methods in her book on non-classical logics [6]. Her approach is even more far-reaching than she seems to have realized: There is no need for a special treatment of the quantiﬁers of predicate logic if you just choose the proper setting. That setting is abstraction logic.

We construct a special model

\mathfrak{R} = (U; X; V; I; \mathfrak{S})

, which we call Rasiowa Abstraction Algebra, for any logic

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

that extends

{\mathcal{L}}_E

Constructing $U$

The basic idea of the approach is due to Lindenbaum and Tarski and is mostly standard: Construct a model by considering the equivalence classes of terms that can be proven to be equal according to the logic. Note that while the original approach considers only variable-free terms and sentences, our approach works with terms which are allowed to contain free variables. Furthermore, there is no need (or possibility, for that matter) for us to distinguish between terms and sentences. This makes our completeness proof conceptually simple and elegant.

The relation

≈

{\mathcal{T}_{{X}}({\mathfrak{S}})}

is thus deﬁned as

s ≈ t \quad\text{iff}\quad {\mathcal{L}} ⊢ s = t

This is obviously an equivalence relation:

The relation is reﬂexive, because $A = A$ is a theorem in ${\mathcal{L}}_E$ .
The relation is symmetric, because $(A = B) ⇒ (B = A)$ is a theorem in ${\mathcal{L}}_E$ .
The relation is transitive, because $(A = B) ⇒ ((B = C) ⇒ (A = C))$ is a theorem in ${\mathcal{L}}_E$ .

We let

U

be the set of equivalence classes of

{\mathcal{T}_{{X}}({\mathfrak{S}})}

with respect to this relation:

U = {\mathcal{T}_{{X}}({\mathfrak{S}})}\, / ≈

For

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

we write

{[t]_{\mathfrak{R}}}

for its corresponding equivalence class in

U

Equivalence of de Bruijn Terms

For

t' \in {\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

we write

{[{t'}]^{\mathcal{B}}_{\mathfrak{R}}}

to denote

{[t]_{\mathfrak{R}}}

where

t

is any term in

{\mathcal{T}_{{X}}({\mathfrak{S}})}

such that

\alpha(t) = t'

. This is well-deﬁned, because if

s \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

such that

\alpha(s) = t'

as well, then

\alpha(s) = \alpha(t)

and thus

s = t

will be derivable in

{\mathcal{L}}

using the axioms of

{\mathcal{L}}_E

For

s, t \in {\mathcal{B}_{{X}}^{m}({\mathfrak{S}})}

we write

s ≈_m t

iff

{[{s / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{t / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

for all substitutions

\sigma : {{{\overline{m}}} \rightarrow {{{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}}}}

Note that

s ≈_0 t

is equivalent to

{[s]^{\mathcal{B}}_{\mathfrak{R}}} = {[t]^{\mathcal{B}}_{\mathfrak{R}}}

Assume

c

is an abstraction of

\mathfrak{S}

and has shape

(m; {p_0, \ldots, p_{n-1}})

. If for all

i \in {\overline{n}}

$s_i, t_i \in {\mathcal{B}_{{X}}^{m}({\mathfrak{S}})}$ ,
$({\operatorname{FreeAtoms}({s_i})} \cup {\operatorname{FreeAtoms}({t_i})})\, \cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq p_i$ ,
$s_i ≈_m t_i$ ,

then

{[{(c\, s_0 \ldots s_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{(c\, t_0 \ldots t_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}}

To see this, let

s = (c\, s_0 \ldots s_{n-1})

and

t = (c\, t_0 \ldots t_{n-1})

. The ﬁrst two conditions guarantee that both

s

and

t

are in

{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

. Now consider

s', t' \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

such that

\alpha(s') = s

and

\alpha(t') = t

. We can choose

s'

and

t'

such that

\begin{array}{rcl} s' & = & (c\, x_0 \ldots x_{m-1}.\, s'_0 \ldots s'_{n-1}) \\ t' & = & (c\, x_0 \ldots x_{m-1}.\, t'_0 \ldots t'_{n-1}) \\ \end{array}

for some variables

x_j

and some terms

s'_i

and

t'_i

. Then for all

i \in {\overline{n}}

\begin{array}{rcl} s_i & = & \alpha'(s'_i, \emptyset[\overline{x_{p_i} \coloneqq p_i}]) \\[0.3em] t_i & = & \alpha'(t'_i, \emptyset[\overline{x_{p_i} \coloneqq p_i}]) \end{array}

This implies

\begin{array}{rclcl} \alpha({s'_i}) & = & {s_i} / {\emptyset[\overline{\uparrow\hspace{-0.15em}{{p_i}} \coloneqq x_{p_i}}]} & = & {s_i} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq x_0, \ldots, \uparrow\hspace{-0.15em}{{(m - 1)}} \coloneqq x_{m - 1}]}\\[0.3em] \alpha({t'_i}) & = & {t_i} / {\emptyset[\overline{\uparrow\hspace{-0.15em}{{p_i}} \coloneqq x_{p_i}}]} & = & {t_i} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq x_0, \ldots, \uparrow\hspace{-0.15em}{{(m - 1)}} \coloneqq x_{m - 1}]}\\ \end{array}

From

s_i ≈_m t_i

follows therefore

{[{\alpha({s'_i})}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{\alpha({t'_i})}]^{\mathcal{B}}_{\mathfrak{R}}}

and

{[{s'_i}]_{\mathfrak{R}}} = {[{t'_i}]_{\mathfrak{R}}}

, thus

{\mathcal{L}} ⊢ s'_i = t'_i \quad \text{for all}\ i \in {\overline{n}}

From this we can prove in

{\mathcal{L}}

the theorem

s' = t'

, which implies

{[s]^{\mathcal{B}}_{\mathfrak{R}}} = {[t]^{\mathcal{B}}_{\mathfrak{R}}}

Deﬁning $\Phi_m$

For

m > 0

we deﬁne

\Phi_m : {{{\mathcal{B}_{{X}}^{m}({\mathfrak{S}})}} \rightarrow {({{U^m} \rightarrow U})}}

via

\Phi_m(t)({[{t_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{t_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) = {[{{t} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq t_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq t_{m-1}]}}]^{\mathcal{B}}_{\mathfrak{R}}}

\Phi_m

has the following properties:

$\Phi_m$ is well-deﬁned
$\Phi_m(s) = \Phi_m(t)$ implies $s ≈_m t$
$\Phi_m(t) \in {\mathcal{F}_{m}^{p}(U)}$ implies that there exists $s$ with $\Phi_m(t) = \Phi_m(s)$ and ${\operatorname{FreeAtoms}({s})}\, \cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq p$

To see 1., let us ﬁrst deﬁne

\Phi'_m : {{{\mathcal{B}_{{X}}^{m}({\mathfrak{S}})}} \rightarrow {({{{{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}}^m} \rightarrow {{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}}})}}

via

\Phi'_m(t)(t_0, \ldots, t_{m-1}) = {t} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq t_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq t_{m-1}]}

It is clear that

\Phi'_m

is well-deﬁned. Furthermore, assume we are given

{s_0, \ldots, s_{m-1}}

such that

s_i ≈_0 t_i

. The following theorem can be derived in

{\mathcal{L}}_E

A_0 = B_0 ⇒ \ldots ⇒ A_{m-1} = B_{m-1} ⇒ T[{A_0, \ldots, A_{m-1}}] = T[{B_0, \ldots, B_{m-1}}]

Applying the substitution

\sigma = \emptyset[T \coloneqq t,\,A_0 \coloneqq s_0, \ldots ,A_{m-1} \coloneqq s_{m-1},\, B_0 \coloneqq t_0, \ldots, B_{m-1} \coloneqq t_{m-1}]

to this theorem yields

\Phi'_m(t)(s_0, \ldots, s_{m-1}) ≈_0 \Phi'_m(t)(t_0, \ldots, t_{m-1})

To show 2., let us assume that

s ≈_m t

does not hold. Then there is a regular substitution

\sigma

with domain

{\overline{m}}

such that

{[{s / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} \neq {[{t / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

. Setting

r_i = \sigma(\uparrow\hspace{-0.15em}{i})

we see that

\Phi_m(s)({r_0, \ldots, r_{m-1}}) = {[{s / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

and

\Phi_m(t)({r_0, \ldots, r_{m-1}}) = {[{t / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

and thus

\Phi_m(s) \neq \Phi_m(t)

To verify 3., let us assume we have

t \in {\mathcal{B}_{{X}}^{m}({\mathfrak{S}})}

with

\Phi_m(t) \in {\mathcal{F}_{m}^{p}(U)}

, and that

\uparrow\hspace{-0.15em}{i} \in {\operatorname{FreeAtoms}(t)}

for some

i \notin p

. If we vary only those arguments of

\Phi_m(t)

corresponding to those positions

i

, then this function must be constant, and does therefore not depend on those positions

{\langle {i_0, \ldots, i_{k-1}} \rangle}

. We can therefore deﬁne

s = t / {\emptyset[i_0 \coloneqq ⊤, \ldots, i_{k-1} \coloneqq ⊤]}

Then

\Phi_m(t) = \Phi_m(s)

and

{\operatorname{FreeAtoms}(s)}\, \cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq p

Constructing $I$

Next, we are constructing the interpretation

I(c)

of an abstraction

c

\mathfrak{R}

Assume the arity of $c$ is zero. Then we set $I(c) = {[{(c.)}]_{\mathfrak{R}}}$
Assume the valence of $c$ is zero, and its arity is $n > 0$ . We set $I(c)({[{t_0}]_{\mathfrak{R}}}, \ldots, {[{t_{n-1}}]_{\mathfrak{R}}}) = {[{(c.\, t_0 \ldots t_{n-1})}]_{\mathfrak{R}}}$ To show that this is well-deﬁned, assume ${[{s_i}]_{\mathfrak{R}}} = {[{t_i}]_{\mathfrak{R}}}$ for all $i \in {\overline{n}}$ . Then $s_i = t_i$ is a theorem of ${\mathcal{L}}$ for each $i$ , and we can derive that $(c.\, s_0 \ldots s_{n-1}) = (c.\, t_0 \ldots t_{n-1})$ holds in ${\mathcal{L}}$ as well, using just the axioms of ${\mathcal{L}}_E$ .
Assume $c$ has shape $(m; {p_0, \ldots, p_{n-1}})$ with $m > 0$ . For $f_i \in {\mathcal{F}_{m}^{{p_i}}(U)}$ we set $I(c)({f_0, \ldots, f_{n-1}}) = \begin{cases} {[{(c\, f'_0 \ldots f'_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}} & \text{if}\ f'_i\ \text{exist with}\ \Phi_m(f'_i) = f_i\\ & \text{and}\ {\operatorname{FreeAtoms}({f'_i})}\, \cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq p_i\\\hline {[{⊤}]_{\mathfrak{R}}} & \text{otherwise} \end{cases}$ This is well-deﬁned because of the properties of $\Phi_m$ and $≈_m$ stated earlier.

Applying Valuations

Let

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

be a regular substitution.

It induces a de Bruijn valuation

\sigma'

D

U

as follows:

\sigma'(x) = \begin{cases} {[{\sigma(x)}]^{\mathcal{B}}_{\mathfrak{R}}} & \text{if}\ x \in X_0 \cup (D\, \cap \uparrow\hspace{-0.15em}{{\mathbb{N}}}) \\ \Phi_{{x_{\operatorname{arity}}}}(\sigma(x)) & \text{if}\ x \in X \setminus X_0 \end{cases}

Then for any

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

with

{\operatorname{FreeAtoms}(t)} \subseteq D

we have

{\sigma'}\llbracket{t}\rrbracket = {[{{t} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

We show this by induction over

t

Assume $t =\, \uparrow\hspace{-0.15em}{n}$ . Then $\uparrow\hspace{-0.15em}{n} \in D$ and ${\sigma'}\llbracket{t}\rrbracket = {\sigma'}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket = {[{\sigma(\uparrow\hspace{-0.15em}{n})}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{{t} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}$
Assume $t = x \in X_0$ . Then $x \in D$ and ${\sigma'}\llbracket{t}\rrbracket = {\sigma'}\llbracket{{x}}\rrbracket = {[{\sigma(x)}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{{t} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}$
Assume $t = x[{t_0, \ldots, t_{n-1}}]$ where $x \in X \setminus X_0$ . Then $x \in D$ and $\begin{array}{rcl} {\sigma'}\llbracket{t}\rrbracket & = & {\sigma'}\llbracket{{x[{t_0, \ldots, t_{n-1}}]}}\rrbracket\\[0.3em] & = & \sigma'(x)({\sigma'}\llbracket{{t_0}}\rrbracket, \ldots, {\sigma'}\llbracket{{t_{n-1}}}\rrbracket) \\[0.3em] & = & \Phi_n(\sigma(x))({[{{t_0} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{{t_{n-1}} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}) \\[0.3em] & = & {[{{\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq {t_0} / {\sigma}, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq {t_{n-1}} / {\sigma}]}}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.3em] & = & {[{({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq {t_0} / {\sigma} + n, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq {t_{n-1}} / {\sigma} + n]}) - n}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.3em] & = & {[{{x[{t_0, \ldots, t_{n-1}}]} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}\\[0.3em] & = & {[{{t} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} \end{array}$
Assume $t = (a\, t_0 \ldots t_{n-1})$ where $a$ is an abstraction with arity $n$ and valence $0$ : $\begin{array}{ll} {\sigma'}\llbracket{t}\rrbracket \\[0.5em] = {\sigma'}\llbracket{{(a\, t_0 \ldots t_{n-1})}}\rrbracket \\[0.5em] = I(a)({\sigma'}\llbracket{{t_0}}\rrbracket, \ldots, {\sigma'}\llbracket{{t_{n-1}}}\rrbracket) \\[0.5em] = I(a)({[{{t_0} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{{t_{n-1}} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}) \\[0.5em] = {[{(a.\, t'_0 \ldots t'_{n-1})}]_{\mathfrak{R}}}&\text{where}\ \alpha(t'_i) = {t_i} / {\sigma} \\[0.5em] = {[{(a\, t''_0 \ldots t''_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}}&\text{where}\ t''_i = {t_i} / {\uparrow^{0}\hspace{-0.15em}({\sigma})} = {t_i} / {\sigma} \\[0.5em] = {[{{(a\, t_0 \ldots t_{n-1})} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}\\[0.5em] = {[{t / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} \end{array}$
Assume $t = (a\, t_0 \ldots t_{n-1})$ where $a$ is an abstraction of shape $(m; {p_0, \ldots, p_{n-1}})$ with $m > 0$ . $\begin{array}{l} {\sigma'}\llbracket{t}\rrbracket \\[0.5em] = {\sigma'}\llbracket{{(a\, t_0 \ldots t_{n-1})}}\rrbracket \\[0.5em] = I'(a)({f_0, \ldots, f_{n-1}}) \\[0.5em] \quad\begin{array}{l} \text{where}\ f_i({[{b_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{b_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) \\[0.5em] \phantom{\text{where}}\quad = {\uparrow^{m}\hspace{-0.15em}({\sigma'})[\uparrow\hspace{-0.15em}{0} \coloneqq {{[{b_0}]^{\mathcal{B}}_{\mathfrak{R}}}}, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq {{[{b_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}}]}\llbracket{{t_i}}\rrbracket \\[0.5em] \phantom{\text{where}}\quad = {[{{(\uparrow^{m}\hspace{-0.15em}({\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq b_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq b_{m-1}])'}\llbracket{{t_i}}\rrbracket}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.5em] \phantom{\text{where}}\quad = {[{{t_i} / {(\uparrow^{m}\hspace{-0.15em}({\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq b_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq b_{m-1}])}}]^{\mathcal{B}}_{\mathfrak{R}}} \end{array} \\[0.5em] = {[{(a\, f'_0 \ldots f'_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}} \quad \text{where}\ \Phi_m(f'_i) = f_i,\\[0.5em] \overset{(*)}= {[{(a\, t'_0 \ldots t'_{n-1})}]^{\mathcal{B}}_{\mathfrak{R}}} \quad\text{where}\ t'_i = {t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})} \\[0.5em] = {[{{(a\, t_0 \ldots t_{n-1})} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.5em] = {[{t / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} \end{array} \\[0.5em]$ Equation $(*)$ holds if we can show $\Phi_m(t'_i) = f_i$ : $\begin{array}{l} \Phi_m(t'_i)({[{b_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{b_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) \\[0.5em] = {[{{t'_i} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq b_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq b_{m-1}]}}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.5em] = {[{{({t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})})} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq b_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq b_{m-1}]}}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.5em] = {[{{t_i} / {(\uparrow^{m}\hspace{-0.15em}({\sigma})[\uparrow\hspace{-0.15em}{0} \coloneqq b_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq b_{m-1}])}}]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.5em] = f_i({[{b_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{b_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) \end{array}$

Constructing $V$

Now

V \subseteq {\includegraphics[height=0.5em]{24ABA16B-23E3-4B4F-B1D2-76BD855A72E9}}({X}, U)

is deﬁned as follows:

V = \left\{ \nu \in {\includegraphics[height=0.5em]{B08794D7-0099-4A9A-9247-416DC84C6A86}}({X}, U) \mid \nu = \sigma'\ \text{for some regular}\ \sigma : {{X} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} \right\}

An equivalent deﬁnition of

V

V = \left\{ \nu \in {\includegraphics[height=0.5em]{8767FCEC-CF8E-4ABB-B12D-D48A3778AA2D}}({X}, U) \mid \forall\, x \in X \setminus X_0.\, \exists\, t \in {\mathcal{B}_{{X}}^{{{x_{\operatorname{arity}}}}}({\mathfrak{S}})}.\, \nu(x) = \Phi_{{x_{\operatorname{arity}}}}(t) \right\}

We need to check that

V

fulﬁlls the criteria set out for it in our logic algebra deﬁnition.

Assume $\nu = \sigma' \in V$ , and $x \in X_0$ and $u \in U$ . There is $t$ such that $u = {[t]^{\mathcal{B}}_{\mathfrak{R}}}$ and thus $\nu[x \coloneqq u] = \sigma'[x \coloneqq u] = (\sigma[x \coloneqq t])' \in V$

Assume $\nu = \sigma' \in V$ , and that $\theta : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}$ is a regular substitution with $D \subseteq X$ . We need to show that also $\nu_\theta \in V$ .

Assume $x \in X \setminus X_0$ and $m = {x_{\operatorname{arity}}}$ .
- For $x \in D$ we get $\begin{array}{l} \nu_\theta(x)({[{t_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{t_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) \\[0.3em] \quad = {\nu[\uparrow\hspace{-0.15em}{0} \coloneqq {[{t_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq {[{t_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}]}\llbracket{{\theta(x)}}\rrbracket\\[0.3em] \quad = {\sigma'[\uparrow\hspace{-0.15em}{0} \coloneqq {[{t_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq {[{t_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}]}\llbracket{{\theta(x)}}\rrbracket\\[0.3em] \quad = {(\sigma[\uparrow\hspace{-0.15em}{0} \coloneqq t_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq t_{m-1}])'}\llbracket{{\theta(x)}}\rrbracket\\[0.3em] \quad = {[{{\theta(x)} / {(\sigma[\uparrow\hspace{-0.15em}{0} \coloneqq t_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq t_{m-1}])} }]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.3em] \quad = {[{{({\theta(x)} / {\sigma})} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq t_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq t_{m-1}]} }]^{\mathcal{B}}_{\mathfrak{R}}} \\[0.3em] \quad = \Phi_m({\theta(x)} / {\sigma})({[{t_0}]^{\mathcal{B}}_{\mathfrak{R}}}, \ldots, {[{t_{m-1}}]^{\mathcal{B}}_{\mathfrak{R}}}) \end{array}$ Thus $\nu_\theta(x) = \Phi_m({\theta(x)} / {\sigma})$ .
- For $x \notin D$ we get $\nu_\theta(x) = \nu(x) = \sigma'(x) = \Phi_m(\sigma(x))$ .
Together this implies $\nu_\theta \in V$ .

$\mathfrak{R}$ is a Model for ${\mathcal{L}}$

The tuple

\mathfrak{R} = (U; X; V; I; \mathfrak{S})

we constructed is a logic algebra:

$(U; I; \mathfrak{S})$ is an abstraction algebra by construction.
We veriﬁed that $V$ has the required properties.
Certainly $\mathfrak{S}$ is an extension of ${\mathfrak{S}_0}$ .
Assume $I(\text{⇒})(I(⊤), {[{b}]_{\mathfrak{R}}}) = I(⊤)$ for $b \in {\mathcal{T}_{{X}}({\mathfrak{S}})}$ . Using the deﬁnition of $I$ in $\mathfrak{R}$ , this is equivalent to ${[{⊤ ⇒ b}]_{\mathfrak{R}}} = {[{⊤}]_{\mathfrak{R}}}$ . This means that we can prove $(⊤ ⇒ b) = ⊤$ in ${\mathcal{L}}$ , and thus also $⊤ ⇒ b$ . Application of modus ponens together with Axiom 0 yields ${\mathcal{L}} ⊢ b$ , and Axiom 8 delivers ${\mathcal{L}} ⊢ b = ⊤$ , and thus ${[{b}]_{\mathfrak{R}}} = {[{⊤}]_{\mathfrak{R}}} = I(⊤)$
Let $f : {U \rightarrow U}$ such that $f(u) = I(⊤)$ for all $u \in U$ .

We deﬁne $f' \in {\mathcal{B}_{{X}}^{1}({\mathfrak{S}})}$ by $f' = ⊤$ . Then $\Phi_m(f')(u) = {[{⊤}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{⊤}]_{\mathfrak{R}}} = I(⊤) = f(u)$ This means $\Phi_m(f') = f$ and therefore $I(∀)(f) = {[{(∀\, ⊤)}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{∀ x. ⊤}]_{\mathfrak{R}}}$ We can prove $(∀ x. ⊤) = ⊤$ in ${\mathcal{L}}$ . This yields $I(∀)(f) = {[{∀ x. ⊤}]_{\mathfrak{R}}} = {[{⊤}]_{\mathfrak{R}}} = I(⊤)$

We need to show that

\mathfrak{R}

is a model for all axioms

a \in {\mathbb{A}}

{\mathcal{L}}

Assume

\nu = \sigma' \in V

. Then

{\nu}\llbracket{a}\rrbracket = {\sigma'}\llbracket{a}\rrbracket = {[{{\alpha(a)} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}}

. Because

a

is an axiom, we can prove

{\mathcal{L}} ⊢ a

. Choose

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

such that

\alpha(t) = {\alpha(a)} / {\sigma}

. With proof rule

\operatorname{SUBST}

we can derive

{\mathcal{L}} ⊢ t

. Thus

{\nu}\llbracket{a}\rrbracket = {[{{\alpha(a)} / {\sigma}}]^{\mathcal{B}}_{\mathfrak{R}}} = {[t]_{\mathfrak{R}}} = {[{⊤}]_{\mathfrak{R}}} = I(⊤)

We conclude that

\mathfrak{R}

is indeed a model of

{\mathcal{L}}

Completeness

An abstraction logic

{\mathcal{L}} = (\mathfrak{S}; X; {\mathbb{A}})

is called complete if every valid term is also a theorem, i.e. if for all

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

{\mathcal{L}} ⊨ t \quad\text{implies}\quad {\mathcal{L}} ⊢ t

{\mathcal{L}}

extends

{\mathcal{L}}_E

, then

{\mathcal{L}}

is complete.

This can be seen easily now. Construct the Rasiowa Abstraction Algebra

\mathfrak{R} = (U; X; V; I; \mathfrak{S})

as a model for

{\mathcal{L}}

. The canonical substitution

\iota : {X \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

is deﬁned by

\begin{array}{rcll} \iota(x) & = & x & \text{if}\ x \in X_0 \\ \iota(x) & = & x[\uparrow\hspace{-0.15em}{0}, \ldots, \uparrow\hspace{-0.15em}{{({{x}_{\operatorname{arity}}}-1)}}] & \text{if}\ x \in X \setminus X_0 \end{array}

Obviously

{t'} / {\iota} = t'

holds for all

t' \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

. Consequently,

{\iota'}\llbracket{t}\rrbracket = {[{{\alpha(t)} / {\iota}}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{\alpha(t)}]^{\mathcal{B}}_{\mathfrak{R}}} = {[{t}]_{\mathfrak{R}}}

holds for all

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

Assume that

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

is valid. Because of

\iota' \in V

this implies

{[{t}]_{\mathfrak{R}}} = {\iota'}\llbracket{t}\rrbracket = I(⊤) = {[{⊤}]_{\mathfrak{R}}}

which shows that

{\mathcal{L}} ⊢ t = ⊤

, and therefore also

{\mathcal{L}} ⊢ t

Matching and Uniﬁcation

Given two terms

s, t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

, it is natural to ask and a common task in machine-assisted reasoning to unify

s

and

t

, i.e. to ask for a substitution

\sigma

such that

s / {\sigma} = t / {\sigma}

A related and easier problem is to match the pattern

s

t

, i.e. to ﬁnd a substitution

\sigma

such that

s / {\sigma} = t

Given that abstraction syntax can be seen as a special case of higher-order syntax, we can adapt the results from higher-order uniﬁcation. Experiments in that direction have been carried out, and a higher-order uniﬁcation algorithm [11] has been adapted for both abstraction uniﬁcation [12] and abstraction matching [13]. These experiments have been carried out before the inception of abstraction logic, therefore the notation used in them is slightly different. The resulting algorithms are somewhat simpler than the original ones, as there is no need for iteration and no need to compensate for

\beta/\eta

-equivalence.

Second-order matching is decidable, and second-order uniﬁcation is semi-decidable [14]. Given that abstraction syntax can also be seen as a special case of second-order syntax, as a consequence abstraction matching is decidable, and abstraction uniﬁcation is semi-decidable. One would hope that maybe abstraction uniﬁcation is even decidable, but the requirements of Goldfarb’s undecidability proof for second-order uniﬁcation [15] seem to carry over to abstraction uniﬁcation.

Uniﬁcation and matching are especially important in automated reasoning. Superposition is the basis of modern automated reasoning systems, and it is interesting to observe that the approach of superposition to work with theorems of the form

s = ⊤

is very natural in abstraction logic. There are current efforts [16] to bridge the gap between ﬁrst-order automated theorem proving and higher-order automated theorem proving. It would certainly make sense to have a pit stop at abstraction automated theorem proving on that journey.

References

[1]Steven Obua. (2021). Practical Types, https://doi.org/10.47757/practical.types.1.

[2]Steven Obua. (2021). Practal — Practical Logic: A Bicycle for Your Mathematical Mind, https://doi.org/10.47757/practal.1.

[3]Saul A. Kripke. (2013). Fregean Quantification Theory, https://doi.org/10.1007/s10992-013-9299-x.

[4]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. (2019). From LCF to Isabelle/HOL, https://doi.org/10.1007/s00165-019-00492-1.

[5]Clemens Ballarin. (2014). Locales: A Module System for Mathematical Theories, https://doi.org/10.1007/s10817-013-9284-7.

[6]Helena Rasiowa. (1974). An algebraic approach to non-classical logics, https://doi.org/10.1016/s0049-237x(09)x7004-7.

[7]Helena Rasiowa, Roman Sikorski. (1963). The Mathematics of Metamathematics.

[8]Helena Rasiowa. (1973). Introduction to Modern Mathematics, https://doi.org/10.1016/c2013-0-11892-2.

[9]Arthur Charguéraud. (2012). The Locally Nameless Representation, https://doi.org/10.1007/s10817-011-9225-2.

[10]Helena Rasiowa. (1951). Algebraic Treatment of the Functional Calculi of Heyting and Lewis, https://doi.org/10.4064/fm-38-1-99-126.

[11]Petar Vukmirović, Alexander Bentkamp, Visa Nummelin. (2021). Efficient Full Higher-Order Unification, https://arxiv.org/abs/2011.09507.

[12]Steven Obua. (2021). Unification in practal-light, https://github.com/practal/practal-light/blob/728de5bfffa28d296d611db2c7388c069fc0b711/Sources/practal-light/Tools/Unification.swift.

[13]Steven Obua. (2021). Matching in practal-light, https://github.com/practal/practal-light/blob/728de5bfffa28d296d611db2c7388c069fc0b711/Sources/practal-light/Tools/Matching.swift.

[14]Gilles Dowek. (2001). Higher-Order Unification and Matching, https://doi.org/10.1016/B978-044450813-3/50018-7.

[15]Warren D. Goldfarb. (1979). The Undecidability of the Second-Order Unification Problem, https://doi.org/10.1016/0304-3975(81)90040-2.

[16]Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret. (2021). Making Higher-Order Superposition Work, https://doi.org/10.1007/978-3-030-79876-5_24.

Abstraction Logic

Introduction

Preliminaries

Algebra

Syntax

Semantics

De Bruijn Terms

α\alphaα-Equivalence

Substitution

De Bruijn Abstraction Algebra

Logic

Proofs

Soundness

Several Abstraction Logics

Consistency

Rasiowa Abstraction Algebra

Constructing UUU

Equivalence of de Bruijn Terms

Deﬁning Φm\Phi_mΦm​

Constructing III

Applying Valuations

Constructing VVV

R\mathfrak{R}R is a Model for L{\mathcal{L}}L

Completeness

Matching and Uniﬁcation

References

$\alpha$ -Equivalence

Constructing $U$

Deﬁning $\Phi_m$

Constructing $I$

Constructing $V$

$\mathfrak{R}$ is a Model for ${\mathcal{L}}$