#  Uniform Algebras:
Models and constructive Completeness for
Full, Simply Typed $\lambda$Prolog

Gianluca Amato
University of Chieti–Pescara
<EMAIL_ADDRESS>Mary DeMarco
Wesleyan University
<EMAIL_ADDRESS>James Lipton
Wesleyan University
<EMAIL_ADDRESS>
(May 23, 2024)

###### Abstract

This paper introduces a model theory for resolution on Higher Order
Hereditarily Harrop formulae (HOHH), the logic underlying the $\lambda$Prolog
programming language, and proves soundness and completeness of resolution. The
semantics and the proof of completeness of the formal system is shown in
several ways, suitably adapted to deal with the impredicativity of higher-
order logic, which rules out definitions of truth based on induction on
formula structure. First, we use the least fixed point of a certain operator
on interpretations, in the style of Apt and Van Emden, Then a constructive
completeness theorem is given using a proof theoretic variant of the
Lindenbaum algebra, which also contains a new approach to establishing cut-
elimination.

###### Contents

  1. 1 Preface
  2. 2 Syntax of the Logic and the Programming Language
    1. 2.1 The ICTT Calculus and HOHH Programs
    2. 2.2 Deduction
    3. 2.3 The UCTT Calculus
    4. 2.4 Levels and Signatures
    5. 2.5 Proof procedures for HOHH Formulae
    6. 2.6 Renaming Apart Derivations
    7. 2.7 Some specialization properties of UCTT
    8. 2.8 Herbrand-Robinson Derivation: “True” Resolution
  3. 3 Semantics
    1. 3.1 The Main Obstacles
    2. 3.2 Applicative Structures
    3. 3.3 Uniform Algebras
    4. 3.4 Soundness
  4. 4 Completeness
    1. 4.1 Why the Semantics is Intuitionistic
    2. 4.2 Enriched Resolution
  5. 5 Some alternative models
    1. 5.1 Completeness: Substitution Semantics
    2. 5.2 Lindenbaum Algebra and UCTT
      1. 5.2.1 A $\mathbb{P}$-indexed Lindenbaum Algebra for UCTT
      2. 5.2.2 The Algebra of Ideals
    3. 5.3 Indexed Models and Fibrations
  6. A Appendix
    1. A.1 The Variable Indexing Problem
    2. A.2 Distributive Lattices and Heyting Algebras
    3. A.3 Logic Programming Proof procedures
      1. A.3.1 A sketch of the equivalence of the uniform proof system with the RES(t) system.

##  1 Preface

HOHH is an executable fragment of an intuitionistic sequent presentation of
Church’s theory of types, here called ICTT, introduced by Miller and Nadathur
in the early 1990s and shown to be an instance of their notion of an abstract
logic programming language in [30].

A number of fragments of HOHH have been shown to be suitable for logic
programming, among them the Higher-Order Horn fragment (HOH) and the First-
Order Hereditarily Harrop formulas (FOHH).

An enrichment of HOHH, with higher-order unification and a certain degree of
type polymorphism, constitutes the framework for the $\lambda$Prolog
programming language. This language allows programming in typed higher-order
intuitionistic logic, with a declarative treatment of modules via implication
and with universally quantified goals, and the ability to handle abstract
syntax via lambda-tree syntax as well as abstract data types. Recently there
has been a lot of work to embed it, or a variant such as ELPI, in proof
assistants like Coq [40, 41, 12, 39].

Model theories have been defined for some HOHH fragments. Miller [29] defined
an indexed variant of Kripke semantics in 1989 for the $\forall$-free part of
FOHH. DeMarco extended these models to full FOHH and HOHH in [10], and defined
an equivalent Kripke semantics, in 1999. This was the first time a sound and
complete semantics appeared for (intensional) HOHH with the Apt-Van Emden
bottom-up $T_{P}$ operator. This paper expands the results in DeMarco’s
dissertation [10] in considering other classes of models as well.

Independently, Kripke semantics for a core HOHH _with constraints_ was given
in [26]. Implicitly, this gives a Kripke model theory for the logic of
$\lambda$Prolog by choosing the right constraint system, with
$\beta\eta$-reduction handled by equational constraint manipulation. The
applicability to $\lambda$Prolog is indirect, as it is based on a constraint-
based sequent calculus and not on resolution rules. As a result the semantics
is not operational, as the one introduced in this paper (based on Nadathur’s
[33]) is, and does not have the flexibility of our broader class of algebraic
models. Lastres [23, 13] produced a denotational semantics for FOHH and gave
definitions for the higher-order case, in 2002\. Also, the classical higher-
order Horn fragment was shown sound and complete with respect to a declarative
semantics introduced by Wolfram in [44], and independently by Blair and Bai in
[5], and Wadge in [43, 7]. Interestingly, [44] builds on the Takahashi–Andrews
V-complex model theory [38, 4] originally introduced to solve the Takeuti
conjecture for cut-elimination in classical higher-order logic, inducting on
types to deal with the impossibility of inducting on higher-order formulas,
which form an impredicative class. However, the larger hereditarily Harrop
fragment considered here requires intuitionistic logic as discussed in the
cited papers by Miller and Nadathur, and, consequently, an intuitionistic
model theory. See [11] for semantics of ICTT, the intuitionistic version of
Church’s type theory of which HOHH is an executable fragment.

HOHH with uniform proofs is here shown sound and complete with respect to
Uniform Algebras, an indexed version of typed Omega-set semantics similar to
that introduced by Rasiowa and Sikorski [37, 42] and Fourman and Scott [15],
for higher-order logic, and used to model ICTT in [11]. A bottom-up semantics
is also developed here, based on these structures, producing a minimal term
model as the least fixed point of an appropriate continuous operator.

The reader should note that (2) essentially mimics the AUGMENT rule [30] of
the uniform proof theory for $\lambda$Prolog for which reason we term it
operational semantics.

It is easily shown sound and complete for resolution, and admits a minimal
Herbrand–style model, definable as a suitable fixed point. What is harder is
to show that it agrees with full semantic logical consequence. In other words,
that an equivalent model of type (1) above exists. The formal difference above
between (1) and (2) reflects, in the semantics, the difference between full
provability and uniform provability.

The equivalence of the two notions of deduction was shown syntactically in
[30]. Semantic equivalence for two corresponding model theories (one for HOHH
and one for ICTT) was shown directly for the FOHH fragment in [10], and for
the ICTT/HOHH logics with constraints in [26].

We now proceed to define the syntax and proof theory of HOHH. In order to
justify the presence of (numerically) indexed variables in the syntax we
briefly discuss in the Appendix the problem that arises in proof search if we
do not enforce a device for keeping track of the change of signature that
takes place when solving universally quantified goals to avoid the
inconsistency that arises from allowing pre-existing logic variables to unify
with constants.

In order to reflect this problem _semantically_ we construct a countable
hierarchy of universes. We will need a supply of countably many fresh
variables and constants at each integer level $i$ and at every type $\alpha$,
as is further explained in the development of the UCTT type theory, below.

##### Indexed models, operationality and bottom-up semantics

In [29], Miller produced an indexed variant of Kripke models for a first-order
fragment of $\lambda$Prolog in which the conventional definition of truth in
Kripke semantics at a possible world $p$ in an arbitrary poset:

$p\Vdash A\supset B\qquad\mbox{\it iff \quad for every}\quad q\geq p,\qquad
q\Vdash A\,{\Rightarrow}\,q\Vdash B$ (1)

is replaced by:

$P\ |\\!\\!\\!\\!\\!\models D\supset G\qquad\mbox{\it iff }\qquad P,D\
|\\!\\!\\!\\!\\!\models G$ (2)

where $P$ and $D$ must be program formulae and $G$ a goal. Since the set of
possible worlds is fixed in advance, and consists of formulae, this semantics
— as far as programs are concerned — has some of the flavor of a term model.
In this paper, the model theory is in no sense restricted to term models: we
supply arbitrary carriers for all types, including that of program formulae.
In this way we generalize Miller’s semantics in [29], in addition to extending
it to higher order logic with implication and universal quantification in
goals as well.

We now proceed to define the syntax and proof theory of HOHH. In order to
justify the presence of (numerically) indexed variables in the syntax we
briefly discuss in the Appendix the problem that arises in proof search if we
do not enforce a device for keeping track of the change of signature that
takes place when solving universally quantified goals.

##  2 Syntax of the Logic and the Programming Language

The fundamental aim of this paper is to define a semantics for an executable
fragment of logic, one that need not extend easily to the full underlying
logic. It is the underlying logic (ICTT), however, that gives declarative
content to a logic program, and it is for this reason that we term a model
theory for ICTT, as developed in [11], declarative and a model theory for HOHH
operational.

Before presenting the calculus we review the definition of HOHH programs and
goals, upon which UCTT based.

###  2.1 The ICTT Calculus and HOHH Programs

We recall the definitions of the Intuitionistic fragment of Church’s Theory of
Types (ICTT) upon which the HOHH is built and programs defined.

Church’s calculus consists of a collection of higher-order functional types
together with a simply typed lambda-calculus of terms. Connectives and
quantifiers are given explicitly as typed constants in the language. The set
of base types must include a type of logical formulas, as well as a type of
individuals. Proofs are defined by a sequent calculus for logical formulas. In
more detail:

Type expressions

are formed from a set of base types (which must include at least the type
$\iota$ of individuals and $o$ of truth values, or formulae) via the
functional (or arrow) type constructor: if $\alpha$ and $\beta$ are types then
so is $\alpha\\!\rightarrow\\!\beta$. Church’s notation for functional type
expressions is sometimes more convenient because of its brevity:
$(\beta\alpha)$ denotes the type $\alpha\\!\rightarrow\\!\beta$. Association,
in Church’s notation, is to the left whereas arrow terms associate to the
right: $\alpha\beta\gamma$ denotes $(\alpha\beta)\gamma$, meaning
$\gamma\\!\rightarrow\\!\beta\\!\rightarrow\\!\alpha$, which is the same as
$\gamma\\!\rightarrow\\!(\beta\\!\rightarrow\\!\alpha)$. We will use his
notation interchangeably with arrow notation, especially with complex type
expressions.

Terms

are always associated with a type expression, and are built up from typed
constants and typed variables (countably many at each type $\alpha$):
$x^{1}_{\alpha},x^{2}_{\alpha},\ldots,y^{1}_{\alpha},y^{2}_{\alpha},\ldots$
according to the following definition:

  1. 1.

A variable $x_{\alpha}$ is a term of type $\alpha$.

  2. 2.

A constant of type $\alpha$ is a term of type $\alpha$.

  3. 3.

If $t_{1}$ is a term of type $\alpha\\!\rightarrow\\!\beta$ and $t_{2}$ is a
term of type $\alpha$ then $t_{1}t_{2}$ is a term of type $\beta$, called an
application.

  4. 4.

If $t$ is a term of type $\beta$ then $\lambda x_{\alpha}.t$ is a term of type
$\alpha\\!\rightarrow\\!\beta$, called an abstraction.

Terms may be displayed subscripted with their associated type, when
convenient. We omit such subscripts from variables when clear from context, or
when the information is of no interest.

Logical Constants

The following logical constants are available to define formulas:

$\top_{o},\bot_{o},\land_{ooo},\lor_{ooo},\supset_{ooo},$

as well as

$\Sigma_{o(o\alpha)}\quad\mbox{\small and }\quad\Pi_{o(o\alpha)},$

the latter two existing for all types $\alpha$.

Note that because of currying in Church’s type theory, the constants
$\wedge,\vee$ corresponding to the usual binary logical connectives, have
higher types $ooo$, i.e. $o\\!\rightarrow\\!(o\\!\rightarrow\\!o)$.

The meaning of the logical constants $\land$, $\lor$ and $\supset$ is evident,
while $\Sigma$ and $\Pi$ are used to define the quantifiers $\exists$ and
$\forall$: $\exists x_{\alpha}.P_{o}$ is an abbreviation for
$\Sigma_{o(o\alpha)}\lambda x_{\alpha}.P_{o}$ and $\forall x_{\alpha}.P_{o}$
is an abbreviation for $\Pi_{o(o\alpha)}\lambda x_{\alpha}.P_{o}$. Also,
$f(x_{\alpha})$ is an abbreviation of $f_{\beta\alpha}x_{\alpha}$, for some
$\beta$. We will often write logical formulas in infix form, e.g. $A\supset
B,A\wedge B$. This should be viewed as informal notation for the true terms
involved: $\supset_{ooo}AB,\wedge_{ooo}AB$.

##### Reduction

Two terms are called _$\alpha$ -convertible_ if it is possible to obtain one
from the other by renaming bound variables. We recall that a $\beta$-redex is
a term $(\lambda x.t)u$, formed by application of an abstraction to any
compatibly typed term. The contractum (or $\beta$-contraction) of such a term
is defined to be any term $t[u/x]$ resulting from the substitution (after
renaming of bound variables if necessary to avoid capture) of $u$ for all free
occurrences of $x$ in $t$. $\beta$-contraction also refers to the binary
relation between redices and contracta. The transitive closure of this binary
relation and its extension to terms containing redices in subterms is called
$\beta$-reduction. Contraction of $\eta$-redices $\lambda x.tx$ to $t$ when
$x$ does not occur freely in $t$ induces $\eta$-reduction. In this paper we
will refer to the combination of both reductions, $\beta\eta$-reduction as
$\lambda$-reduction, and the reflexive, symmetric, transitive closure of this
relation as $\lambda$-equivalence. If a term cannot be $\lambda$-reduced we
say it is in _normal form_.

In Church’s Theory, as in Andrews, Miller and Nadathur’s work, a canonical
linear ordering of variables is used to ensure the existence of unique
_principal_ normal forms111A term in principal normal form, as defined in [8]
is a term in normal form in which no variable occurs both free and bound, and
in which bound variables must be consecutive variables in increasing order,
with no omissions, save those variables which occur freely in the term. In [8]
it is shown that for each normal term there is a unique equivalent term in
principal normal form. ${\bf nf(}{t}{\bf)}$ for each term $t$, by enforcing a
specific choice of bound variables. Since we do not want to bother with
$\lambda$-equivalence and $\alpha$-conversion, in the following we assume that
all terms are always in principal normal form, and automatically converted to
principal normal form at the end of every operation.

######  Definition 2.1.

A formula is any term of type $o$. An atomic formula is a term of type $o$
which is not $\lambda$-equivalent to any term whose head is a logical
constant.

An atomic formula (in normal form) is either a variable $X_{o}$ or a term of
the form $pt_{1}\cdots t_{m}$ with the $t_{i}$ (each of type $\alpha_{i}$) in
normal form and $p$ a non-logical constant or variable of type
$\alpha_{1}\rightarrow\cdots\alpha_{m}\rightarrow o$. If $p$ is a constant,
the formula is called _rigid_ , otherwise _flex_.

${\Gamma}\,\vdash\,{\top}\qquad{\Gamma,U}\,\vdash\,{U}$

${\Gamma,B\land
C}\,\vdash\,{A}{\Gamma,B,C}\,\vdash\,{A}\qquad{\Gamma}\,\vdash\,{B\land
C}\lx@proof@logical@and{\Gamma}\,\vdash\,{B}{\Gamma}\,\vdash\,{C}$

${\Gamma,B\lor
C}\,\vdash\,{A}\lx@proof@logical@and{\Gamma,B}\,\vdash\,{A}{\Gamma,C}\,\vdash\,{A}\qquad{\Gamma}\,\vdash\,{B_{1}\lor
B_{2}}{\Gamma}\,\vdash\,{B_{i}}$

