This article is obsolete. It has been superseded by
© 2021 Steven Obua

Abstraction Logic

by Steven Obua
Cite as:
Oct 22, 2021
Abstraction Logic is introduced as a foundation for Practical Types [1] and Practal [2]. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.


The goal of Practical Types [1] is to provide a foundation for formal machine-assisted reasoning that anyone would find 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 first-order logic, abstraction logic has a single universe of discourse, i.e. it is one-sorted. It goes even further than ordinary first-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 specifications 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 first-order logic needs axiom schemata consisting of infinitely 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 first-order logic. Similarly, abstraction logic is not limited to Practical Types, it can provide a foundation for many applications where currently first-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 first 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 defined 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 L{\mathcal{L}} that extends Deduction Logic with Equality , and use it to prove completeness  of any such L{\mathcal{L}}, including intuitionistic and classical abstraction logic. We conclude by briefly discussing matching and unification  of abstraction syntax terms.


Let’s fix some general notation first:


A shape σ\sigma prescribes a number mm of binders and a number nn of parameters. Furthermore it assigns to each parameter the set of binders it depends on. A shape is therefore written as (m;p0,,pn1)(m; p_0, \ldots, p_{n-1}) where m,nNm, n \in \mathbb{N}, and each pip_i is a subset of m{\overline{{m}}}. Furthermore we require that there are no superfluous binders: i=0n1pi=m\bigcup_{i=0}^{n-1} p_i = {\overline{{m}}} We call mm the valence of the shape, and nn its arity. Above condition implies that a shape with arity 00 necessarily has valence 00. It also implies that for a unary shape its sole parameter will depend on all binders.
An abstraction signature S=(a0:σ0,,ak1:σk1)\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1}) is a list of kk different abstractions aia_i, where each abstraction aia_i is associated with its shape σi\sigma_i.
An abstraction algebra A=(U;I;S){\mathfrak{A}} = (U; I; \mathfrak{S}) is a non-empty set UU together with an abstraction signature S\mathfrak{S} and an interpretation II which interprets an abstraction aia_i as an element I(ai)I(a_i) of the set ΛU(σi){\Lambda_{U}({\sigma_i})}. The set ΛU(σi){\Lambda_{U}({\sigma_i})} will be defined shortly.
Examples of abstractions and their shapes are:
We require an abstraction aa of shape σ\sigma to be an element of ΛU(σ){\Lambda_{U}({\sigma})}. We define ΛU(σ){\Lambda_{U}({\sigma})} for σ=(m;p0,,pn1)\sigma = (m; {p_0, \ldots, p_{n-1}}) as follows: ΛU(σ)={Uif n=0Fmp0(U)××Fmpn1(U)Uif n1 {\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 m1m \geq 1 and pmp \subseteq {\overline{{m}}}, we define Fmp(U){\mathcal{F}_{m}^{p}(U)} as follows: Fmp(U)={Uif p={fπmp(U)fUpU}UmUif p {\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 πmp(U):UmUp{\pi_m^p(U)} : {{U^m} \rightarrow {U^{|{p}|}}} are defined for p=i0,,in1p = {\langle {i_0, \ldots, i_{n-1}} \rangle} via (u0,,um1)(ui0,,uin1)(u_0, \ldots, u_{m-1}) \mapsto (u_{i_0}, \ldots, u_{i_{n-1}})
In particular, if the valence of σ\sigma is 00 and its arity nn, then ΛU(σ)={Uif n=0UnUif n0 {\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 is 11, then ΛU(σ)=F1p0(U)××F1pn1(U)U{\Lambda_{U}({\sigma})} = {{{\mathcal{F}_{1}^{{p_0}}(U)} \times \ldots \times {\mathcal{F}_{1}^{{p_{n-1}}}(U)}} \rightarrow U}, where F1pi(U){\mathcal{F}_{1}^{{p_i}}(U)} is either UU or UU{U \rightarrow U}, depending on whether pi=p_i = \emptyset or pi={0}p_i = \{0\}, respectively.
Continuing our previous examples, we can now say the following:
Bounded universal quantification x:T.P[x]\forall x : T.\, P[x] has shape (1;{},{0})(1; \{\}, \{0\}), and is therefore interpreted as an element of U×(UU)U{{U \times ({U \rightarrow U})} \rightarrow U}.
Another example is defined by funeqx.Tf[x]g[x]x:T.f[x]=g[x]\operatorname{funeq} x.\, T\, f[x]\, g[x] ≝ \forall x : T.\, f[x] = g[x] The shape of funeq\operatorname{funeq} is (1;{},{0},{0})(1; \{\}, \{0\}, \{0\}), and therefore funeq:U×(UU)×(UU)U\operatorname{funeq} : {{U \times ({U \rightarrow U}) \times ({U \rightarrow U})} \rightarrow U}


Given an abstraction signature S=(a0:σ0,,ak1:σk1)\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1}) and a set of variables XX, we define the set TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})} of terms over S\mathfrak{S}. We require variables and abstractions not to overlap, of course, i.e. aiXa_i \notin X for all iki \in {\overline{{k}}}. We also require each variable xXx\in X to be associated with a fixed arity xarityN{x_{\operatorname{arity}}} \in \mathbb{N}.
The set TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})} of terms is then defined inductively as follows:
Note that with this definition all terms in TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})} are wellformed, although the definition 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 Free(t){\operatorname{Free}({t})} of a term tTX(S)t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}. We define Free(t){\operatorname{Free}(t)} recursively, following the inductive definition of TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})}: Free(x[t0,,txarity1])={x}Free(t0)Free(txarity1)Free((ax0xm1.t0tn1))= (Free(t0){xi0,0,,xi0,p01}) (Free(t1){xi1,0,,xi1,p11}) (Free(tn1){xin1,0,,xin1,pn11})where σa=(m;p0,,pn1)and pj=ij,0,,ij,pj1 jn \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 Free(t)={\operatorname{Free}(t)} = \emptyset, the term tt is called closed.
The following table examines our previous examples in terms of abstraction syntax: x=y(=.x y)x,yx.P[x](x.P[x])Pλx:T.A[x](λx.TA[x])T,Ax:T.P[x](x.TP[x])T,Pfuneqx.Tf[x]g[x](funeqx.Tf[x]g[x])T,f,gx:T.f[x]=g[x](x.T(=.f[x]g[x]))T,f,g \begin{array}{c|c|c} {\includegraphics[height=0.5em]{A10D021D-5882-44D4-B25D-23270BF7F086}} & {\includegraphics[height=0.5em]{7E37D7C6-876D-42D0-97EF-4EA4FA1B0387}} & {\includegraphics[height=0.5em]{9EFF3EE0-A68A-4915-BD4B-1C43A740F06C}} \\\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 xx is a free variable of the expression λx:x. x\lambda x : x.\ x Although the variable xx is bound in the second parameter of λ\lambda, it occurs free in the first parameter of λ\lambda, and is therefore a free variable of the entire expression.


