x.t)_{\varphi}$ should be

$\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[y/x])_{\varphi[d/y]}$ where
$y\in{\textbf{fvar}}$ is a fresh variable replacing the bound variable
$x\in{\textbf{bvar}}$,

but we prefer to use the more informal notation, letting $x$ to benote both a
variable in bvar and a fresh variable in fvar.

The notation $\mathfrak{U}(P)$ where $P$ is a program rather than a single
program formula, is meant to denote $\mathfrak{U}(\bigwedge P)$ if $P$ is non-
empty, $\top_{\sf p}$ otherwise.

The last condition for ensuring $\mathfrak{U}$ is a model of the lambda-
calculus above, called the environmental model condition in [31], asserts the
existence and uniqueness of a “right” interpretation of abstraction. It
ensures the equivalence of semantic and syntactic substitution even in the
absence of functional extensionality.

######  Lemma 3.8 (Free variables).

Let $\langle{\mbox{${\mathfrak{D}}$},\mathfrak{U},\Omega,\mathcal{I}}\rangle$
be a uniform algebra and $N$ any term. If $\varphi$ and $\varphi^{\prime}$ are
two D-assignments that agree on the free variables of $N$, then
$\mathfrak{U}(N)_{\varphi}=\mathfrak{U}(N)_{\varphi^{\prime}}$.

######  Lemma 3.9 (Substitution).

Let $\langle{\mbox{${\mathfrak{D}}$},\mathfrak{U},\Omega,\mathcal{I}}\rangle$
be a uniform algebra and let $\theta$ be the substitution
$\\{t_{1}/x_{1},\dots,t_{n}/x_{n}\\}$, abbreviated
$[\overline{t}/\overline{x}]$. Then, for any term $N$,
$\mathfrak{U}(N\theta)_{\varphi}=\mathfrak{U}(N)_{\varphi[\overline{\mathfrak{U}(t)_{\varphi}}/\overline{x}]}$.

The proofs of these lemmas are routines, by induction on the structure of
$\lambda$-terms. For the case $N=\lambda x.M$, we must appeal to the
uniqueness provision of the environmental model condition of Definition 3.5.

######  Lemma 3.10.

In any uniform algebra
$\langle{\mbox{${\mathfrak{D}}$},\mathfrak{U},\Omega,\mathcal{I}}\rangle$, if
$\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(P)$, then for any renaming-
apart substitution $\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$, substitution
$\gamma$ and D-assignment $\varphi$, we have
$\mathfrak{U}(G\delta\gamma\supset
A_{r}\delta\gamma)_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(P\gamma)_{\varphi}$.

###### Proof.

The lemma is trivially true if $P$ is empty. Therefore, assume $P$ to be non-
empty. By definition of elab, there exists $D\in P$ such that
$\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(D)$. Moreover,
$\mathfrak{U}(P\gamma)_{\varphi}=\bm{\bigwedge}_{D^{\prime}\in
P\gamma}\mathfrak{U}(D^{\prime})_{\varphi}\sqsupseteq_{\sf
p}\mathfrak{U}(D\gamma)_{\varphi}$, hence it is enough to prove that
$\mathfrak{U}(G\delta\gamma\supset
A_{r}\delta\gamma)_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(D\gamma)_{\varphi}$. The proof is by induction on the
complexity of the program formula $D$.

If $D=G\supset A_{r}$ there are no bound variables. Hence, we have
$\delta=\epsilon$ and the result is trivial since $G\gamma\supset
A_{r}\gamma=D\gamma$.

If $D=D_{1}\wedge D_{2}$, then assume without loss of generality that
$\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(D_{1})$. By inductive
hypothesis, we have $\mathfrak{U}(G\delta\gamma\supset
A_{r}\delta\gamma)_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(D_{1}\gamma)_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(D_{1}\gamma)_{\varphi}\bm{\wedge}\mathfrak{U}(D_{2}\gamma)_{\varphi}=\mathfrak{U}((D_{1}\wedge
D_{2})\gamma)_{\varphi}$.

Finally, if $D=\forall x_{1}.D^{\prime}$ then $\forall x_{2}\ldots
x_{n}(G\supset A_{r})\in\textsf{elab}(D^{\prime})$. By inductive hypothesis,
we have

$\mathfrak{U}(G\delta\gamma\supset
A_{r}\delta\gamma)_{\varphi}=\mathfrak{U}(G\delta^{\prime}\gamma\gamma^{\prime}\supset
A_{r}\delta^{\prime}\gamma\gamma^{\prime})_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(D^{\prime}\gamma\gamma^{\prime})_{\varphi}$

where $\delta^{\prime}=\\{w_{2}/x_{2},\ldots,w_{n}/x_{n}\\}$ and
$\gamma^{\prime}=\\{\gamma(w_{1})/x_{1}\\}$. By Lemma 3.9 we have
$\mathfrak{U}(D^{\prime}\gamma\gamma^{\prime})_{\varphi}=\mathfrak{U}(D^{\prime}\gamma)_{\varphi[v/x_{1}]}$,
where $v=\mathfrak{U}(\gamma(w_{1}))_{\varphi}$. Then, by eta-conversion and
the definition of uniform algebra:

$\mathfrak{U}(D^{\prime}\gamma)_{\varphi[v/x_{1}]}=\mathfrak{U}((\lambda
x_{1}.D^{\prime}\gamma)x_{1})_{\varphi[v/x_{1}]}={\sf
App}(\mathfrak{U}(\lambda
x_{1}.D^{\prime}\gamma)_{\varphi[v/x_{1}]},v)\enspace.$

Since $\lambda x_{1}.D^{\prime}\gamma$ does not contain $x_{1}$ free, using
Lemma 3.8 we have ${\sf App}(\mathfrak{U}(\lambda
x_{1}.D^{\prime}\gamma)_{\varphi[v/x_{1}]},v)={\sf App}(\mathfrak{U}(\lambda
x_{1}.D^{\prime}\gamma)_{\varphi},v)$ and

${\sf App}(\mathfrak{U}(\lambda
x_{1}.D^{\prime}\gamma)_{\varphi},v)\sqsubseteq_{\sf p}{\sf
App}(\bm{\Pi}_{{\sf p}({\sf p}\alpha)},\mathfrak{U}(\lambda
x_{1}.D^{\prime}\gamma)_{\varphi})=\mathfrak{U}(\forall
x_{1}.D^{\prime}\gamma)_{\varphi}=\mathfrak{U}(D\gamma)_{\varphi}\enspace.\qed$

###  3.4 Soundness

Let ${\mathfrak{A}}$ be the state $\langle{i};{P}\mid{G}\rangle$. For the rest
of the paper we will abbreviate our notation by writing
${\llbracket{G}\rrbracket_{\varphi}}$ instead of $\mathfrak{U}_{\varphi}(G)$
and ${\llbracket{\langle{i};{P}\mid{G}\rangle}\rrbracket_{\varphi}}$ instead
of $\mathcal{I}_{i}(\mathfrak{U}_{\varphi}(P),\mathfrak{U}_{\varphi}(G))$. We
extend the semantic operator $\llbracket{\\_}\rrbracket$ to state vectors by
defining

${\llbracket{{\mathfrak{A}}_{1}\otimes\cdots\otimes{\mathfrak{A}}_{n}}\rrbracket_{\varphi}}={\llbracket{{\mathfrak{A}}_{1}}\rrbracket_{\varphi}}\wedge_{\Omega}\cdots\wedge_{\Omega}{\llbracket{{\mathfrak{A}}_{n}}\rrbracket_{\varphi}}.$

and

${\llbracket{{\Box}}\rrbracket_{=}}\top_{\Omega}\enspace.$

######  Theorem 3.11.

Let ${\mathfrak{A}}$ and ${\mathfrak{B}}$ be state vectors. Suppose there is a
resolution

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

Then in any uniform algebra, with any D-assignment

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}_{1}\theta}\rrbracket_{\varphi}}.$

The proof is by induction on the length of the given resolution. Choose a
uniform algebra
$\mathbb{A}=\langle{\mbox{${\mathfrak{D}}$},\mathfrak{U},\Omega,\mathcal{I}}\rangle$,
where ${\mathfrak{D}}$ is the uniform applicative structure $\langle{{\sf
D},{\sf App},\mbox{\sf Const},\mbox{\sf Inc},{\sf M}_{{\sf p}}}\rangle$. Let
$\varphi$ be a D-assignment.

###### Proof.

There is nothing to show in the case of a proof of length 0. Let us
inductively assume that for all deductions of length less that some natural
number $n>0$, the conclusion of the theorem holds. Now suppose the given
deduction has length $n$. We consider all possible first steps.

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}}}\,{{\mathfrak{A}}_{2}}$

where $G\gamma=\top$ and $\gamma\theta^{\prime}=\theta$ when restricted to the
free variables in the initial state vector. By induction hypothesis, applied
to the deduction starting from the second state vector, we have

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\gamma\theta^{\prime}\otimes\langle{i};{P\gamma\theta^{\prime}}\mid{\top}\rangle\otimes{\mathfrak{B}}\gamma\theta^{\prime}}\rrbracket_{\varphi}}={\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{\top}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}}.$

Since $\top$ is (the normal form of) $G\gamma\theta^{\prime}$ this is
precisely what the theorem claims.

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}}}\,{{\mathfrak{A}}_{2}}$

where $\forall\vec{x}(G\supset A_{r})$ is a clause in $\textsf{elab}(P)$,
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ is the renaming-apart
substitution, $A_{r}\delta\gamma=A\gamma$ and $\gamma\theta^{\prime}=\theta$
when restricted to the free variables in the initial state vector. By
induction hypothesis

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\gamma\theta^{\prime}\otimes\langle{i};{P\gamma\theta^{\prime}}\mid{G\delta\gamma\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\gamma\theta^{\prime}}\rrbracket_{\varphi}}\enspace.$

Now

${\llbracket{{\mathfrak{A}}\gamma\theta^{\prime}\otimes\langle{i};{P\gamma\theta^{\prime}}\mid{G\delta\gamma\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\gamma\theta^{\prime}}\rrbracket_{\varphi}}={\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\gamma\theta^{\prime}}\rrbracket_{\varphi}}},{{\llbracket{G\delta\gamma\theta^{\prime}}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}\enspace.$

By Lemma 3.10 $\mathfrak{U}(G\delta\gamma\theta^{\prime}\supset
A_{r}\delta\gamma\theta^{\prime})_{\varphi}\sqsubseteq_{{\sf
p}}\mathfrak{U}(P\gamma\theta^{\prime})_{\varphi}$, and by condition (16) of
the Definition 3.4 of a valuation, this implies

$\mathcal{I}_{i}({{\llbracket{P\gamma\theta^{\prime}}\rrbracket_{\varphi}}},{{\llbracket{G\delta\gamma\theta^{\prime}}\rrbracket_{\varphi}}})\leq_{\Omega}\mathcal{I}_{i}({{\llbracket{P\gamma\theta^{\prime}}\rrbracket_{\varphi}}},{{\llbracket{A_{r}\delta\gamma\theta^{\prime}}\rrbracket_{\varphi}}})=\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{A_{r}\delta\gamma\theta^{\prime}}\rrbracket_{\varphi}}})\enspace.$

From this, and the fact that
$A_{r}\delta\gamma\theta^{\prime}=A\gamma\theta^{\prime}=A\theta$, we conclude

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{A\theta}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$

which is what we wanted to show.

and:

Suppose the first step is an instance of the and-rule:

${{\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}}}\,{{\mathfrak{A}}_{2}}.$

By the induction hypothesis

$\displaystyle{\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G_{1}\theta}\rangle\otimes\langle{i};{P}\mid{G_{2}\theta}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{1}\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{2}\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$

Since

$\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{(G_{1}\wedge
G_{2})\theta}\rrbracket_{\varphi}}})=\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{1}\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{2}\theta}\rrbracket_{\varphi}}}),$

we have

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{(G_{1}\wedge
G_{2})\theta}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}},$

as we wanted to show.

or:

Suppose the first step is an instance of the or-rule:

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

for $k\in\\{1,2\\}$. By the induction hypothesis

$\displaystyle{\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{G_{k}\theta}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{k}\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$

Since

$\displaystyle\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{k}\theta}\rrbracket_{\varphi}}})$
$\displaystyle\leq$
$\displaystyle\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{1}\theta}\rrbracket_{\varphi}}})\vee_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G_{2}\theta}\rrbracket_{\varphi}}})$
$\displaystyle=$
$\displaystyle\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{(G_{1}\vee
G_{2})\theta}\rrbracket_{\varphi}}})$

we have

${\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta\otimes\langle{i};{P\theta}\mid{(G_{1}\vee
G_{2})\theta}\rangle\otimes{\mathfrak{B}}\theta}\rrbracket_{\varphi}}\enspace,$

as we wanted to show.

null / augment:

The proof for these rules are similar to the previous cases and are left to
the reader.

instance:

Suppose the given proof starts with an instance step:

${{\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}}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta^{\prime}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}_{2}},$

where $\theta^{\prime}$ is an extension, possibly by the identity, of the
substitution $\theta$ to include fresh variables occuring in $t$. Thus
${\mathfrak{A}}\theta^{\prime}={\mathfrak{A}}\theta,{\mathfrak{B}}\theta^{\prime}={\mathfrak{B}}\theta,P\theta^{\prime}=P\theta$
and $G[t/x]\theta^{\prime}=G\theta[t\theta^{\prime}/x]$. Letting
$u=t\theta^{\prime}$ and applying the inductive hypothesis to the deduction
starting with the second state, we have

$\displaystyle{\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G\theta[u/x]}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{\exists
x.(G\theta)}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{(\exists
x.G)\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}},$

which is what we wanted to show.

generic:

Suppose the given proof starts with a generic step:

${{\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}}}\,{{\mathfrak{A}}_{2}}.$

Let $\alpha$ be the type of $x$ (and $c$). Pick $d\in{\sf D}_{i,\alpha}$ and
define $\mathbb{A}^{d}$ to be the uniform algebra
$\langle{\mbox{${\mathfrak{D}}$}^{d},\mathfrak{U},\Omega,\mathcal{I}}\rangle$
where $\mbox{${\mathfrak{D}}$}^{d}$ is the uniform applicative structure
$\langle{{\sf D},{\sf App},\mbox{\sf Const}^{d},\mbox{\sf Inc},{\sf M}_{{\sf
p}}}\rangle$ with the same domains as ${\mathfrak{D}}$, but where $\mbox{\sf
Const}_{(i+1)\alpha}^{d}(c)=\mbox{\sf Inc}_{(i+1)i\alpha}(d)$, (which we will
also denote by $d$) and hence $\mathfrak{U}(c)_{\varphi}=d$.

Applying the induction hypothesis (and the substitution lemma) to the uniform
algebra $\mathbb{A}^{d}$ we have

$\displaystyle{\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i+1}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G\theta[c/x]}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{G\theta}\rrbracket_{\varphi[d/x]}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\varphi}}\wedge_{\Omega}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\sf
App}({\llbracket{\lambda
x.G\theta}\rrbracket_{\varphi}},d)})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}.$

Since the choice of $d$ was arbitrary in ${\sf D}_{i,\alpha}$, we may take the
meet of the right hand side over all $d\in{\sf D}_{i,\alpha}$, obtaining, by
clause (14) of Definition 3.4

$\displaystyle{\llbracket{{\mathfrak{A}}_{2}}\rrbracket_{\varphi}}$
$\displaystyle\leq_{\Omega}$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\wedge_{\Omega}}}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{\Pi_{{\sf
g}({\sf g}\alpha)}\lambda
x.G\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}}$
$\displaystyle=$
$\displaystyle{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\wedge_{\Omega}}}\mathcal{I}_{i}({{\llbracket{P\theta}\rrbracket_{\varphi}}},{{\llbracket{\forall
x.G\theta}\rrbracket_{\varphi}}})\wedge_{\Omega}{\llbracket{{\mathfrak{B}}\theta}\rrbracket_{\varphi}},$

where we have acitly used the fact that ${\llbracket{\Pi_{{\sf g}({\sf
g}\alpha)}\lambda x.G\theta}\rrbracket_{\varphi}}={\sf
App}(\overline{\Pi}_{{\sf g}({\sf g}\alpha)},{\llbracket{\lambda
x.G\theta}\rrbracket_{\varphi}})$. This completes the proof of the theorem. ∎

##  4 Completeness

We now establish completeness of resolution. First of all, we need to define
the an auxiliary notation for the set of all instances of a program clause.

######  Definition 4.1 (extension of a program).