${\Gamma,B\supset
C}\,\vdash\,{A}\lx@proof@logical@and{\Gamma}\,\vdash\,{B}{\Gamma,C}\,\vdash\,{A}\qquad{\Gamma}\,\vdash\,{B\supset
C}{\Gamma,B}\,\vdash\,{C}$

${\Gamma,\forall
x.P}\,\vdash\,{A}{\Gamma,P[t/x]}\,\vdash\,{A}\qquad{\Gamma}\,\vdash\,{\forall
x.P}{\Gamma}\,\vdash\,{P[c/x]}$

${\Gamma,\exists
x.P}\,\vdash\,{A}{\Gamma,P[c/x]}\,\vdash\,{A}\qquad{\Gamma}\,\vdash\,{\exists
x.P}{\Gamma}\,\vdash\,{P[t/x]}$

${\Gamma}\,\vdash\,{B}{\Gamma}\,\vdash\,{\bot}$

Constants appearing in rules marked with an asterisk are fresh.

Figure 1: Higher-order Sequent Rules of $\textsf{ICTT}^{c}$.

###  2.2 Deduction

We assume familiarity with Gentzen’s sequent calculus, and in particular the
intuitionistic LJ (see e.g. [17]). We present here, in Figure 1, a sequent
system for ICTT, similar to that of e.g. [30] of Miller et al. Following them,
we modify the $\forall_{R}$ and $\exists_{L}$ rules of the calculus to use
fresh constants instead of fresh eigenvariables. We call the modified calculus
$\textsf{ICTT}^{c}$. It is easily seen equivalent to the more conventional
version. Since all formulas are in principal normal form, we avoid the need
for Miller and Nadathur’s $\lambda$-rule (which allows replacement of any
parts of a sequent by $\lambda$-equivalent formulas). In the rest of the
paper, with ICTT we denote the $\textsf{ICTT}^{c}$ calculus in Figure 1.

In the sequent calculus displayed above all sequents ${\Gamma}\,\vdash\,{A}$
consist of a set of formulas (antecedents) $\Gamma$ and a single formula $A$
(consequent). The symbol $U$ in the identity rule stands for any atomic
formula. The rules of inference shown in the figure consist of premisses: the
zero, one or two sequents above the line and conclusions: the lone sequent
below the line.

######  Lemma 2.2.

Left-weakening, left-contraction and CUT are derived rules in ICTT.

The first claim is a very easy consequence, by induction on proof depth, of
the fact that the two initial sequents in ICTT, the sequents
${\Gamma}\,\vdash\,{\top}$ and ${\Gamma,U}\,\vdash\,{U}$ are allowed for any
set of formulas $\Gamma$. The derivability of CUT in ICTT is established in
[11].

###  2.3 The UCTT Calculus

##### Programs and Goals

Let ${\mathcal{H}}$ be the set of positive terms, the terms which do not
include $\bot$, $\supset$ or $\forall$; $A$ will refer to an atomic formula
over ${\mathcal{H}}$ and $A_{r}$ to a rigid atomic formula over
${\mathcal{H}}$. Let $G$ refer to a goal formula, $D$ to a definite clause
(that is, a single program formula), and $P$ to a set of program formulae;
$P\cup D$ or $P,D$ when clear from context, will stand for $P\cup\\{D\\}$. All
programs and goals are assumed in normal form.

######  Definition 2.3.

HOHH program formulae $D$ and goal formulae $G$ are given by:

$\displaystyle D$ $\displaystyle::=$ $\displaystyle A_{r}\mid G\supset
A_{r}\mid D\land D\mid\forall x.D$ $\displaystyle G$ $\displaystyle::=$
$\displaystyle\top\mid A\mid G\lor G\mid G\land G\mid\exists x.G\mid D\supset
G\mid\forall x.G$

##### Bound and free variables

In order to simplify working with terms and substitutions, the language of the
UCTT fragment we now define will contain countably many symbols to be used
only as bound variables in logical formulas, and countably many symbols for
free variables, also called _logic variables_. Free and bound variables are
disjoint. The definition of principal normal form is simplified, since no
variables may occur both free and bound. Occasionally we will need to be
especially careful about free and bound variables and our notational
conventions. To this end we make the following definition.

######  Definition 2.4.

We define the set bvar of bound variables, and the set fvar, of free, or logic
variables. The bvar set has countably many variables of each of the types
specified below.

######  Remark 2.5.

The reader should be aware of certain uses of notation in this paper. For
example, when we define the instance resolution rule below, we replace a goal
of the form $\exists x.G$ by the goal $G[t/x]$ where $t$ is an arbitrary term
_all of whose free variables are in_ fvar. We are replacing the _freely
occurring_ bvar $x$ in $G$ by the term $t$. The result of this replacement is
a goal in which all freely occurring variables are in fvar. In other words,
variables in bvar may occur freely, but only in intermediate computations.

##### Subtypes of the formula type

and functions are barred from the calculus to make it impossible to form
illegal programs or goals. In particular, all terms appearing in atomic
formulae are positive. UCTT has, in addition, the following restrictions

  1. 1.

The base types are the types $\iota$ of individuals, ${\sf h}$ of (positive)
logical formulae, ${\sf a}$ of atoms, ${\sf r}$ of rigid atoms, ${\sf p}$ of
programs and ${\sf g}$ of goals, in addition to any user-defined types.

  2. 2.

There are inclusions between types as indicated in Figure 2. Thus, a term
$t_{\sf a}$ of atomic type may also be viewed as a term of goal type. One way
of formalizing this inclusion is to add constants such as ${\sf Inc}_{{\sf
a}{\sf r}}$, $\mbox{\sf Inc}_{{\sf p}{\sf a}}$ ${\sf Inc}_{{\sf g}{\sf a}}$.
We will occasionally display these maps explicitly, but to save the reader
fatigue, we will eventually employ them tacitly in the semantics (as
inclusions). Other implicit inclusions are shown as dashed lines above.

  3. 3.

All other types are functional types $\beta\alpha$.

  4. 4.

The logical constants are $\top_{\sf g}$, $\top_{\sf h}$, $\land_{{\sf p}{\sf
p}{\sf p}}$, $\land_{{\sf g}{\sf g}{\sf g}}$, $\land_{{\sf h}{\sf h}{\sf h}}$,
$\lor_{{\sf g}{\sf g}{\sf g}}$, $\lor_{{\sf h}{\sf h}{\sf h}}$, $\supset_{{\sf
g}{\sf g}{\sf p}}$, $\supset_{{\sf p}{\sf r}{\sf g}}$, $\Sigma_{{\sf g}({\sf
g}\alpha)}$, $\Sigma_{{\sf h}({\sf h}\alpha)}$, $\Pi_{{\sf g}({\sf
g}\alpha)}$, $\Pi_{{\sf p}({\sf p}\alpha)}$ and $\Pi_{{\sf h}({\sf
h}\alpha)}$.

  5. 5.

Constants of type ${\sf r}\alpha_{1},\cdots\alpha_{n}$ and both constants and
variables of type ${\sf a}\alpha_{1}\cdots\alpha_{n}$ are allowed, for $n\geq
0$, and $\alpha_{i}={\sf h}$ or a non-logical type.

  6. 6.

There may be no other constants or variables of types ${\sf p}$ or ${\sf g}$,
nor of functional types involving ${\sf p}$ or ${\sf g}$, other than those
which come from the included types ${\sf r}\subseteq{\sf a}\subseteq{\sf g}$.
For example $X_{\sf a}$ is a legal term of type ${\sf g}$, because it is a
legal atom, but $X_{{\sf p}{\sf g}}$ is not, since it could never have been
formed in ${\sf a}$.

Note that because of the typing of $\supset$ it is impossible to construct
negative formulae in ${\sf h}$ or as subformulae of atomic formulae.

${{\sf g}}$${{\sf r}}$${{\sf a}}$${{\sf h}}$${o}$${{\sf p}}$IncIncIncInc
Figure 2: Type Structure of UCTT

###  2.4 Levels and Signatures

As discussed in the Appendix A.1 we will need to construct a countable
hierarchy of universes (signatures), in order to avoid the inconsistency that
arises from allowing pre-existing logic variables to unify with constants
introduced during execution for the sake of universal goals.

Let ${\cal U}_{0}(\alpha)$ include all constants and variables in bvar of type
$\alpha$, along with countably many logic variables in fvar; constants and
variables of ${\cal U}_{0}$ are labelled with the integer $0$, indicated with
a subscript unless clear from context or immaterial to the discussion at hand.
The set ${\cal U}_{i}(\alpha)$ will include ${\cal U}_{j}(\alpha)$ for all
$j<i$ along with a new set of countably many logic variables in fvar and
countably many fresh constants of type $\alpha$, labelled with the index $i$.

A (positive) term over ${\cal U}_{i}$ contains only typed constants and
variables from $\bigcup_{\alpha}{\cal U}_{i}(\alpha)$. A program over ${\cal
U}_{i}$ is a program whose terms are all over ${\cal U}_{i}$.

We will often refer to the level of a term, program, goal, set of goals, or
individual or sequences of states, to be defined below. It always refers to
the maximum label of any constant or logic variable present in the
corresponding structure. If $t$ is a term, we write ${\sf fv}({t})$ to refer
to the set of free variables in $t$. If $S$ is a set of terms, then ${\sf
fv}({S})$ is the union of all ${\sf fv}({t})$ with $t\in S$.

##### Substitutions

Substitutions are functions from variables to terms with finite support. That
is to say, off of a finite set of variables, a substitution must coincide with
the identity function. We will refer to the set of variables not fixed by a
substitution as its domain or support. The image of a substitution when
restricted to its set of support will be called its range. As is often done in
the literature, we will sometimes just mean the set of free variables
occurring in this image.

We will call a substitution legal if its range is in the set of positive
terms, it preserves type, and is level-preserving, so that only a term over
the universe ${\cal U}_{i}$ is substituted for a logic variable of label $i$.
The level of a substitution is the maximum level of all the terms in its
range. Since substitutions will almost always be legal in this paper (which
will not stop us from reminding the reader of their legality from time to
time) we distinguish notationally between substitutions, represented by Greek
letters such as
$\theta,\theta_{1},\theta_{2},\ldots,\varphi,\varphi_{1},\varphi_{2}\ldots$,
and instantiations $Q[t/x]$ which denote the result of replacing all free
occurrences of $x$ in the goal, program, state or state vector $Q$ by the term
$t$. Unless explicitly stated, instantiations may violate the level
restriction imposed on substitutions, but never type preservation. If we call
an instantiation legal, we mean levels are preserved.

##### Applying a substitution to a term.

If $\theta$ is a substitution, we will abuse language and denote its lifting
to a function on terms with the same symbol. This lifting is defined as
follows

$\theta(t)=t[\theta(x_{1})/x_{1},\ldots,\theta(x_{n})/x_{n}]$

where $x_{1},\ldots,x_{n}$ are precisely the variables in the domain of
$\theta$. Note that no capturing of free variables may occur since we have
disjoint sets for free and bound variables. We will write the application of a
substitution $\theta$ to a variable (or term) $u$ as $u\theta$ as an
alternative to $\theta(u)$.

Now that we have defined the application of a substitution to a term,
composition of substitutions makes sense. We will write compositions of
substitutions in diagrammatic form: $\theta_{1}\theta_{2}$ is the substitution
that maps a variable $x$ to $\theta_{2}(\theta_{1}(x))$.

When a substitution is applied to a set of terms, it is understood to be
applied to each term separately. This notation will be used in particular for
programs.

In order to avoid many problems with possible variable name clashes in
deductions, we will make use of a particularly useful kind of substitution.

######  Definition 2.6.

We will say a substitution is safe or idempotent if the free variables in its
range are disjoint from its domain.

It is easy to see that a substitution $\theta$ is safe precisely when it is
idempotent in the usual algebraic sense, namely when $\theta\theta=\theta$.

###  2.5 Proof procedures for HOHH Formulae

We now present two non-deterministic transition systems we call RES(Y) and
RES(t), along the lines of [33] but with some significant notational
differences, as a proof theory for UCTT. These differences are discussed in
some detail in Section A.3 in the appendix.

Instead of the constrained sequent system that was used in [30] to define
uniform proofs we use an operational proof system so as better to model the
behavior of programs. Rather than attempt to automate the $\land_{L}$ and
$\forall_{L}$ rules of the sequent calculus explicitly, we decompose the
program into simple clauses.

We begin with a few technical lemmas.

######  Lemma 2.7.

The following complexity measure defines a well-ordering on program formulas.

  * •

$\delta(A_{r})=0$

  * •

$\delta(G\supset A_{r})=0$

  * •

$\delta(D_{1}\wedge D_{2})=1+max\\{\delta(D_{1}),\delta(D_{2})\\}$

  * •

$\delta(\forall xD)=1+\delta(D)$

An easy consequence is

######  Lemma 2.8.

For all program formulas $D$ and terms $t$, $\delta(D[t/x])=\delta(D)$.

######  Definition 2.9 (elaboration of a program).

Given a program formula $D$ we define the set of _clauses_ $\textsf{elab}(D)$,
the _elaboration_ of $D$, by induction on the complexity of $D$, as follows:

  * •

$\textsf{elab}(A_{r})=\\{A_{r}\\}$

  * •

$\textsf{elab}(G\supset A_{r})=\\{G\supset A_{r}\\}$

  * •

$\textsf{elab}(D_{1}\wedge
D_{2})=\textsf{elab}(D_{1})\cup\textsf{elab}(D_{2})$

  * •

$\textsf{elab}(\forall xD)=\\{\forall xD^{\prime}\mid
D^{\prime}\in\textsf{elab}(D)\\}.$

Moreover, if $P$ is a program, we have $\textsf{elab}(P)=\bigcup_{D\in
P}\textsf{elab}(D)$.

Formally, in order to respect the condition that only variables in fvar may
occur freely, the definiton of $\textsf{elab}(\forall xD)$ should be
$\\{\forall xD^{\prime}[x/X]\mid D^{\prime}\in\textsf{elab}(D[X/x])\\}$, where
$X\in{\textbf{fvar}}$ does not occur in $D$. However, when the formal
definition is too cumbersome, like in this case, we prefer to use a more
informal but intuitive notation, using the same symbol to denote both the
bound variable in bvar and the replaced variable in fvar.

We will need some technical lemmas about elab.

######  Lemma 2.10.

Given a program formula $D$ and a clause $K\in\textsf{elab}(D)$:

  * •

the set of free variables occuring in $K$ is a subset of the set of free
variables occuring in $D$;

  * •

the complexity of $K$ is not greater than the complexity of $D$.

###### Proof.

Immediate by induction on the complexity of $D$. ∎

######  Lemma 2.11 (clause instance).

Let $D$ be a program formula and $\theta$ be a substitution, either legal or
not. If $K\in\textsf{elab}(P)$ then $K\theta\in\textsf{elab}(P\theta)$.

###### Proof.

The proof is by induction on the complexity of $D$. If $D=G\supset A_{r}$,
then $K=D$ and $\textsf{elab}(D\theta)=\textsf{elab}(G\theta\supset
A\theta)=\\{G\theta\supset A\theta\\}=\\{D\theta\\}$. The case when $D$ is a
rigid atom is similar to the previous one. If $D=D_{1}\wedge D_{2}$, assume
$K\in\textsf{elab}(D_{j})$ for $j\in\\{1,2\\}$. By inductive hypotehsis,
$K\theta\in\textsf{elab}(D_{j}\theta)$, hence
$K\theta\in\textsf{elab}(D_{1}\theta\wedge
D_{2}\theta)=\textsf{elab}(D\theta)$.