Given a set FF of variables, and a set UU, a valuation ν\nu of FF in UU is a mapping that assigns to each xFx \in F with xarity=0{x_{\operatorname{arity}}} = 0 an element ν(x)U\nu(x) \in U, and to each xFx \in F with xarity1{x_{\operatorname{arity}}} \geq 1 a function ν(x)UxarityU\nu(x) \in {{U^{{x_{\operatorname{arity}}}}} \rightarrow U}. We denote the set of valuations of FF in UU by (F,U){\includegraphics[height=0.5em]{E58E2822-8758-4F64-8D6D-B65CBBD65A47}}(F, U).
Let S\mathfrak{S} be an abstraction signature, and A=(U;I;S){\mathfrak{A}} = (U; I; \mathfrak{S}) an abstraction algebra with signature S\mathfrak{S}. Given a term tTX(S)t \in {\mathcal{T}_{X}({\mathfrak{S}})}, any valuation ν\nu of Free(t){\operatorname{Free}(t)} in UU determines an element νtU{\nu}\llbracket{t}\rrbracket \in U, recursively defined as follows:
If tt is a closed term, then νt{\nu}\llbracket{t}\rrbracket is independent of the choice of the valuation ν\nu in UU, and we can therefore define tA=νt{{\llbracket t \rrbracket}_{{\mathfrak{A}}}} = {\nu}\llbracket{t}\rrbracket