Given a program formula $D$ of level $i$ and $j\geq i$, we define the
_extension_ of $D$ at level $j$ as

$\begin{split}[j;D]=\\{A_{r}\gamma\leftarrow G\gamma\mid&\ \forall x_{1}\ldots
x_{n}(G\supset
A_{r})\in\textsf{elab}(D),\gamma=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\},\\\ &\
t_{1},\ldots,t_{n}\text{ are positive terms of level $j$ or
less}\\}\enspace.\end{split}$

If $P$ is a program of level $i$ and $j\geq i$, we define

$[j;P]=\bigcup_{D\in P}[j;D]\enspace.$

The following lemma is a direct consequence of the definition of the extension
of a program, and will be useful in some of the proofs.

######  Lemma 4.2.

Consider the transition system $\to_{i}$ on program formulas (of level $i$ or
less) given by the following transition rules:

  * •

$D_{1}\wedge D_{2}\to_{i}D_{k}$ for $k\in\\{1,2\\}$;

  * •

$\forall x_{\alpha}D\to_{i}D[t_{\alpha}/x_{\alpha}]$ for any positive term $t$
of level $i$.

Then, for any program formula $D$, we have that $Q\in[i;D]$ iff
$D\to_{i}^{*}Q\not\to_{i}$.

###### Proof.

Assume $Q=G\supset A\in[i;D]$ and we prove $D\to_{i}^{*}Q\not\to_{i}$. First
of all, note that $Q\supset A\not\to_{i}$ is immediate. We know there exists
$C=\forall\vec{x}(G_{0}\supset A_{0})\in\textsf{elab}(D)$ and
$\gamma=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ such that $G=G_{0}\gamma$ and
$A=A_{0}\gamma$. We proceed by induction on the complexity of $D$.

If $D=G^{\prime}\supset A^{\prime}$, then it is $G_{0}=G=G^{\prime}$,
$A_{0}=A=A^{\prime}$, hence $G\supset A=D$, and the result follows by
reflexivity of $\to_{i}^{*}$. If $D=D_{1}\wedge D_{2}$, then it is
$C\in\textsf{elab}(D_{k})$ for $k\in\\{1,2\\}$, hence $Q\in[i,D_{k}]$. By
inductive hypothesis, $D_{1}\wedge D_{2}\to_{i}D_{k}\to_{i}^{*}Q$. If
$D=\forall xD^{\prime}$, then $C=\forall xC^{\prime}$ with
$C^{\prime}\in\textsf{elab}(D^{\prime})$. If
$\gamma^{\prime}=\\{t_{2}/x_{2},\ldots,t_{n}/x_{n}\\}$ we also have
$Q^{\prime}=G\gamma^{\prime}\supset A\gamma^{\prime}\in[i;D^{\prime}]$. By
inductive hypothesis, we have $D^{\prime}\to_{i}^{*}Q^{\prime}$. It is easy to
check that $D^{\prime}[t_{1}/x_{1}]\to_{i}^{*}Q^{\prime}[t_{1}/x_{1}]=Q$,
therefore we get the derivation $D\to D^{\prime}[t_{1}/x_{1}]\to_{i}^{*}Q$.

For the opposite equality, we proceed by induction on the length of the
derivation of $D\to_{i}^{*}Q$. If this length is $0$, since $Q\not\to_{i}$,
then $D=Q=G\supset A$, and $Q\in[i;D]$ follows. Otherwise:

  * •

if the derivation has the form $D_{1}\wedge D_{2}\to_{i}D_{k}\to_{i}^{*}Q$,
then $Q\in[i;D_{k}]$ by inductive hypothesis. Therefore $Q=G\gamma\supset
A\gamma$ with $C=\forall\vec{x}(G\supset A)\in\textsf{elab}(D_{k})$ and
$\gamma=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$. Obviously
$C\in\textsf{elab}(D_{1}\wedge D_{2})$, hence $Q\in[i;D_{1}\wedge D_{2}]$.

  * •

if the derivation has the form $\forall xD\to_{i}D[t/x]\to_{i}^{*}Q$, then
$Q\in[i;D[t/x]]$ by inductive hypothesis. Therefore $Q=G\gamma\supset A\gamma$
with $C=\forall\vec{y}(G\supset A)\in\textsf{elab}(D[t/x])$ and
$\gamma=\\{t_{1}/y_{1},\ldots,t_{n}/y_{n}\\}$. By Lemma 2.12 there is $\forall
x\forall\vec{y}C^{\prime}\in\textsf{elab}(\forall x.D)$ such that
$C=C^{\prime}[t/x]$, whence $Q\in[i;\forall x.D]$ with
$\gamma=\\{t/x,t_{1}/y_{1},\ldots,t_{n}/y_{n}\\}$. ∎

In what follows, take $\Omega$ to be the Boolean algebra
$\\{\top,\bot\\}$.444The reader should note that this does not make our
semantics classical. See Section 4.1 for details. In the next section we will
consider broader classes of lattices Consider the uniform applicative
structure (which we will call the term structure) $\mathfrak{T}=\langle{\sf
D},{\sf App},\mbox{\sf Const},\mbox{\sf Inc},{\sf M}_{{\sf p}}\rangle$ with
${\sf D}_{i,\alpha}$ the set of principal normal forms of UCTT-terms of type
$\alpha$ and level $i$ or less; let ${\sf App}$ and Const build the obvious
terms and Inc consist of the appropriate inclusions. The (commutative) pre-
ordered monoid structure ${\sf M}_{{\sf p}}$ is given as follows. Let
$P\sqsubseteq_{\sf p}P^{\prime}$ iff $[i;P]\subseteq[i;P^{\prime}]$. The
monoid and product operations are supplied by the logical constants
$\wedge_{{\sf p}{\sf p}{\sf p}}$ and $\Pi_{{\sf p}{({\sf p}\alpha)}}$. The
requirement on $\Pi$ in Definition 3.2, namely that for any $f,d$ ${\sf
App}(f,d)\sqsubseteq_{\sf p}{\sf App}(\Pi_{{\sf p}({\sf p}\alpha)},f)$ is
easily checked, since ${\sf App}(\Pi,f)=\Pi f$, which is beta-eta equivalent
to $\Pi\lambda x.fx$ and hence $\forall x.fx$ for any $x\in{\textbf{bvar}}$.
The requirement thus reduces to [$i;fd$]$\subseteq$ [$i;\forall x.fx$], which
follows easily from the definition of [$i;P$].

The quickest path to completeness is to show that, with the term structure
$\mathfrak{T}$, the interpretation $I_{\vdash}$ given by

$(I_{\vdash})_{i}(P,G)=\top_{\Omega}\iff{\langle{i};{P}\mid{G}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

gives rise to a genuine uniform algebra. Thus any closed program-goal pair
true in all uniform algebras is provable. Since we want a bit more, namely how
to define such a structure by approximation from below, we will take a more
circuitous approach.

We show how to define a higher-order analogue of the least Herbrand Model,
which validates only resolution-derivable states, as the join of a countable
directed set of finitary partial models here called weak valuations. Weak
valuations, defined only on the term structure, are closer to the proof theory
than uniform algebras, and our main result will follow from showing that, in
the limiting case, such valuations give rise to a uniform algebra.

A weak valuation for the uniform applicative structure $\mathfrak{T}$ is an
indexed family of functions $I=\\{I_{i}:i\in\mathbb{N}\\}$, where for each
natural number $i$, $I_{i}:{\sf D}_{{i},{{\sf p}}}\times{\sf D}_{{i},{{\sf
g}}}\rightarrow\Omega$ satisfying the two monotonicity conditions

$\displaystyle P\sqsubseteq_{\sf p}Q$ $\displaystyle\,{\Rightarrow}\,$
$\displaystyle I_{i}({P},{G})\leq_{\Omega}I_{i}({P},{G}),$ (17) $\displaystyle
i\leq j$ $\displaystyle\,{\Rightarrow}\,$ $\displaystyle
I_{i}({P},{G})\leq_{\Omega}I_{j}({P},{G})$ (18)

as well as the conditions

$\displaystyle I_{i}({P},{\top})$ $\displaystyle=$
$\displaystyle\top_{\Omega}$ (19) $\displaystyle I_{i}({P},{G_{1}\wedge
G_{2}})$ $\displaystyle\leq_{\Omega}$ $\displaystyle
I_{i}({P},{G_{1}})\wedge_{\Omega}I_{i}({P},{G_{2}})$ (20) $\displaystyle
I_{i}({P},{G_{1}\vee G_{2}})$ $\displaystyle\leq_{\Omega}$ $\displaystyle
I_{i}({P},{G_{1}})\vee_{\Omega}I_{i}({P},{G_{2}})$ (21) $\displaystyle
I_{i}({P},{Q\supset G})$ $\displaystyle\leq_{\Omega}$ $\displaystyle
I_{i}({P\wedge Q},{G})$ (22) $\displaystyle I_{i}({P},{\exists x_{\alpha}G})$
$\displaystyle\leq_{\Omega}$
$\displaystyle\bigvee\\{I_{i}({P},{G[t_{\alpha}/x_{\alpha}]}):t_{\alpha}\in{\sf
D}_{i,\alpha}\\}$ (23) $\displaystyle I_{i}({P},{\forall x_{\alpha}G})$
$\displaystyle\leq_{\Omega}$ $\displaystyle
I_{i+1}({P},{G[c_{\alpha}/x_{\alpha}]})\quad\mbox{\small for all
$c_{\alpha}\in{\sf D}_{i+1,\alpha}\setminus{\sf D}_{i,\alpha}$.}$ (24)

Moreover, given $P\in{\sf D}_{{i},{{\sf p}}}$, $G\in{\sf D}_{{i},{{\sf g}}}$
and fresh constants $c_{\alpha},c^{\prime}_{\alpha}\in{\sf D}_{i+1,\alpha}$,
the following invariant condition must hold:

$I_{i+1}({P[c_{\alpha}/x_{\alpha}]},{G[c_{\alpha}/x_{\alpha}]})=I_{i+1}({P[c^{\prime}_{\alpha}/x_{\alpha}]},{G[c^{\prime}_{\alpha}/x_{\alpha}]})\enspace.$
(25)

Note that we are using a more compact notation w.r.t. the definition of
uniform algebra (Definition 3.4), since we are only considering term
structures here. In particular, we are compeltely omitting the Inc operators,
since they are just inclusions.

We will call a weak interpretation bounded if it satisfies the additional
condition

$I_{i}({P},{A_{r}})\ \leq_{\Omega}\ \bigvee\\{I_{i}({P},{G}):A_{r}\leftarrow
G\in[i;P]\\}\quad\mbox{\small for rigid atoms $A_{r}$ }.$ (26)

As we shall see below, the only weak valuations we will need to prove the
completeness theorem, (the $T^{n}(I_{\bot})$ below) satisfy it automatically.

######  Lemma 4.3.

If $\Omega$ is a lattice then the set ${\cal J}$ of weak valuations form a
lattice with the same suprema and infima and the same distributive laws with
the partial order

$I\sqsubseteq I^{\prime}:=(\forall i\in\mathbb{N})\
I_{i}\sqsubseteq_{i}I_{i}^{\prime}$

where the order $\sqsubseteq_{i}$ on the valuation fibers $I_{i}$ is defined
pointwise.

Since the the order (on the $I_{i}$ and the $I$) is built up pointwise, it is
easily seen to inherit the structure of a complete lattice from $\Omega$. In
particular, the lattice has a bottom element given by
$I_{\bot}(P,G)=\top_{\Omega}\mbox{ if }G=\top\mbox{ else }\bot_{\Omega}$. The
top weak valuation maps all arguments to $\top_{\Omega}$.

We now define an operators on weak valuations and show it is continuous.

######  Definition 4.4.

Let $T:{\cal J}\rightarrow{\cal J}$ be the following function:

$\displaystyle T(I)_{i}(P,\top)$ $\displaystyle=$ $\displaystyle\top_{\Omega}$
$\displaystyle T(I)_{i}(P,A)$ $\displaystyle=$ $\displaystyle
I_{i}(P,A)\vee\bigvee\\{I_{i}({P},{G}):A\leftarrow
G\in[i;P]\\}\quad\mbox{\small$A$ atomic}$ $\displaystyle
T(I)_{i}(P,G_{1}\wedge G_{2})$ $\displaystyle=$ $\displaystyle
I_{i}({P},{G_{1}})\wedge_{\Omega}I_{i}({P},{G_{2}})$ $\displaystyle
T(I)_{i}(P,G_{1}\vee G_{2})$ $\displaystyle=$ $\displaystyle
I_{i}({P},{G_{1}})\vee_{\Omega}I_{i}({P},{G_{2}})$ $\displaystyle
T(I)_{i}(P,Q\supset G)$ $\displaystyle=$ $\displaystyle I_{i}({P\wedge
Q},{G})$ $\displaystyle T(I)_{i}(P,\exists x_{\alpha}G)$ $\displaystyle=$
$\displaystyle\bigvee_{t_{\alpha}\in{\sf
D}_{{i},{\alpha}}}I_{i}({P},{G[t_{\alpha}/x_{\alpha}]})$ $\displaystyle
T(I)_{i}(P,\forall x_{\alpha}G)$ $\displaystyle=$ $\displaystyle
I_{i+1}({P},{G[c_{\alpha}/x_{\alpha}]})\text{ \small for any
$c_{\alpha}\in{\sf D}_{i+1,\alpha}\setminus{\sf D}_{i,\alpha}$}$

Note that, in the last rule, the choice of $c_{\alpha}$ is irrelevant, thanks
to (25).

Some comments on this defintion are in order. First, the reader should resist
any temptation to see it as an inductive definition on formula structure. $T$
is defined separately for each kind of logical formula in terms of the pre-
existing values of $I$, itself already defined on all goals. Thus none of the
impredicativity problems discussed in the introduction arise in this
definition.

The first clause of the definition, which is the truth-value analogue of the
$T_{P}$ operator of Apt and Van Emden [27], may be reformulated in the
following simpler and more familiar way

$T(I)_{i}(P,A)\ =\ \bigvee\\{I_{i}({P},{G}):A\leftarrow
G\in[i;P]\\}\quad\mbox{\small for $A$ an atomic goal formula}.$

The additional disjunct in our definition is a technical convenience that
enforces the inflationary character of $T$ for all weak interpretations. In
the proof of the completeness theorem we will only consider interpretations
which are finite iterates of $T$ on the least interpretation $I_{\bot}$, in
which case the condition (26) is automatically satisfied and $T$ is trivially
inflationary.

Below we show that $T$ is well defined, mapping weak valuations to weak
valuations. Until then we will only assume it maps weak valuations to
$\Omega$-valued functions.

Note that once we have shown $T$ is well-defined, its monotonicity as an
operator on weak valuations is immediate since the order on weak valuations is
defined pointwise, and $T$ is defined exclusively in terms of the lattice
operators on $\Omega$, all of them monotone.

######  Lemma 4.5.

The operator $T$ is inflationary: $I\sqsubseteq T(I)$ for any weak valuation
$I$. It is well-defined on ${\cal J}$, that is to say it takes weak valuations
to weak valuations, and it is continuous: if $\\{I_{n}:n\in\mathbb{N}\\}$ is
an increasing sequence of weak valuations, then

$T\left(\bigsqcup_{n}I_{n}\right)=\bigsqcup_{n}T(I_{n}).$

###### Proof.

#####  $T$ is inflationary

We begin by showing $T$ is inflationary, just as a function from weak
valuations to $\Omega$-valued operations on program-goal pairs. This must be
shown pointwise: for any $i,P,G$ we have
$I_{i}({P},{G})\leq_{\Omega}T(I)_{i}(P,G)$. We consider some of the various
cases for $G$:

$G$ is an atom $A$:

This case is immediate, since the value of $T$ is defined as the supremum of
the value of $I$ and another expression, as discussed above.

$G_{1}\wedge G_{2}$:

By assumption $I_{i}({P},{G_{1}\wedge
G_{2}})\leq_{\Omega}I_{i}({P},{G_{1}})\wedge_{\Omega}I_{i}({P},{G_{2}})$,
which coincides with $T(I)_{i}(P,G_{1}\wedge G_{2})$.

other cases:

The remaining cases are similar and left to the reader.

#####  $T$ is well defined

Now to show that $T$ is well defined, we must show that if $I$ is a weak
valuation, then $T(I)$ is too.

The monotonicity properties (17, 18) follow easily from the monotonicity of
operators in the clauses of the definition of $T$, and the fact that the
supremum in the atomic case of the definition of $T$ is taken over a bigger
set of clauses for bigger programs.

The logical cases are straightforward consequences of the inflationary
character of $T$. For example, $T(I)_{i}(P,G_{1}\wedge
G_{2})=I_{i}({P},{G_{1}})\wedge_{\Omega}I_{i}({P},{G_{2}})$. Since $T$ is
inflationary, the value of the right hand side is less than or equal to
$T(I)_{i}(P,G_{1})\wedge_{\Omega}T(I)_{i}(P,G_{2})$. In the universal case,
$T(I)_{i}(P,\forall xG)=I_{i+1}({P},{G[c/x]})\leq I_{i+2}({P},{G[c/x]})$. By
the invariant condition (25),
$I_{i+2}({P},{G[c/x]})=I_{i+2}({P},{G[c^{\prime}/x]})$ for any constant
$c^{\prime}$ of level $i+1$, and finally
$I_{i+2}({P},{G[c^{\prime}/x]})=T(I)_{i+1}(P,\forall xG)$. The remaining cases
involving logical constants similarly follow from the fact that $T$ is
inflationary.

For the invariant condition (25), the only non-trivial case is the atomic one.
Given programs $\bar{P}\in{\sf D}_{{i},{{\sf p}}}$ and atom $\bar{A}\in{\sf
D}_{{i},{{\sf a}}}$, let us denote $\bar{P}[c_{\alpha}/x_{\alpha}]$ and
$\bar{A}[c_{\alpha}/x_{\alpha}]$ by $P$ and $A$ respectively, while
$\bar{P}[c^{\prime}_{\alpha}/x_{\alpha}]$ and
$\bar{A}[c^{\prime}_{\alpha}/x_{\alpha}]$ will be denoted by $P^{\prime}$ and
$A^{\prime}$ respectively. It is enough to prove that $T(I)_{i+1}(P,A)\leq
T(I)_{i+1}(P^{\prime},A^{\prime})$. We have that:

$T(I)_{i+1}(P,A)=I_{i+1}(P,A)\vee\bigvee\\{I_{i+1}(P,G):A\leftarrow
G\in[i+1;P]\\}$

First, note that $I_{i+1}(P,A)=I_{i+1}(P^{\prime},A^{\prime})$. Consider now
the clause $A\leftarrow G\in[i+1;P]$. We would like to write $G$ as
$\bar{G}[c_{\alpha}/x_{\alpha}]$ for some goal $\bar{G}$, in order to use the
invariant property of $I$, but this is not possible since $G$ might contain
$x_{\alpha}$. Therefore, let $\hat{x}_{\alpha}$ be a fresh variable of type
$\alpha$ and same level as $x_{\alpha}$, not occurring in $A\leftarrow G$ nor
in $P$. Let $\hat{A}$, $\hat{G}$ and $\hat{P}$ be obtained by replacing
$c_{\alpha}$ in $A$, $G$ and $P$ with $\hat{x}_{\alpha}$, in such a way that
$A=\hat{A}[c_{\alpha}/\hat{x}_{\alpha}]$,
$G=\hat{G}[c_{\alpha}/\hat{x}_{\alpha}]$ and
$P=\hat{P}[c_{\alpha}/\hat{x}_{\alpha}]$. Note also that
$A^{\prime}=\hat{A}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}]$ and
$P^{\prime}=\hat{P}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}]$.