Finally, if $D=\forall x\bar{D}$ and using the more formal definition given
above, we have that $K=\forall x(\bar{D}^{\prime}[x/X])$ with
$\bar{D}^{\prime}\in\textsf{elab}(\bar{D}[X/x])$ and $X\in{\textbf{fvar}}$
does not occur in $\bar{D}$. Now consider a variable $w$ which does not occur
in $\bar{D}$, $\bar{D}^{\prime}$ and $\theta$. By inductive hypothesis,
$\bar{D}^{\prime}[w/X]\in\textsf{elab}(\bar{D}[X/x][w/X])=\textsf{elab}(\bar{D}[w/x])$.
Again, by inductive hypothesis,

$\bar{D}^{\prime}[w/X]\theta\in\textsf{elab}(\bar{D}[w/x]\theta)=\textsf{elab}(\bar{D}\theta[w/x]).$

Therefore, by definition of the elaboration of a program, $\forall
x(\bar{D}^{\prime}[w/X]\theta[x/w])\in\textsf{elab}(\forall
x(\bar{D}\theta))=\textsf{elab}((\forall
x\bar{D})\theta)=\textsf{elab}(D\theta)$. Finally, note that

$\forall x(\bar{D}^{\prime}[w/X]\theta[x/w])=\forall
x(\bar{D}^{\prime}[w/X][x/w])\theta=(\forall
x\bar{D}^{\prime}[x/X])\theta=K\theta.\qed$

In the following prove, we omit the renaming of a bound variable $x$ with the
free variable $X$, and we use the same letter to denote both the free and
bound variable, although they are technically different. The following lemma
is a partial converse of the preceding one.

######  Lemma 2.12.

Let $D$ be a program formula, $t$ a term and $K$ a clause. If
$K\in\textsf{elab}(D[t/x])$ for any term $t$, then there is a clause $\forall
xK^{\prime}$ in $\textsf{elab}(\forall xD)$ such that $K^{\prime}[t/x]=K$.

###### Proof.

We sketch a proof by induction on the program formula $D$. If $K$ is a clause
in $\textsf{elab}((G\supset A_{r})[t/x])$ then $K=(G\supset A_{r})[t/x]$ and
obviously $\forall x(G\supset A_{r})\in\textsf{elab}(\forall x(G\supset
A_{r}))$. The case when $D$ is a rigid atom is similar to the previous one.
The inductive cases are given by $D_{1}\wedge D_{2}$ and $\forall xD_{0}$. In
the first case, $K\in\textsf{elab}((D_{1}\wedge D_{2})[t/x])$, hence in one of
$\textsf{elab}((D_{i}[t/x])$ for $i=1$ or $2$. By the induction hypothesis,
there is a clause $\forall xK^{\prime}$ in $\textsf{elab}(\forall xD_{i})$
with $K^{\prime}[t/x]=K$. But since $\textsf{elab}(\forall
xD_{i})\subseteq\textsf{elab}(\forall x(D_{1}\wedge D_{2}))$ we are done. Now
suppose $K\in\textsf{elab}(\forall y(D[t/x]))$ where since $y$ is in bvar, $y$
is not free in $t$. Then $K\in\\{\forall yD^{\prime}\mid
D^{\prime}\in\textsf{elab}(D[t/x])\\}$, so $K=\forall y.D^{\prime}$ for some
$D^{\prime}$ in $\textsf{elab}(D[t/x])$. By the induction hypothesis, there is
$K^{\prime}\in\textsf{elab}(D)$ such that $K^{\prime}[t/x]=D^{\prime}$. Thus,
$\forall x\forall yK^{\prime}\in\textsf{elab}{\forall xD}$ and $(\forall
yK^{\prime})[t/x]=K$. ∎

######  Lemma 2.13 (clause generalization).

Let $D$ a program formula, $x$ a variable, $c$ a costant and
$K\in\textsf{elab}(D[c/x])$. Then there is a clause
$\hat{K}\in\textsf{elab}(D)$ such that $\hat{K}[c/x]=K$.

###### Proof.

Follows by induction on the complexity of $D$, like the previous lemmas. ∎

######  Lemma 2.14.

Suppose $K\in\textsf{elab}(D)$ where $D$ is a program formula. If
${\Gamma,K}\,\vdash\,{G}$ then ${\Gamma,D}\,\vdash\,{G}$.

###### Proof.

We proceed by induction on the height of the proof of
${\Gamma,K}\,\vdash\,{G}$. We consider several cases, according to the last
rule used in this proof.

If the last (and only) rule is $\top_{R}$, then the lemma holds trivially. For
all the other rules, the cases when $K$ is not the principal formula easily
follows by induction. However, particular care must be given to the
$\forall_{R}$ and $\exists_{L}$, due to the freshness conditions.

  * •

if the last rule used is $\forall_{R}$, then we have

${\Gamma,K}\,\vdash\,{\forall x.G}{\Gamma,K}\,\vdash\,{G[c/x]}$

where $c$ is a fresh constant. It easy to check that in the proof of
${\Gamma,K}\,\vdash\,{G[c/x]}$ we can replace $c$ with any constant
$c^{\prime}$ to get a proof of ${\Gamma,K}\,\vdash\,{G[c^{\prime}/x]}$.
Therefore, consider any $c^{\prime}$ which does not occur freely in $D$ or
$\Gamma$. By inductive hypothesis, we have
${\Gamma,D}\,\vdash\,{G[c^{\prime}/x]}$ and since $c^{\prime}$ does not occur
in $\Gamma,D$, by $\forall_{R}$ we get ${\Gamma,D}\,\vdash\,{\forall xG}$.

  * •

if the last rule used is $\exists_{L}$, the proof proceeds as above.

When we restrict our attention to the case in which $K$ is the principal
formula, only Ax and left rules need to be considered. Moreover, if the last
rule is $\exists_{L}$, $\vee_{L}$ or $\wedge_{L}$, then $K$ cannot be the
principal formula.

  * •

If the last rule is Ax, then $K=A_{r}$ is a rigid atom, and the proof follows
by induction on the complexity of $D$. If $D=A_{r}$, then the result follows
by left contraction. If $D=D_{1}\wedge D_{2}$, then $K\in\textsf{elab}(D_{i})$
for some $i\in\\{1,2\\}$. By inductive hypothesis, $D_{i},K\vdash G$, the
result follows from the $\wedge_{L}$ rule and left weakening. The other cases
for $D$ are incompatible with the form of $K$.

  * •

If the last rule is $\forall_{L}$, i.e., $K=\forall xK^{\prime}$, we have

${\Gamma,\forall
xK^{\prime}}\,\vdash\,{G}{\Gamma,K^{\prime}[t/x]}\,\vdash\,{G}$

We now proceed by induction on the complexity of $D$. The cases when $D$ is an
atom or an implication are not consistent with $K$. If $D=\forall xD^{\prime}$
then $K^{\prime}\in\textsf{elab}(D^{\prime})$. By Lemma 2.11 we have that
$K^{\prime}[t/x]\in\textsf{elab}(D^{\prime}[t/x])$, hence by inductive
hypothesis on the height of the proof,
${\Gamma,D^{\prime}[t/x]}\,\vdash\,{G}$. The result follows from the
$\forall_{L}$ rule. Finally, if $D=D_{1}\wedge D_{2}$ then $\forall
xK^{\prime}\in\textsf{elab}(D_{j})$ for $j\in\\{1,2\\}$. By inductive
hypothesis on the structure of $D$, we have ${\Gamma,D_{j}}\,\vdash\,{G}$ and
the result follows from the $\wedge_{L}$ rule and left weakening.

  * •

If the last rule is $\supset_{L}$, i.e., $K=G^{\prime}\supset A$, we have

${\Gamma,G^{\prime}\supset
A}\,\vdash\,{G}\lx@proof@logical@and{\Gamma}\,\vdash\,{G^{\prime}}{\Gamma,A}\,\vdash\,{G}$

We now proceed by induction on the complexity of $D$. If $D=G^{\prime}\supset
A$, there is nothing to prove. If $D=D_{1}\wedge D_{2}$, then
$G^{\prime}\supset A\in\textsf{elab}(D_{i})$ for some $i$. By inductive
hypothesis, we have a proof of $\Gamma,D_{i}\vdash G$, and we get the proof of
$\Gamma,D\vdash G$ using the $\wedge_{L}$ rule and left weakening. The other
cases are not consistent with the form of $K$. ∎

######  Definition 2.15.

Let the signatures be given as above.

A state is a triple $\langle{i};{P}\mid{G}\rangle$ where $i$ is a non-negative
integer, $P$ is a program and $G$ a goal, both over the signature ${\cal
U}_{i}$; $i$ is referred to as the state index.

A state vector
$\langle{i_{1}};{P_{1}}\mid{G_{1}}\rangle,\dots,\langle{i_{j}};{P_{j}}\mid{G_{j}}\rangle,\dots,\langle{i_{n}};{P_{n}}\mid{G_{n}}\rangle$
is a finite sequence of states. State vectors will be abbreviated to $\
{\mathfrak{A}},\ \langle{i};{P}\mid{G}\rangle,\ {\mathfrak{B}}$, where
${\mathfrak{A}}$ and ${\mathfrak{B}}$ denote (possibly empty) finite sequences
of states. The empty or null state vector is denoted ${\Box}$.

The full structure of state vectors is required on several accounts: indices
allow manipulation of universal quantification in goals, as discussed above;
programs must be displayed because they are susceptible to change during
execution, as they may be augmented to prove conditional goals. Vectors of
multiple states are necessary for the decomposition and subsequent tracking of
conjunctive goals, since, under resolution, the state
$\langle{i};{P}\mid{G_{1}\wedge G_{2}}\rangle$ spawns two independent states
$\langle{i};{P}\mid{G_{1}}\rangle,\langle{i};{P}\mid{G_{2}}\rangle$. These, in
turn may undergo independent updates of $i$ and $P$ depending on the structure
of their respective goals.

When a substitution is applied to a state vector ${\mathfrak{A}}$, it is
understood to be applied to the program and to the goal of each state in the
vector. For example, if ${\mathfrak{A}}$ were the vector
$\langle{i_{1}};{P_{1}}\mid{G_{1}}\rangle,\dots,\langle{i_{n}};{P_{n}}\mid{G_{n}}\rangle$,
then ${\mathfrak{A}}\theta$ would be
$\langle{i_{1}};{P_{1}\theta}\mid{G_{1}\theta}\rangle,\dots,\langle{i_{n}};{P_{n}\theta}\mid{G_{n}\theta}\rangle$.

##### Resolution rules

The resolution reduction rules for HOHH include many of those familiar from
the first-order case. We make minor changes for handling higher-order terms.
We will use the tensor symbol $\otimes$ rather than the comma to indicate
concatenation of states and state-vectors, to make clear the distinction
between formalized conjunction of goals written with conjunctions, (or with
commas in traditional Horn program code) and its meta-mathematical counterpart
on states.

Formally, resolution $\mathbf{\leadsto}$, is a ternary relation on

${\textit{state vectors}\times\textit{subs}\times\textit{state vectors}},$

but where we write
$\mathfrak{A}\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\mathfrak{B}$
instead of $\mathbf{\leadsto}(\mathfrak{A},\theta,\mathfrak{B})$.

Certain instances of resolution below are annotated with connectives
$\forall,\exists,\supset,\wedge,\vee$. They denote the identity substitution,
although clearly they give more information, namely the rule invoked. All
resolution rules below show a transition of a state vector of the form
${\mathfrak{A}}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{B}}$ to
another state vector. The distinguished state $\langle{i};{P}\mid{G}\rangle$
in such a transition is called the selected state of the resolution step, and
the rule used, the selected rule.

null

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{\top}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}{}\otimes{\mathfrak{B}}{}$

deletion of $\top$ goals.

true

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{A}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}{\theta}\otimes{\langle{i};{P\theta}\mid{\top}\rangle}\otimes{\mathfrak{B}}{\theta}$

where $A$ atomic, $A\theta=\top$ and $\theta$ is not the identity.

When $\theta$ is the identity substitution, this is not a legal resolution
step since it makes no progress. In practice, the null step above would be
performed instead.

backchain

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{A^{\prime}}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}{\theta}\otimes{\langle{i};{P\theta}\mid{G\delta\theta}\rangle}\otimes{\mathfrak{B}}{\theta}$

where $A^{\prime}$ atomic and rigid, $\forall x_{1}\cdots\forall
x_{n}(G\supset A)\in\textsf{elab}(P)$,
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ is a substitution mapping
variables $x_{1},\ldots,x_{n}$ to fresh variables of level $i$ or less, and
$\theta$ is a legal substitution such that $A^{\prime}\theta=A\delta\theta$.
Here _fresh_ means that the variable has never occured before in the
derivation.

axiom

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{A^{\prime}}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}{\theta}\otimes{\mathfrak{B}}{\theta}$

where $A^{\prime}$ atomic and rigid, $\forall x_{1}\cdots\forall
x_{n}A\in\textsf{elab}(P)$ and $\delta,\theta$ as for the backchain step: this
is essentially backchain for clauses without body.

orj

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{G_{1}\lor
G_{2}}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\lor}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i};{P}\mid{G_{j}}\rangle}\otimes{\mathfrak{B}}$
$(j\in\\{1,2\\})$

and

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{G_{1}\land
G_{2}}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\land}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle}\otimes{\mathfrak{B}}$

instance

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{\exists
x.G}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i};{P}\mid{G[t/x]}\rangle}\otimes{\mathfrak{B}}$

where $t$ is a term of level $i$ or less.

augment

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{D\supset
G}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\supset}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i};{P\cup
D}\mid{G}\rangle}\otimes{\mathfrak{B}}$

generic

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{\forall
x.G}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i+1};{P}\mid{G[c_{i+1}/x]}\rangle}\otimes{\mathfrak{B}}$

where $c_{i+1}$ is a fresh constant of label $i+1$ in
${\mathcal{U}}_{i+1}\setminus{\mathcal{U}}_{i}$.

It should be remarked that the main utility of the true rule is to dispatch
goals of the form $\langle{i};{P}\mid{X_{o}}\rangle$ or
$\langle{i};{P}\mid{Xt_{1}\cdots t_{m}}\rangle$ where the logic variable $X$
is of type $\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{m}\rightarrow o$ and
does not occur in $P$ or any other state. Since free variables in goals arise
because at some earlier stage they were existentially quantified after which
the instance rule was applied, this rule, implicitly proposed by Nadathur in a
proof procedure described in [33], formalizes as a logic programming step the
deduction of the sequent $P\vdash\exists x.xt_{1}\cdots t_{m}$ by
instantiating $x$ at $\lambda u_{1}\cdots\lambda u_{m}\top$.

######  Definition 2.16.

A resolution, or derivation, or deduction d, is a sequence of resolution steps

$\mathfrak{A}_{1}\stackrel{{\scriptstyle\theta_{1}}}{{\mathbf{\leadsto}}}\mathfrak{A}_{2}\cdots\mathfrak{A}_{n-1}\stackrel{{\scriptstyle\theta_{n-1}}}{{\mathbf{\leadsto}}}\mathfrak{A}_{n}$

Such a sequence is sometimes denoted

${\mathfrak{A}_{1}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}_{n}}$

with the convention that $\theta$ is the composition
$\theta_{1}\cdots\theta_{n}$ of all the intervening substitutions with domain
restricted to the variables free in  $\mathfrak{A}_{1}$. The substitution
$\theta$ is called the _computed answer (substitution)_ of the derivation. A
resolution ending in ${\Box}$ is called a successful resolution.

Note that a single state vector ${\mathfrak{A}}$ may itself be viewed as a
derivation with no steps. Here are some notational conventions that will be
useful below.

######  Definition 2.17.