De Bruijn Terms

Terms TX(S){\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 (ax.x)(a\, x.\, x) and (ay.y)(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 definitions are inspired by this approach. We first define de Bruijn preterms BXpre(S){\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}:
The idea is that a term like (axy.(b.xy)(cx.xy))(a\, x\, y.\, (b.\, x\, y)\, (c\, x.\, x\, y)) corresponds to the de Bruijn term (a(b01)(c02))(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 α:TX(S)BXpre(S)\alpha : {{{\mathcal{T}_{{X}}({\mathfrak{S}})}} \rightarrow {{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}}} Let X0={xXxarity=0}X_0 = \{x \in X \mid {{x}_{\operatorname{arity}}} = 0\}. To define α\alpha, we first define a function α:TX(S)×(X0N)BXpre(S)\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: α(x[t0,,tn1],η)=x[α(t0,η),,α(tn1,η)]if η is undefined at xα(x,η)=η(x)if η is defined at xα((ax0xm1.t0tn1),η)=(at0tn1)where the shape of a=(m;p0,,pn1)and for all  in, ti=α(ti,(η+m)[xpipi]) \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:UNf : {U ↪ {\mathbb{N}}} and any mNm \in \mathbb{N} we define f=f+mf' = f + m in the obvious way such that f(u)=f(u)+mf'(u) = f(u) + m holds if ff is defined at uUu \in U.
Then we can define α\alpha by α(t)=α(t,)\alpha(t) = \alpha'(t, \emptyset)
Of particular interest are those elements of BXpre(S){\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': BXh(S)={α(t,η)(t,η)TX(S)×(X0h)}BX(S)=h=0BXh(S) \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 BX0(S){\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}. We call BX(S){\mathcal{B}_{{X}}({\mathfrak{S}})} the set of de Bruijn terms, and BXh(S){\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} is the set of de Bruijn terms with at most hh holes.
Instead of defining 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 FreeAtoms(t){\operatorname{FreeAtoms}(t)} of a de Bruijn preterm tBXpre(S)t \in {\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}: FreeAtoms(t)=FreeAtoms0(t)FreeAtomsl(n)={if n<l{nl}if nlFreeAtomsl(x[t0,,tn1])={x}i=0n1FreeAtomsl(ti)FreeAtomsl((at0tn1))=i=0n1FreeAtomsl+m(ti)where m is the valence of a \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 BX(S){\mathcal{B}_{{X}}({\mathfrak{S}})} are then those de Bruijn preterms tt such that for every subpreterm of tt of the form (at0tn1)(a\,t_0 \ldots t_{n-1}) the inclusion FreeAtoms(ti)mpi {\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}} holds for all ini \in {\overline{n}}. Here the shape of aa is (m;p0,,pn1)(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 BXh(S)={tBX(S)FreeAtoms(t)Nh}{\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\}


We say that two terms ss and tt in TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})} are α\alpha-equivalent iff α(s)=α(t)\alpha(s) = \alpha(t)
The importance of α\alpha-equivalence stems from the fact that it is the same as semantical equivalence. We call ss and tt in TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})} semantically equivalent iff for any abstraction algebra (U;I;S)(U; I; \mathfrak{S}), and for any valuation ν(X,U)\nu \in {\includegraphics[height=0.5em]{EA73FE70-E33E-4531-B01C-8C47083D2BFD}}({X}, U), we have ν(s)=ν(t)\nu(s) = \nu(t).
We first show that α\alpha-equivalence implies semantical equivalence.
To this end, we define valuations also on de Bruijn terms. Given a set FF of variables and a subset NN of N\mathbb{N}, a de Bruijn valuation ν\nu of FNF\, \cup \uparrow\hspace{-0.15em}{{N}} in UU is a mapping such that ν\nu is a valuation of FF in UU, and additionally, ν\nu assigns to each n\uparrow\hspace{-0.15em}{{n}} an element ν(n)U\nu(\uparrow\hspace{-0.15em}{{n}}) \in U for all nNn \in N.
Any valuation ν\nu of FreeAtoms(t){\operatorname{FreeAtoms}({t})} in UU determines an element νtU{\nu}\llbracket{t}\rrbracket \in U: νn=ν(n)νx[t0,,tn1]=ν(x)(νt0,,νtn1)ν(at0tn1)=I(a)(νt0,,νtn1)if the valence of a is 0ν(at0tn1)=I(a)(f0,,fn1)if the valence of a is m1where fi(u0,,um1)=m(ν)[0u0,,(m1)um1]tifor all (u0,,um1)Um \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 II' is a slight modification of the interpretation II in that where I(a)I(a) expects an element eUe \in U as one of its arguments, I(a)I'(a) will accept a constant function (u0,,um1)e({u_0, \ldots, u_{m-1}}) \mapsto e instead. Otherwise, II' and II are identical.
The valuation m(ν)\uparrow^{m}\hspace{-0.15em}({\nu}) is derived from ν\nu via m(ν)(x)=ν(x)where xXm(ν)((m+n))=ν(n)where nN \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 defined iff the right hand sides are defined.
It is not immediately obvious that ν(at0tn1){\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket is well-defined, because in order to be able to apply I(a)I'(a) to (f0,,fn1)({f_0, \ldots, f_{n-1}}), the fif_i cannot be just any functions in UmU{{U^m} \rightarrow U}. Assuming that the shape of aa is (m;p0,,pn1)(m; {p_0, \ldots, p_{n-1}}), if pi=p_i = \emptyset, fif_i must be a constant function, and for pip_i \neq \emptyset, fif_i needs to be in Fmpi(U){\mathcal{F}_{m}^{{p_i}}(U)}. But this is easily seen to be the case, given that νtνt{\nu'}\llbracket{t}\rrbracket \neq {\nu}\llbracket{t}\rrbracket only holds if ν\nu' and ν\nu have a different assignment for some qFreeAtoms(t)q \in {\operatorname{FreeAtoms}(t)}, and according to our earlier observation , FreeAtoms(ti)mpi{\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}}.
Given a valuation ν(X,U)\nu \in {\includegraphics[height=0.5em]{59D36504-10AA-4132-A799-7F0B72E08685}}({X}, U), together with an injective function η:X0N\eta : {{X_0} ↪ {\mathbb{N}}}, the corresponding de Bruijn valuation νη\nu_\eta is defined as νη(x)=ν(x)where xXνη(n)=ν(x)where η(x)=n \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 tTX(S)t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}, any valuation ν(X,U)\nu \in {\includegraphics[height=0.5em]{573C560E-B7CF-40F0-91DA-F89AEBAB3EFB}}({X}, U), and any injective η:X0N\eta : {{X_0} ↪ {\mathbb{N}}}, we have νηα(t,η)=νt {\nu_\eta}\llbracket{{\alpha'(t, \eta)}}\rrbracket = {\nu}\llbracket{t}\rrbracket\quad
The proof is by induction over tt:
In particular, for tTX(S)t \in {\mathcal{T}_{{X}}({\mathfrak{S}})} and ν(X,U)\nu \in {\includegraphics[height=0.5em]{68F70D64-B406-49B7-864E-B5C7DAC3FF3D}}({X}, U): να(t)=νt {\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket An immediate consequence is that α\alpha-equivalence implies semantical equivalence: Let ss and tt be α\alpha-equivalent terms in TX(S){\mathcal{T}_{{X}}({\mathfrak{S}})}, i.e. α(s)=α(t)\alpha(s) = \alpha(t). Then for all valuations ν(X,U)\nu \in {\includegraphics[height=0.5em]{75166EFF-162F-4514-BE94-E38A75FB4F02}}({X}, U), we have νs=να(s)=να(t)=νt{\nu}\llbracket{s}\rrbracket = {\nu}\llbracket{{\alpha(s)}}\rrbracket = {\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket


Before showing that semantical equivalence implies α\alpha-equivalence in the next section , we will first consider how to perform substitution of (some of) the free atoms in a de Bruijn term.
A substitution is a function σ:DBX(S)\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} with domain DXND \subseteq X\, \cup \uparrow\hspace{-0.15em}{{\mathbb{N}}}. Application t/σt / {\sigma} of a substitution σ:DBX(S)\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} to a de Bruijn term tBX(S)t \in {\mathcal{B}_{{X}}({\mathfrak{S}})} is recursively defined as follows: n/σ=σ(n)if n is in the domain of σn/σ=nif n is not in the domain of σx[t0,,tn1]/σ=(σ(x)/[0t0,,(n1)tn1])nif x is in the domain of σ;here  denotes the empty substitution,and ti=(ti/σ)+nx[t0,,tn1]/σ=x[t0/σ,,tn1/σ]if x is not in the domain of σ(at0tn1)/σ=(at0tn1) where ti=ti/m(σ),given the valence of a is m \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 definition we used the expression t+zt + z for tBX(S)t \in {\mathcal{B}_{{X}}({\mathfrak{S}})} and zZz \in \mathbb{Z}. This expression is only defined if for all nFreeAtoms(t)\uparrow\hspace{-0.15em}{n} \in {\operatorname{FreeAtoms}(t)}, we have n+z0n + z \geq 0. Then: t+z=t+0zn+lz=nif n<ln+lz=(n+z)if nlx[t0,,tn1]+lz=x[t0+lz,,tn1+lz](at0tn1)+lz=(a(t0+l+mz)(tn1+l+mz))where the valence of a is m \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 define m(σ)\uparrow^{m}\hspace{-0.15em}({\sigma}) for a substitution σ:DBX(S)\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} and mNm \in \mathbb{N} by m(σ)(x)=σ(x)+xaritymfor xXDm(σ)((m+n))=σ(n)+mfornD \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 m(σ)\uparrow^{m}\hspace{-0.15em}({\sigma}) is a substitution with domain (XD){(m+n)nD}(X \cap D) \cup \{\uparrow\hspace{-0.15em}{{(m + n)}} \mid\, \uparrow\hspace{-0.15em}{n} \in D\}.
We define the free atoms of a substitution σ:DBX(S)\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} by FreeAtoms(σ)=nDFreeAtoms(σ(n))xDX{qxarityqFreeAtoms(σ(x))xarity)} \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 σ:DBX(S)\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} regular if FreeAtoms(σ)X{\operatorname{FreeAtoms}({\sigma})} \subseteq X.
For regular σ\sigma we have σ(x)BXxarity(S)\sigma(x) \in {\mathcal{B}_{{X}}^{{{x_{\operatorname{arity}}}}}({\mathfrak{S}})} for all xDXx \in D \cap X and σ(n)BX0(S)\sigma(\uparrow\hspace{-0.15em}{n}) \in {\mathcal{B}_{{X}}^{0}({\mathfrak{S}})} for all nD\uparrow\hspace{-0.15em}{n} \in D.
Note that if σ\sigma is regular, then m(σ)\uparrow^{m}\hspace{-0.15em}({\sigma}) is regular, too.
Given a de Bruijn valuation ν\nu of FF in UU, any regular substitution σ:DBX(S)\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}} with FreeAtoms(σ)F{\operatorname{FreeAtoms}({\sigma})} \subseteq F induces a de Bruijn valuation νσ\nu_\sigma of FDF \cup D in UU via νσ(q)=ν(q)if qFDνσ(n)=νσ(n)if nDνσ(x)=νσ(x)if xDX0νσ(x)=(u0,,un1)ν[0u0,,(n1)un1]σ(x)if xDX and where xarity=n>0 \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} <