By Definition 4.1, there exists a clause $\forall x(G_{0}\supset
A_{0})\in\textsf{elab}(P)$ and a substitution
$\gamma=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ of level $i+1$ or less such that
$G=G_{0}\gamma$ and $A=A_{0}\gamma$. Consider the constant replacer $\xi$
mapping $c_{\alpha}$ to $c^{\prime}_{\alpha}$. By Lemma 2.24 we have that
there is a clause $\forall\vec{x}(G_{0}\xi\supset
A_{0}\xi)\in\textsf{elab}(P\xi)=\textsf{elab}(P^{\prime})$ and again by
Definition 4.1, $A_{0}\xi(\gamma\xi)\leftarrow
G_{0}\xi(\gamma\xi)\in[i+1;P^{\prime}]$. Note that
$G_{0}\xi(\gamma\xi)=G_{0}\gamma\xi=G\xi=\hat{G}[c_{\alpha}/\hat{x}_{\alpha}]\xi=\hat{G}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}]$
and
$A_{0}\xi(\gamma\xi)=A_{0}\gamma\xi=A\xi=\hat{A}[c_{\alpha}/\hat{x}_{\alpha}]\xi=\hat{A}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}]$,
which is also equal to $A^{\prime}$.

Therefore, in the right side of $T(I)_{i+1}(P^{\prime},A^{\prime})$ the term
$I_{i+1}(\hat{P}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}],\hat{G}[c^{\prime}_{\alpha}/\hat{x}_{\alpha}])$
appears. By hypothesis, this is equal to the term
$I_{i+1}(\hat{P}[c_{\alpha}/\hat{x}_{\alpha}],\hat{G}[c_{\alpha}/\hat{x}_{\alpha}])=I_{i+1}(P,G)$.
Therefore, each disjunct in $T(I)_{i+1}(P,A)$ has a corresponding disjunct in
$T(I)_{i+1}(P^{\prime},A^{\prime})$, proving $T(I)_{i+1}(P,A)\leq
T(I)_{i+1}(P^{\prime},A^{\prime})$.

#####  $T$ is continuous

The proof of continuity reduces to applying various distributivity properties,
the assumed $\wedge\bigvee$ distributive law, and the fact that suprema
commute with suprema. More precisely, we make use of the facts that in any
lattice with enough suprema

  * •

$\bigvee_{i}\bigvee_{j}m_{ij}=\bigvee_{j}\bigvee_{i}m_{ij}$.

  * •

If $k_{n}$ and $l_{n}$ are possible infinite increasing sequences in $\Omega$
then $\bigvee_{n}k_{n}\wedge\bigvee_{m}l_{m}=\bigvee_{n}(k_{n}\wedge l_{n})$.
This follows just from $\wedge\bigvee$ distributivity in $\Omega$ and the fact
that for any $m,n$ the meet $k_{n}\wedge l_{m}$ is bounded by $(k_{m}\vee
k_{n})\wedge(l_{m}\vee l_{n})$ which is $k_{max(m,n)}\wedge l_{max(m,n)}$.

We consider the various cases.

Atomic case:

$\displaystyle\Big{(}\bigsqcup_{n}T(I_{n})\Big{)}_{i}(P,A)$ $\displaystyle=$
$\displaystyle\bigvee_{n}T(I_{n})_{i}(P,A)$ $\displaystyle=$
$\displaystyle\bigvee_{n}\big{[}(I_{n})_{i}(P,A)\vee\bigvee\\{(I_{n})_{i}({P},{G}):A\leftarrow
G\in[i;P]\\}\big{]}$ $\displaystyle=$
$\displaystyle\Big{(}\bigvee_{n}(I_{n})_{i}(P,A)\Big{)}\vee\bigvee\Big{\\{}\bigvee_{n}(I_{n})_{i}({P},{G}):A\leftarrow
G\in[i;P]\Big{\\}}$ $\displaystyle=$
$\displaystyle\Big{(}\bigsqcup_{n}I_{n}\Big{)}_{i}(P,A)\vee\bigvee\Big{\\{}\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}({P},{G}):A\leftarrow
G\in[i;P]\Big{\\}}$ $\displaystyle=$ $\displaystyle
T\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}(P,A)$

repeatedly using the commutation of joins with joins.

conjunction:

$\displaystyle\Big{(}\bigsqcup_{n}T(I_{n})\Big{)}_{i}(P,G_{1}\wedge G_{2})$
$\displaystyle=$ $\displaystyle\bigvee_{n}T(I_{n})_{i}(P,G_{1}\wedge G_{2})$
$\displaystyle=$
$\displaystyle\bigvee_{n}[(I_{n})_{i}(P,G_{1})\wedge(I_{n})_{i}(P,G_{2})]$
$\displaystyle=$
$\displaystyle\bigvee_{n}(I_{n})_{i}(P,G_{1})\wedge\bigvee_{n}(I_{n})_{i}(P,G_{2})$
$\displaystyle=$
$\displaystyle\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}(P,G_{1})\wedge\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}(P,G_{2})$
$\displaystyle=$ $\displaystyle
T\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}(P,G_{1}\wedge G_{2}).$

$\exists$ case:

$\displaystyle\Big{(}\bigsqcup_{n}T(I_{n}))_{i}(P,\exists x_{\alpha}G)$
$\displaystyle=$ $\displaystyle\bigvee_{n}T(I_{n})_{i}(P,\exists x_{\alpha}G)$
$\displaystyle=$ $\displaystyle\bigvee_{n}\bigvee_{t_{\alpha}\in{\sf
D}_{{i},{\alpha}}}(I_{n})_{i}(P,G[t_{\alpha}/x_{\alpha}])$ $\displaystyle=$
$\displaystyle\bigvee_{t_{\alpha}\in{\sf
D}_{{i},{\alpha}}}\bigvee_{n}(I_{n})_{i}(P,G[t_{\alpha}/x_{\alpha}])$
$\displaystyle=$ $\displaystyle\bigvee_{t_{\alpha}\in{\sf
D}_{{i},{\alpha}}}\Big{(}\bigsqcup
I_{n}\Big{)}_{i}(P,G[t_{\alpha}/x_{\alpha}])$ $\displaystyle=$ $\displaystyle
T\Big{(}\bigsqcup_{n}I_{n}\Big{)}_{i}(P,\exists x_{\alpha}G)$

$\forall$ case:

$\displaystyle\Big{(}\bigsqcup_{n}T(I_{n})\Big{)}_{i}(P,\forall x_{\alpha}G)$
$\displaystyle=$ $\displaystyle\bigvee_{n}T(I_{n})_{i}(P,\forall x_{\alpha}G)$
$\displaystyle=$
$\displaystyle\bigvee_{n}(I_{n})_{i+1}(P,G[c_{\alpha}/x_{\alpha}])$
$\displaystyle=$
$\displaystyle\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i+1}(P,G[c_{\alpha}/x_{\alpha}])$
$\displaystyle=$ $\displaystyle
T\Big{(}\bigsqcup_{n}(I_{n})\Big{)}_{i}(P,\forall x_{\alpha}G)$

where it is assumed that we always take the same generic witness $c_{\alpha}$
for all $n$. ∎

By Kleene’s fixed point theorem, $T$ has a least fixed point
$T^{\infty}(I_{\bot})$, which we will call ${I^{{}^{\ast}}\\!\\!}$, and it is
the supremum of the finite iterates of $T$ applied to the least weak valuation
$\mathcal{I}_{\bot},T(\mathcal{I}_{\bot}),T^{2}(\mathcal{I}_{\bot}),\ldots$.

We now want to show that those program-goal pairs mapped to $\top_{\Omega}$ by
${I^{{}^{\ast}}\\!\\!}$, the least fixed point of $T$, are precisely those
provable by resolution with the identity substitution. This will give us
completeness of uniform algebras once we show ${I^{{}^{\ast}}\\!\\!}$ is a
genuine valuation, and not just a weak one. Because of the different way weak
valuations treat universal goals, this is not so straightforward, and first
requires showing directly the soundness of ${I^{{}^{\ast}}\\!\\!}$.

We need to show first that one property of genuine valuations is shared by
${I^{{}^{\ast}}\\!\\!}$, namely (16).

######  Lemma 4.6.

If $G\supset A_{r}\sqsubseteq_{\sf p}P$ then
${I^{{}^{\ast}}\\!\\!}_{i}(P,G)\leq_{\Omega}{I^{{}^{\ast}}\\!\\!}_{i}(P,A_{r})$.

###### Proof.

By definition, $G\supset A_{r}\sqsubseteq_{\sf p}P$ means $[i;G\supset
A_{r}]\subseteq[i;P]$ for each $i>0$. Since $[i;G\supset A_{r}]=\\{G\supset
A_{r}\\}$, this is equivalent to $G\supset A_{r}\in[i;P]$.

By Definition 4.4 of $T$, for any natural number $n$ (and any index $i$)

$T^{n+1}(I_{\bot})_{i}(P,A)=T^{n}(I_{\bot})_{i}(P,A)\vee\bigvee_{A\leftarrow
G^{\prime}\in[i;P]}T^{n}(I_{\bot})_{i}(P,G^{\prime}).$

Since $A\leftarrow G\in[i;P]$, $T^{n}(I_{\bot})_{i}(P,G)$ is one of the terms
over which the supremum is being taken. Therefore,
$T^{n}(I_{\bot})_{i}(P,G)\leq T^{n+1}(I_{\bot})_{i}(P,A)$. Taking suprema,
(first on the right, then on the left), we obtain
$T^{\infty}(I_{\bot})_{i}(P,G)\leq T^{\infty}(I_{\bot})_{i}(P,A)$ as we wanted
to show. ∎

######  Lemma 4.7.

Resolution in UCTT is sound for the interpretation ${I^{{}^{\ast}}\\!\\!}$ in
the following sense: if ${\mathfrak{A}}$ is a state vector and there is a
resolution

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

then for each state $\langle{i};{P}\mid{G}\rangle$ in ${\mathfrak{A}}$,
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G)=\top_{\Omega}$.

This proof, by induction on the length of the given resolution, is quite
similar to the soundness proof for uniform algebras, in fact simpler in many
of the inductive cases since only the identity substitution is involved, but
with the added wrinkle that we must manipulate the infinite joins that define
${I^{{}^{\ast}}\\!\\!}$. Without loss of generality, thanks to the
instantiation lemma, we may assume that the resolution is flat.

###### Proof.

If the proof has length $0$, then ${\mathfrak{A}}={\Box}$ and the result is
trivially true. We now suppose $n>0$ and that the result holds for any
deduction of length less than $n$. Assume the resolution
${{\mathfrak{A}}}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
has length $n$. If the derivation has the form

${\mathfrak{A}}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto}}}{\mathfrak{A}}\otimes{\mathfrak{C}}\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle[id]}}{{\leadsto\cdots\leadsto}}}{\Box}$

where $\langle{i};{P}\mid{G}\rangle$ is the selected state, the inductive
hypothesis automatically gives the theorem for all states in ${\mathfrak{A}}$
and ${\mathfrak{B}}$. Therefore, the only state which is interesting to
examine is the selected state. We now consider the possible cases arising in
the first step.

null:

Suppose the given resolution is of the form

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

For the state $\langle{i};{P}\mid{\top}\rangle$, we have that
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\top)=\top_{\Omega}$ by definition of weak
evaluation.

true:

The case for true resolution step is vacuous. Since all substitutions are
identities in a flat derivation, the true step is not allowed.

backchain:

Suppose the given resolution is of the form

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

where $\forall x(G\supset A_{r})\in\textsf{elab}(P)$,
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ is the renaming apart derivation
and $\theta$ the unificator of $A$ and $A_{r}\delta$, which is the identitity
on the variables of the initial state vector. By inductive hypothesis
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G\delta\theta)=\top_{\Omega}$. By definition
of the extension of a program $A\leftarrow G\delta\theta\in[i;P]$. Therefore

$\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,A)$ $\displaystyle=$
$\displaystyle\bigvee_{n}T^{n+1}(I_{\bot})_{i}(P,A)$ $\displaystyle=$
$\displaystyle\bigvee_{n}\Big{(}T^{n}(I_{\bot})_{i}(P,A)\vee\bigvee\\{T^{n}(I_{\bot})_{i}(P,G^{\prime})\mid
A\leftarrow G^{\prime}\in[i;P]\\}\Big{)}$ $\displaystyle\geq$
$\displaystyle\bigvee_{n}T^{n}(I_{\bot})_{i}(P,G\delta\theta)$
$\displaystyle=$ $\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G\delta\theta)$
$\displaystyle=$ $\displaystyle\top_{\Omega},$

as we wanted to show.

and:

Suppose the given deduction is of the form