If ${\bf d}$ is a resolution its first and last state will be denoted by
$\mathsf{first}(d)$ and $\mathsf{last}(d)$, its length by $\ell({\bf d})$. We
write ${\sf fv}({{\bf d}})$ to mean the set of all free variables occurring
anywhere in the sequence.

In general, many of our results will be stated for derivations with identity
computed answers. They may be generalized to the case of arbitrary
derivations, but this is not always immediate. If one wants to pursue this
direction, it might be convenient to use a domain of existentially quantified
substitutions, such $\textit{ISubst}_{\sim}$ in [2] or ESubst in [19].

For technical reasons, we will often restrict our interest to a particular
case of derivations for which not only the computed answer is the identity,
but also each intervening substitution has a very particular form.

######  Definition 2.18 (flat derivations).

A derivation
$\mathfrak{A}_{1}\stackrel{{\scriptstyle\theta_{1}}}{{\mathbf{\leadsto}}}\mathfrak{A}_{2}\cdots\mathfrak{A}_{n-1}\stackrel{{\scriptstyle\theta_{n-1}}}{{\mathbf{\leadsto}}}\mathfrak{A}_{n}$
is called flat when:

  * •

there are no occurrences of the true rule;

  * •

if the $i$-th step is an occurrence of the backchain or axiom rule, then
$\theta_{i}$ is safe and $\mathsf{dom}(\theta_{i})$ is restricted to the fresh
variables used to rename apart bound variables (the range of $\delta$, see the
definition of these two rules ).

We write

${\mathfrak{A}}_{1}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\mathfrak{A}}_{2}$

to denote a flat derivation.

###  2.6 Renaming Apart Derivations

We now focus on the relation between renamings and derivations. We start with
a technical lemma which explains how renaming of a substitution, intended as a
syntactic object, may be obtained trough composition.

######  Lemma 2.19.

Given a substitution $\theta=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ and a
renaming $\rho$, we have that
$\rho^{-1}\theta\rho=\\{t_{1}\rho/x_{1}\rho,\ldots,t_{n}\rho/x_{n}\rho\\}$.
Moreover, if $\theta$ is safe than $\rho^{-1}\theta\rho$ is safe, too.

###### Proof.

Let use denote $\rho^{-1}\theta\rho$ by $\eta$. First of all, it is obvious
that $x\rho\eta=x\theta\rho$ for each $x\in{\cal V\,}$. Therefore, for each
$i\in\\{1,\ldots,n\\}$, we have $x_{i}\rho\theta=t_{i}\rho\neq x_{i}\rho$. On
the contrary if $x$ is not one of the $x_{i}$’s, then
$x\notin\mathsf{dom}(\theta)$, hence $x\rho\eta=x\rho$. Therefore,
$\mathsf{dom}(\eta)=\\{x_{1}\rho,\ldots,x_{n}\rho\\}$. Finally, the
preservation of safety is easy to check. ∎

######  Definition 2.20.

A renaming is called _neutral_ if it maps variables to variables of the same
level.

The following lemma states that we can apply a neutral renaming to a
derivation and obtain another well-formed derivation.

######  Lemma 2.21.

Given a derivation ${\bf
d}:{\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$
and a neutral renaming $\rho$, there is a derivation ${\bf
d}^{\prime}:{\mathfrak{A}}\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\theta\rho}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}\rho$
obtained from ${\bf d}$ by renaming all state vectors and substitutions with
$\rho$. Moreover, if ${\bf d}$ is flat, then ${\bf d}^{\prime}$ is flat, too.

###### Proof.

Consider ${\bf d}^{\prime}$ obtained from ${\bf d}$ by renaming all state
vectors and substitutions with $\rho$, whereas the renaming of a substitution
$\gamma$ is $\rho^{-1}\gamma\rho$. For the moment, assume that ${\bf
d}^{\prime}$ is a derivation, and we prove that its computed substitution is
$\rho^{-1}\theta\rho$.

Assume that $\gamma_{1},\ldots,\gamma_{n}$ are the substitutions occurring in
${\bf d}$. Its computed substitution is
$\theta=(\gamma_{1}\cdots\gamma_{n})_{|X}$ where $X={\sf
fv}({{\mathfrak{A}}})$. The corresponding substitutions occurring in ${\bf
d}^{\prime}$ are $\rho^{-1}\gamma_{1}\rho,\ldots,\rho^{-1}\gamma_{n}\rho$, and
the computed substitution is
$\eta=(\rho^{-1}\gamma_{1}\cdots\gamma_{n}\rho)_{|Y}$ where $Y={\sf
fv}({{\mathfrak{A}}\rho})=\rho(X)$. It is easy to check that
$\eta=\rho^{-1}\theta\rho$. If $y\in\rho(X)$ the $y\rho^{-1}\in X$, hence
$y\eta=y\rho^{-1}\gamma_{1}\cdots\gamma_{n}\rho=y\rho^{-1}(\gamma_{1}\cdots\gamma_{n})_{|X}\rho=y\rho^{-1}\theta\rho$.
If $y\notin\rho(X)$, then $y\rho^{-1}\notin X$, hence $y\eta=y$ and
$y\rho^{-1}\theta\rho=y\rho^{-1}\rho=y$.

Note that, if ${\bf d}$ is safe, than ${\bf d}^{\prime}$ does not contain any
occurrence of the true rule, and all the substitutions in the backchain and
axiom steps are safe. The condition on the domain of these substitutions will
be checked later, completing the proof that ${\bf d}^{\prime}$ is safe, too.

We now prove by induction on the lenght of ${\bf d}$ that ${\bf d}^{\prime}$
is actually a derivation. The case when ${\bf d}$ has length zero is trivial.
For the inductive step, we consider different subcases according to the first
rule used in the derivation.

true:

The deduction ${\bf d}$ has the following shape:

$\hbox
to0.0pt{$\underbrace{{\mathfrak{A}}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}\gamma\otimes\langle{i};{P\gamma}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma}_{{\bf
d}_{1}}$\hss}{\mathfrak{A}}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}\overbrace{{\mathfrak{A}}\gamma\otimes\langle{i};{P\gamma}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}}^{{\bf
d}_{2}}$

while ${\bf d}^{\prime}$ is

$\hbox
to0.0pt{$\underbrace{{\mathfrak{A}}\rho\otimes\langle{i};{P\rho}\mid{G\rho}\rangle\otimes{\mathfrak{B}}\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\gamma\rho}}{{\leadsto}}}{\mathfrak{A}}\gamma\rho\otimes\langle{i};{P\gamma\rho}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma\rho}_{{\bf
d}^{\prime}_{1}}$\hss}{\mathfrak{A}}\rho\otimes\langle{i};{P\rho}\mid{G\rho}\rangle\otimes{\mathfrak{B}}\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\gamma\rho}}{{\leadsto}}}\overbrace{{\mathfrak{A}}\gamma\rho\otimes\langle{i};{P\gamma\rho}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\theta\rho}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}\rho}^{{\bf
d}^{\prime}_{2}}$

By inductive hypothesis ${\bf d}^{\prime}_{2}$ is a derivation. Note that,
since $\gamma$ is not the identity, the $\rho^{-1}\gamma\rho$ is not the
identity subtitution. Therefore ${\bf d}^{\prime}$ is a derivation, too.

backchain:

The proof is similar to the previous case, with

${\bf
d}={\mathfrak{A}}\otimes\langle{i};{P}\mid{A^{\prime}}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}\gamma\otimes\langle{i};{P\gamma}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{B}}\gamma\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}$

and

${\bf
d}^{\prime}={\mathfrak{A}}\rho\otimes\langle{i};{P\rho}\mid{A^{\prime}\rho}\rangle\otimes{\mathfrak{B}}\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\gamma\rho}}{{\leadsto}}}{\mathfrak{A}}\gamma\rho\otimes\langle{i};{P\gamma\rho}\mid{G\delta\gamma\rho}\rangle\otimes{\mathfrak{B}}\gamma\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\theta\rho}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}\rho$

We need to check that the conditions for the correct application of the
backchain rule are satisfied. Note that, since ${\bf d}$ is a derivation,
there is a clause $\forall x_{1}\cdots\forall x_{n}(G\supset
A)\in\textsf{elab}(P)$ such that $A\delta\gamma=A^{\prime}\gamma$, where
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ is the renaming-apart
substitution. By Lemma 2.11, we also have a clause $\forall x_{1}\cdots\forall
x_{n}(G\rho\supset A\rho)\in\textsf{elab}(P\rho)$. Consider
$\delta^{\prime}=\rho^{-1}\delta\rho=\\{\rho(w_{1})/\rho(x_{1}),\ldots,\rho(w_{n})/\rho(x_{n})\\}$.
Note that, since $w_{i}$ is fresh in the original derivation, $\rho(w_{i})$ is
fresh in the new one, hence $\delta^{\prime}$ is a renaming-apart
substitution. Since $\rho^{-1}\gamma\rho$ is an unifier for
$A\rho\delta^{\prime}$ and $A^{\prime}\rho$, and since
$G\rho\delta^{\prime}\rho^{-1}\gamma\rho=G\delta\gamma\rho$, the conditions
for the correct application of the backchain rule are satisfied.

Moreover, if ${\bf d}$ is flat then
$\mathsf{dom}(\gamma)\subseteq\\{w_{1},\ldots,w_{n}\\}$. It turns out that
$\rho^{-1}\gamma\rho$ is safe and
$\mathsf{dom}(\rho^{-1}\gamma\rho)\subseteq\\{\rho(w_{1}),\ldots,\rho(w_{n})\\}=\mathsf{dom}(\delta^{\prime})$,
which was the missing condition fot ensuring that ${\bf d}^{\prime}$ is flat.

axiom:

This is a simpler case of the backchain rule.

instance:

In this case

${\bf d}={\mathfrak{A}}\otimes\langle{i};{P}\mid{\exists
x.G}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\exists}}{{\leadsto}}}{\mathfrak{A}}\otimes\langle{i};{P}\mid{G[t/x]}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\theta^{\prime}}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}$

and

${\bf d}^{\prime}={\mathfrak{A}}\rho\otimes\langle{i};{P\rho}\mid{\exists
x.G\rho}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\exists}}{{\leadsto}}}{\mathfrak{A}}\rho\otimes\langle{i};{P\rho}\mid{G[t/x]\rho}\rangle\otimes{\mathfrak{B}}\rho\mathrel{\stackrel{{\scriptstyle\rho^{-1}\theta^{\prime}\rho}}{{\leadsto\cdots\leadsto}}}{\mathfrak{C}}\rho$

where all but the first step in ${\bf d}^{\prime}$ are valid by inductive
hypothesis. Note that $G[t/x]\rho=G\rho[t\rho/x]$, and since $\rho$ is
neutral, $t$ and $t\rho$ have the same level. Hence the first step in ${\bf
d}^{\prime}$ is valid, too.

null, or, and, augment, generic:

These cases follow immediately by the inductive hypothesis. ∎

In general, in all the proofs which follow, we will omit discussing the axiom
rule, since it is a simpler case of the backchain rule.

Using the previous result, the following lemma states that substitutions in a
derivation can be chosen not only to be idempotent (as we require) but in such
a way as to avoid any finite set of variables not containing any of the
variables of the first and last state vector.

######  Lemma 2.22.