${{\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[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

By induction hypothesis ${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G_{k})=\top_{\Omega}$
for every $k\in\\{1,2\\}$. Now for every natural number $n$ we have

$T^{n+1}(I_{\bot})(P,G_{1}\wedge
G_{2})=T^{n}(I_{\bot})_{i}(P,G_{1})\wedge_{\Omega}T^{n}(I_{\bot})_{i}(P,G_{2}).$

Taking first the supremum of the left hand side and then of the right, and
using $\wedge\bigvee$-distributivity we have

${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G_{1}\wedge
G_{2})\geq{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G_{1})\wedge_{\Omega}{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G_{1}),$

from which we obtain ${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G_{1}\wedge
G_{2})=\top_{\Omega}$, as we wanted to show.

or / augment:

The proofs for these rules are similar to the previous ones, and left to the
reader.

instance:

Suppose the given resolution is of the following form

${{\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[id]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

By induction hypothesis
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])=\top_{\Omega}$, whence

$\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\exists xG)$ $\displaystyle=$
$\displaystyle\bigvee_{n}T^{n+1}(I_{\bot})_{i}(P,\exists xG)$ $\displaystyle=$
$\displaystyle\bigvee_{n}\bigvee_{u\in
D_{i,\alpha}}T^{n}(I_{\bot})_{i}(P,G[u/x])$ $\displaystyle\geq$
$\displaystyle\bigvee_{n}T^{n}(I_{\bot})_{i}(P,G[t/x])$ $\displaystyle=$
$\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])$ $\displaystyle=$
$\displaystyle\top_{\Omega},$

as we wanted to show.

generic:

Suppose the given resolution is of the following form

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

for a fresh constant $c$ of label $i$. By induction hypothesis
${I^{{}^{\ast}}\\!\\!\\!}_{i+1}(P,G[c/x])=\top_{\Omega}$, whence

$\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\forall xG)$ $\displaystyle=$
$\displaystyle\bigvee_{n}T^{n+1}(I_{\bot})_{i}(P,\forall xG)$ $\displaystyle=$
$\displaystyle\bigvee_{n}T^{n}(I_{\bot})_{i+1}(P,G[c/x])$ $\displaystyle\geq$
$\displaystyle{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[c/x])$ $\displaystyle=$
$\displaystyle\top_{\Omega},$

with a fixed canonical choice of the witness $c$ for all the iterates of
$T^{n}$.

∎

######  Theorem 4.8.

Suppose ${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G)=\top_{\Omega}$. Then there is a
resolution

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

###### Proof.

Since $\top_{\Omega}$ is join irreducible in $\Omega$, the condition
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G)=\top_{\Omega}$ implies that for some
$k\in\mathbb{N}$ we must have ${T^{k}(I_{\bot})}_{i}({P},{G})=\top_{\Omega}$.
Thus it will suffice to show that this condition implies the conclusion of the
theorem for any $k$. The proof is by induction on $k$ (not on goal structure).

For $k=0$, the claim is trivial. ${(I_{\bot})}_{i}({P},{G})=\top_{\Omega}$ can
only happen if $G=\top$ in which case there is a one step resolution

${\langle{i};{P}\mid{\top}\rangle}\,\stackrel{{\scriptstyle\text{null}}}{{\mathbf{\leadsto}}}\,{{\Box}}$

Now we suppose the theorem holds for all $i,P,G$ for $k=n$ and assume
$\,{T^{n+1}(I_{\bot})}_{i}({P},{G})=\top_{\Omega}$. We may as well assume that
$n+1$ is the least iteration $k$ of $T$ for which this holds, else we are done
by the induction hypothesis.

Now we consider the six cases that arise depending on the structure of $G$.
The reader should not take this to be a proof by induction on the structure of
$G$, which would lead us right into the trap of inducting over an
impredicative higher-order formal system. We never appeal inductively to the
truth of the claim for subformulas, only to the truth of the claim for smaller
iterations of $T$.

atomic:

If the goal is a flex atomic formula, the statement is vacuously true, since
the $I_{i}^{*}(P,G)=\bot_{\Omega}$ in this case. If the goal is a rigid atomic
formula $A_{r}$, then ${T^{n+1}(I_{\bot})}_{i}({P},{A_{r}})=\top_{\Omega}$ and
by join-irreducibility of $\top_{\Omega}$ (trivially in $\\{\top,\bot\\}$) one
of the disjuncts on the right hand side of the first clause of Definition 4.4
must evaluate to $\top_{\Omega}$. In particular this means for some
$A_{r}\leftarrow G\in[i;P]$ we have
${T^{n}(I_{\bot})}_{i}({P},{G})=\top_{\Omega}$, and by the induction
hypothesis there is a resolution
${\langle{i};{P}\mid{G}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

By definition of the extension of the program, there is a clause
$\forall\vec{x}(G_{0}\supset A_{0})\in\textsf{elab}(P)$ and
$\gamma=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ such that $A_{0}\gamma=A_{r}$
and $G_{0}\gamma=G$, with terms $t_{1},\ldots,t_{n}$ of level $i$ or less.
Therefore, consider $\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$ a renaming-
apart substitution and $\gamma^{\prime}=\\{t_{1}/w_{1},\ldots,t_{n}/w_{n}\\}$,
we have

${\langle{i};{P}\mid{A_{r}}\rangle}\,\stackrel{{\scriptstyle\gamma^{\prime}}}{{\mathbf{\leadsto}}}\,{\langle{i};{P}\mid{G}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\ \stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

since $G_{0}\delta\gamma^{\prime}=G$ and
$A_{0}\delta\gamma^{\prime}=A_{r}\gamma^{\prime}=A_{r}$.

goal $\top$:

If the goal is $\top$, there is a one-step SLD proof using the null rule.

disjunction:

If the goal is of the form $G_{1}\lor G_{2}$, then we have, by the definition
of $T$, and irreducibility of $\top_{\Omega}$,
${T^{n}(I_{\bot})}_{i}({P},{G_{j}})=\top_{\Omega}$ for some $j\in\\{1,2\\}$.
By the induction hypothesis, we have a derivation
${\langle{i};{P}\mid{G_{j}}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
which by the or rule extends to ${\langle{i};{P}\mid{G_{1}\lor
G_{2}}\rangle}\,\stackrel{{\scriptstyle\vee}}{{\mathbf{\leadsto}}}\,{\langle{i};{P}\mid{G_{j}}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\ \stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

conjunction:

If the goal is $G_{1}\land G_{2}$, then, by definition of $T$, we have both
${T^{n}(I_{\bot})}_{i}({P},{G_{1}})=\top_{\Omega}$ and
${T^{n}(I_{\bot})}_{i}({P},{G_{2}})=\top_{\Omega}$. By inductive hypothesis on
$n$ iterations of $T$ there are two resolutions ${\bf
d}_{1}:{\langle{i};{P}\mid{G_{1}}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$,
${\bf
d}_{2}:{\langle{i};{P}\mid{G_{2}}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

Consider new derivations ${\bf d}_{1}^{\prime}$ and ${\bf d}_{2}^{\prime}$
obtained from ${\bf d}_{1}$ and ${\bf d}_{2}$ by renaming variables and
constant in such a way that the only variables and constants in common between
them are those which are already in common in the original state vectors.

Then we may build a new derivation starting from
$\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle$ by
first appending the state $\langle{i};{P}\mid{G_{2}}\rangle$ to all state
vectors of ${\bf d}^{\prime}_{1}$, then continuing with ${\bf
d}^{\prime}_{2}$:

$\hbox
to0.0pt{$\underbrace{\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto\cdots\leadsto}}}\langle{i};{P}\mid{G_{2}}\rangle}_{{\bf
d}_{1}\otimes\langle{i};{P}\mid{G_{2}}\rangle}$\hss}\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto\cdots\leadsto}}}\overbrace{\langle{i};{P}\mid{G_{2}}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto\cdots\leadsto}}}{\Box}}^{{\bf d}^{\prime}_{2}}\enspace.$

Prefixing with the step $\langle{i};{P}\mid{G_{1}\wedge
G_{2}}\rangle\mathrel{\stackrel{{\scriptstyle\wedge}}{{\leadsto}}}\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle$
we have the required derivation.

implication:

In case ${T^{n+1}(I_{\bot})}_{i}({P},{D\supset G^{\prime}})=\top_{\Omega}$, we
have ${T^{n}(I_{\bot})}_{i}({P\cup D},{G^{\prime}})=\top_{\Omega}$ and so by
the induction hypothesis, we have a derivation ${\langle{i};{P\cup
D}\mid{G^{\prime}}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
By the augment rule, we then have the desired SLD resolution
${\langle{i};{P}\mid{D\supset
G^{\prime}}\rangle}\,\stackrel{{\scriptstyle\supset}}{{\mathbf{\leadsto}}}\,{\langle{i};{P\cup
D}\mid{G^{\prime}}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\ \stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

exists:

Assume ${T^{n+1}(I_{\bot})}_{i}({P},{\exists
x_{\alpha}G^{\prime}})=\top_{\Omega}$. Then

$\top_{\Omega}=\bigvee_{t_{\alpha}\in
D_{i.\alpha}}T^{n}(I_{\bot})_{i}({P},{G^{\prime}[t_{\alpha}/x_{\alpha}]}).$

Since $\top_{\Omega}$ is join-irreducible in $\Omega$, for some positive term
$t$ of level $i$ or less,
${T^{n}(I_{\bot})}_{i}({P},{G^{\prime}[t_{\alpha}/x_{\alpha}]})=\top_{\Omega}$
and by the induction hypothesis there is a derivation
${\langle{i};{P}\mid{G^{\prime}[t_{\alpha}/x_{\alpha}]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
This new derivation can be extended to ${\langle{i};{P}\mid{\exists
x_{\alpha}G^{\prime}}\rangle}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{\langle{i};{P}\mid{G^{\prime}[t_{\alpha}/x_{\alpha}]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\ \stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

forall:

Suppose $G$ is of the form $\forall x_{\alpha}G^{\prime}$, so
${T^{n+1}(I_{\bot})}_{i}({P},{\forall x_{\alpha}G^{\prime}})=\top_{\Omega}$.
Then, for some fresh constant $c_{\alpha}$ of level $i+1$, we have
${T^{n}(I_{\bot})}_{i+1}({P},{G^{\prime}[c_{\alpha}/x_{\alpha}]})=\top_{\Omega}$.
By induction hypothesis there is a deduction

${\langle{i+1};{P}\mid{G^{\prime}[c_{\alpha}/x_{\alpha}]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$

and therefore

${\langle{i};{P}\mid{\forall
x_{\alpha}G^{\prime}}\rangle}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{\langle{i+1};{P}\mid{G^{\prime}[c_{\alpha}/x_{\alpha}]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace.$

∎

We note that we have shown that $I^{{}^{\ast}}\\!\\!$ coincides with the
proof-theoretic mapping $I_{\vdash}$ defined by

$(I_{\vdash})_{i}(P,G)=\top_{\Omega}\text{ just in case
}{\langle{i};{P}\mid{G}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Now we will show that $I^{{}^{\ast}}\\!\\!$ is an $\Omega$-interpretation for
$\Omega=\\{\top_{\Omega},\bot_{\Omega}\\}$ as given by Definition 3.4.

######  Lemma 4.9.

If $\Omega=\\{\top_{\Omega},\bot_{\Omega}\\}$, then ${I^{{}^{\ast}}\\!\\!}$ is
an $\Omega$-interpretation, and taking $\llbracket{t}\rrbracket_{\varphi}={\bf
nf(}{t\varphi}{\bf)}$, we have that $\langle{\mathfrak{T},\llbracket{\
}\rrbracket,\Omega,{I^{{}^{\ast}}\\!\\!}\ }\rangle$ is a uniform algebra.

###### Proof.

We have already shown in Lemma 4.6 that $I^{{}^{\ast}}\\!\\!$ satisfies
property (16) of valuations. Inspection of the proof of Lemma 4.7 shows that
we have already proven that the left-hand sides of equations (9, 10, 11, 12,
13) in the definition of valuation are greater than or equal to the right-hand
sides. Since $T$ is well-defined, $I^{{}^{\ast}}\\!\\!$ is a weak valuation,
which shows the inequalities going the other way. Monotonicity conditions (8)
and (15) are already part of the definition of weak evaluation. It remains to
prove both (7) and (14).

The proof of (7), i.e.,
${I^{{}^{\ast}}\\!\\!\\!}_{i}(A_{r},A_{r})=\top_{\Omega}$ for each rigid atom
$A_{r}$, follows immediately follows from the completeness theorem, given the
derivation

$\langle{i};{A_{r}}\mid{A_{r}}\rangle\mathrel{\stackrel{{\scriptstyle
id}}{{\leadsto}}}\top\mathrel{\stackrel{{\scriptstyle
null}}{{\leadsto}}}{\Box}\enspace.$

We use soundness and completeness of $I^{{}^{\ast}}\\!\\!$ to show the
universal case (14). Suppose ${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\forall
x.G)=\top_{\Omega}$. Then there is a deduction ${\langle{i};{P}\mid{\forall
xG}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
hence a derivation

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

By the first half of the generic constants corollary (Corollary 2.37) 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}.$
(28)

By soundness of $I^{{}^{\ast}}\\!\\!$, for any such $t$ we have
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])=\top_{\Omega}$. Taking infima we
obtain $\bigwedge_{t}{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])=\top_{\Omega}$.

Using the second half of the generic constants corollary (Corollary 2.37),
which tells us that if for every suitable term $t$ there is a deduction (28)
then there is one of the form (27), we obtain the converse, namely that if
$\bigwedge_{t}{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])=\top_{\Omega}$ then
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\forall x.G)=\top_{\Omega}$. Since
$\Omega=\\{\top_{\Omega},\bot_{\Omega}\\}$, this is enough to ensure that
${I^{{}^{\ast}}\\!\\!\\!}_{i}(P,\forall
x.G)=\bigwedge_{t}{I^{{}^{\ast}}\\!\\!\\!}_{i}(P,G[t/x])$. ∎

######  Corollary 4.10 (Completeness).

Let $P$ and $G$ be closed program and goal formulas respectively. If
$\mathcal{I}_{i}({\mathfrak{U}(P)},{\mathfrak{U}(G)})=\top_{\Omega}$ in all
uniform algebras $\mathfrak{U}$ (ranging over all $\Omega$) then there is an
SLD proof of $G$ from $P$ whose substitutions are the identity on the free
variables of $P$ and $G$.

###### Proof.

It suffices just to consider just the two-element Boolean algebra, where,
obviously, $\top$ is join irreducible, the uniform algebra
$(\mathfrak{T},\llbracket{\\_}\rrbracket,\Omega,{I^{{}^{\ast}}\\!\\!}\ )$
defined in Lemma 4.9 and the identity valuation $\varphi$. Then, the result is
an immediate corollary of Theorem 4.8. ∎

It should be noted that by a straightforward adaptation of the proof of the
corresponding theorem in Miller et al. [30], and Theorem A.4 in the Appendix,
an SLD proof of $G$ from $P$ exists iff a proof of ${P}\,\vdash\,{G}$ exists
in ICTT. Thus,
$\mathcal{I}_{i}({\mathfrak{U}(P)},{\mathfrak{U}(G)})=\top_{\Omega}$ in all
uniform algebras $\mathfrak{U}$ if and only if
$\llbracket{{P}\,\vdash\,{G}}\rrbracket=\top$ in all ICTT global models
${\mathfrak{E}}$, as defined in [11].

######  Theorem 4.11.

Let $\Omega$ be a complete Heyting Algebra in which $\top_{\Omega}$ is join-
irreducible. Assume
$\mathcal{I}_{i}({\mathfrak{U}(P)},{\mathfrak{U}(G)})_{\varphi}=\top_{\Omega}$
in all uniform algebras $(\mathfrak{T},\mathfrak{U},\Omega,\mathcal{I})$ and
environments $\varphi$. Then, there is an SLD derivation
${\langle{i};{P}\mid{G}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\cdots\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

###### Proof.

We consider the uniform algebra
$(\mathfrak{T},\llbracket{\\_}\rrbracket,\Omega,{I^{{}^{\ast}}\\!\\!})$ where
$\mathfrak{T}$ is the uniform term algebra defined at the beginning of this
section and ${I^{{}^{\ast}}\\!\\!}$ the valuation
$T^{\infty}(\mathcal{I}_{\bot})$ discussed above, and where we fix the
environment $\varphi$ to be the identity and take $\llbracket{\\_}\rrbracket$
(with the identity environment) to be the interpretation that maps open UCTT
terms to their normal form. ∎

###  4.1 Why the Semantics is Intuitionistic

Even if we choose $\Omega$ to be a Boolean Algebra, (such as the two element
algebra) our completeness theorem is for intuitionistic logic. This is
immediate from the fact that we obtain completeness at all, above.
Nonetheless, it is worth pointing out why a potentially classical algebra of
truth values will not sacrifice the inuitionistic character of our semantics.

The main reason is that the object of truth values $\Omega$ is modelling the
metatheory, whereas, the program denotations are modelling the theory, as the
following remark should make clear. One should think of

$I(p,g)=u\in\Omega$

as saying something similar to what, in Kripke semantics, would read

$``p\Vdash g^{\prime\prime}\mbox{ has truth-value }u.$

Just to illustrate, we will look at the term-model semantics of the
classically, but not intuitionistically valid law: $(P\supset Q)\vee(Q\supset
P)$, using the empty program.

$\displaystyle I(\varnothing,(P\supset Q)\vee(Q\supset P))$ $\displaystyle=$
$\displaystyle I(\varnothing,P\supset Q)\vee I(\varnothing,Q\supset P)$
$\displaystyle=$ $\displaystyle I(P,Q)\vee I(Q,P)$

If $Q$ and $P$ are distinct atoms, neither $I(P,Q)$ nor $I(Q,P)$ will, in
general, be true.

Thus the cHa $\Omega$ gives us an extra degree of freedom to interpret the
metatheory of the underlying Kripke-like structure. How this can be exploited
is the subject of the rest of the paper.

###  4.2 Enriched Resolution

We now need to consider an enriched notion of resolution, in which arbitrary
instantiations of variables are allowed in a single step. We can think of this
as a way of making the converse of the instantiation lemma (Lemma 2.29),
called the _lifting lemma_ in the first-order Horn case [27] which _fails_ in
RES(t), hold.

If the lifting lemma held, for any state $\langle{i};{P}\mid{G}\rangle$ from
which we can resolve to ${\Box}$, the following resolution would have to exist

${\langle{i};{P}\mid{X}\rangle}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{\theta}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

where $X$ is a predicate variable of type $o$. It is impossible to guarantee
the existence of a deduction with this particular substitution (it does exist
with $\\{X/\top\\}$) unless there happens to be a clause in $\textsf{elab}(P)$
whose head is $G$, which is not even allowed if $G$ is non-atomic. But, in a
sense, the obstacle seems more a “side-effect” of the existence of higher-
order variables than essential.

######  Definition 4.12.

Let $\theta$ be a substitution, ${\mathfrak{A}},{\mathfrak{B}}$ state vectors,
$P$ a program and $G$ a goal. Then the sub resolution rule is defined by the
following transition:

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

We will say that a sequence of resolution steps possibly using this additional
sub-rule is a $\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}$resolution, and
write

${{\mathfrak{A}}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{{\mathfrak{B}}}$
(29)

to indicate that such an enriched resolution has taken place with $\theta$ the
composition of all intervening substitutions, restricted to the variables free
in the initial state.

First we show that *-deduction enriched with the possible use of the sub-rule
is sound for our semantics, from which we immediately obtain its
conservativity over standard resolution.

######  Theorem 4.13.

If there is a deduction
${{\mathfrak{A}}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{{\mathfrak{B}}}$
then in any uniform algebra
${\llbracket{{\mathfrak{B}}}\rrbracket_{\eta}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\eta}}$.

The proof, by induction on the length of
$\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}$-deductions, proceeds
identically to the preceding soundness proof for
$\mathbf{\leadsto}$-resolution. The only new case to consider is a proof that
starts with a sub-step, in which case we have to show that this single step is
sound. But if
${\mathfrak{A}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto}}}{\mathfrak{A}}\theta$
then the conclusion of the soundness theorem, namely
${\llbracket{{\mathfrak{B}}}\rrbracket_{\eta}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\eta}}$,
reduces, in this case, where ${\mathfrak{B}}$ is ${\mathfrak{A}}\theta$, to
${\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\eta}}\leq_{\Omega}{\llbracket{{\mathfrak{A}}\theta}\rrbracket_{\eta}}$,
which is trivially true.

######  Corollary 4.14.

$\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}$-deduction is conservative,
for closed program-goal pairs over $\mathbf{\leadsto}$. If there is a
deduction
${{\mathfrak{A}}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{\Box}$,
then there is a deduction
${{\mathfrak{A}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.

###### Proof.

If there is a deduction
${{\mathfrak{A}}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{\Box}$,
then by soundness,
$\top_{\Omega}\leq_{\Omega}{\llbracket{{\mathfrak{A}}}\rrbracket_{\eta}}$ in
any uniform algebra, with any environment. By the completeness theorem, there
is a proof
${{\mathfrak{A}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$.
∎

The enriched $\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}$-deduction
trivially satisfies what was called a “lifting” lemma in the discussion
following the proof of Lemma 2.29: if there is a resolution

${\bf
d}:{{\mathfrak{A}}\theta}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\varphi}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{{\mathfrak{B}}}$

then the substitution $\theta$ can be lifted

${{\mathfrak{A}}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta\varphi}}{{\cdots}}\,\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}\,{{\mathfrak{B}}}\enspace.$

Just consider a variant ${\bf d}^{\prime}$ of ${\bf d}$ which does not contain
any variable in ${\sf fv}({\theta})\setminus{\sf fv}({{\mathfrak{A}}\theta})$,
and precede its first step with one sub-step
${\mathfrak{A}}\stackrel{{\scriptstyle*}}{{\mathbf{\leadsto}}}^{\theta}{\mathfrak{A}}\theta$.
Thus, although $\mathbf{\leadsto}$ does not satisfy lifting, it can be
conservatively added.

With the sub-rule added to resolution, we are obviously also able to restrict
the instance rule to replacement of existentially quantified variables by
fresh logic variables:

${\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[z/x]}\rangle}\otimes{\mathfrak{B}}$

with $z$ fresh and of level $i$ or less since subsequent instantiation of $z$
can then be carried out using the sub rule.

##  5 Some alternative models

###  5.1 Completeness: Substitution Semantics

Inspection of the soundness and completeness theorems show that we may allow
$\Omega$ to be any complete Heyting Algebra in which the top element is join-
irreducible. Furthermore, the bottom-up (fixed point) characterization of the
least term-model used in the completeness theorem still holds.

We will now investigate how the as yet untapped degree of freedom we have in
choosing the object of truth values $\Omega$ can be exploited to give more
operationally sensitive information about programs.

######  Definition 5.1.

Define the preorder $\leq_{s}$ on safe (i.e. idempotent) substitutions as
follows.

$\theta\leq_{\sf s}\varphi\mbox{ iff }\exists\gamma(\varphi=\theta\gamma).$

We will also define the partial order $\theta\sqsubseteq\varphi$ to mean that
$\varphi$ extends $\theta$ to a possibly larger domain, i.e. $\varphi$
restricted to the variables in the domain of $\theta$ is identical to
$\theta$.

Note that $\theta\sqsubseteq\varphi$ is a special case of $\theta\leq_{\sf
s}\varphi$ for safe substitutions, since what we mean by the domain of a
substitution is the set of variables $x$ for which $x\neq\theta(x)$. In
conventional mathematical terms, its true domain is the entire set of
variables, so if $\theta\sqsubseteq\varphi$ then letting $\gamma$ be the
substitution

$\gamma(x)=\begin{cases}\varphi(x)&\mbox{ if
$x\in\mathsf{dom}(\varphi)\setminus\mathsf{dom}(\theta)$}\\\
x&\mbox{otherwise,}\end{cases}$

we have $\varphi=\theta\gamma$. This definition is consistent precisely
because $\varphi$ and $\theta$ are assumed safe. Any variable $x$ among ${\sf
fv}({t})$ for some $t$ in the range of $\theta$ is also a variable in the
range of $\varphi$ by definition of $\theta\sqsubseteq\varphi$, hence not in
the domain of $\varphi$.

Also $\sqsubseteq$ is a partial order, but $\leq_{\sf s}$ is not since
$\theta\leq_{\sf s}\varphi\wedge\varphi\leq_{\sf s}\theta$ implies that
$\theta\sim\varphi$ but not necessarily that $\theta=\varphi$

######  Definition 5.2.

Let ${\Omega}_{\sf s}$ be the set of all upward $\leq_{\sf s}$-closed sets of
safe substitutions. That is to say $U\in{\Omega}_{\sf s}$ iff for every $u\in
U$ if $u\leq_{\sf s}v$ then $v\in U$.

It is easy to see that ${\Omega}_{\sf s}$ has a topology (the so-called
Alexandroff Topology induced by a preorder), that is to say, the set
$\top_{\sf s}$ of all safe substitutions and the empty set are in
${\Omega}_{\sf s}$, and ${\Omega}_{\sf s}$ is closed under unions and finite
(in fact, arbitrary) intersections. We also have that $\top_{\sf s}$ is join-
irreducible, since $U=\top_{\sf s}$ iff the identity substitution $id$ is in
$U$. Thus,

$\top_{\sf s}\subseteq V\cup V^{\prime}\quad\mbox{iff}\quad id\in V\cup
V^{\prime}\quad\mbox{iff}\quad id\in V\quad\mbox{or}\quad id\in
V^{\prime}\quad\mbox{iff}\quad\top_{\sf s}=V\quad\mbox{or}\quad\top_{\sf
s}=V^{\prime}.$

Thus, $({\Omega}_{\sf s},\subseteq)$ is a cHa, and is a suitable object of
truth values for a uniform algebra. We now define one such algebra, the
substitution-algebra, over ${\Omega}_{\sf s}$.

######  Definition 5.3.

Let $\mathbb{S}=\langle{\mbox{${\mathfrak{D}}_{\sf
s}$},\llbracket{\,}\rrbracket,{\Omega}_{\sf s},{\mathcal{I}_{\sf s}}}\rangle$
be the uniform algebra defined as follows. Take $(\mbox{${\mathfrak{D}}_{\sf
s}$},\llbracket{\,}\rrbracket)$ to be the underlying structure of the term-
model, i.e. the same uniform applicative structure used in the completeness
theorem, above. Define

$({{\mathcal{I}_{\sf s}}})_{i}(P,G)=\\{\theta:\theta\mbox{ is safe, of level
$i$ or less, and
}{\langle{i};{P\theta}\mid{G\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\\},$
(30)

where the domain of $\theta$ is not necessarily restricted to the variables
free in $P,G$.

Note that the condition on the substitutions $\theta$ mentioned in Definition
5.3, namely that they are not restricted to the program and goal pairs, is
essential here, otherwise the r.h.s. of (30) would not be upward closed. It is
easily seen so, since for any substitution $\gamma$, if
${\langle{i};{P\theta}\mid{G\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
then
${\langle{i};{P\theta\gamma}\mid{G\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{id}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
by Corollary 2.32.

######  Lemma 5.4.

The indexed family of mappings ${\mathcal{I}_{\sf s}}$ defined in (30) makes
$\mathbb{S}$ into a uniform algebra.

###### Proof.

We must check that ${\mathcal{I}_{\sf s}}$ satisfies all the conditions of
Definition 3.4, above.

condition (7):

If $A_{r}$ is a rigid atom, we have the following derivation

$\langle{i};{A_{r}}\mid{A_{r}}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto}}}\langle{i};{A_{r}}\mid{\top}\rangle\mathrel{\stackrel{{\scriptstyle
null}}{{\leadsto}}}{\Box}$

Therefore ${\mathit{i}d}\in{({\mathcal{I}_{\sf s}})_{i}}({A_{r}},{A_{r}})$,
and hence ${({\mathcal{I}_{\sf s}})_{i}}({A_{r}},{A_{r}})=\top_{\sf s}$.

condition (8):

If $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{G})$ then there is a
derivation

${\langle{i};{P\theta}\mid{G\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace.$

By Corollary 2.36 there is also a derivation

${\langle{i+1};{P\theta}\mid{G\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}\enspace,$

hence $\theta\in{({\mathcal{I}_{\sf s}})_{i+1}}({P},{G})$.

condition (9):

It states that $\mathcal{I}_{i}({P},{\top})=\top_{\Omega}$, which is
immediate.

condition (10):

Suppose $\theta$ is in ${({\mathcal{I}_{\sf s}})_{i}}({P},{G_{1}\wedge
G_{2}})$. Then there is a resolution

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

By the product lemma (Lemma 2.28) this condition is equivalent to the
existence of resolutions
${\langle{i};{P\theta}\mid{G_{1}\theta}\rangle}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$
and
${\langle{i};{P\theta}\mid{G_{2}\theta}\rangle}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}$,
or equivalently, $\theta\in{({\mathcal{I}_{\sf
s}})_{i}}({P},{G_{1}})\cap{({\mathcal{I}_{\sf s}})_{i}}({P},{G_{2}})$.

condition (11) and (12):

These cases are immediate, since the existence of an identity derivation of
${\Box}$ from $\langle{i};{P\theta}\mid{G_{1}\theta\vee G_{2}\theta}\rangle$
is equivalent to the existence of such a derivation from
$\langle{i};{P\theta}\mid{G_{i}\theta}\rangle$ for some $i\in\\{1,2\\}$, and
the existence of an identity derivation of ${\Box}$ from
$\langle{i};{P\theta}\mid{Q\theta\supset G\theta}\rangle$ to one from
$\langle{i};{P\theta\wedge Q\theta}\mid{G\theta}\rangle$.

condition (13):

Suppose $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{\exists xG})$, where $x$
is of type $\alpha$. This is equivalent to the existence of a flat deduction

${\langle{i};{P\theta}\mid{\exists
x(G\theta)}\rangle}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{\langle{i};{P\theta}\mid{G\theta[t/x]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}{}\enspace.$

By the specialization lemma (Lemma 2.31), there is also a derivation of

$\langle{i};{P\theta}\mid{G\theta[t/x]\theta}\rangle\mathrel{\stackrel{{\scriptstyle[{\mathit{i}d}]}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

and since $G\theta[t/x]\theta=G[t/x]\theta$, we have
$\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{G})$. Hence
$\theta\in\bigvee_{d\in{\sf D}_{i,\alpha}}{({\mathcal{I}_{\sf
s}})_{i}}({P},{G[d/x]})$, which, in the term structure is equivalent to the
right hand side of condition (13).

Conversely, if $\theta\in\bigvee_{d\in{\sf D}_{i,\alpha}}{({\mathcal{I}_{\sf
s}})_{i}}({P},{G[d/x]})$, then for some term $t$

${\langle{i};{P\theta}\mid{G[t/x]\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Since $(G[t/x]\theta)=G\theta[t\theta/x]$, we have

${\langle{i};{P\theta}\mid{\exists
x(G\theta)}\rangle}\,\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}\,{\langle{i};{P\theta}\mid{G\theta[t\theta/x]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle{\mathit{i}d}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}{}\enspace,$

and hence that $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{\exists xG})$.

condition (14):

Suppose $\theta$ is in ${({\mathcal{I}_{\sf s}})_{i}}({P},{\forall xG})$, with
$x$ of type $\alpha$. Then there is a derivation

${\langle{i};{P\theta}\mid{(\forall
xG)\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Since no bound variable is in the domain of $\theta$, the goal $(\forall
xG)\theta$ is equivalent to $\forall x(G\theta)$, and the rest of the
derivation must be of the form

${\langle{i};{P\theta}\mid{\forall
x(G\theta)}\rangle}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{\langle{i+1};{P\theta}\mid{G\theta[c/x]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle{\mathit{i}d}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

By the (first claim) of the corollary on generic constants (Corollary 2.37),
for any positive term $t$, there is a derivation

${\langle{i};{P\theta}\mid{G\theta[t/x]}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box},$

and hence, for any positive term $u$, letting $t=u\theta$,

${\langle{i};{P\theta}\mid{G[u/x]\theta}\rangle}\,{\mathbf{\leadsto}}\,\stackrel{{\scriptstyle{{\mathit{i}d}}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box}.$

Therefore, $\theta\in\bigcap_{u\in{\sf D}_{i,\alpha}}{({\mathcal{I}_{\sf
s}})_{i}}({P},{G[u/x]})$.

Conversely, suppose $\theta\in\bigcap_{u\in{\sf
D}_{i,\alpha}}{({\mathcal{I}_{\sf s}})_{i}}({P},{G[u/x]})$. In particular,
taking as $u$ a fresh constant $c$ of level $i$ and type $\alpha$, we have

$\langle{i};{P\theta}\mid{G\theta[c/x]}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

By looking at the proof of the second part of the corollary on generic
constants (Corollary 2.37), it is clear that this is enough to ensure the
existence of a derivation

$\langle{i+1};{P\theta}\mid{G\theta[c^{\prime}/x]}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

where $c^{\prime}$ is a fresh contant of level $i+1$, hence

${\langle{i};{P\theta}\mid{(\forall
x.G)\theta}\rangle}\,\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}\,{\langle{i+1};{P\theta}\mid{G\theta[c^{\prime}/x]}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle{\mathit{i}d}}}{{\cdots}}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{\Box},$

and $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{\forall xG})$, as we wanted
to show.

condition (15):

Assume $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{G})$ and
$P\sqsubseteq_{\sf p}P^{\prime}$. Then, there is a derivation

$\langle{i};{P\theta}\mid{G\theta}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

Since $P\sqsubseteq_{\sf p}P^{\prime}$, we have
$\textsf{elab}(P)\subseteq\textsf{elab}(P^{\prime})$. It is easy to check
that, under this condition, we have a derivation

$\langle{i};{P^{\prime}\theta}\mid{G\theta}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

hence $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P^{\prime}},{G})$.

condition (16):

Let $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{G})$ and $G\supset
A_{r}\sqsubseteq_{\sf p}P$. Then, there is a derivation

$\langle{i};{P\theta}\mid{G\theta}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace.$

and $[i;G\supset A_{r}]\subseteq[i;P]$. Since $[i;G\supset
A_{r}]=\\{G\leftarrow A_{r}\\}$, this means there is a clause $\forall
x(G^{\prime}\supset A^{\prime}_{r})\in\textsf{elab}(P)$ and
$\gamma^{\prime}=\\{t_{1}/x_{1},\ldots,t_{n}/x_{n}\\}$ such that
$G^{\prime}\gamma^{\prime}=G$ and $A^{\prime}_{r}\gamma^{\prime}=A_{r}$.
Therefore, by considering the renaming-apart substitution
$\delta=\\{w_{1}/x_{1},\ldots,w_{n}/x_{n}\\}$, we have that
$\gamma=\\{t_{1}/w_{1},\ldots,t_{n}/w_{n}\\}\theta$ is an unifier for
$A_{r}^{\prime}\delta$ and $A\theta$ which is the identity over the variables
of $A\theta$, since $A_{r}\delta\gamma=A_{r}\gamma^{\prime}\theta=A_{r}\theta$
and $A_{r}\theta\theta=A_{r}\theta$ since $\theta$ is safe. Threfore, we have
a derivation:

$\langle{i};{P\theta}\mid{A_{r}\theta}\rangle\mathrel{\stackrel{{\scriptstyle\gamma}}{{\leadsto\cdots\leadsto}}}\langle{i};{P\theta}\mid{G\theta}\rangle\mathrel{\stackrel{{\scriptstyle{\mathit{i}d}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

whence $\theta\in{({\mathcal{I}_{\sf s}})_{i}}({P},{A_{r}})$.

∎

###  5.2 Lindenbaum Algebra and UCTT

We will now weaken the definition of Uniform Algebras to a class of structures
maintaining soundness, using an idea in [42]. It has long been known that it
is sufficient for a complete semantics to stipulate only that the object of
truth-values $\Omega$ contain enough infinitary meets and joins to interpret
quantifiers and implication. In particular, the parametrized family
$\\{I_{i}(P,G)_{\eta[x:=d]}\mid d\in D_{i,\alpha}\\}$ must have a meet and
join, and the $\wedge\bigvee$ distributive law must hold for existing joins.
Furthermore, we will restrict meets and joins to the interpretation of
different goals _with the same ambient program $P$_. Letting $\mathbb{P}$
stand for the partially ordered set of programs, we will define a model
_indexed over_ $\mathbb{P}$, as explained below.

Then we will show how to build a (global) uniform algebra out of
$\mathbb{P}$-indexed and parametrized algebras, using an _ideal completion_ to
build the algebra, a construction with a long history in lattice theory and
logic. See [42] for details.

####  5.2.1 A $\mathbb{P}$-indexed Lindenbaum Algebra for UCTT

We are now going to give constructive completeness theorem for UCTT which uses
a Lindenbaum-style algebra construction. In essence program-goal pairs are
interpreted as “themselves” in the object of truth-values. More precisely, we
will map states $\langle{i};{P}\mid{G}\rangle$ to equivalence classes
$[{{{P}}\vdash{{G}}}]_{i}$ of sequents in ICTT, with respect to an equivalence
relation to be defined below. We first fix our notation conventions. We will
write an indexed sequent ${P}\vdash_{i}{G}$ with natural number index $i$ to
indicate that the formulas in $P,G$ are over universe ${\cal U}_{i}$. Thus, if
the notation ${P}\vdash_{i}{G}$ is correct with respect to levels, so does
${P}\vdash_{k}{G}$ for any $k>i$. Indices may be omitted if clear from
context, or when it is clear that they are ranging over all possible natural
number values, as in the definition below.

######  Definition 5.5.

We define the binary relation $\leq_{\cal T}$ on indexed ICTT sequents as
follows: ${P}\vdash{G}\leq_{\cal T}{P^{\prime}}\vdash{G^{\prime}}$ if and only
if in some metatheory ${\cal T}\,$, presumed constructive, we can prove that
if the sequent ${P}\vdash{G}$ has a cut-free proof in ICTT then so does
${P^{\prime}}\vdash{G^{\prime}}$. We also describe this state of affairs by
$\mbox{${\cal
T}\,$}\mathbf{\vdash}\\!\\!\\!\\!\\!\\!\vdash\>{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}\,{\Rightarrow}\,{P^{\prime}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G^{\prime}}$, omitting mention of ${\cal T}\,$when clear from
context. We will also use the notation
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ (with or
without numerical index) to abbreviate the predicate “there is a cut-free
proof of ${P}\vdash{G}$.”

We denote by $\sim_{\cal T}$ the equivalence relation induced by this order,
i.e.

${P}\vdash_{i}{G}\sim_{\cal T}{P^{\prime}}\vdash_{k}{G^{\prime}}\quad\mbox{
iff }\quad{P}\vdash_{i}{G}\leq_{\cal
T}{P^{\prime}}\vdash_{k}{G^{\prime}}\quad\mbox{ and
}\quad{P^{\prime}}\vdash_{k}{G^{\prime}}\leq_{\cal T}{P}\vdash_{i}{G},$

and write the induced equivalence classes thus:
$[{{{P}}\vdash{{G}}}]_{i}=\\{{P^{\prime}}\vdash_{k}{G^{\prime}}:{P}\vdash_{i}{G}\sim_{\cal
T}{P^{\prime}}\vdash_{k}{G^{\prime}}\\}.$

Cut-elimination holds in ICTT [11], but we do not require it to be provable in
${\cal T}\,$in the results that follow.

The reader should note that it is possible for a sequent indexed by $i$ to
imply sequents with other indices. For example, any sequent lies below the
identity ${A}\vdash_{i}{A}$ for any $i$ and, say, any atom $A$ over ${\cal
U}_{i}$. It is easy to see that $\leq_{\cal T}$ is a preorder, $\sim_{\cal T}$
an equivalence relation and $[{{{P}}\vdash{{G}}}]_{i}$ is well-defined. We
will abuse language and use the same symbol for the preorder $\leq_{\cal T}$
and the induced order on equivalence classes.

The reader should note that

######  Lemma 5.6.

Let $\Omega_{\ell}$ be the poset of equivalence classes
$[{{{P}}\vdash{{G}}}]_{i}$ with order induced by $\leq_{\cal T}$. Then the
following suprema and infima exist in $\Omega_{\ell}$:

  * •

$[{{{P}}\vdash{{G_{1}}}}]_{i}\wedge_{\cal
T}[{{{P}}\vdash{{G_{2}}}}]_{i}=[{{{P}}\vdash{{G_{1}\wedge G_{2}}}}]_{i}$

  * •

$[{{{P}}\vdash{{G_{1}}}}]_{i}\vee_{\cal
T}[{{{P}}\vdash{{G_{2}}}}]_{i}=[{{{P}}\vdash{{G_{1}\vee G_{2}}}}]_{i}$

  * •

$\bigvee_{t\in{\sf
D}_{i,\alpha}}[{{{P}}\vdash{{G[t/x_{\alpha}]}}}]_{i}=[{{{P}}\vdash{{\exists
x_{\alpha}G}}}]_{i}$

  * •

$\bigwedge_{t\in{\sf
D}_{i,\alpha}}[{{{P}}\vdash{{G[t/x_{\alpha}]}}}]_{i}=[{{{P}}\vdash{{\forall
x_{\alpha}G}}}]_{i}$

The operations are indexed over a fixed program $P$. More formally, we can
think of $\Omega_{\ell}$ as a mapping from programs $P$ in $\mathbb{P}$ to the
set of all (equivalence classes of) pairs $[{{{P}}\vdash{{G}}}]_{i}$ for goals
$G$. The $\wedge$ and $\vee$ operations are defined on each of these sets, but
not for pairs with different programs.

The choice of ${\cal T}\,$matters in this lemma. It must be strong enough to
support the arguments below. A key point here is that these arguments are
clearly constructive. It will suffice, for our purposes to take ${\cal T}\,$to
be the constructive set-theory IZF [6, 28] although a considerably weaker
theory could be used.

###### Proof.

For the first claim, observe that
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G_{1}\wedge
G_{2}}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{1}}\mbox{ and }{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{2}}$, by induction on the depth of the given proof. If the depth
is 0, then ${P}\vdash{G_{1}\wedge G_{2}}$ was derived by the identity axiom,
i.e. $P=P^{\prime},G_{1}\wedge G_{2}$, where $G_{1},G_{2}$ must be supposed
core formulas, i.e. both program and goal formulas. But then, applying
$\wedge_{L}$ to the axiom ${P^{\prime},G_{1},G_{2}}\vdash{G_{i}}$, we have
${P^{\prime},G_{1}\wedge G_{2}}\vdash{G_{i}}$.

The inductive cases are easy. Consider the last rule used in a cut-free proof
of ${P}\vdash{G_{1}\wedge G_{2}}$. Because of the program-goal structure of
$P,G$ the only possibilities are $\wedge_{R}$, which would give us the desired
result immediately, or the $\forall_{L},\supset_{L}$ and $\wedge_{L}$ rules.
In the latter cases, we apply the inductive hypothesis to the relevant premiss
to obtain the desired proof. From this we have that any sequent below
${P}\vdash{G_{1}\wedge G_{2}}$ is below the infimum of the other two.

Now suppose ${Q}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{1}}\mbox{ and }{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{2}}$. Then ${Q}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{1}\wedge G_{2}}$, so $[{{{P}}\vdash{{G_{1}\wedge
G_{2}}}}]_{i}\sim_{\cal T}[{{{P}}\vdash{{G_{1}}}}]_{i}\wedge_{\cal
T}[{{{P}}\vdash{{G_{2}}}}]_{i}$.

One direction of the second claim follows from $\vee_{R}$:
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{i}}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{1}\vee G_{2}}$. To show the other direction we must show

${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G_{1}\vee
G_{2}}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{1}}\mbox{ or }{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G_{2}}$

making use of the fact that $P$ is a program formula. Thus the sequent
${P}\vdash{G_{1}\vee G_{2}}$ could not have been derived by the identity
axiom, since disjunctions are not allowed on the left. If the last rule used
was $\vee_{R}$ we are done. If it was one of the three allowed left rules, we
proceed as in the preceding case, applying the induction hypothesis to the
relevant premiss(es).

For the third claim we use $\exists_{R}$ for one direction, and then establish
the existence property for cut-free proofs of program formulas

${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{\exists
x_{\alpha}G}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G[t/x_{\alpha}]}\mbox{ for some }t\in{\sf D}_{i,\alpha}$

As above, we induct on the depth of the given cut-free proof. The depth cannot
be 0 (or if the reader prefers to say it this way, the base case is vacuously
true) since an existential formula cannot be a program formula. Suppose the
claim holds for all shorter cut-free proofs of an existential goal from a
program formula. If the last rule used was $\exists_{R}$ we are done.
Otherwise one of the three allowed left rules was used, and applying the
induction hypothesis to the relevant premiss(es) we are done.

This result almost gives the other direction of the third claim. Since
$t_{\alpha}\in{\sf D}_{i,\alpha}$ means that $t$ is a positive formula, we
need to appeal to Theorem 3.2.14 of Nadathur’s dissertation and the subsequent
Miller _et al._ [32, 30] to show that if a cut-free proof of
${P}\vdash{\exists x_{\alpha}G}$ exists, then there must be a cut-free proof
for a positive witness.

Finally, the fourth claim follows from the fact that if
$[{{{Q}}\vdash{{G}}}]_{i}\leq_{\cal T}[{{{P}}\vdash{{G[t/x]}}}]_{i}$ for each
$t\in{\sf D}_{i,\alpha}$, then
${Q}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ implies the
existence of a cut-free proof of every positive instance, in particular, for
$t$ a fresh variable, whence, by $\forall_{R}$, the derivability of
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{\forall
x_{\alpha}G}$. For the other direction argue by induction as in the preceding
cases. If a cut-free proof of ${P}\vdash{\forall x_{\alpha}G}$ has depth 0,
then $P=P^{\prime},\forall xG$, and $G$ is both a program and goal formula.
But then we can produce the desired cut-free proof for any positive instance
$t$ using the identity axiom and $\forall_{L}$:

${P^{\prime},\forall xG}\vdash{G[t/x]}{P^{\prime},G[t/x]}\vdash{G[t/x]}$

For the inductive case, suppose the last rule used was $\forall_{R}$. Then $x$
does not occur freely in the final sequent, and there is a cut-free proof of
its immediate premises, of the form ${P}\vdash{G}$. It is a straightforward
exercise to show, by induction on the length of this proof, that a cut-free
proof of ${P}\vdash{G}[t/x]$ must also exist. If the last rule used is one of
the three allowed left rules, the argument proceeds as above. ∎

######  Lemma 5.7 (Generalized contraction).

Suppose $Q\in[i;P]$ for some $i$. If
${P,Q}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ then
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$.

###### Proof.

By definition of extension there is a program formula $D\in P$ such that
$Q\in[i;D]$. We consider a generalization of the proof where $Q$ is any
formula derivable from $D$ through $\to_{i}$, and we prove the result by
induction on the length $n$ of the derivation.

If $n=0$, then $Q=D=G\supset A$, and the resut follows from contraction in
ICTT. Otherwise, consider the last step in the derivation of $Q$ through the
transition system in Lemma 4.2.

$Q_{1}\wedge Q_{2}\to_{i}Q_{k}$:

Then the derivation is of the following form: $D\to_{i}^{n-1}\,Q_{1}\wedge
Q_{2}\rightarrow Q_{k}$. Assume without loss of generality that $k=1$. By the
induction hypothesis, if ${P,Q_{1}\wedge
Q_{2}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ then
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$. Now suppose
${P,Q_{1}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$. Then
${P,Q_{1},Q_{2}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$
by weakening-left (an easily derived rule of ICTT), so ${P,Q_{1}\wedge
Q_{2}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ by
$\wedge_{L}$, hence ${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}$.

$\forall xQ^{\prime}\to_{i}Q^{\prime}[t/x]$:

By the induction hypothesis ${P,\forall
xQ^{\prime}}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$
implies ${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$. Now
suppose ${P,Q^{\prime}[t/x]}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}$ and use $\forall_{L}$. ∎

Now we are able to prove the following lemma.

######  Lemma 5.8.

If $G\supset R\in[i;P]$ and
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ then
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{R}$.

###### Proof.

We have that ${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{G}$, and trivially
${P,R}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{R}$. By arrow-
left ${P,G\supset R}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}{R}$. By the preceding lemma
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{R}$ ∎

Now we use $\Omega_{\ell}$ as an object of truth-values for a parametrically
complete uniform algebra over the term model.

######  Definition 5.9.

Let $\mathbb{L}=\langle{\mbox{${\mathfrak{D}}_{\sf
s}$},\mathfrak{U},\text{$\Omega_{\ell}$},\mbox{${\cal L}$}}\rangle$ be the
parametrically complete uniform algebra defined as follows. Take
$(\mbox{${\mathfrak{D}}_{\sf s}$},\mathfrak{U})$ to be the underlying
structure of the term-model, i.e. the same uniform applicative structure used
in the first completeness theorem, above. Define the indexed family of
mappings $\mbox{${\cal L}$}_{i}:{\sf D}_{i,{\sf p}}\times{\sf D}_{i,{\sf
g}}\rightarrow\text{$\Omega_{\ell}$}$ as follows.

$\mbox{${\cal L}$}_{i}(P,G)=[{{{P}}\vdash{{G}}}]_{i}$ (31)

######  Theorem 5.10.

The mappings $\mbox{${\cal L}$}_{i}$ make $\mathbb{L}$ into a p.c. uniform
algebra.

###### Proof.

We check all the conditions of Definition 3.4, above.

condition (7):

Let $R$ be a rigid atom of level $i$. Then $\mbox{${\cal
L}$}_{i}(R,R)=[{{{R}}\vdash{{R}}}]_{i}=\top_{\text{$\Omega_{\ell}$}}$.

condition (8):

Since ${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}_{i}{G}\,{\Rightarrow}\,{P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf
cf}}\\!}}_{i+1}{G}$ this case is immediate.

condition (9):

It states that $\mbox{${\cal
L}$}_{i}(P,\top)=[{{{P}}\vdash{{\top}}}]_{i}=\top_{\text{$\Omega_{\ell}$}}$
and it is immediate.

condition (10):

$\mbox{${\cal L}$}_{i}(P,G_{1}\wedge G_{2})=[{{{P}}\vdash{{G_{1}\wedge
G_{2}}}}]_{i}=[{{{P}}\vdash{{G_{1}}}}]_{i}\wedge_{\cal
T}[{{{P}}\vdash{{G_{2}}}}]_{i}$ by the preceding lemma.

conditions (11), (13), (14):

Similar to the previous case.

condition (12):

It is immediate, by $\supset_{R}$ in one direction and cut-free invertibility
of $\supset_{R}$ by a straightforward induction on the length of proofs in the
other.

condition (15):

We have to show that $P\sqsubseteq P^{\prime}$ implies $\mbox{${\cal
L}$}_{i}(P,G)\leq_{\cal T}\mbox{${\cal L}$}_{i}(P^{\prime},G)$. We can prove
that $P\sqsubseteq P^{\prime}$ implies
$\textsf{elab}(P)\subseteq\textsf{elab}(P^{\prime})$. Now use Lemma 2.14.

condition (16):

We need to prove that

$(G\supset_{{\sf p}{\sf g}{\sf r}}R)\sqsubseteq_{\sf p}P\textrm{ implies
}\mbox{${\cal L}$}_{i}({P},{G})\leq_{\Omega}\mbox{${\cal
L}$}_{i}({P},{\mbox{\sf Inc}_{{\sf g}{\sf a}}(\mbox{\sf Inc}_{{\sf a}{\sf
r}}(R))}).$

Note that $(G\supset_{{\sf p}{\sf g}{\sf r}}R)\sqsubseteq_{\sf p}P$ implies
that $(G\supset_{{\sf p}{\sf g}{\sf r}}R)\in[i;P]$, so by Lemma 5.8 if
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{G}$ then
${P}\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}{R}$. ∎

####  5.2.2 The Algebra of Ideals

We now define a complete Heyting algebra $\widehat{\Omega}$ as follows. The
elements are sets of members $[{{{P}}\vdash{{G}}}]_{i}$ of $\Omega_{\ell}$
ranging over all programs $P$ and goals $G$ _downward closed under_
$\leq_{\cal T}$. We define $\bigvee$ and $\bigwedge$ by union and
intersection. We call these sets $S$ _ideals_. They are also required to
satisfy the additional condition

$X\subseteq S\mbox{ and }\bigvee
X\in\text{$\Omega_{\ell}$}\quad\,{\Rightarrow}\,\quad\bigvee X\in S$

The ideals together with their members form a topology, in fact an Alexandroff
topology (closed under arbitrary intersections) as is well known, so they are
also a Heyting Algebra $\widetilde{\Omega}$, which is what we require.

Define, for each $[{{{P}}\vdash{{G}}}]_{i}$ in $\Omega_{\ell}$, the induced
_principal ideal_ $\langle\\!\langle{P}|{G}\rangle\\!\rangle_{i}$ to be the
set

$\\{[{{{Q}}\vdash{{H}}}]_{i}\,:\,[{{{Q}}\vdash{{H}}}]_{i}\leq_{\cal
T}[{{{P}}\vdash{{G}}}]_{i}\\}$

######  Definition 5.11.

Let $\widetilde{\Omega}$ be as defined above. We now define an interpretation

$\mathfrak{I}:{\sf D}_{\sf p}\times{\sf D}_{{\sf
g}}\rightarrow\widetilde{\Omega}$

tacitly indexed over the signatures $i$, as follows

$\mathfrak{I}(P,G)=\langle\\!\langle{P}|{G}\rangle\\!\rangle$

Now the results of Lemma 5.6 and Theorem 5.10 easily give us the following
theorem.

######  Theorem 5.12.

$\mathfrak{I}$ and $\widetilde{\Omega}$ define a uniform algebra, not just a
$\mathbb{P}$-indexed model.

###### Proof.

First observe that $\mathfrak{I}_{i}(R,R)$ and $\mathfrak{I}_{i}(P,\top)$ each
equal the set of all pair classes $[{{{P}}\vdash{{G}}}]_{i}$, which is
$\top_{\widetilde{\Omega}}$, since
$R\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}R$ and
$P\>\vdash^{{}^{\\!\\!\\!{}_{\mbox{\scriptsize\sf cf}}\\!}}\top$. We check a
few of the remaining conditions (10),(11),(12),(13),(14).

condition (10):

$\langle\\!\langle{P}|{G\wedge
G^{\prime}}\rangle\\!\rangle=\langle\\!\langle{P}|{G}\rangle\\!\rangle\cap\langle\\!\langle{P}|{G}\rangle\\!\rangle$
since if $[{{{Q}}\vdash{{H}}}]_{i}\in\langle\\!\langle{P}|{G\wedge
G^{\prime}}\rangle\\!\rangle$ then $[{{{Q}}\vdash{{H}}}]_{i}\leq_{\cal
T}[{{{P}}\vdash{{G\wedge G^{\prime}}}}]_{i}$, hence
$[{{{Q}}\vdash{{H}}}]_{i}\leq_{\cal T}[{{{P}}\vdash{{G}}}]_{i}$ and
$[{{{Q}}\vdash{{H}}}]_{i}\leq_{\cal T}[{{{P}}\vdash{{G}}}]_{i}$ by Lemma 5.6,
therefore
$[{{{Q}}\vdash{{H}}}]_{i}\in\langle\\!\langle{P}|{G}\rangle\\!\rangle\cap\langle\\!\langle{P}|{G^{\prime}}\rangle\\!\rangle$.
The converse follows similarly by the same lemma.

conditions (11),(13),(14):

The arguments are similar and left to the reader.

condition (12):

From Theorem 5.10 we know that $[{{{P}}\vdash{{D\supset G}}}]_{i}=[{{{P\wedge
D}}\vdash{{G}}}]_{i}$ for each $i$. Therefore, also
$\mathfrak{I}_{i}(P,D\supset G)=\mathfrak{I}_{i}(P\wedge D,G)$.

conditions (15) and (16):

Similar to the previous one. ∎

We can now give a second proof of completeness, using the results of [30] and
the lemmas just established.

######  Theorem 5.13.

If the program-goal pair $P$, $G$ is mapped to $\top$ in all uniform algebras,
then the sequent $P\vdash G$ is derivable by a uniform proof.

###### Proof.

If $P,G$ is sent to $\top_{\widetilde{\Omega}}$ then $P\vdash G$ has a cut-
free proof. By the results of Miller et. al., it has a uniform proof. ∎

##### Semantic proof of uniformity

A considerable reworking of the tools developed in this section is required to
show, directly in the semantics, that validity in the algebra of ideals just
developed implies a uniform proof. It amounts to showing that the implication
operator in a Heyting Algebra interpretation coincides with the index-shifting
treatment of implication in goals in uniform algebras, which is beyond the
scope of this paper. Such a _semantic proof of uniformity_ is given, in the
setting of Kripke models and $\lambda$Prolog with constraints, in [26]. We
expect to explore the Lindenbaum-style model further in future work.

###  5.3 Indexed Models and Fibrations

For the reader familiar with category theory, it should be clear that we have
been working throughout the paper with certain categories indexed over a
category $\mathbb{P}$ of programs. Because of the operational interpretation
given to implications in goals, it is usually sufficient to take these
categories to be c$\mathbb{L}$AT, a category of parametrically complete
lattices, indexed over a category of programs, whose objects are interpreted
goals or state vectors with existing $\bigvee,\bigwedge,\top,\bot$ preserving
maps.

For this treatment of both the syntax and semantics of Horn and Hereditarily
Harrop logic programming, see, e.g., [1]. Some other categorical treatments
are [20, 22, 21, 14].

##  Appendix A Appendix

###  A.1 The Variable Indexing Problem

Consider the following incorrect “deduction” of

$\forall x.Qxx\supset\exists y\forall z.Qyz$

from the empty program.

$\begin{array}[]{ll}&\mbox{\tt?- }\forall x.Qxx\supset\exists y\forall
z.Qyz\\\ \stackrel{{\scriptstyle\supset}}{{\mathbf{\leadsto}}}&\forall x.Qxx\
\mbox{\tt?- }\exists y\forall z.Qyz\\\
\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}&\forall x.Qxx\
\mbox{\tt?- }\forall z.Qyz\\\
\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}&\forall x.Qxx\
\mbox{\tt?- }Qyc\\\
\stackrel{{\scriptstyle[c/y]}}{{\mathbf{\leadsto}}}&{\Box}\end{array}$