Let d be a derivation
${\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$.
If $X$ is a finite set of variables such that $X\cap({\sf
fv}({{\mathfrak{A}}})\cup{\sf fv}({{\mathfrak{B}}})\cap{\sf
fv}({\theta}))=\varnothing$, then there is a derivation of ${\bf
d}^{\prime}:{\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$,
none of whose free variables lie in $X$. Moreover, if ${\bf d}$ is flat, then
${\bf d}^{\prime}$ is flat, too.

###### Proof.

Let $\rho$ be a neutral renaming which maps variables in $X$ to variables not
in $X$ or ${\sf fv}({{\bf d}})$. The derivation we are looking for is the one
obtained by Lemma 2.21. ∎

Due to the freshness condition in the generic rule, we sometimes need to
rename apart not only variable, but also constants.

######  Definition 2.23 (constant replacer).

A _constant replacer_ is a function mapping constants to constants of the same
type, which is the identity everywhere but for a finite set of constants. If
$X$ is any syntactic object and $\xi$ a constant renamer, $X\xi$ will be the
result of replacing every constant $c$ with $\xi(c)$. Similarly to
substitution, we define:

  * •

the _domain_ of a costant replacer $\xi$ to be the set
$\mathsf{dom}(\xi)=\\{c\mid\xi(c)\neq c\\}$;

  * •

the _range_ of a costant replacer $\xi$ to be the set
$\mathsf{rng}(\xi)=\xi(\mathsf{dom}(\theta))$;

  * •

the constant occuring in $\xi$ to be the set
$\mathsf{oc}(\xi)=\mathsf{dom}(\xi)\cup\mathsf{rng}(\xi)$.

A constant replacer which maps every constants to another one of the same
level is called _neutral_ , while a bijective constant replacer is called a
_constant renamer_.

######  Lemma 2.24 (clause constant replacing).

Consider a constant replacer $\xi$. If there is a clause
$K\in\textsf{elab}(D)$ then there is a clause $K\xi\in\textsf{elab}(D\xi)$.

###### Proof.

The proof is immediate by induction on the complexity of $D$. ∎

######  Lemma 2.25 (constant renaming).

Given a derivation ${\bf
d}:{\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$
and a neutral constant renamer $\xi$, there is a derivation ${\bf
d}^{\prime}:{\mathfrak{A}}\xi\mathrel{\stackrel{{\scriptstyle\theta\xi}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}\xi$
obtained from ${\bf d}$ by applying $\xi$ to all state vectors and
substitutions. Moreover, if ${\bf d}$ is flat, then ${\bf d}^{\prime}$ is
flat, too.

###### Proof.

Consider ${\bf d}^{\prime}$ obtained from ${\bf d}$ by applying $\xi$ to all
state vectors and substitutions, where the application of $\xi$ to a
substitution $\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ is the substitution
$\\{t_{1}\xi/x_{1},\ldots,t_{n}\xi/x_{n}\\}$. The proof is similar to the one
in Lemma 2.21.

We first assume that ${\bf d}^{\prime}$ is a derivation, and prove that its
computed substitution is $\theta\xi$. Assume that
$\gamma_{1},\ldots,\gamma_{n}$ are the substitutions occurring in ${\bf d}$.
Its computed substitution is $\theta=(\gamma_{1}\cdots\gamma_{n})_{|X}$ where
$X={\sf fv}({{\mathfrak{A}}})$. The corresponding substitutions occurring in
${\bf d}^{\prime}$ are $\gamma_{1}\xi,\ldots,\gamma_{n}\xi$, and the computed
substitution is $\eta=((\gamma_{1}\xi)\cdots(\gamma_{n}\xi))_{|X}$. It is easy
to check that
$(\gamma_{1}\xi)\cdots(\gamma_{n}\xi)=(\gamma_{1}\cdots\gamma_{n})\xi$, whence
$\theta=\eta$. Regarding flatness, since $\xi$ does not act on variables, if
${\bf d}$ is flat, then ${\bf d}^{\prime}$ is flat, too.

We now prove that ${\bf d}^{\prime}$ is a derivation. First of all, since
$\xi$ is injective, freshness conditions for constants introduced by the
generic rule in ${\bf d}^{\prime}$ are respected. The rest of the proof is by
induction on the length of ${\bf d}$. The case when ${\bf d}$ has length zero
is trivial. For the inductive step, we consider different cases according to
the first rule used in the derivation.

backchain:

The derivation ${\bf d}$ has the form

${\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{A}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\theta^{\prime}}}{{\leadsto\cdots\leadsto}}}{\Box}$

for some clause $\forall x_{1}\cdots\forall x_{n}(G\supset
A^{\prime})\in\textsf{elab}(P)$ and
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ a renaming-apart substitution
such that $A^{\prime}\delta\gamma=A\gamma$. Meanwhile, ${\bf d}^{\prime}$ is

${\mathfrak{A}}_{1}\xi\otimes\langle{i};{P\xi}\mid{A\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi\mathrel{\stackrel{{\scriptstyle\gamma\xi}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi\otimes\langle{i};{P\xi}\mid{G\delta\gamma\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi\mathrel{\stackrel{{\scriptstyle\theta^{\prime}\xi}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}\xi$

By Lemma 2.24, there is a clause $\forall x_{1}\cdots\forall x_{n}(G\xi\supset
A^{\prime}\xi)\in\textsf{elab}(P\xi)$. Moreover, it is easy to check that if
$A^{\prime}\delta\gamma=A\gamma$ then $A^{\prime}\delta\gamma\xi=A\gamma\xi$,
while $A\gamma\xi=A\xi(\gamma\xi)$ and
$A^{\prime}\delta\gamma\xi=A^{\prime}\xi\delta(\gamma\xi)$, i.e., $\gamma\xi$
is an unifier of $A\xi$ and $A^{\prime}\xi\delta$. Morevoer
$G\delta\xi\gamma\xi=G\delta(\gamma\xi)$. Therefore, the first step of
derivation ${\bf d}^{\prime}$ is valid, while validity of the rest of the
derivation follows by inductive hypothesis.

true:

This case is similar to the backchain one.

null, and, or, augment:

Immediate by induction hypothesis.

generic:

The derivation ${\bf d}$ has the form

${\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{\forall
x.G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{i+1};{P}\mid{G[c/x]}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$

where $c$ is a fresh constant of level $i+1$, while ${\bf d}^{\prime}$ is

${\mathfrak{A}}_{1}\xi\otimes\langle{i};{P\xi}\mid{(\forall
x.G)\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi\otimes\langle{i+1};{P\xi}\mid{G[c/x]\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi\mathrel{\stackrel{{\scriptstyle\theta\xi}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}\xi$

Since $G[c/x]\xi=G\xi[\xi(c)/x]$, $\xi(c)$ is of level $i+1$ and by inductive
hypotehsis, ${\bf d}^{\prime}$ is a valid derivation.

instance:

This case is similar to the generic one. ∎

Using the previous result, the following lemma states that constants in a
derivation can be chosen to avoid any finite set of constants not containing
any of the constants of the first and last state vector.

######  Lemma 2.26.

Let ${\bf d}$ be a derivation
${\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$.
If $X$ is a finite set of constant not appearing in ${\mathfrak{A}}$,
${\mathfrak{B}}$ and $\theta$, then there is a derivation of ${\bf
d}^{\prime}:{\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$,
none of whose constants lie in $X$. Moreover, ${\bf d}^{\prime}$ is flat if
${\bf d}$ is flat.

###### Proof.

Let $\xi$ be a neutral constant renamer which maps variables in $X$ to
variables not in $X$ nor in ${\bf d}$. The derivation we are looking for is
the one obtained by Lemma 2.25. ∎

A particular case of Lemmas 2.22 and 2.26 wll be particularly usefult later
and regards successful derivations with identity computed answer. In this
case:

######  Lemma 2.27.

Let ${\bf d}$ be a derivation
${\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}$,
$X$ is a set of variables and $C$ a set of constants. Then, there exists a
derivation ${\bf
d}^{\prime}:{\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}$
whose newly introduced variables and constants do not belong to $X$ or $C$.

In the following, we will use Lemma 2.27, even implicitly, to ensure that
variables introduced in derivations are fresh.

Finally, we examine a way to combine two derivations into a new one:

######  Lemma 2.28 (product lemma).

If there are resolutions ${\bf
d}_{a}:{{\mathfrak{A}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
and ${\bf
d}_{b}:{{\mathfrak{B}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$,
then there is a resolution ${\bf
d}:{{\mathfrak{A}}\otimes{\mathfrak{B}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{[{\mathit{i}d}]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
Moreover, ${\bf d}$ is flat if ${\bf d}_{a}$ and ${\bf d}_{b}$ are both flat.

###### Proof.

Using Lemma 2.22 consider a variant ${\bf d}^{\prime}_{a}$ of ${\bf d}_{a}$
which does not use any variable in ${\sf fv}({{\mathfrak{B}}})\setminus{\sf
fv}({{\mathfrak{A}}})$. Now, given $X$ the set of variables occurring in ${\bf
d}^{\prime}_{a}$, use Lemma 2.27 to obtain a derivation ${\bf d}^{\prime}_{b}$
which

  * •

does not use any variable in $X\setminus{\sf fv}({{\mathfrak{B}}})$;

  * •

does not introduce with the _generic_ rule any constant occuring in ${\bf
d}^{\prime}_{a}$

Then, we first take the derivation

${\bf
d}^{\prime}_{a}\otimes{\mathfrak{B}}:{\mathfrak{A}}\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\mathfrak{B}}$

obtained by concatenating each state vector in ${\bf d}^{\prime}_{a}$ with
${\mathfrak{B}}$. Then, ${\bf d}$ is the concatenation of ${\bf
d}^{\prime}_{a}\otimes{\mathfrak{B}}$ with ${\bf d}^{\prime}_{b}$. ∎

The preceding operation might be generalized to the case where the computed
substitutions are not identities. Moreover, other operations might be defined
to turn derivations into a rich algebraic structure. We do not pursue this
here, but refer the reader to [9] for details.

###  2.7 Some specialization properties of UCTT

######  Lemma 2.29 (Instantiation Lemma).

Let ${\mathfrak{A}}$ be a state vector. Suppose there is a deduction

${{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{\theta}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

with computed substitution $\theta$. Then there is a flat deduction of the
same or shorter length

${{\mathfrak{A}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

###### Proof.

We prove this by induction on the length $\ell$ of the given proof. The cases
$\ell=0$ is trivial. Now assume the given deduction has length $\ell>0$ and
that the first step is

null:

Then the deduction has the following shape:

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{\top}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle
null}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By the inductive hypothesis applied to the deduction starting from the second
state vector, there is a derivation

${{\mathfrak{A}}\theta\otimes{\mathfrak{B}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By Lemmas 2.22 and 2.26 we may assume that fresh variables and constants
introduced in this derivation do not occur in $P\theta$. Therefore,

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{\top}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle
null}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

is a flat derivation.

true:

Then the deduction has the following shape:

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\gamma}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\gamma\otimes\langle{i};{P\gamma}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta^{\prime}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By induction hypothesis, applied to the deduction starting from the second
state vector, there is a deduction

${{\mathfrak{A}}\gamma\theta^{\prime}\otimes\langle{i};{P\gamma\theta^{\prime}}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma\theta^{\prime}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

Since $\gamma\theta^{\prime}=\theta$ when restricted to the free variables in
the initial state vector, this is actually a derivation

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{\top}\rangle\otimes{\mathfrak{B}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

which is what we wanted to prove.

backchain:

We assume the proof has the following shape:

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{A}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\gamma}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\gamma\otimes\langle{i};{P\gamma}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{B}}\gamma}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta^{\prime}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

where $\forall x_{1},\ldots x_{n}(G\supset A^{\prime})\in\textsf{elab}(P)$,
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ is the renaming-apart
subtitution and $A^{\prime}\delta\gamma=A\gamma$ and
$\gamma\theta^{\prime}=\theta$ when restricted to variables free in the
initial state vector. Applying the induction hypothesis to the derivation of
length $\ell-1$ starting with the second state vector, we have

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G\delta\gamma\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By Lemmas 2.22 and 2.26 we can assume that fresh variables and constants
introduced in this derivation are disjoint from those in $A\theta$. By the
clause instance lemma (Lemma 2.11), we have
$\forall\vec{x}(G\gamma\theta^{\prime}\supset
A^{\prime}\gamma\theta^{\prime})\in\textsf{elab}(P\theta)$. Consider a new set
of fresh variables $w^{\prime}_{1},\ldots,w^{\prime}_{n}$ and the renaming
apart substitution
$\delta^{\prime}=\\{w^{\prime}_{1}/x_{1},\ldots,w^{\prime}_{n}/x_{n}\\}$ for
this clauses. Consider also
$\gamma^{\prime}=\\{w_{1}\gamma\theta^{\prime}/w^{\prime}_{1},\ldots,w_{n}\gamma\theta^{\prime}/w^{\prime}_{n}\\}$.

We want to prove that $\gamma^{\prime}$ is an unifier of $A\theta$ and
$A^{\prime}\gamma\theta^{\prime}\delta^{\prime}$. Since
$A\theta=A^{\prime}\delta\gamma\theta^{\prime}$, we need to prove that
$A^{\prime}\delta\gamma\theta^{\prime}\gamma^{\prime}=A^{\prime}\gamma\theta^{\prime}\delta^{\prime}\gamma^{\prime}$.
It is enough to prove that
$x\delta\gamma\theta^{\prime}\gamma^{\prime}=x\gamma\theta^{\prime}\delta^{\prime}\gamma^{\prime}$
for each $x\in{\sf fv}({A^{\prime}})$. Note that
$x\delta\gamma\theta^{\prime}$ does not contain any of the new fresh
$w^{\prime}_{i}$’s, hence
$x\delta\gamma\theta^{\prime}\gamma^{\prime}=x\delta\gamma\theta^{\prime}$. We
distinguish two cases:

  * •

if $x=x_{i}$ for one of the bound variables of the clause, then
$x_{i}\gamma\theta^{\prime}\delta^{\prime}\gamma^{\prime}=x_{i}\delta^{\prime}\gamma^{\prime}$
since $\gamma\theta^{\prime}$ does not contain variables in bvar, and
$x_{i}\delta^{\prime}\gamma^{\prime}=w^{\prime}_{i}\gamma^{\prime}=w_{i}\gamma\theta^{\prime}=x_{i}\delta\gamma\theta^{\prime}$.

  * •

if $x$ is not one of the bound variable of the clause, then
$x\gamma\theta^{\prime}\delta^{\prime}\gamma^{\prime}=x\gamma\theta^{\prime}=x\delta\gamma\theta^{\prime}$.

For the same reason
$G\gamma\theta^{\prime}\delta^{\prime}\gamma^{\prime}=G\delta\gamma\theta^{\prime}\gamma^{\prime}$.
Therefore, the following is a legal derivation of length at most $\ell$

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{A\theta}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle\gamma^{\prime}}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G\delta\gamma\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

as we wanted to show. Note that $\gamma^{\prime}$ respects the conditions for
flat derivations.

and:

Suppose the given deduction is

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{G_{1}\wedge
G_{2}}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\wedge}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Applying the induction hypothesis to the resolution beginning with the second
step, we obtain a deduction

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G_{1}\theta\wedge
G_{2}\theta}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle\wedge}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G_{1}\theta}\rangle\otimes\langle{i};{P\theta}\mid{G_{2}\theta}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

or:

The proof is similar to the one for the null case.

instance:

Suppose the given deduction is

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{\exists
xG}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i};{P}\mid{G[t/x]}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta^{\prime}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

where $\theta^{\prime}=\theta$ when restricted to the free variables in the
original state vector. Using this fact, together with the induction hypothesis
on the deduction beginning with the second state vector, we have

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G[t/x]\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

Since $x\in{\textbf{bvar}}$, hence it does not occur free in
$\theta^{\prime}$, $G[t/x]\theta^{\prime}=G\theta[t\theta^{\prime}/x]$. Note
that, since all substitutions are valid, $t\theta^{\prime}$ is a term of the
same level of $x$ or less. Using $t\theta^{\prime}$ as the witness for the
instance step, we obtain the existence of a deduction of length at most $\ell$

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{(\exists
xG)\theta}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G\theta[t\theta^{\prime}/x]}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

as we wanted to show.

generic:

Then the deduction has the following shape:

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{\forall
x.G}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i+1};{P}\mid{G[c/x]}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

By inductive hypothesis, we have a derivation

${{\mathfrak{A}}\theta\otimes\langle{i+1};{P\theta}\mid{G[c/x]\theta}\rangle\otimes{\mathfrak{B}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

Since $x\in{\textbf{bvar}}$, we have $G[c/x]\theta=G\theta[c/x]$. Therefore,
we get the derivation

${{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{\forall
x.G\theta}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes\langle{i+1};{P\theta}\mid{G\theta[c/x]}\rangle\otimes{\mathfrak{B}}\theta}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.\qed$

A natural question to ask here is whether we can also establish the converse
of this lemma, usually known in the literature, in perhaps a slightly
different form, as the lifting lemma. This question is taken up in Section
4.2.

We now give a number of technical results about resolution proofs that will be
needed to prove soundness and completeness with respect to our semantics.

######  Lemma 2.30 (Left weakening).

Let ${\bf
d}:{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}$
be a derivation. For each program $P^{\prime}$ of level $i$ or less such that
$\textsf{elab}(P^{\prime})\supseteq\textsf{elab}(P)$, there is a derivation
${\bf
d}^{\prime}:{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}$.

###### Proof.

First of all, assume without loss of generality that ${\bf d}$ does not use
any variable or constant occuring in ${\sf fv}({P^{\prime}})\setminus{\sf
fv}({\mathsf{first}({\bf d})})$. The proof is by induction on the length of
${\bf d}$, and it is quite straightforward once we observe that if
$\textsf{elab}(P^{\prime})\supseteq\textsf{elab}(P)$, then also
$\textsf{elab}(P^{\prime}\gamma)\supseteq\textsf{elab}(P\gamma)$ for each
substitution $\gamma$ and
$\textsf{elab}(P^{\prime},D)\supseteq\textsf{elab}(P,D)$ for each program
formula $D$. We show just a few cases.

If ${\bf d}$ has length zero, the result is trivial. For the inductive step,
we first distinguish two cases.

##### First case

If the selected goal is not $\langle{i};{P}\mid{G}\rangle$, then assume
without loss of generality that it is in ${\mathfrak{A}}_{1}$. Then

${\bf
d}:{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}^{\prime}_{1}\gamma\otimes\langle{i};{P\gamma}\mid{G\gamma}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Note that we need flatness of ${\bf d}$ to conclude that the computed answer
of the substitution starting from the second state vector is
$[{\mathit{i}d}]$. By inductive hypothesis, there exists a fresh derivation

${\bf
d}^{\prime\prime}:{\mathfrak{A}}^{\prime}_{1}\otimes\langle{i};{P^{\prime}\gamma}\mid{G\gamma}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Due to the choice of ${\bf d}$, the same rule used in the first step of ${\bf
d}$ may be also applied to
${\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}$.
Therefore, the derivation we are looking for is

${\bf
d}^{\prime}:{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}^{\prime}_{1}\otimes\langle{i};{P^{\prime}\gamma}\mid{G\gamma}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

##### Second case

If the selected goal is $\langle{i};{P}\mid{G}\rangle$, we proceed according
to the rule used.

and:

The derivation ${\bf d}$ has the form

${\bf d}:{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G_{1}\wedge
G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Applying two times the inductive hypothesis on the derivation starting from
the second step of ${\bf d}$, we obtain a fresh derivation

${\bf
d}^{\prime\prime}:{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G_{1}}\rangle\otimes\langle{i};{P^{\prime}}\mid{G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

whence

${\bf
d}^{\prime}:{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G_{1}\wedge
G_{2}}\rangle{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G_{1}}\rangle\otimes\langle{i};{P^{\prime}}\mid{G_{2}}\rangle\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

backchain:

The derivation ${\bf d}$ has the form

${\bf
d}:{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{A_{r}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}_{1}\gamma\otimes\langle{i};{P\gamma}\mid{H}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

By inductive hypothesis, we have a fresh derivation

${\bf
d}^{\prime\prime}:{\mathfrak{A}}_{1}\gamma\otimes\langle{i};{P^{\prime}\gamma}\mid{H}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Since $\textsf{elab}(P^{\prime})\supseteq\textsf{elab}(P)$ and since ${\bf d}$
does not use variables in ${\sf fv}({P^{\prime}})\setminus{\sf
fv}({\mathsf{first}({\bf d})})$, the same backchain step used in ${\bf d}$ may
be also applied to $\langle{i};{P^{\prime}}\mid{A_{r}}\rangle$. Therefore we
obtain:

${\bf
d}^{\prime}:{\mathfrak{A}}_{1}\otimes\langle{i};{P^{\prime}}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}_{1}\gamma\otimes\langle{i};{P^{\prime}\gamma}\mid{H}\rangle\otimes{\mathfrak{A}}_{2}\gamma\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

other rules:

The proof is similar to what is shown above. ∎

######  Lemma 2.31 (Specialization).

Let ${\mathfrak{A}}$ be a state vector. If there is a deduction

${\bf
d}:{{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace,$
(3)

a variable $x\in{\textbf{fvar}}$ of level $i$ and a term $t$ of level $i$ or
less, then there is a deduction

${{\mathfrak{A}}[t/x]}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

###### Proof.

First of all, assume $x\in{\sf fv}({{\mathfrak{A}}})$, otherwise there is
nothing to prove. Moreover, without loss of generality, we may assume ${\bf
d}$ does not use any variable in ${\sf fv}({t})\setminus{\sf
fv}({{\mathfrak{A}}})$. The proof is by induction on the length $\ell$ of the
given deduction. Suppose the deduction has length 0. Then there is nothing to
prove. Suppose the lemma holds for all shorter deductions, and now consider
all possible rules used in the first step.

true:

The case for true resolution step is vacuous. Since all substitutions are
identities, ${\bf d}$ cannot contain a true step.

backchain:

We assume that the proof looks like this

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{A}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\gamma}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i};{P}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

for some clause $\forall\vec{y}(G\supset A^{\prime})\in\textsf{elab}(P)$,
where $\delta=\\{w_{1}/y_{1},\ldots,w_{n}/y_{n}\\}$ is the renaming-apart
substitution and $A^{\prime}\delta\gamma=A$ (since the derivation is flat,
hence $\gamma$ is the identity on the variables of $A$). By induction
hypothesis, there is a fresh derivation

${{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{G\delta\gamma[t/x]}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By the hypothesis at the beginning of the proof, we have that $\gamma(x)=x$,
$G\delta\gamma[t/x]=G[t/x]\delta\gamma$. By the clause instance lemma (Lemma
2.11) we have that $\forall\vec{y}(G[t/x]\supset
A[t/x])\in\textsf{elab}(P[t/x])$. Then the following resolution exists

${{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{A[t/x]}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,\stackrel{{\scriptstyle\gamma}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{G[t/x]\delta\gamma}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

since $\gamma$ is an unifier of $A[t/x]$ and $A^{\prime}[t/x]$:
$A[t/x]\gamma=A[t/x]$ and
$A^{\prime}[t/x]\delta\gamma=A^{\prime}\delta\gamma[t/x]=A[t/x]$.

instance:

Suppose the first step of the given deduction is an instance step

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{\exists
yG}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i};{P}\mid{G[s/y]}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By induction hypothesis there is a proof

${{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{G[s/y][t/x]}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Letting $s^{\prime}=s[t/x]$ and taking $s^{\prime}$ as the witness used in the
first instance step, we have a deduction

$\begin{array}[]{ll}{{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{\exists
y(G[t/x])}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}&\\\
\hskip
30.00005pt\,{{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{G[t/x][s^{\prime}/y]}\rangle\otimes{\mathfrak{B}}{[t/x]}}&\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\end{array}$

as we wanted to show.

generic:

Suppose the first step of the given deduction is an instance of the generic
rule

${{\mathfrak{A}}\otimes\langle{i};{P}\mid{\forall
yG}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{i+1};{P}\mid{G[c/y]}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

Since $y\in{\textbf{bvar}}$ we have $G[c/y][t/x]=G[t/x][c/y]$ so, applying the
induction hypothesis to the shorter proof starting at the second state vector
above, we obtain a deduction

$\begin{array}[]{ll}{{\mathfrak{A}}{[t/x]}\otimes\langle{i};{P[t/x]}\mid{(\forall
yG)[t/x]}\rangle\otimes{\mathfrak{B}}{[t/x]}}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}&\\\
\hskip
30.00005pt\,{{\mathfrak{A}}{[t/x]}\otimes\langle{i+1};{P[t/x]}\mid{G[t/x][c/y]}\rangle\otimes{\mathfrak{B}}{[t/x]}}&\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\end{array}$

The arguments for the null, augment and or cases are easy and left to the
reader. ∎

Iteration of this lemma easily proves a bit more.

######  Corollary 2.32.

Let ${\mathfrak{A}}$ be a state vector and $\theta$ a substitution. If there
is a deduction

${{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

then there is a deduction

${{\mathfrak{A}}\theta}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace.$

###### Proof.

The proof is immediate if $\theta$ is safe, since it is enough to proceed one
binding at a time by using Lemma 2.31. If $\theta$ is not safe, it is
possibile to find safe derivations $\theta_{1}$ and $\theta_{2}$ such that
${\mathfrak{A}}\theta={\mathfrak{A}}\theta_{1}\theta_{2}$. If
$\theta=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$, consider the fresh variables
$w_{1},\ldots w_{n}$ and the renaming
$\rho=\\{w_{1}/x_{1},x_{1}/w_{1},\ldots,w_{n}/x_{n},x_{n}/w_{n}\\}$. Then let
$\theta_{1}=\\{t_{1}\rho/x_{1},\ldots,t_{n}\rho/x_{n}\\}$ and
$\theta_{2}=\rho$, we have
${\mathfrak{A}}\theta={\mathfrak{A}}\theta_{1}\theta_{2}$. Therefore, we
obtain the required derivation by applying Lemma 2.31 one binding at a time,
first with the bindings of $\theta_{1}$, then with the bindings of
$\theta_{2}$. ∎

######  Lemma 2.33 (Constant replacement).

If there is a deduction

${\mathfrak{A}}[c/x]\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

where $x$ is a variable of level $i$ and $c$ a constant of level $i$ or less,
then there exists a deduction

${\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

###### Proof.

Using Lemma 2.27, we may assume that ${\bf
d}:{\mathfrak{A}}[c/x]\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$
does not use the variable $x$. Therefore, it should be quite evident that the
derivation we are looking for is obtained from ${\bf d}$ by replacing every
occurrence of $c$ with $x$. The fact that the level of $c$ is less or equal to
the level of $x$ ensures that every valid substitution remains valid after the
replacement. ∎

For the following lemma, we need to introduce new pieces of notation. Assume
${\mathfrak{A}}$ is a state vector whose states are all at level one or more.
Then, we denote by ${\mathfrak{A}}{\downarrow}$ the state vector obtained
reducing by one the level of all the states. Note that, in the general case,
${\mathfrak{A}}{\downarrow}$ might not be a valid state vector.

######  Lemma 2.34 (Level reduction).

Suppose ${\mathfrak{A}}$ is a state vector whose states are all at level $i>0$
or more. Let:

  * •

$\xi$ be a constant replacer mapping every constant of level $j\geq i$
occuring in ${\mathfrak{A}}$ to a constant of level $j-1$ or less, and every
constant of level $j<i$ occuring in ${\mathfrak{A}}$ to a constant of the same
level;

  * •

$\theta$ be a substitution mapping every variable of level $j\geq i$ occuring
in ${\mathfrak{A}}$ to a term of level $j-1$ or less, and every variable of
level $j<i$ occuring in ${\mathfrak{A}}$ to a term of the same level.

If there is a flat deduction

${\bf
d}:{{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace,$

then there is a flat deduction

${{\mathfrak{A}}\xi\theta{\downarrow}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

of the same length.

###### Proof.

First of all, note that by Lemma 2.27 we may assume that fresh variables and
constants introduced in ${\bf d}$ are disjoint from $\mathsf{oc}(\xi)$ and
${\sf fv}({\theta})$. Also note that ${\mathfrak{A}}\xi\theta{\downarrow}$ is
a valid state vector, since applying $\xi$ and $\theta$ reduces by one the
effective level of each program – goal pair. The proof is by induction on the
length $\ell$ of the given proof, with the base case ($\ell=0$) trivial. For
the inductive step, we proceed according to the first rule used in the
derivation.

backchain:

Suppose ${\bf d}$ begins with the backchain rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{A}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

for some clause $\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(P)$, renaming-
apart derivation $\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ and unifier
$\gamma$ such that $A=A\gamma=A_{r}\delta\gamma$. Let $\xi^{\prime}$ and
$\theta^{\prime}$ be extensions of $\xi$ and $\theta$ mapping new constants
and variables of level $j\geq i$ occurring in $G\delta\gamma$ but not in
${\mathfrak{A}}$ to constants and variables of level $j-1$, and behaving like
$\xi$ and $\theta$ everywhere else. By Lemmas 2.11 and 2.24 it turns out that
there is a clause $\forall\vec{x}(G\xi\theta\supset
A_{r}\xi\theta)\in\textsf{elab}(P\xi\theta)$.

Consider
$\gamma^{\prime}=\\{w_{1}\gamma\xi^{\prime}\theta^{\prime}/w_{1},\ldots,w_{n}\gamma\xi^{\prime}\theta^{\prime}/w_{n}\\}$
and observe that it is a legal substitution. It is the case that
$\gamma^{\prime}$ is an unifier for $A\xi\theta$ and $A_{r}\xi\theta\delta$.
Actually $A\xi\theta$ does not contain variables $\\{w_{1},\ldots,w_{n}\\}$,
hence $A\xi\theta\gamma^{\prime}=A\xi\theta$. Since $\xi$ and $\theta$ do not
contain $w_{1},\ldots,w_{n}$, and since $\xi^{\prime}\theta^{\prime}$ behave
on $A_{r}$ like $\xi\theta$, we have

$A_{r}\xi\theta\delta\gamma^{\prime}=A_{r}\xi\theta\\{w_{1}\gamma\xi^{\prime}\theta^{\prime}/x_{1},\ldots,w_{n}\gamma\xi^{\prime}\theta^{\prime}/x_{n}\\}=A_{r}\xi^{\prime}\theta^{\prime}\\{w_{1}\gamma\xi^{\prime}\theta^{\prime}/x_{1},\ldots,x_{n}\gamma\xi^{\prime}\theta^{\prime}/x_{n}\\}\enspace.$

Now, since $\xi^{\prime}$ and $\theta^{\prime}$ do not contain variables
$x_{1},\ldots,x_{n}$, and since $\xi^{\prime}\theta^{\prime}$ behave on $A$
like $\xi\theta$, we have

$A^{\prime}\xi^{\prime}\theta^{\prime}\\{w_{1}\gamma\xi^{\prime}\theta^{\prime}/x_{1},\ldots,w_{n}\gamma\xi^{\prime}\theta^{\prime}/x_{n}\\}=A\\{w_{1}\gamma/x_{1},\ldots,w_{n}\gamma/x_{n}\\}\xi^{\prime}\theta^{\prime}=A^{\prime}\delta\gamma\xi^{\prime}\theta^{\prime}=A\xi^{\prime}\theta^{\prime}=A\xi\theta\enspace.$

Similarly,
$G\xi\theta\delta\gamma^{\prime}=G\delta\gamma\xi^{\prime}\theta^{\prime}$.
Note that
${\mathfrak{A}}_{1}\xi\theta={\mathfrak{A}}_{1}\xi^{\prime}\theta^{\prime}$
and ${\mathfrak{A}}_{2}\xi\theta={\mathfrak{A}}_{2}\xi^{\prime}\theta$.
Moreover, $P\xi^{\prime}\theta^{\prime}=P\xi\theta$,
$A\xi^{\prime}\theta^{\prime}=A\xi\theta$ and
$G\delta\gamma\xi^{\prime}\theta^{\prime}$ have level $j-1$ or less, therefore
we can replace the index $j$ with $j-1$ in the first state vector and by
inductive hypothesis we get

${\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{A\xi\theta}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle\gamma^{\prime}}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi^{\prime}\theta^{\prime}{\downarrow}\otimes\langle{j-1};{P\xi^{\prime}\theta^{\prime}}\mid{G\delta\gamma\xi^{\prime}\theta^{\prime}}\rangle\otimes{\mathfrak{A}}_{2}\xi^{\prime}\theta^{\prime}{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

and:

Suppose ${\bf d}$ begins with the and rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G_{1}\wedge
G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G_{1}}\rangle\otimes\langle{j};{P}\mid{G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Applying the induction hypothesis to the shorter deduction starting from the
second step, we have a deduction

${\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{(G_{1}\wedge
G_{2})\xi\theta}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}\\\
{\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{G_{1}\xi\theta}\rangle\otimes\langle{j-1};{P\xi\theta}\mid{G_{2}\xi\theta}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

instance:

Suppose ${\bf d}$ begins with the instance rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{\exists_{y}G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\exists}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G[t/y]}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

Consider $\xi^{\prime}$ and $\theta^{\prime}$ which behave like $\xi$ and
$\theta$, but map all fresh constants and variables of level $l\geq i$ in $t$
to fresh constants and variables respectively of level $l-1$ of the same type.
Then, by inductive hypothesis, we have the derivation

${\mathfrak{A}}_{1}\xi^{\prime}\theta^{\prime}{\downarrow}\otimes\langle{j-1};{P\xi^{\prime}\theta^{\prime}}\mid{G[t/y]\xi^{\prime}\theta^{\prime}}\rangle\otimes{\mathfrak{A}}_{2}\xi^{\prime}\theta^{\prime}{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

Note that
${\mathfrak{A}}_{1}\xi^{\prime}\theta^{\prime}={\mathfrak{A}}_{1}\xi\theta$,
${\mathfrak{A}}_{2}\xi^{\prime}\theta^{\prime}={\mathfrak{A}}_{2}\xi\theta$,
$P\xi^{\prime}\theta^{\prime}=P\xi\theta$ and
$G[t/y]\xi^{\prime}\theta^{\prime}=G\xi\theta[t\xi^{\prime}\theta^{\prime}/y]$,
hence we have the following deduction:

${\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{(\exists_{y}G)\xi\theta}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle\exists}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{G\xi\theta[t\xi\theta^{\prime}/y]}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

generic:

Suppose ${\bf d}$ begins with the generic rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{\forall_{y}G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j+1};{P}\mid{G[d/y]}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

where $d$ is a constant of level $j+1$. Consider $\xi^{\prime}$ which behaves
like $\xi$ but maps the constant $d$ to a fresh constant $d^{\prime}$ of level
$j$ and the same type of $d$. Then, by inductive hypothesis we have

${\mathfrak{A}}_{1}\xi^{\prime}\theta{\downarrow}\otimes\langle{j};{P\xi^{\prime}\theta^{\prime}}\mid{G[d/y]\xi\theta^{\prime}}\rangle\otimes{\mathfrak{A}}_{2}\xi^{\prime}\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

with ${\mathfrak{A}}_{1}\xi^{\prime}\theta={\mathfrak{A}}_{1}\xi\theta$,
${\mathfrak{A}}_{2}\xi^{\prime}\theta={\mathfrak{A}}_{2}\xi\theta$,
$P\xi^{\prime}\theta=P\xi\theta$,
$G[d/y]\xi^{\prime}\theta=G\xi\theta[d^{\prime}/y]$. Hence, we have the
deduction

${\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j-1};{P\xi\theta}\mid{(\forall_{y}G)\xi\theta}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi\theta{\downarrow}\otimes\langle{j};{P\xi\theta}\mid{G\xi\theta[d^{\prime}/y]}\rangle\otimes{\mathfrak{A}}_{2}\xi\theta{\downarrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

other cases:

They are similar to the previous ones. ∎

######  Lemma 2.35.

Suppose ${\mathfrak{A}}$ is a state vector whose states are all at level $i>0$
or more. Let $\xi$ be a constant replacer mapping constants of level $j\geq i$
occuring in ${\mathfrak{A}}$ to constants of level $j+1$. If there is a flat
deduction

${\bf
d}:{{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace,$

then there is a flat deduction

${{\mathfrak{A}}\xi{\uparrow}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

of the same length.

###### Proof.

Note that by Lemma 2.27 we may assume that fresh variables and constants
introduced in ${\bf d}$ are disjoint from $\mathsf{oc}(\xi)$. The proof is by
induction on the length of the derivation. The base case is trivial. For the
inductive step, we consider the first rule used in the derivation.

backchain:

Suppose ${\bf d}$ begins with the backchain rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{A}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G\delta\gamma}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

for some clause $\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(P)$, renaming-
apart derivation $\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ and unifier
$\gamma$ such that $A=A\gamma=A_{r}\delta\gamma$. By Lemma 2.24 turns out that
there is a clause $\forall\vec{x}(G\xi\supset
A_{r}\xi)\in\textsf{elab}(P\xi)$. Consider now:

  * •

$\delta^{\prime}=\\{x_{1}/w^{\prime}_{1},\ldots,x_{n}/w^{\prime}_{n}\\}$, a
new renaming apart derivation, where $w^{\prime}_{1},\ldots,w^{\prime}_{n}$
are fresh variables, whose level is one more than the level of the
corresponding $w_{i}$;

  * •

$\gamma^{\prime}=\\{w_{1}\gamma\xi/w^{\prime}_{1},\ldots,w_{n}\gamma\xi/w^{\prime}_{n}\\}$.

Note that $\gamma^{\prime}$ is a legal substitution, since the level of each
$w_{i}\gamma\xi$ is at most the level of $w_{i}$ plus one. It is the case that
$\gamma^{\prime}$ is an unifier for $A\xi$ and $A_{r}\xi\delta^{\prime}$,
since $A\xi\gamma^{\prime}=A\xi$ and

$A_{r}\xi\delta^{\prime}\gamma^{\prime}=A_{r}\xi\\{w_{1}\gamma\xi/x_{1},\ldots,w_{n}\gamma\xi/x_{n}\\}=A_{r}\\{w_{1}\gamma\xi/x_{1},\ldots,w_{n}\gamma\xi/x_{n}\\}\xi=A_{r}\delta\gamma\xi=A\xi\enspace.$

In the same way, we have that $G\xi\delta^{\prime}\gamma=G\delta\gamma\xi$.
Therefore, by induction on the derivation starting from the second state
vector, we have

${\mathfrak{A}}_{1}\xi{\uparrow}\otimes\langle{j+1};{P\xi}\mid{A\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi{\uparrow}\mathrel{\stackrel{{\scriptstyle\gamma^{\prime}}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi{\uparrow}\otimes\langle{j+1};{P\xi}\mid{G\delta\gamma\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi{\uparrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

and:

Suppose ${\bf d}$ begins with the and rule

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G_{1}\wedge
G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{G_{1}}\rangle\otimes\langle{j};{P}\mid{G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Applying the induction hypothesis to the shorter deduction starting from the
second step, we get the deduction

${\mathfrak{A}}_{1}\xi{\uparrow}\otimes\langle{j+1};{P\xi}\mid{(G_{1}\wedge
G_{2})\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi{\uparrow}\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}\\\
{\mathfrak{A}}_{1}\xi{\uparrow}\otimes\langle{j+1};{P\xi}\mid{G_{1}\xi}\rangle\otimes\langle{j+1};{P\xi}\mid{G_{2}\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi{\uparrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

generic:

Suppose ${\bf d}$ begins with the generic rule:

${\mathfrak{A}}_{1}\otimes\langle{j};{P}\mid{\forall_{x}G}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\otimes\langle{j+1};{P}\mid{G[d/x]}\rangle\otimes{\mathfrak{A}}_{2}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Let $\xi^{\prime}$ be a costant replacer which behaves like $\xi$ but mapping
$d$ to a constant $d^{\prime}$ of level $j+2$. Note that
${\mathfrak{A}}_{1}\xi^{\prime}={\mathfrak{A}}_{1}\xi$,
${\mathfrak{A}}_{2}\xi^{\prime}={\mathfrak{A}}_{2}\xi$, $P\xi^{\prime}=P\xi$
and $G\xi[d^{\prime}/x]=G[d/x]\xi^{\prime}$. By induction hypothesis, we have
a derivation,

${\mathfrak{A}}_{1}\xi{\uparrow}\otimes\langle{j+1};{P\xi}\mid{\forall_{x}G\xi}\rangle\otimes{\mathfrak{A}}_{2}\xi{\uparrow}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}_{1}\xi^{\prime}{\uparrow}\otimes\langle{j+2};{P}\mid{G[d/x]\xi^{\prime}}\rangle\otimes{\mathfrak{A}}_{2}\xi^{\prime}{\uparrow}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

other cases:

They are similar to the previous ones. ∎

######  Corollary 2.36 (Level increase).

If there is a derivation of the form

$\langle{i};{P}\mid{G}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto\cdots\leadsto}}}{\Box}$

then there is a derivation

$\langle{i+1};{P}\mid{G}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

###### Proof.

First of all, without loss of generality we may assume that the derivation of
$\langle{i};{P}\mid{G}\rangle$ is flat. The result follow by applying Lemma
2.35 with $\xi$ being the identity function. ∎

######  Corollary 2.37 (Generic constants).

If there is a deduction

${\langle{i+1};{P}\mid{G[c/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

where $c$ is a fresh constant of level $i+1$, $x$ is not free in $P$ and $P,G$
is a program-goal pair of level $i$, then for any positive term $t$ of level
$i$ of the appropriate type there is a deduction

${\langle{i};{P}\mid{G[t/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
(4)

Conversely if $P,G$ and $c$ satisfy the stated conditions and for any positive
term $t$ of level $i$ there is a deduction (4) then there is a deduction
${\langle{i+1};{P}\mid{G[c/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

###### Proof.

For the first claim note that, without loss of generality, we may assume $x$
to be a variable of level $i$. Consider the constant renamer $\xi$ mapping $c$
to a constant $c^{\prime}$ of level $i$. Using Lemma 2.34 we get a derivation
${\langle{i};{P}\mid{G[c^{\prime}/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
Then, by Lemma 2.33, we get
${\langle{i};{P}\mid{G}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
and finally, by Lemma 2.31,
${\langle{i};{P}\mid{G[t/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
for any term $t$ of level $i$ or less.

For the converse claim, consider the case when $t$ is a fresh constant
$c^{\prime}$ of level $i$ and we get a deduction
${\langle{i};{P}\mid{G[c^{\prime}/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
If $c$ is a fresh constant of level $i+1$ and $\xi$ is a constant replacer
mapping $c^{\prime}$ to $c$, then by Lemma 2.35 we have
${\langle{i+1};{P}\mid{G[c/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{[id]}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
∎

###  2.8 Herbrand-Robinson Derivation: “True” Resolution

The nondeterministic resolution rule system just given, equivalent (see A.3.1)
to the Miller-Nadathur-Pfenning-Scedrov [30] definition of the uniform proof
system HOHH, captures some of the behavior of a logic programming
implementation of HOHH, especially since we use backchain and elab, but not
all. As in Prolog, witnesses to existential queries are not magically guessed
in one step. They are produced incrementally by successive unifications when
the substitution generating rules backchain, true, identity occur in the
derivation. In other words _instead of ranging over all possible terms, the
existential quantifier’s range can be restricted to witnesses produced by
unification of queries and clause heads to determine how $\forall_{L}$ and
$\exists_{R}$ should be executed. _ This is a central component of logic
programming, and part of the import of Herbrand’s Theorem and Robinson’s work
in the Horn Clause context222See the discussion on p.130 of Miller et al. [30]
regarding the deliberate omission of backchain in their definition of uniform
proofs..

The purpose of this paper is to give several semantics with respect to which
the proof system of $\lambda$Prolog is sound and complete, _not_ to analyze or
optimize proof search, which has been done in great detail by Nadathur [32,
35, 34, 33]. Thus, we work with the non-deterministic RES(t) system, with all
unifiers allowed, not just those produced by UNIFY and SIMPL. We replace
existentially quantified variables with arbitrary terms, and show, in the
appendix that our system is equivalent to uniform proofs, and hence to more
efficient proof procedures in the literature. We also omit discussion of the
special kind of polymorphism present in $\lambda$Prolog, which deserves a
paper in its own right, as does the use of focusing [25, 3].

Our soundness and completeness theorems, however, hold for these practical
resolution systems.

######  Theorem 2.38.

The resolution system $RES(Y)$ obtained by replacing instance in the rule
system above by the $\exists_{Y}$ rule

${\mathfrak{A}}\otimes{\langle{i};{P}\mid{\exists
x.G}\rangle}\otimes{\mathfrak{B}}\
\stackrel{{\scriptstyle\exists_{Y}}}{{\mathbf{\leadsto}}}\
{\mathfrak{A}}\otimes{\langle{i};{P}\mid{G[Y/x]}\rangle}\otimes{\mathfrak{B}}$
(5)

where $Y$ is a fresh logic variable in fvar of level $i$ or less, is
equivalent to the one presented above: a goal succeeds in the first with some
computed substitution $\theta$ if and only if it does with the second, with
possibly another, more general substitution.

A detailed treatment of this for FOHH resolution can be found in [33], which
also discusses how the argument must change, using results in [32, 35, 34], to
adapt it to the HOHH case.

Theorem A.4 in the Appendix, asserting the equivalence of RES(t) with uniform
proofs, obviously establishes equivalence of our resolution system with any
proof procedure equivalent to uniform proofs, in particular the one presented
using a rule similar to RES(Y) and a restricted class of unifiers, in [33].

##  3 Semantics

###  3.1 The Main Obstacles

If it is to capture the declarative content of programs, a model theory for
HOHH must interpret an intuitionistic fragment of Church’s type theory. In
particular, it must be a model for the simply typed lambda-calculus, sound for
$\beta\eta$ conversion. It must also supply a carrier for predicates and
interpret the logical constants. Since quantifiers and connectives are higher-
order constants in the language, the interpretation of terms cannot be easily
divorced from the meaning of propositions. This is one of the reasons we
construct a model in which the object of truth values, a (parametrically)
complete Heyting Algebra, is distinct from the carriers of the types of
propositions.

##### Impredicativity

In Church’s Type theory, instances of quantified formulas may have arbitrarily
large complexity, since variables of logical type range over formulas. For
example, any formula $G$ including $\varphi$ itself may be an instance of the
formula $\varphi=\exists x_{o}.x_{o}$ Thus the subformula relation does not
give rise to a well-founded order on formulas. This means we may not define
truth in a model by induction on subformula structure. For this reason
assignments of truth values to atomic formulas may not suffice to specify a
model, and common elementary properties (e.g. monotonicity of truth in Kripke
models) cannot be defined by fiat for atoms and extended by induction to all
formulas. There are a number of ways to deal with this kind of problem, most
famously the approaches due to Takahashi, Tait, Andrews and Girard to prove
cut-elimination in impredicative systems (see [4, 11] for extensions of these
techniques to classical and intuitionistic versions of Church’s calculus).
Sometimes one is able to define models, and prove completeness by inducting on
something else, e.g. type structure, term-complexity, or, as with our
treatment of completeness here, the number of iterations of an operator used
to build initial models.

For this reason, truth in the models defined in this paper, is not inductively
defined. The conditions a definition of truth must satisfy with respect to the
connectives and quantifiers must be seen as constraints to be met by a
particular model construction.

There are, in addition, a series of requirements peculiar to logic programming
that must be met to supply a semantics with respect to which resolution
deductions on HOHH are sound and complete. We summarize them here.

##### Breaking truth-functionality of higher-order predicates:

In $\lambda$Prolog we observe the following behavior.

       Program:
          module ntf.
          type p o.                               p :- q.
          type q o.                               q :- p.
          type f o -> o.                         f(p).

       Queries:
          ?- f(p).
          solved

          ?- f(q).
          no

          ?- f(p & p).
          no

The logical equivalence of $p$ and $q$, or of $p$ and $p\wedge p$ plays no
role in the search for a proof of $f(q)$ or of $f(p\wedge p)$. In other words,
the following inference fails in ICTT, the underlying logic of
$\lambda$Prolog, when $A,B$ are propositions and the type of $p$ is
$o\rightarrow o$:

$\frac{\textstyle{A\longleftrightarrow B}}{\textstyle{p(A)\rightarrow p(B)}}$
(6)

There are good programming language reasons for omitting this inference. For
example, a goal

                            $\cdots$ ,p(t) :- $\cdots,\,\cdots$ ?- p(u).

with $t,u$ of the type of propositions, proceeds by higher-order unification
of $t$ and $u$ and the appropriate modification of the stack of current goals.
If (6) were a legitimate derived rule, we would have to invoke the entire
theorem proving mechanism of $\lambda$Prolog to see if $t$ and $u$ were
logically equivalent. Note that, if appropriate syntactic restrictions are
imposed on programs, truth-functionality becomes computationally feasible
(see, for example, [43, 7]).

Thus, if HOHH-resolution is to be sound and complete with respect to our model
theory, the meaning of the formula $f(p\wedge p)$ must not be identified with
$f(p)$. Once again, this is achieved by separating the object of truth values
$\Omega$ from the carrier Do of propositions. Although $p$ and $p\wedge p$
will have the same truth value in $\Omega$, they will not be identified in Do,
making it possible to consistently assign different truth values to $f(p\wedge
p)$ and $f(p)$.

Our model theory for UCTT is an indexed variant of Heyting Applicative
Structure semantics for the intuitionistic version of Church’s Theory of types
given in [11]. It brings together several of the ideas discussed above:

  * •

Miller’s indexed model theory [29] for a first-order fragment of FOHH (meaning
is assigned to goals $G$ with respect to ambient programs $P$);

  * •

stratification of carriers to represent different index levels, i.e. change of
ambient signatures;

  * •

separate carriers for programs and goals and their components, and an object
$\Omega$ of truth values distinct from the carrier of logical formulae.

The carrier of the program type is a pre-ordered monoid, and so, in
particular, has a Kripke-like structure. Unlike Miller’s model, the carriers
of programs and goals do not consist of the programs and goals themselves, but
of interpreted programs and goals.

The interpretation of logic (program-goal pairs) in our semantics arises from
the composition of two maps:

${\sf p}\times{\sf
g}\stackrel{{\scriptstyle\mathfrak{U}\times\mathfrak{U}}}{{\longrightarrow}}{\sf
D}_{{i},{{\sf p}}}\times{\sf D}_{{i},{{\sf
g}}}\stackrel{{\scriptstyle\mathcal{I}}}{{\rightarrow}}\Omega$

where ${\sf p}$ and ${\sf g}$ stand for the sets of terms of program and goal
type respectively, mapped by $\mathfrak{U}$ into carriers of their type in
some Uniform Applicative Structure $\mathfrak{D}$, defined below, and
$\mathcal{I}=\\{\mathcal{I}_{i}:i\in\mathbb{N}\\}$ is an integer-indexed
family of maps from stratified carriers ${\sf D}_{{i},{{\sf p}}}\times{\sf
D}_{{i},{{\sf g}}}$ into the object of truth values $\Omega$. Readers familiar
with Miller’s forcing notation [29] will see that our interpretation
$I_{i}(\mathfrak{U}(P),\mathfrak{U}(G))=\top_{\Omega}$ of the program-goal
pair $P,G$ corresponds to his

$\mathcal{I},P\ |\\!\\!\\!\\!\\!\models G.$

But we generalize his forcing in a number of ways: we include universal
quantification (which requires adding the signature-levels $i\in\mathbb{N}$),
higher-order logic (which requires the presence of an applicative structure to
model lambda-abstraction and application), and we factor our interpretation
through a structure which supplies carriers ${\sf D}_{{i},{{\sf p}}},{\sf
D}_{{i},{{\sf g}}}$ for programs as well as goals.

We now give the details. We start by recapitulating the definition of a
standard notion of model for the simply typed lambda-calculus, which will be
built into our structures. They were first introduced systematically by H.
Friedman in [16], although obviously implicit to a lesser or greater degree in
[18, 24, 36]. (See also [31] for a detailed discussion.)

###  3.2 Applicative Structures

Let ${\cal S}$ be a language for ICTT, that is to say a set of typed
constants.

######  Definition 3.1.

A typed applicative structure $\langle{\sf D},{\sf App},\mbox{\sf
Const}\rangle$ for ${\cal S}$ consists of an indexed family ${\sf D}=\\{{\sf
D}_{\alpha}\\}$ of sets ${\sf D}_{\alpha}$ for each type $\alpha$, an indexed
family ${\sf App}$ of functions ${\sf App}_{\alpha,\beta}:{\sf
D}_{\beta\alpha}\times{\sf D}_{\alpha}\rightarrow{\sf D}_{\beta}$ for each
pair $(\alpha,\beta)$ of types, and an (indexed) intepretation function
$\mbox{\sf Const}=\\{\mbox{\sf Const}_{\alpha}\\}$ taking constants of each
type $\alpha$ to elements of ${\sf D}_{\alpha}$.

A typed applicative structure is (functionally) extensional if for every $f$,
$g$ in ${\sf D}_{\beta\alpha}$, ${\sf App}(f,d)={\sf App}(g,d)$ for all
$d\in{\sf D}_{\alpha}$ implies $f=g$.

The models we construct in this paper are extensional. It should be noted,
however, that we do not work with equality, so there is no way to explicitly
specify (or prove) extensionality in the theory. We now modify the semantics,
first to introduce the richer notion of indexed terms, and to model some of
the relationships between certain logical types.

We retain the notation ${\cal S}$ for the language we are working over, by
which we mean a set of UCTT-typed constants, each with its associated level.

######  Definition 3.2.

A uniform ${\cal S}$-applicative structure
$\mbox{${\mathfrak{D}}$}=\langle{\sf D},{\sf App},\mbox{\sf Const},\mbox{\sf
Inc},{\sf M}_{{\sf p}}\rangle$ for UCTT is an extensional, typed applicative
structure indexed over the natural numbers. That is to say:

  * •

${\sf D}$ is a family of sets ${\sf D}_{{i},{\alpha}}$ for each index $i$ and
type $\alpha$;

  * •

${\sf App}$ is a family of functions, indexed over the natural numbers and
pairs of types

${\sf App}_{i\beta\alpha}:{\sf D}_{{i},{\beta\alpha}}\times{\sf
D}_{{i},{\alpha}}\rightarrow{\sf D}_{{i},{\beta}};$

  * •

Const is a family of fuctions, indexed over natural numbers and types, such
that $\mbox{\sf Const}_{i\alpha}$ maps constants of type $\alpha$ and label
$i$ to elements of ${\sf D}_{{i},{\alpha}}$.

In addition, the structure contains a family of injective functions $\mbox{\sf
Inc}_{i{\sf p}{\sf r}}:{\sf D}_{{i},{{\sf r}}}\rightarrow{\sf D}_{{i},{{\sf
p}}}$, $\mbox{\sf Inc}_{i{\sf g}{\sf a}}:{\sf D}_{{i},{{\sf
a}}}\rightarrow{\sf D}_{{i},{{\sf g}}}$, $\mbox{\sf Inc}_{i{\sf a}{\sf
r}}:{\sf D}_{{i},{{\sf r}}}\rightarrow{\sf D}_{{i},{{\sf a}}}$, $\mbox{\sf
Inc}_{i{\sf g}{\sf h}}:{\sf D}_{{i},{{\sf h}}}\rightarrow{\sf D}_{{i},{{\sf
g}}}$ and $\mbox{\sf Inc}_{(i+1)i\alpha}:{\sf D}_{{i},{\alpha}}\rightarrow{\sf
D}_{{i+1},{\alpha}}$ (and by composition $\mbox{\sf Inc}_{jk\alpha}$ for
$j\geq k$, with $\mbox{\sf Inc}_{jj\alpha}$ the identity), which must satisfy
$\mbox{\sf Inc}_{ij\beta}({\sf App}(g,s))={\sf App}(\mbox{\sf
Inc}_{ij(\beta\alpha)}(g),\mbox{\sf Inc}_{ij\alpha}(s))$. Indexes may be
omitted when clear from the context or irrelevant to the discussion.

Also, ${\sf D}_{{i},{{\sf p}}}$ has a pre-ordered monoid structure ${\sf
M}_{i,{\sf p}}=\langle{\sf D}_{{i},{{\sf p}}},\sqsubseteq_{{\sf p}},\top_{\sf
p},\bm{\wedge}_{{\sf p}{\sf p}{\sf p}},\bm{\Pi}_{{\sf p}({\sf
p}\alpha)}\rangle$ where:

  * •

$\sqsubseteq_{\sf p}$ is a pre-order over ${\sf D}_{{i},{{\sf p}}}$;

  * •

$\bm{\wedge}_{{\sf p}{\sf p}{\sf p}}=\mbox{\sf Inc}_{i0({\sf p}{\sf p}{\sf
p})}(\mbox{\sf Const}(\wedge_{{\sf p}{\sf p}{\sf p}}))\in{\sf D}_{i,{\sf
p}{\sf p}{\sf p}}$ is a binary operation;

  * •

$\top_{\sf p}\in{\sf D}_{i,{\sf p}}$ is an identity element for
$\bm{\wedge}_{{\sf p}{\sf p}{\sf p}}$;

  * •

for every type $\alpha$, $\bm{\Pi}_{{\sf p}({\sf p}\alpha)}=\mbox{\sf
Inc}_{i0({\sf p}({\sf p}\alpha))}(\mbox{\sf Const}(\Pi_{{\sf p}({\sf
p}\alpha)}))\in{\sf D}_{{i},{{\sf p}({\sf p}\alpha)}}$ is an unary operator

such that for $p,q\in{\sf D}_{{i},{{\sf p}}}$, $d\in{\sf D}_{{i},{\alpha}}$
and $f\in{\sf D}_{{i},{{\sf p}\alpha}}$, $p\sqsubseteq_{\sf p}p\bm{\wedge}q$,
$\land_{{\sf p}{\sf p}{\sf p}}$ is commutative up to equivalence induced by
$\sqsubseteq_{{\sf p}}$ (that is to say $p\land q$ and $q\land p$ are
$\sqsubseteq_{\sf p}$ equivalent) and ${\sf App}(f,d)\sqsubseteq_{\sf p}{\sf
App}(\bm{\Pi}_{{\sf p}({\sf p}\alpha)},f)$.

######  Definition 3.3.

Given a uniform applicative structure, we will often refer to the interpreted
parameters or, equivalently, the interpreted constants of the structure, as
the elements $\mbox{\sf Const}(c)$ where $c$ ranges over logical constants, or
the non-logical constants of ${\cal S}$. When the structure is clear from
context, we will write $\overline{{c}}$ (or just $c$ if clear from context)
for the interpreted constants, in particular the logical ones. With an abuse
of notation, we will also denote by $\overline{{c}}$ any possible injection of
$\mbox{\sf Inc}_{j0\alpha}(\mbox{\sf Const}(c))$, as it is needed in the
context.

###  3.3 Uniform Algebras

We define a valuation function from the uniform applicative structure into an
object of truth values, namely a distributive lattice, or in some cases a
Heyting algebra $\Omega$333These structures must have enough suprema and
infima as will be specified below.. A recapitulation of the definitions and
some simple properties of distributive lattices and Heyting Algebras is given
in the appendix. We distinguish the lattice operations from their formal
counterparts in the syntax with subscripts $\Omega$ where necessary.

######  Definition 3.4.

Let $\Omega$ be a distributive lattice (or a Heyting Algebra). An
$\Omega$-valuation on a uniform applicative structure ${\mathfrak{D}}$ is a
function $\mathcal{I}:i\times{\sf D}_{{i},{{\sf p}}}\times{\sf D}_{{i},{{\sf
g}}}\rightarrow\Omega$, $i\in\mathbb{N}$, satisfying the condition

$\mathcal{I}_{i}({\mbox{\sf Inc}_{{\sf p}{\sf r}}(r)},{\mbox{\sf Inc}_{{\sf
g}{\sf a}}(\mbox{\sf Inc}_{{\sf a}{\sf r}}(r))})=\top_{\Omega}$ (7)

for rigid atoms, the monotonicity condition

$\mathcal{I}_{i}({p},{g})\leq_{\Omega}\mathcal{I}_{i+1}({\mbox{\sf
Inc}_{(i+1)i}(p)},{\mbox{\sf Inc}_{(i+1)i}(g)})$ (8)

and the following equalities:

$\displaystyle\mathcal{I}_{i}({p},{\overline{{\top}}_{\sf g}})$
$\displaystyle=\top_{\Omega}$ (9)
$\displaystyle\mathcal{I}_{i}({p},{g\overline{{\wedge}}_{{\sf g}{\sf g}{\sf
g}}g^{\prime}})$
$\displaystyle=\mathcal{I}_{i}({p},{g})\land_{\Omega}\mathcal{I}_{i}({p},{g^{\prime}})$
(10) $\displaystyle\mathcal{I}_{i}({p},{g\overline{{\vee}}_{{\sf g}{\sf g}{\sf
g}}g^{\prime}})$
$\displaystyle=\mathcal{I}_{i}({p},{g})\lor_{\Omega}\mathcal{I}_{i}({p},{g^{\prime}})$
(11) $\displaystyle\mathcal{I}_{i}({p},{q\overline{{\supset}}_{{\sf g}{\sf
g}{\sf p}}g})$ $\displaystyle=\mathcal{I}_{i}({p\land_{{\sf p}{\sf p}{\sf
p}}q},{g})$ (12) $\displaystyle\mathcal{I}_{i}({p},{{\sf
App}(\overline{{\Sigma}}_{{\sf g}({\sf g}\alpha)},f)})$
$\displaystyle=\bigvee_{d\in{\sf D}_{{i},{\alpha}}}\mathcal{I}_{i}({p},{{\sf
App}(f,d)})$ $\displaystyle\textrm{ for }f\in{\sf D}_{{i},{{\sf g}\alpha}}$
(13) $\displaystyle\mathcal{I}_{i}({p},{{\sf App}(\overline{{\Pi}}_{{\sf
g}({\sf g}\alpha)},f)})$ $\displaystyle=\bigwedge_{d\in{\sf
D}_{{i},{\alpha}}}\mathcal{I}_{i}({p},{{\sf App}(f,d)})$
$\displaystyle\textrm{ for }f\in{\sf D}_{{i},{{\sf g}\alpha}}.$ (14)

For ${\cal I}$ to be an $\Omega$-valuation, the infima and suprema on the
right hand side in the last two conditions must exist. We also add the
following conditions on $\sqsubseteq_{\sf p}$:

$\displaystyle p\sqsubseteq_{\sf p}p^{\prime}$ $\displaystyle\textrm{ implies
}\mathcal{I}_{i}({p},{g})\leq_{\Omega}\mathcal{I}_{i}({p^{\prime}},{g})$ (15)
$\displaystyle(g\supset_{{\sf p}{\sf g}{\sf r}}r)\sqsubseteq_{\sf p}p$
$\displaystyle\textrm{ implies
}\mathcal{I}_{i}({p},{g})\leq_{\Omega}\mathcal{I}_{i}({p},{\mbox{\sf
Inc}_{{\sf g}{\sf a}}(\mbox{\sf Inc}_{{\sf a}{\sf r}}(r))})$ (16)

Since an ordering of formulas in higher-order logic that allows instances of
quantified formulas to be considered as subformulas does not give rise to a
well-ordering (as discussed in Section 3.1) the reader should resist any
attempt to view conditions (10, 11, 12), etc., as inductive definitions. They
are the properties that a valuation must satisfy, and it remains to be shown
that such valuations exist. We will construct one as the limit of finite
approximations following Lemma 4.5 below.

Finally, we interpret the logic in our structure. We will need to make use of
assignments or environments to handle free variables. A D-assignment $\varphi$
is a function from the free variables of the language into ${\sf D}$ which
respects indices and types. That is to say, if $x$ of type $\alpha$ has label
$i$, then $\varphi(x)\in{\sf D}_{i,\alpha}$.

######  Definition 3.5.

A uniform algebra or model for UCTT is a quadruple
$\langle{\mbox{${\mathfrak{D}}$},\mathfrak{U},\Omega,\mathcal{I}}\rangle$,
where ${\mathfrak{D}}$ is a uniform applicative structure $\langle{{\sf
D},{\sf App},\mbox{\sf Const},\mbox{\sf Inc},{\sf M}_{{\sf p}}}\rangle$,
$\mathfrak{U}$ is a family of maps $\mathfrak{U}=\\{\mathfrak{U}_{\varphi}\\}$
from terms of level $i$ and type $\alpha$ to ${\sf D}_{i,\alpha}$ idsexed over
D-assignments $\varphi$, $\Omega$ is a distributive lattice and $\mathcal{I}$
an $\Omega$-valuation satisfying certain conditions spelled out below.

$\displaystyle\mathfrak{U}(c)_{\varphi}=$ $\displaystyle\ \mbox{\sf Const}(c)$
$\displaystyle\mathfrak{U}(x)_{\varphi}=$ $\displaystyle\ \varphi(x)$
$\displaystyle\mathfrak{U}(t_{1}t_{2})_{\varphi}=$ $\displaystyle\ {\sf
App}(\mathfrak{U}(t_{1})_{\varphi},\mathfrak{U}(t_{2})_{\varphi})$
$\displaystyle\mathfrak{U}(\lambda x.t)_{\varphi}=$ the unique member of
${\mathfrak{D}}$ s.t. ${\sf App}(\mathfrak{U}(\lambda
x.t)_{\varphi},d)=\mathfrak{U}(t)_{\varphi[d/x]}$

######  Remark 3.6.

In the definition of $\mathfrak{U}(t_{1}t_{2})_{\varphi}$ there are some
implicit inclusions we have omitted to ease notation. If $t_{1}$ has level
$i$, $t_{2}$ has level $j$ and $m=\max(i,j)$, the full definition of
$\mathfrak{U}(t_{1}t_{2})_{\varphi}$ should be

$\mathfrak{U}(t_{1}t_{2})_{\varphi}={\sf App}(\mbox{\sf
Inc}_{mi}\mathfrak{U}(t_{1})_{\varphi},\mbox{\sf
Inc}_{mj}\mathfrak{U}(t_{2})_{\varphi})\enspace.$

######  Remark 3.7.

Like in the definition of elab, in order to respect the condition that only
variables in fvar may occur freely, the definiton of $\mathfrak{U}(\forall