versus the following failed deduction in which a counter keeps track of
changing signatures, and the (indexed) logic variable $y_{0}$ created when
signature 0 was the ambient signature, is inhibited from unification with
constant $c_{1}$ belonging to signature 1.

$\begin{array}[]{lll}&0&\emptyset\ \mbox{\tt?- }\forall x.Qxx\supset\exists
y\forall z.Qyz\\\
\stackrel{{\scriptstyle\supset}}{{\mathbf{\leadsto}}}&0&\forall x.Qxx\
\mbox{\tt?- }\exists y\forall z.Qyz\\\
\stackrel{{\scriptstyle\exists}}{{\mathbf{\leadsto}}}&0&\forall x.Qxx\
\mbox{\tt?- }\forall z.Qy_{0}z\\\
\stackrel{{\scriptstyle\forall}}{{\mathbf{\leadsto}}}&1&\forall x.Qxx\
\mbox{\tt?- }Qy_{0}c_{1}\\\ &&FAIL\end{array}$

###  A.2 Distributive Lattices and Heyting Algebras

In the interest of making this paper more self-contained we briefly
recapitulate some elementary definitions.

######  Definition A.1.

A lattice is a partially ordered (nonempty) set with two operations $\land$
and $\lor$, the meet and join, satisfying the following axioms for all members
$a$, $b$ and $c$ of the set:

$\displaystyle a\leq a\lor b\ \ \ \ \ b\leq a\lor b$ (32) $\displaystyle
a\land b\leq a\ \ \ \ \ a\land b\leq b$ (33) $\displaystyle a\leq c\textrm{
and }b\leq c\textrm{ implies }a\lor b\leq c$ (34) $\displaystyle c\leq
a\textrm{ and }c\leq b\textrm{ implies }c\leq a\land b$ (35)

A lattice is distributive if for all members $a$, $b$ and $c$ of the partially
ordered set,

$\displaystyle a\land(b\lor c)=(a\land b)\lor(a\land c)$ (36) $\displaystyle
a\lor(b\land c)=(a\lor b)\land(a\lor c)$ (37)

The join $\bigvee S$ of an arbitrary set S, if it exists, is the least upper
bound of the set. Likewise, the meet $\bigwedge S$ would be its greatest lower
bound. A lattice is called complete if arbitrary joins and meets exist.

The meet and join operations serve to model conjunction and disjunction.
Because of the way implications in goals can be handled by _shifting_ or
_reindexing_ , namely by augmenting the program, HOHH sequents do not strictly
requite a semantic implication operator, although the interpretations will
remain (as we will show) but we need an additional operator corresponding to
implication. The following definition of a Heyting (or pseudo-Boolean) algebra
is taken from [42].

######  Definition A.2.

A Heyting algebra $\Omega$ is a lattice with a least element $\bot$ and an
operation $\rightarrow$ defined on all pairs of elements of $\Omega$ such that

$a\land b\leq c\textrm{ if and only if }a\leq b\rightarrow c$ (38)

In a complete Heyting algebra, arbitrary meets and joins exist.

In later sections, we will consider complete Heyting algebras, as well as
those with only certain parametrized infinite meets and joins corresponding to
universal and existential quantification.

It can be shown [42] that a Heyting algebra is distributive and that if
$\bigvee B$ exists then

$a\land\bigvee B=\bigvee\\{a\land b:b\in B\\},$ (39)

an identity called $\wedge\bigvee$ distributivity. It is clear from (33) and
(38) that a Heyting algebra has a top element ($a\rightarrow a$ for any $a$),
which we denote $\top$. The following characterization of the arrow connective
will be useful below. Any complete lattice satisfying $\wedge\bigvee$
distributivity (39) can be turned into a Heyting algebra by defining

$a\rightarrow b:=\bigvee\\{x:x\wedge a\leq b\\}.$ (40)

Furthermore, in any (not necessarily complete) Heyting algebra, the supremum
on the right hand side of (40) exists, and the identity holds.

The canonical example of a Heyting Algebra is the collection of open sets in
any topological space.

######  Example A.3.

The open subsets of $\mathbb{R}$ form a Heyting algebra with $\lor$ denoting
union, $\land$ the intersection (and the interior of the intersection in the
case of infinite joins), $\leq$ the subset relation, $\bot$ the empty set and
$a\rightarrow b:=\bigcup\\{w:w\cap a\subseteq b\\}$. Then $\top$ is evidently
$\mathbb{R}$ and (39) holds, but the dual statement

$a\lor\bigwedge B=\bigwedge\\{a\lor b:b\in B\\}$

need not: let $a$ be $\mathbb{R}\setminus\\{0\\}$ and $B$ be the set of
intervals $\\{(-\frac{1}{n},\frac{1}{n}):n\in\mathbb{N}\\}$. Here
$a\lor\bigwedge B=a\lor\emptyset=a$ but $\bigwedge\\{a\lor b:b\in
B\\}=\bigwedge\\{\mathbb{R}:b\in B\\}=\mathbb{R}$.

The failed dual to $\wedge\bigvee$-distributivity corresponds, in standard
semantics for first-order logic, to the truth of the formula $A\lor\forall
x.B(x)\textrm{ iff }\forall x.(A\lor B(x))$, which is not an
intuitionistically valid principle, and therefore something we do not want to
satisfy in our models. This formula corresponds in turn to Axiom $6^{\alpha}$
of Church’s classical Theory of Types [8].

###  A.3 Logic Programming Proof procedures

We remind the reader that a _uniform proof_ in ICTT is a proof satisfying the
following conditions:

  * •

only program formulas $D$ may appear as antecedents in a sequent, and only
goal formulas in the consequent, as defined in Definition 2.3,

  * •

In the $\forall_{L}$ and $\exists_{R}$ rules, the witness $t$ must be a
_positive term_ in ${\sf h}$ (${\mathcal{H}}_{2}$ in [30]),

  * •

Every sequent with a nonatomic consequent is the conclusion of a right rule.

In [34] and [33] Miller and Nadathur define proof procedures for Higher-Order
Horn and First-order Hereditarily Harrop Program-Goal pairs, and show them
sound and complete with respect to Uniform Proofs. In [33], Nadathur extends
the procedure to the higher-order (HOHH) case.

Our two formulations of a proof procedure are based on theirs but have a
somewhat different flavor, so we briefly discuss the relationship between
them. Miller and Nadathur define a _state_ to be a triple
$\langle{G,P,I}\rangle$ where $G,P$ are a program-goal pair and $I$ is a
natural number bounding the labels (our levels) of all constants and variables
appearing in $G,P$. Instead of our state _vectors_ they use a tuple
$\langle{\mbox{${\cal G}$},\mbox{${\cal C}\,$},\mbox{${\cal V}$},\mbox{${\cal
L}$},\theta}\rangle$ where ${\cal G}$ is a _set_ of states, ${\cal
C}\,$,${\cal V}$ a set of constants and variables, ${\cal L}$ a _labelling
function_ mapping $\mbox{${\cal C}\,$}\cup\mbox{${\cal V}$}$ to the set of
natural numbers (to indicate their levels). In defining proof rules as a set
of transitions between such tuples they have no need of a selection rule,
since all such transitions involve a non-deterministic choice of an active
member of ${\cal G}$.

####  A.3.1 A sketch of the equivalence of the uniform proof system with the
RES(t) system.

Now we show that our derived resolution system RES(t) is sound and complete
with respect to uniform proofs.

######  Theorem A.4.

Let ${\sf\textsf{ICTT}}^{c}$ be the sequent calculus in Figure 1, with all
constants $c$ drawn from the collection $\bigcup_{\alpha}{\cal U}_{i}(\alpha)$
defined in Section 2.4. Let $P$ be a program and $G$ a goal formula. Then

(i)

If the levels of $P$ and $G$ are less than or equal to $i\in\mathbb{N}$, and
sequent $P\vdash G$ has a uniform proof there is a successful derivation in
RES(t) of $\langle{i};{P}\mid{G}\rangle$ with computed answer the identity
substitution (with respect to the free variables in $P,G$).

(ii)

Let
${{\mathfrak{A}}}\,\mathbf{\leadsto}\,\stackrel{{\scriptstyle\theta}}{{\cdots}}\,\mathbf{\leadsto}\,{{\Box}}$
be a resolution sequence in RES(t), and $\langle{i};{P}\mid{G}\rangle$ a state
in ${\mathfrak{A}}$. Then there is a uniform proof $P\theta\vdash_{U}G\theta$.

###### Proof of (i).

Without loss of generality, all resolution sequences below will be assumed
_flat_ (Lemma 2.29). We induct on the _depth_ of a given uniform proof.
Suppose $P\vdash G$ has a uniform proof. If it is a single identity sequent,
i.e. an occurrence of rule $Ax$ in Figure 1 with conclusion
${P,A}\,\vdash\,{A}$ with $A$ atomic, then $\langle{i};{P,A}\mid{A}\rangle$
resolves to $\langle{i};{P,A}\mid{\top}\rangle$ in one step, and then to
${\Box}$. We have a similar result if the proof is a single instance of
$\top_{R}$.

If the uniform proof has depth greater than 1, we need to consider the last
rule used. If it is one of $\wedge_{R}$, $\vee_{R}$ or $\supset_{R}$ this
corresponds directly to a resolution step, and the induction hypothesis gives
us the rest of the sequence to ${\Box}$.

If the last rule used is

$\exists_{R}$:

this means there is an uniform proof of $P\vdash G[t/x]$ for some term $t$ of
an undetermined level. Consider $t^{\prime}$ obtained from $t$ by replacing
every variable or constant of level greater than $i$ with a fresh variable or
constant of level $i$ or less. Then, by routine arguments we can prove that
there is an uniform proof of $P\vdash G[t^{\prime}/x]$. By inductive
hypothesis, we have a successful derivation of
$\langle{i};{P}\mid{G[t^{\prime}/x]}\rangle$. Hence, a single instance step
suffices for our proof.

$\forall_{R}$:

this means there is an uniform proof of $P\vdash G[c/x]$ where $c$ is a fresh
constant of an undetermined level. Then, by routine arguments we can prove
that there is an uniform proof of $P\vdash G[c^{\prime}/x]$, where
$c^{\prime}$ is a consant of level $i+1$. By inductive hypothesis, we have a
successful derivation of $\langle{i+1};{P}\mid{G[c^{\prime}/x]}\rangle$.
Hence, a single generic step suffices for our proof.

We consider now the left rules, when the consequent is atomic. Only
$\wedge_{L},\supset_{L},\forall_{L}$ apply in a uniform proof, since
$\vee,\exists$ may not occur as principal connectives on the left.

$\wedge_{L}$:

Suppose the given uniform proof ends with the following rule

${P,D_{1}\wedge D_{2}}\,\vdash\,{G}{P,D_{1},D_{2}}\,\vdash\,{G}$

The induction hypothesis gives us a resolution sequence

${\langle{i};{P,D_{1},D_{2}}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$
(41)

Since $\textsf{elab}(P\cup\\{D_{1},D_{2}\\})=\textsf{elab}(P\cup\\{D_{1}\wedge
D_{2}\\})$, by the left-weakening lemma (Lemma 2.30) we have

${\langle{i};{P,D_{1}\wedge D_{2}}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$

as we wanted to show.

$\supset_{L}$:

Suppose the last step in the given uniform proof is

${P,G\supset
A}\,\vdash\,{K}\lx@proof@logical@and{P}\,\vdash\,{G}{P,A}\,\vdash\,{K}$

with $K$ atomic. By the induction hypothesis we have RES(t) sequences

${\langle{i};{P}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\
{{\Box}}\qquad{\langle{i};{P,A}\mid{K}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$

where in the two derivations, the only variables in common may be taken to be
the ones in common in the two initial states. We now consider two cases in the
second resolution sequence above. Suppose backchain against the clause $A$
never occurs in this sequence, i.e. any backchain step only makes use of
$\textsf{elab}(P)$. Then an easy induction on length shows that $A$ can be
omitted, and by left weakening, we have

${\langle{i};{P,G\supset A}\mid{K}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$

If backchain against the clause $A$ does occur using a substitution $\theta$
then the resolution sequence has the following form where the first occurrence
of such a backchain step is displayed, and where weakening left has been used
to add $G\supset A$ to the program

$\langle{i};{P,G\supset
A,A}\mid{K}\rangle\mathrel{\stackrel{{\scriptstyle\theta_{1}}}{{\leadsto\cdots\leadsto}}}{\mathfrak{A}}\otimes\langle{j};{P,Q,G\supset
A,A}\mid{K^{\prime}}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto}}}\\\
\mathrel{\stackrel{{\scriptstyle\theta}}{{\leadsto}}}{\mathfrak{A}}\theta\otimes\langle{j};{P,Q,G\supset
A,A}\mid{\top}\rangle\otimes{\mathfrak{B}}\theta\mathrel{\stackrel{{\scriptstyle\theta_{2}}}{{\leadsto\cdots\leadsto}}}{\Box}\enspace,$

where $j\geq i$, $A\theta=K^{\prime}\theta$ and $\theta_{1}\theta\theta_{2}$
is the identity when restricted to the free variables of the original state
vector. Note that from ${\mathfrak{A}}\theta\otimes\langle{j};{P,Q,G\supset
A,A}\mid{\top}\rangle\otimes{\mathfrak{B}}\theta\mathrel{\stackrel{{\scriptstyle\theta_{2}}}{{\leadsto\cdots\leadsto}}}{\Box}$
we may easily extract a derivation
${\mathfrak{A}}\theta\otimes{\mathfrak{B}}\theta\mathrel{\stackrel{{\scriptstyle\theta_{2}}}{{\leadsto\cdots\leadsto}}}{\Box}$
by removing a null step.

We now _replace the first backchain step against $A$ with a backchain against
the clause $G\supset A$_ to obtain

${\langle{i};{P,G\supset
A,A}\mid{K}\rangle}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta_{1}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\otimes\langle{j};{P,Q,G\supset
A,A}\mid{K^{\prime}}\rangle\otimes{\mathfrak{B}}}\,\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\,{{\mathfrak{A}}\theta\otimes\langle{};{P,Q\theta,G\supset
A,A}\mid{G}\rangle\otimes{\mathfrak{B}}\theta}$

Now using the first sequence in the induction hypothesis, we have
${\langle{i};{P}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}$. By
weakening left (Lemma 2.30) and level increase (Corollary 2.36) we have
${\langle{j};{P,Q\theta,G\supset A,A}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}$.
Thus we obtain a resolution sequence

${{\mathfrak{A}}\theta\otimes\langle{j};{P,Q\theta,G\supset
A,A}\mid{G}\rangle\otimes{\mathfrak{B}}\theta}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\
{{\mathfrak{A}}\theta\otimes{\mathfrak{B}}\theta}\enspace.$

Attaching ${{\mathfrak{A}}\theta\otimes{\mathfrak{B}}\theta}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle\theta_{2}}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\
{{\Box}}$ from above, we obtain ${\langle{i};{P,G\supset A,A}\mid{K}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}$.
Repeating this process for all subsequent backchains against $A$ leaves us
with a resolution sequence in which $A$ is never used (which can be
established more formally by an easy induction on the length of the resolution
sequence), and can therefore be removed.

$\forall_{L}$:

Suppose the given uniform proof ends with

${P,\forall xD}\,\vdash\,{G}{P,D[t/x]}\,\vdash\,{G}$

giving us, by the induction hypothesis,

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

If no backchain step occurs using clauses in $\textsf{elab}(D[t/x])$ in this
proof, then it is straightforward to show, by induction on the length of the
resolution sequence, that

${\langle{i};{P,\forall xD}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$

Otherwise, suppose the first backchain step using a clause in
$\textsf{elab}(D[t/x])$, say $\forall\vec{z}(H\supset K^{\prime})$, has the
form

${\mathfrak{A}}\otimes{\langle{j};{P,D[t/x]}\mid{K}\rangle\otimes{\mathfrak{B}}}\
\stackrel{{\scriptstyle\theta}}{{\mathbf{\leadsto}}}\
{{\mathfrak{A}}\theta\otimes\langle{j};{P,D[t/x]}\mid{H^{\prime}}\rangle\otimes{\mathfrak{B}}\theta}$

with $\sigma$ the standardizing apart substitution from bound variables into
fresh variables, $\theta(\sigma(H))=H^{\prime}$ and
$\theta(\sigma(K^{\prime}))=K$ ($\theta$ the identity on the free variables of
$P,D[t/x],K$ since we are assuming the derivation to be flat). By Lemma 2.12
there is a clause $\forall
x\forall\vec{z}(\hat{H}\supset\hat{K})\in\textsf{elab}(\forall xD)$ with
$\hat{H}[t/x]=H$ and $\hat{K}[t/x]=K^{\prime}$. For a fresh variable $w$, let
the substitutions $\theta^{\prime},\sigma^{\prime}$ be defined by
$\sigma^{\prime}(x)=w$ and $\theta^{\prime}(w)=t$ and otherwise identical to
$\sigma,\theta$. Then the following is a legal backchain step

${\mathfrak{A}}\otimes{\langle{j};{P,\forall
xD}\mid{K}\rangle\otimes{\mathfrak{B}}}\
\stackrel{{\scriptstyle\theta^{\prime}}}{{\mathbf{\leadsto}}}\
{{\mathfrak{A}}\theta\otimes\langle{j};{P,\forall
xD}\mid{\hat{H}\sigma^{\prime}\theta^{\prime}}\rangle\otimes{\mathfrak{B}}\theta}$

with $\hat{H}\sigma^{\prime}\theta^{\prime}=H^{\prime}$. Continuing this way
with every relevant backchain step we obtain a successful resolution sequence
of the form

${\langle{i};{P,\forall xD}\mid{G}\rangle}\
\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\,\stackrel{{\scriptstyle
id}}{{\cdots}}\,\stackrel{{\scriptstyle}}{{\mathbf{\leadsto}}}\ {{\Box}}.$

∎

###### Proof of (ii).

Part (ii) of this theorem is established, in a different setting, in the proof
of Theorem 13 of [33], which shows that given a closed program formula $P$ and
a goal $G$, if there is a derivation (using the proof procedure of that paper)
of $G$ relative to $P$, there is a substitution $\theta$ (the associated
answer substitution) such that for any instance $G^{\prime}$ of $G\theta$
there is an _intuitionistic_ proof of $P\vdash G^{\prime}$. By [30] the
existence of an intuitionistic proof for a program-goal pair implies the
existence of a uniform one. Our claim is weaker, since we allow arbitrary
unifiers and arbitrary instantiations of existentially quantified variables. A
direct proof is given here to show that our variant proof system RES(t) is
also sound with respect to uniform proofs.

We induct on the length of the given RES(t) derivation. The base cases are
easy and left to the reader. We also note that if we first assume
$\langle{i};{P}\mid{G}\rangle$ in ${\mathfrak{A}}$ is _not_ the selected goal,
the sequence looks like this:

${\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G}\rangle\otimes{\mathfrak{A}}_{2}\
\stackrel{{\scriptstyle{\theta_{0}}}}{{\mathbf{\leadsto}\
}}{\mathfrak{A}}_{1}\theta_{0}\otimes\langle{i};{P\theta_{0}}\mid{G\theta_{0}}\rangle\otimes{\mathfrak{A}}_{2}\theta_{0}\
{\mathbf{\leadsto}}\stackrel{{\scriptstyle{\theta_{1}}}}{{\cdots}}\mathbf{\leadsto}\
{\Box}$

possibly with identity substitution $\theta_{0}$. By induction hypothesis,
letting $\theta=\theta_{0}\theta_{1}$ we have $P\theta\vdash_{U}G\theta$.

Suppose the claim holds for sequences of length less than $\ell$ and consider
all possible first steps where $\langle{i};{P}\mid{G}\rangle$ is the selected
goal.

null

Assume the resolution sequence has the form

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

We have $P\vdash_{U}\top$ by the $\top_{R}$ rule in ICTT.

true

Suppose the resolution sequence has the following form:

${\mathfrak{A}}\otimes\langle{i};{P}\mid{A}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\varphi}}{{\leadsto}}}{\mathfrak{A}}\varphi\otimes\langle{i};{P\varphi}\mid{\top}\rangle\otimes{\mathfrak{B}}\varphi\mathrel{\stackrel{{\scriptstyle\eta}}{{\leadsto\cdots\leadsto}}}{\Box}$

where $A\varphi=\top$ and $\theta$ is $\varphi\eta$ restricted to the free
variables in the first state vector. Inductive hypothesis immediately gives an
uniform proof of $P\varphi\eta\vdash\top\eta$, that is
$P\theta\vdash_{U}\top$.

and

is a straightforward case: if the resolution sequence is

${\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G_{1}\wedge
G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\
\stackrel{{\scriptstyle{\wedge}}}{{\mathbf{\leadsto}\
}}{\mathfrak{A}}_{1}\otimes\langle{i};{P}\mid{G_{1}}\rangle\otimes\langle{i};{P}\mid{G_{2}}\rangle\otimes{\mathfrak{A}}_{2}\
{\mathbf{\leadsto}}\stackrel{{\scriptstyle{\varphi}}}{{\cdots}}\mathbf{\leadsto}\
{\Box}$

the induction hypothesis gives $P\varphi\vdash_{U}G_{1}\varphi$ and
$P\varphi\vdash_{U}G_{2}\varphi$, so by $\wedge$-right
$P\varphi\vdash_{U}(G_{1}\wedge G_{2})\varphi$

backchain

Suppose the resolution sequence has the following form:

${\mathfrak{A}}\otimes\langle{i};{P}\mid{A^{\prime}}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\varphi}}{{\leadsto}}}{\mathfrak{A}}\varphi\otimes\langle{i};{P\varphi}\mid{G\varphi}\rangle\otimes{\mathfrak{B}}\varphi\mathrel{\stackrel{{\scriptstyle\eta}}{{\leadsto\cdots\leadsto}}}{\Box}$

where $\forall\vec{x}(G\supset A_{r})\in\textsf{elab}(P)$, $\delta$ is the
renaming-apart substitution and $A^{\prime}\varphi=A_{r}\delta\varphi$. By the
induction hypothesis and the identity rule we have

$P\varphi\eta\vdash_{U}G\varphi\eta\mbox{ and
}P\varphi\eta,A_{r}\delta\varphi\eta\vdash_{U}A^{\prime}\varphi\eta$

so by $\supset$-left

$P\varphi\eta,G\varphi\eta\supset
A_{r}\delta\varphi\eta\vdash_{U}A^{\prime}\varphi\eta.$

By the $U$-contraction lemma, we have
$P\varphi\eta\vdash_{U}A^{\prime}\varphi\eta$ hence
$P\theta\vdash_{U}A^{\prime}\theta$.

instance

Suppose the resolution sequence has the following form

${\mathfrak{A}}\otimes\langle{i};{P}\mid{\exists
xG}\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\eta}}{{\leadsto\cdots\leadsto}}}{\Box}$

with $t$ in ${\cal U}_{i}$. By the induction hypothesis
$P\eta\vdash_{U}G[t/x]\eta$, hence $P\eta\vdash_{U}(G\eta)[t\eta/x]$. By
$\exists_{R}$ we have $P\eta\vdash_{U}\exists x(G\eta)$ so
$P\eta\vdash_{U}(\exists xG)\eta$.

augment

Easy application of $\supset_{R}$, left to the reader.

generic

Suppose the resolution sequence has the following form:

${\mathfrak{A}}\otimes\langle{i};{P}\mid{\forall
xG}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\forall}}{{\leadsto}}}{\mathfrak{A}}\otimes\langle{i+1};{P}\mid{G[c_{i+1}/x]}\rangle\otimes{\mathfrak{B}}\mathrel{\stackrel{{\scriptstyle\eta}}{{\leadsto\cdots\leadsto}}}{\Box}$

By the induction hypothesis, there is a proof of
$P\eta\vdash_{U}G[c_{i+1}/x]\eta$ where $c_{i+1}$ is fresh. Since $\eta$ is
level preserving and $G$ is of level $i$ or less, the constant $c_{i+1}$
cannot appear in $G\eta$. Therefore, a single application of the $\forall_{R}$
rule gives $P\vdash_{U}\forall xG$. ∎

## References