HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories

TL;DR

This paper introduces HoCHC, a resolution proof system for higher-order constrained Horn clauses that is sound, complete, and invariant under semantics, enabling transfer of decidability results from first-order logic to higher-order logic.

Contribution

It presents a simple, refutationally complete resolution system for higher-order logic modulo theories, with proofs of soundness, completeness, and properties like compactness and semi-decidability.

Findings

Proves HoCHC's soundness and refutational completeness.

Establishes compactness theorem and semi-decidability for HoCHC.

Demonstrates transfer of decidability results from first-order logic to higher-order logic.

Abstract

We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) - a system of higher-order logic modulo theories - and prove its soundness and refutational completeness w.r.t. the standard semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. Moreover a variant of the well-known translation from higher-order to 1st-order logic is shown to be sound and complete for HoCHC in standard semantics. We illustrate how to transfer decidability results for (fragments of) 1st-order logic modulo theories to our higher-order setting, using as example the Bernays-Schonfinkel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.

Equations

$$\begin{array}[]{l}\mathsf{let}\;\mathit{add}\,x\,y=x+y\\ \mathsf{letrec}\;\mathit{iter}\,f\,s\,n=\mathsf{if}\;{n\leq 0}\;\mathsf{then}\ {s}\ \mathsf{else}\;f\,n\,(\mathit{iter}\,f\,s\,(n-1))\\ \qquad\mathsf{in}\;\lambda n.\mathsf{assert}\;\big{(}n\geq 1\,\to\,(\mathit{iter}\,\mathit{add}\,n\,n>n+n)\big{)}\end{array}$$

$$\begin{array}[]{l}\forall x,y,z\,.\,\big{(}z=x+y\to\operatorname{Add}\,x\,y\,z\big{)}\\ \forall f,s,n,x\,.\,\big{(}n\leq 0\wedge s=x\to\operatorname{Iter}\,f\,s\,n\,x\big{)}\\ \forall f,s,n,x\,.\,\big{(}n>0\wedge\exists y\,.\,(\operatorname{Iter}\,f\,s\,(n-1)\,y\wedge f\,n\,y\,x)\\ \qquad\qquad\qquad\qquad\to\operatorname{Iter}\,f\,s\,n\,x\big{)}\\ \forall n,x\,.\,\big{(}n\geq 1\wedge\operatorname{Iter}\,\operatorname{Add}\,n\,n\,x\;\to\;x>n+n\big{)}\end{array}$$

$$\Delta ⊢x:\Delta (x)x\in \mathrm{dom}(\Delta )\Delta ⊢c:\sigma c:\sigma \in \Sigma \Delta ⊢M_1{M}_2:{\sigma }_2\text{lx@proof@logical@and}\Delta ⊢M_1:{\sigma }_1\to {\sigma }_2\Delta ⊢M_2:{\sigma }_1\Delta ⊢\lambda x.M:\Delta (x)\to \rho \Delta ⊢M:\rho$$

$$\Delta ⊢\circ :o\to o\to o\circ \in \{\wedge ,\vee \}\Delta ⊢\neg M:o\Delta ⊢M:o\Delta ⊢{\exists }_{\tau }:(\tau \to o)\to o$$

$$\begin{array}[]{lrclr}\hbox{\em Argument type}&\tau&::=&\iota\mid\rho\\ \hbox{\em Relational type}&\rho&::=&o\mid\tau\to\rho\\ \hbox{\em 1st-order type}&\sigma_{\operatorname{{FO}}}&::=&\iota\mid\iota\to o\mid\iota\to\sigma_{\operatorname{{FO}}}\\ \hbox{\em Type}&\sigma&::=&\rho\mid\sigma_{\operatorname{{FO}}},\end{array}$$

$$M::=x\mid c\mid \neg \mid \wedge \mid \vee \mid {\exists }_{\tau }\mid MM\mid \lambda x.M$$

$$\mathrm{and}(b_1)(b_2)$$

$${\mathrm{exists}}_{\tau }(r)$$

$$\mathcal{S}[[\tau \to \sigma ]]$$

$$\mathcal{M}[[\tau \to \sigma ]]$$

$$\mathcal{C}[[\tau \to \sigma ]]$$

$$\mathcal{A}[[x]](\alpha )$$

$$\mathcal{A}[[\wedge ]](\alpha )$$

$$\mathcal{A}[[{\exists }_{\tau }]](\alpha )$$

$$\mathcal{A}[[M_1{M}_2]](\alpha )$$

$$\mathcal{A}[[\lambda x.M]](\alpha )$$

$$\mathcal{A}[[c]](\alpha )$$

$$\mathcal{A}[[\vee ]](\alpha )$$

$$\mathcal{A}[[\neg M]](\alpha )$$

$$\neg (z=x+y)\vee \mathrm{Add}xyz$$

$$\neg (n\le 0)\vee \neg (s=x)\vee \mathrm{Iter}fsnx$$

$$\neg (n>0)\vee \neg \mathrm{Iter}fs(n-1)y\vee \neg (fnyx)\vee \mathrm{Iter}fsnx$$

$$\neg (n\ge 1)\vee \neg \mathrm{Iter}\mathrm{Add}nnx\vee \neg (x\le n+n)$$

$$\begin{array}[]{l}\neg(z=x+y)\,\lor\,\operatorname{Add}\,x\,y\,z\\ \neg\big{(}(n\leq 0\;\land\;s=x)\;\lor\\ \quad\;\;(\exists y\ldotp n>0\land\operatorname{Iter}\,f\,s\,(n-1)\,y\land f\,n\,y\,x)\big{)}\lor\operatorname{Iter}\,f\,s\,n\,x.\end{array}$$

$$\neg x_{R}U$$

$$a_{\beta +1}$$

$$a_{\gamma }$$

$$a_F$$

$$\begin{array}[]{lr}n\precsim_{\iota}n^{\prime}\;\coloneqq\;n=n^{\prime}&(n,n^{\prime}\in{\mathcal{F}}\llbracket\iota\rrbracket)\\ b\precsim_{o}b^{\prime}\;\coloneqq\;b\leq b^{\prime}&(b,b^{\prime}\in{\mathcal{F}}\llbracket o\rrbracket)\\ r\precsim_{\tau\to\sigma}r^{\prime}\;\coloneqq\;\forall s,s^{\prime}\in{\mathcal{F}}\llbracket\tau\rrbracket\ldotp s\precsim_{\tau}s^{\prime}\rightarrow{}\\ \qquad\qquad\qquad\qquad r(s)\precsim_{\sigma}r^{\prime}(s^{\prime})&(r,r^{\prime}\in{\mathcal{F}}\llbracket\tau\to\sigma\rrbracket)\end{array}$$

$${\mathcal{A}}_{\mathrm{LIA}},\alpha \models$$

$$(n=y)\wedge (x=n+y)\wedge (x\le n+n).$$

$$\neg (x_R=0\vee R(x_R-1))\vee R{x}_R\neg (x_{U}R)\vee U{x}_U$$

$$\begin{array}[]{lr}b\precsim_{o}b^{\prime}\;\coloneqq\;b\leq b^{\prime}&(b,b^{\prime}\in{\mathcal{F}}\llbracket o\rrbracket)\\ n\precsim_{\iota}n^{\prime}\;\coloneqq\;n=n^{\prime}&(n,n^{\prime}\in{\mathcal{F}}\llbracket\iota\rrbracket)\\ r\precsim_{\tau\to\sigma}r^{\prime}\;\coloneqq\;\forall s\in{\mathcal{F}}\llbracket\tau\rrbracket,\mathfrak{S}^{\prime}\in\operatorname{dir}_{\precsim_{\tau}}(s)\ldotp\\ \qquad\qquad\qquad r(s)\precsim_{\sigma}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime}(s^{\prime})&(r,r^{\prime}\in{\mathcal{F}}\llbracket\tau\to\sigma\rrbracket)\end{array}$$

$$\mathcal{B}[[M]](\alpha )\precsim \underset{{\mathcal{B}}^{\prime }\in {\mathfrak{B}}^{\prime },{\alpha }^{\prime }\in {\mathfrak{a}}^{\prime }}{⨆}{\mathcal{B}}^{\prime }[[M]]({\alpha }^{\prime }).$$

$$\alpha ⊳x\overline{M}\alpha ⊳\phi \mathcal{A},\alpha \models \phi \alpha ⊳\exists x.M\text{lx@proof@logical@and}r\in \mathcal{F}[[\Delta (x)]]\alpha [x\mapsto r]⊳M$$

$$\alpha ⊳M_1\vee M_2\text{lx@proof@logical@and}i\in \{1,2\}\alpha ⊳M_i\alpha ⊳M_1\wedge M_2\text{lx@proof@logical@and}\alpha ⊳M_1\alpha ⊳M_2$$

$$\mu (E)$$

$$\lfloor D_1\rfloor$$

$$\lfloor D_2\rfloor$$

Full text

I Introduction

Cathcart Burn et al. [1] recently advocated an automatic, programming-language independent approach to verify safety properties of higher-order programs by framing them as solvability problems for systems of higher-order constraints. These systems consist of Horn clauses of higher-order logic, containing constraints expressed in some suitable background theory. Consider the functional program:

[TABLE]

Thus $(\mathit{iter}\,\mathit{add}\,n\,n)$ computes the value $n+\sum_{i=1}^{n}i$.

To verify that the program is safe (i.e. the assertion is never violated), it suffices to find overapproximations of the input-output-graph (i.e. invariants) of the functions that imply the required property. The idea then is to express the problem of finding such a program invariant, logically, as a satisfiability problem for the following higher-order constrained system:

Example 1** (Invariant as system of higher-order constraints).**

[TABLE]

The above are Horn clauses of higher-order logic, obtained by transformation from the preceding program; $\operatorname{Add}:\iota\to\iota\to\iota\to o$ and $\operatorname{Iter}:(\iota\to\iota\to\iota\to o)\to\iota\to\iota\to\iota\to o$ are higher-order relations, and the binary predicates $({\leq},{>},\cdots)$ are formulas of the background theory, Linear Integer Arithmetic (LIA).

*Since the the assertion in the program is violated for $n=1$, the clauses are unsatisfiable. *

Is higher-order logic modulo theories a sensible algorithmic approach to verification? Is it well-founded?

To set the scene, recall that 1st-order logic is semi-decidable: 1st-order validities111Define $\mathbf{V}^{n}(P)$ to be the set of valid sentences of $n$th-order logic with 2-place predicate $P$. Then $\mathbf{V}^{1}({=})$ is recursively enumerable are recursively enumerable; moreover if a formula is unsatisfiable then it is provable by resolution [2, 3]. By contrast, higher-order logic in standard semantics is wildly undecidable. E.g. the set11footnotemark: 1 $\mathbf{V}^{2}(=)$ of valid sentences of the 2nd-order language of equality is not even analytical [4].

This does not necessarily spell doom for the higher-order logic approach. One could consider higher-order logic in Henkin semantics [5], which is, after all, “nothing but many-sorted 1st-order logic with comprehension axioms” [4] (see also [6, 7]). However, because the standard semantics is natural and comparatively simple, it seems to be the semantics of choice in program verification (e.g. monadic 2nd-order logic in model checking, and HOL theorem prover [8, 9] in automated deduction) and in program specification.

In this paper, we study the algorithmic, model-theoretic and semantical properties of higher-order Horn clauses with a 1st-order background theory.

A Complete Resolution Proof System for HoCHC

The main technical contribution of this paper is the design of a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) where the background theory has a unique model [1], and its refutational completeness proof with respect to the standard semantics (Sec. IV). The proof system and its refutational completeness proof are generalised in Sec. VI to arbitrary compact background theories, which may have more than one model.

The completeness proof hinges on a novel model-theoretic insight: we prove that the immediate consequence operator is quasi-continuous, although it is not continuous in the standard Scott sense. Thus, the immediate consequence operator gives rise to a syntactic explanation for unsatisfiability. Moreover, we adapt the proof of the standardisation theorem of the $\lambda$-calculus in [10] to argue that this explanation can be captured by the rules of the resolution proof system.

Canonical Model Property

As shown in [1], a disadvantage of the standard semantics is failure of the least model property (w.r.t. the pointwise ordering). However, we prove in Sec. III that the immediate consequence operator is “sufficiently” monotone and hence (by an extension of the Knaster-Tarski theorem) gives rise to a model of all satisfiable instances.

Compactness Theorem and Semi-decidability of HoCHC

A well-known feature of higher-order logic in standard semantics is failure of the compactness theorem. As a consequence of HoCHC’s refutational completeness, it follows that the compactness theorem does hold for HoCHC (in standard semantics): for every unsatisfiable set $\Gamma$ of HoCHCs, there is a finite subset $\Gamma^{\prime}\subseteq\Gamma$ which is unsatisfiable.

Moreover, if the consistency of conjunctions of atoms in the background theory is semi-decidable, so is HoCHC unsatisfiability. Crucially, this underpins the practicality of the HoCHC-based approach to program verification.

Semantic Invariance

The soundness and completeness of our resolution proof system has another pleasing corollary: satisfiability of HoCHC does not depend on the choice of semantics222within the reasonable bounds formalised by (complete) frames (Sec. V). In particular, this constitutes an alternative proof of the equivalence of standard, monotone and continuous semantics for HoCHCs, without exhibiting explicit translations between semantics. Moreover, this demonstrates that, in contrast to (full) higher-order logic, satisfiability of HoCHCs with respect to standard semantics on the one hand, and to Henkin semantics on the other, coincide.

Semantic invariance is an important advantage for program verification. It follows that one can use (the simpler and more intuitive) standard semantics for specification, but use Henkin semantics for the development of refined proof systems that are complete [11, 12, 13, 14], and use continuous semantics (which enjoys a richer structure) to construct solution methods and in static analysis.

Complete 1st-order Translation

As suggested by the equivalence of standard and Henkin semantics, we show that there is a variant of the standard translation of higher-order logic into 1st-order logic which is sound and complete also for standard semantics, when restricted to HoCHC (Sec. VII).

Decidable Fragments of HoCHC

Satisfiability of finite sets of HoCHCs is trivially decidable for background theories with finite domains. In Sec. VIII, we identify a fragment333Another one (higher-order Datalog) is presented in Sec. -F1. of HoCHC (the Bernays-Schönfinkel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic) with a decidable satisfiability problem by showing equi-satisfiability to clauses w.r.t. a finite number of such background theories.

Outline

We begin with some key definitions in Sec. II. Then we show that even standard semantics satisfies a canonical model property (Sec. III). In Sec. IV, we present the resolution proof system for HoCHC and prove its completeness. In Sec. V we show HoCHC’s semantic invariance and in Sec. VI we generalise the refutational completeness proof to compact background theories, which may have more than one model. In Sec. VII we present a 1st-order translation of higher-order logic and prove it complete when restricted to HoCHC. In Sec. VIII we exhibit decidable fragments of HoCHC. Finally, we discuss related work in Sec. IX, and conclude in Sec. X.

II Technical Preliminaries

This section introduces the syntax and semantics of a restricted form of higher-order logic (Sec. II-A), higher-order constrained Horn clauses (Sec. II-B) and programs (Sec. II-C).

II-A Relational Higher-order Logic

II-A1 Syntax

For a fixed set $\mathfrak{I}$ (intuitively the types of individuals), the set of argument types, relational types, 1st-order types and types (generated by $\mathfrak{I}$) are mutual recursively defined by

[TABLE]

where $\iota\in\mathfrak{I}$. We sometimes abbreviate the (1st-order) type $\underbrace{\iota\to\cdots\to\iota}_{n}\to\iota$ to $\iota^{n}\to\iota$ (similarly for $\iota^{n}\to o$). For types $\tau_{1}\to\cdots\to\tau_{n}\to\sigma$ we also write $\overline{\tau}\to\sigma$. Intuitively, $o$ is the type of the truth values (or Booleans). Besides, $\sigma_{\operatorname{{FO}}}$ contains all (1st-order) types of the form $\iota^{n}\to\iota$ or $\iota^{n}\to o$, i.e. all arguments are of type $\iota$. Moreover, each relational type has the form $\overline{\tau}\to o$.

A type environment (typically $\Delta$) is a function mapping variables (typically denoted by $x,y,z$ etc.) to argument types; for $x\in\operatorname{dom}(\Delta)$, we write $x:\tau\in\Delta$ to mean $\Delta(x)=\tau$. A signature is a set of distinct typed symbols $c:\sigma$, where $c\not\in\operatorname{dom}(\Delta)$ and $c$ is not one of the logical symbols $\neg$, $\land$, $\lor$ and $\exists_{\tau}$ (for argument types $\tau$, which we omit frequently). It is 1st-order if for each $c:\sigma\in\Sigma$, $\sigma$ is 1st-order. We often write $c\in\Sigma$ if $c:\sigma\in\Sigma$ for some $\sigma$.

The set of $\Sigma$-pre-terms is given by

[TABLE]

where $c\in\Sigma$. Following the usual conventions we assume that application associates to the left and the scope of abstractions extend as far to the right as possible. We also write $M\,\overline{N}$ and $\lambda\overline{x}\ldotp M^{\prime}$ for $M\,N_{1}\cdots N_{n}$ and $\lambda x_{1}\ldotp\cdots\lambda x_{n}\ldotp M^{\prime}$, respectively, assuming implicitly that $M$ is not an application. Besides, we abbreviate $\exists_{\tau}(\lambda x\ldotp M)$ as $\exists x\ldotp M$. Moreover, we identify terms up to $\alpha$-equivalence and adopt Barendregt’s variable convention [15].

The typing judgement $\Delta\vdash M:\sigma$ is defined in Fig. 1. We say that $M$ is $\Sigma$-term if $\Delta\vdash M:\sigma$ for some $\sigma$ and it is a $\Sigma$-formula if $\sigma=o$. A $\Sigma$-formula is a 1st-order $\Sigma$-formula if its construction is restricted to symbols $c:\sigma_{\operatorname{{FO}}}\in\Sigma$ and variables ${x:\iota}\in\Delta$, and uses no $\lambda$-abstraction. Finally, for a $\Sigma$-term $M$, $\operatorname{fv}(M)$ is the set of free variables, and $M$ is a closed $\Sigma$-term if $\operatorname{fv}(M)=\emptyset$.

Remark 2**.**

*It follows from the definitions that

(i) each term $\Delta\vdash M:\iota^{n}\to\iota$ can only contain variables of type $\iota$ and constants of non-relational 1st-order type, and contains neither $\lambda$-abstractions nor logical symbols (a similar approach is adopted in [16]);

(ii) $\neg$can only occur in a term if applied to a formula (and not in pre-terms of the form $R\,\neg$).

The following kind of terms is particularly significant:

Definition 3**.**

*A $\Sigma$-term is positive existential if the logical constant “$\neg$” is not a subterm. *

For $\Sigma$-terms $M,N_{1},\ldots,N_{n}$ and variables $x_{1},\ldots,x_{n}$ satisfying $\Delta\vdash N_{i}:\Delta(x_{i})$, the (simultaneous) substitution $M[N_{1}/x_{1},\ldots,N_{n}/x_{n}]$ is defined in the standard way.

II-A2 Semantics

There are two classic semantics for higher-order logic: standard and Henkin semantics [5]. Whereas in standard semantics the interpretation of higher types is uniquely determined by the domains of individuals (quantifiers range over all set-theoretic functions of the appropriate type), it can be stipulated quite liberally in Henkin semantics.

Formally, a pre-frame $\mathcal{F}$ assigns to each type $\sigma$ a non-empty set ${\mathcal{F}}\llbracket\sigma\rrbracket$ such that

1. (i)

${\mathcal{F}}\llbracket o\rrbracket\coloneqq\mathbb{B}\coloneqq\{0,1\}$ and for each type $\sigma_{1}\to\sigma_{2}$, ${\mathcal{F}}\llbracket\sigma_{1}\to\sigma_{2}\rrbracket\subseteq[{\mathcal{F}}\llbracket\sigma_{1}\rrbracket\to{\mathcal{F}}\llbracket\sigma_{2}\rrbracket]$ 2. (ii)

$\operatorname{and},\operatorname{or}\in{\mathcal{F}}\llbracket o\to o\to o\rrbracket$ 3. (iii)

$\exists_{\tau}\in{\mathcal{F}}\llbracket(\tau\to o)\to o\rrbracket$ for each argument type $\tau$

where $[{\mathcal{F}}\llbracket\sigma_{1}\rrbracket\to{\mathcal{F}}\llbracket\sigma_{2}\rrbracket]$ is the set of functions ${\mathcal{F}}\llbracket\sigma_{1}\rrbracket\to{\mathcal{F}}\llbracket\sigma_{2}\rrbracket$ and

[TABLE]

Example 4** (Pre-frames).**

For every $\iota\in\mathfrak{I}$, we fix an arbitrary non-empty set $D_{\iota}$. We define $\mathcal{S}$, $\mathcal{M}$ and $\mathcal{C}$, which we call the standard, monotone and continuous frame, respectively, recursively by ${\mathcal{S}}\llbracket o\rrbracket\coloneqq{\mathcal{M}}\llbracket o\rrbracket\coloneqq{\mathcal{C}}\llbracket o\rrbracket\coloneqq\mathbb{B}$; ${\mathcal{S}}\llbracket\iota\rrbracket\coloneqq{\mathcal{M}}\llbracket\iota\rrbracket\coloneqq{\mathcal{C}}\llbracket\iota\rrbracket\coloneqq D_{\iota}$ for $\iota\in\mathfrak{I}$; and

[TABLE]

where $[P\xrightarrow{m}P^{\prime}]$ ($[P\xrightarrow{c}P^{\prime}]$) is the set of monotone (continuous) functions from the posets $P$ to $P^{\prime}$ (cf. [17]).

Let $\Sigma$ be a signature and $\mathcal{F}$ be a pre-frame. A $(\Sigma,\mathcal{F})$-structure $\mathcal{A}$ assigns to each $c:\sigma\in\Sigma$ an element $c^{\mathcal{A}}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ and we set ${\mathcal{A}}\llbracket\sigma\rrbracket\coloneqq{\mathcal{F}}\llbracket\sigma\rrbracket$ for types $\sigma$. A $(\Delta,\mathcal{F})$-valuation $\alpha$ is a function such that for every $x:\tau\in\Delta$, $\alpha(x)\in{\mathcal{F}}\llbracket\tau\rrbracket$. For a $(\Delta,\mathcal{F})$-valuation $\alpha$, variable $x$ and $r\in{\mathcal{F}}\llbracket\Delta(x)\rrbracket$, $\alpha[x\mapsto r]$ is defined in the usual way.

The denotation ${\mathcal{A}}\llbracket M\rrbracket(\alpha)$ of a term $M$ with respect to $\mathcal{A}$ and $\alpha$ is defined recursively by

[TABLE]

[TABLE]

(assuming $\Delta\vdash M:\rho$ in the last case), where $\left[r\right]_{\sigma}=r$ if $r\in{\mathcal{A}}\llbracket\sigma\rrbracket$ and otherwise $\left[r\right]_{\sigma}\in{\mathcal{A}}\llbracket\sigma\rrbracket$ is arbitrary. Thus, for each term $\Delta\vdash M:\sigma$, ${\mathcal{A}}\llbracket M\rrbracket(\alpha)\in{\mathcal{A}}\llbracket\sigma\rrbracket$.

Being independent of valuations, the denotation of closed terms $M$ is abbreviated as ${\mathcal{A}}\llbracket M\rrbracket$. Besides, for $\Sigma$-formulas $F$, we write $\mathcal{A},\alpha\models F$ if ${\mathcal{A}}\llbracket F\rrbracket(\alpha)=1$, and $\mathcal{A}\models F$ if for all $\alpha^{\prime}$, $\mathcal{A},\alpha^{\prime}\models F$. We extend $\models$ in the usual way to sets of formulas.

A frame is a pre-frame $\mathcal{F}$ that satisfies the

Comprehension Axiom: for each signature $\Sigma$, type environment $\Delta$, $(\Sigma,\mathcal{F})$-structure $\mathcal{A}$, $(\Delta,\mathcal{F})$-valuation $\alpha$, positive existential $\Sigma$-term $\lambda x\ldotp M$, and $r\in{\mathcal{A}}\llbracket\Delta(x)\rrbracket$, ${\mathcal{A}}\llbracket\lambda x\ldotp M\rrbracket(\alpha)(r)={\mathcal{A}}\llbracket M\rrbracket(\alpha[x\mapsto r])$.

Our comprehension axiom ensures that positive existential terms are interpreted in the expected way; it is non-standard in that it is restricted to positive existential formulas.

As a consequence, if $\mathcal{F}$ is a frame then for every relational type $\overline{\tau}\to o$, $\top_{\overline{\tau}\to o}\in{\mathcal{F}}\llbracket\overline{\tau}\to o\rrbracket$, where $1=:\top_{\overline{\tau}\to o}(\overline{r})={\mathcal{A}}\llbracket\lambda\overline{x}\ldotp y\rrbracket(\alpha[y\mapsto 1])(\overline{r})$.

Complete Frames

For types $\sigma$, let ${\sqsubseteq_{\sigma}}\subseteq{\mathcal{F}}\llbracket\sigma\rrbracket\times{\mathcal{F}}\llbracket\sigma\rrbracket$ be the usual partial order defined pointwise for higher types, which is the discrete order on ${\mathcal{F}}\llbracket\iota\rrbracket$ and the “less than or equal” relation on ${\mathcal{F}}\llbracket o\rrbracket$.

For relational types $\rho$ and $\mathfrak{R}\subseteq{\mathcal{F}}\llbracket\rho\rrbracket$, the least upper bound $\bigsqcup_{\rho}\mathfrak{R}$ is defined pointwise, by recursion on $\rho$. In particular, $\bigsqcup_{\overline{\tau}\to o}\emptyset=\bot_{\overline{\tau}\to o}$, where $\bot_{\overline{\tau}\to o}(\overline{r})\coloneqq 0$. For a singleton set $\{f\}\subseteq{\mathcal{F}}\llbracket\iota^{n}\to\iota\rrbracket$ we define $\bigsqcup_{\iota^{n}\to\iota}\{f\}\coloneqq f$. Throughout the paper, we omit type subscripts to reduce clutter because they can be inferred.

A (pre-)frame $\mathcal{F}$ is complete if for every relational $\rho$ and $\mathfrak{R}\subseteq{\mathcal{F}}\llbracket\rho\rrbracket$, $\bigsqcup\mathfrak{R}\in{\mathcal{F}}\llbracket\rho\rrbracket$, i.e. each ${\mathcal{F}}\llbracket\rho\rrbracket$ is a complete lattice ordered by $\sqsubseteq_{\rho}$ with least upper bounds $\bigsqcup_{\rho}$.

Example 5** (complete frames).**

$\mathcal{S}$* is trivially a complete frame. It is not difficult to prove that $\mathcal{M}$ and $\mathcal{C}$ are also complete frames (Sec. -A3).*

1st-order Structures

Let $\Sigma$ be a 1st-order signature. A 1st-order $\Sigma$-structure is a $(\Sigma,\mathcal{S})$-structure. Note that by taking standard frames this coincides with the standard definition in a purely 1st-order setting (cf. e.g. [18]).

Example 6**.**

In the examples we will primarily be concerned with the signature of Linear Integer Arithmetic444with the usual types $0,1:\iota$; ${+},{-}:\iota\to\iota\to\iota$ and $\triangleleft:\iota\to\iota\to o$ for $\triangleleft\;\in\{<,\leq,=,\neq,\geq,>\}$; and we use the common abbreviation $n$ for $\underbrace{1+\cdots+1}_{n}$, where $1\leq n\in\mathbb{N}$ $\Sigma_{\operatorname{LIA}}\coloneqq\{0,1,+,-,<,\leq,=,\neq,\geq,>\}$ and its standard model $\mathcal{A}_{\operatorname{LIA}}$.

II-B Higher-order Constrained Horn Clauses

Assumption**.**

Henceforth, we fix a 1st-order signature $\Sigma$ over a single type of individuals $\iota$ and a 1st-order $\Sigma$-structure $\mathcal{A}$.

Moreover, we fix a signature $\Sigma^{\prime}$ extending $\Sigma$ with (only) symbols of relational type, and a type environment $\Delta$ such that $\Delta^{-1}(\tau)$ is infinite for each argument type $\tau$.

Intuitively, $\Sigma$ and $\mathcal{A}$ correspond to the language and interpretation of the background theory, e.g. $\Sigma_{\operatorname{LIA}}$ together with its standard model $\mathcal{A}_{\operatorname{LIA}}$. In particular, we first focus on background theories with a single model. In Sec. VI we extend our results to a more general setting.

We are interested in whether 1st-order structures can be expanded to larger (higher-order) signatures. This is made precise by the following:

Definition 7**.**

1. (i)

A frame $\mathcal{F}$ expands $\mathcal{A}$ if ${\mathcal{F}}\llbracket\iota\rrbracket={\mathcal{A}}\llbracket\iota\rrbracket$ and $c^{\mathcal{A}}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ for all $c:\sigma\in\Sigma$. 2. (ii)

Suppose $\mathcal{F}$ expands $\mathcal{A}$. Then a $(\Sigma^{\prime},\mathcal{F})$-structure $\mathcal{B}$ is a $(\Sigma^{\prime},\mathcal{F})$-expansion of $\mathcal{A}$ if $c^{\mathcal{A}}=c^{\mathcal{B}}$ for all $c\in\Sigma$.

Remark 8**.**

1. (ii)

By Remark 2 the denotation of terms $\Delta\vdash M:\iota^{n}\to\iota$ is the same for all $(\Sigma^{\prime},\mathcal{F})$-expansions of $\mathcal{A}$ and $(\Delta,\mathcal{F})$-valuations agreeing on $\Delta^{-1}(\tau)$. 2. (ii)

In case $\mathcal{F}$ is complete, the $(\Sigma^{\prime},\mathcal{F})$-expansions of $\mathcal{A}$ ordered by $\sqsubseteq$ constitute a complete lattice with least upper bounds $\bigsqcup$, where $\sqsubseteq$ and $\bigsqcup$ are lifted in a pointwise fashion to $(\Sigma^{\prime},\mathcal{F})$-expansions of $\mathcal{A}$.555This is possible because $(\Sigma^{\prime},\mathcal{F})$-expansions of $\mathcal{A}$ agree on symbols of type $\iota^{n}\to\iota$.

Next, we introduce higher-order constrained Horn clauses and their satisfiability problem.

Definition 9**.**

1. (ii)

An atom is a $\Sigma^{\prime}$-formula that does not contain a logical symbol. 2. (ii)

An atom is a background atom if it is also a 1st-order $\Sigma$-formula. Otherwise it is a foreground atom.

Note that a foreground atom has one of the following forms:

(i) $R\,\overline{M}$where $R\in{(\Sigma^{\prime}\setminus\Sigma)}$,

(ii) $x\,\overline{M}$, or (iii) $(\lambda y\ldotp N)\overline{M}$.

We use $\varphi$ and $A$ (and variants thereof) to refer to background atoms and general atoms, respectively.

Definition 10** (HoCHC).**

1. (ii)

A goal clause is a disjunction $\neg A_{1}\lor\cdots\lor\neg A_{n}$, where each $A_{i}$ is an atom. We write $\bot$ to mean the empty (goal) clause. 2. (ii)

If $G$ is a goal clause, $R\in{(\Sigma^{\prime}\setminus\Sigma)}$ and the variables in $\overline{x}$ are distinct, then $G\lor R\,\overline{x}$ is a definite clause. 3. (ii)

A (higher-order) constrained Horn clause (HoCHC) is a goal or definite clause.

In the following we transform the higher-order sentences in Ex. 1 into HoCHCs (by first converting to prenex normal form and then omitting the universal quantifiers).

Example 11** (A system of HoCHCs).**

Let $\Sigma^{\prime}=\Sigma_{\operatorname{LIA}}\cup\{\operatorname{Add}:\iota\to\iota\to\iota\to o,\operatorname{Iter}:(\iota\to\iota\to\iota\to o)\to\iota\to\iota\to\iota\to o\}$ and let $\Delta$ be a type environment satisfying $\Delta(x)=\Delta(y)=\Delta(z)=\Delta(n)=\Delta(s)=\iota$ and $\Delta(f)=\iota\to\iota\to\iota\to o$.

[TABLE]

We refer to the first three (definite) HoCHCs as $D_{1}$ to $D_{3}$ and to the last (goal) HoCHC as $G$.

Definition 12**.**

Let $\Gamma$ be a set of HoCHCs, and suppose $\mathcal{F}$ is a frame expanding $\mathcal{A}$.

1. (ii)

$\Gamma$* is $(\mathcal{A},\mathcal{F})$-satisfiable if there exists a $(\Sigma^{\prime},\mathcal{F})$-expansion $\mathcal{B}$ of $\mathcal{A}$ satisfying $\mathcal{B}\models\Gamma$.* 2. (ii)

$\Gamma$* is $\mathcal{A}$-Henkin-satisfiable if it is $(\mathcal{A},\mathcal{F})$-satisfiable for some frame $\mathcal{F}$ expanding $\mathcal{A}$.* 3. (ii)

$\Gamma$* is $\mathcal{A}$-standard-satisfiable if it is $(\mathcal{A},\mathcal{S})$-satisfiable.* 4. (ii)

$\Gamma$* is $\mathcal{A}$-monotone-satisfiable if it is $(\mathcal{A},\mathcal{M})$-satisfiable.* 5. (ii)

$\Gamma$* is $\mathcal{A}$-continuous-satisfiable if it is $(\mathcal{A},\mathcal{C})$-satisfiable.*

Observe that $\mathcal{A}$-Henkin satisfiability is trivially implied by all notions of satisfiability in Def. 12.

II-C Programs

Whilst HoCHCs have a simple syntax (thus yielding a simple proof system), our completeness proof relies on programs, which are syntactically slightly more complex.

Definition 13**.**

A program (usually denoted by $\Pi$) is a set of $\Sigma^{\prime}$-formulas $\{\neg F_{R}\lor R\,\overline{x}_{R}\mid R\in{(\Sigma^{\prime}\setminus\Sigma)}\}$ such that for each $R\in\Sigma^{\prime}\setminus\Sigma$, $F_{R}$ is positive existential, the variables in $\overline{x}_{R}$ are distinct, and $\operatorname{fv}(F_{R})\subseteq\operatorname{fv}(R\,\overline{x}_{R})$.

For each goal clause $G$ there is a closed positive existential formula666see Sec. -A2 for details $\operatorname{posex}(G)$ such that for each frame $\mathcal{F}$ and $(\Sigma^{\prime},\mathcal{F})$-structure $\mathcal{B}$, $\mathcal{B}\not\models G$ iff $\mathcal{B}\models\operatorname{posex}(G)$. Similarly, for each finite set of HoCHCs $\Gamma$, there exists a program66footnotemark: 6 $\Pi_{\Gamma}$ such that for each frame $\mathcal{F}$ and $(\Sigma^{\prime},\mathcal{F})$-structure $\mathcal{B}$, $\mathcal{B}\models\{D\in\Gamma\mid D\text{ definite}\}$ iff $\mathcal{B}\models\Pi_{\Gamma}$.

Example 14** (Program).**

The following program corresponds to the set of (definite) HoCHCs of Ex. 11 (modulo renaming of variables):

[TABLE]

III Canonical Model Property

The introduction of monotone semantics for HoCHC in [1] was partly motivated by the observation that the least model property (w.r.t. the pointwise ordering $\sqsubseteq$) fails for standard semantics (but holds for monotone semantics):

Example 15**.**

Consider the program $\Pi$

[TABLE]

with signature $\Sigma^{\prime}=\Sigma_{\operatorname{LIA}}\cup\{R:((\iota\to o)\to o)\to o,U:\iota\to o\}$, a type environment $\Delta$ satisfying $\Delta(x_{R})=(\iota\to o)\to o$ and $\Delta(x_{U})=\iota$ taken from [1]. Let $\mathcal{F}=\mathcal{S}$ be the standard frame and let $\operatorname{neg}\in{\mathcal{S}}\llbracket(\iota\to o)\to o\rrbracket$ be such that $\operatorname{neg}(s)=1$ iff $s=\bot_{\iota\to o}$.

There are (at least) two expansions $\mathcal{B}_{1}$ and $\mathcal{B}_{2}$ defined by $U^{\mathcal{B}_{1}}=\bot_{\iota\to o}$ and $R^{\mathcal{B}_{1}}(s)=1$ iff $s(\bot_{\iota\to o})=1$, and $U^{\mathcal{B}_{2}}=\top_{\iota\to o}$ and $R^{\mathcal{B}_{2}}(s)=1$ iff $s(\top_{\iota\to o})=1$, respectively.

Note that $\mathcal{B}_{1}\models\Pi$, $\mathcal{B}_{2}\models\Pi$ and there are no models smaller than any of these with respect to the pointwise ordering $\sqsubseteq$. Furthermore, neither $\mathcal{B}_{1}\sqsubseteq\mathcal{B}_{2}$ nor $\mathcal{B}_{2}\sqsubseteq\mathcal{B}_{1}$ holds because $R^{\mathcal{B}_{1}}(\operatorname{neg})=1>0=R^{\mathcal{B}_{2}}(\operatorname{neg})$ and for any $n\in{\mathcal{S}}\llbracket\iota\rrbracket$, $U^{\mathcal{B}_{2}}(n)=1>0=U^{\mathcal{B}_{1}}(n)$.

In this section, we sharpen and extend the result: HoCHC does enjoy a canonical (though not least w.r.t. $\sqsubseteq$) model property. More precisely, the structure obtained by iterating the immediate consequence operator (see e.g. [16]) is a model of all satisfiable HoCHCs.

Assumption**.**

For Sec. IV and III we fix a complete frame $\mathcal{F}$ expanding $\mathcal{A}$. Furthermore, let $\Gamma$ be a finite set of HoCHCs and let $\Pi=\Pi_{\Gamma}$ (the program corresponding to $\Gamma$).

If no confusion arises, we refrain from mentioning $\Sigma^{\prime}$, $\Delta$ and $\mathcal{F}$ explicitly.

Given an expansion $\mathcal{B}$ of $\mathcal{A}$, the immediate consequence operator $T_{\Pi}$ returns the expansion $T_{\Pi}(\mathcal{B})$ of $\mathcal{A}$ defined by $R^{T_{\Pi}(\mathcal{B})}\coloneqq{\mathcal{B}}\llbracket\lambda\overline{x}_{R}\ldotp F_{R}\rrbracket$, for relational symbols $R\in\Sigma^{\prime}\setminus\Sigma$. (Recall that $F_{R}$ is the unique positive existential formula such that $\neg F_{R}\lor R\,\overline{x}_{R}\in\Pi$.) Observe that the prefixed points of $T_{\Pi}$ (i.e. structures $\mathcal{B}$ such that $T_{\Pi}(\mathcal{B})\sqsubseteq\mathcal{B}$) are precisely the models of $\Pi$.

Unfortunately, the immediate consequence operator is not monotone w.r.t. $\sqsubseteq$. Hence, we cannot apply the Knaster-Tarski theorem. Therefore, we introduce the notion of quasi-monotonicity and a slightly stronger version of that theorem. This is a warm-up for Sec. IV-A, where we propose quasi-continuity and a version of Kleene’s fixed point theorem.

III-A Quasi-monotonicity

Assumption**.**

Let $L$ be a complete lattice ordered by $\leq$ with least upper bounds $\bigvee$ and least element $\bot$. Furthermore, let $F:L\to L$ be an (endo-)function.

We define

[TABLE]

In particular, $a_{0}=\bot$. Clearly, $a_{F},a_{\beta}\in L$ for all ordinals $\beta$.

Definition 16**.**

Let ${\precsim}\subseteq L\times L$ be a relation.

1. (ii)

$\precsim$* is compatible with $\leq$ if*

1. (C1)

for all $a,b,c\in L$, if $a\precsim b$ and $b\leq c$ then $a\precsim c$, 2. (C2)

*for all $a\in L$ and $A\subseteq\{b\in L\mid b\precsim a\}$, $\bigvee A\precsim a$. * 2. (ii)

$F$* is quasi-monotone if for all $a,b\in L$, $a\precsim b$ implies $F(a)\precsim F(b)$.*

In particular, $\leq$ is compatible to itself and $\bot\precsim a$ for $a\in L$.

Proposition 17**.**

1. $F(a_{F})\leq a_{F}$*and

2. *if $\precsim$ is compatible with $\leq$, $F$ is quasi-monotone and $b\in L$ satisfies $F(b)\leq b$ then $a_{F}\precsim b$.

The proof idea is the same as for the standard Knaster-Tarski theorem, which can be recovered from the above by using $\leq$ for $\precsim$.

III-B Application to the Immediate Consequence Operator

The idea now is to instantiate $L$ with the complete lattice of expansions of $\mathcal{A}$ (see (ii)), and $F$ with the immediate consequence operator $T_{\Pi}$. We denote the structure at stage $\beta$ by $\mathcal{A}_{\beta}$ and the limit structure by $\mathcal{A}_{\Pi}$.

Intuitively, we start from the $\sqsubseteq$-minimal structure assigning $\bot_{\rho}$ to every $R:\rho\in\Sigma^{\prime}\setminus\Sigma$ and we incrementally extend the structure to satisfy more of the program. $\mathcal{A}_{\Pi}$ is a prefixed point of $T_{\Pi}$ (Prop. 17). Therefore,

Corollary 18**.**

$\mathcal{A}_{\Pi}\models\Pi$* and $\mathcal{A}_{\Pi}\models\{D\in\Gamma\mid D\text{ definite}\}$.*

Next, suppose there are relations ${\precsim_{\sigma}}\subseteq{\mathcal{F}}\llbracket\sigma\rrbracket\times{\mathcal{F}}\llbracket\sigma\rrbracket$ (for types $\sigma$) compatible with $\sqsubseteq_{\sigma}$, and

1. (i)

if $\mathcal{B}\precsim\mathcal{B}^{\prime}$ and $\alpha\precsim\alpha^{\prime}$ then ${\mathcal{B}}\llbracket M\rrbracket(\alpha)\precsim{\mathcal{B}^{\prime}}\llbracket M\rrbracket(\alpha^{\prime})$, and 2. (ii)

$b\precsim b^{\prime}$ iff $b\leq b^{\prime}$ for $b,b^{\prime}\in{\mathcal{B}}\llbracket o\rrbracket=\mathbb{B}$,

where we omit type subscripts and lift $\precsim$ in the usual pointwise manner to structures and valuations. Then $T_{\Pi}$ is quasi-monotone. Besides, if $\mathcal{B}$ is an expansion of $\mathcal{A}$ satisfying $\mathcal{B}\models\Pi$ then by Prop. 17, for closed positive existential formulas $F$, ${\mathcal{A}_{\Pi}}\llbracket F\rrbracket\leq{\mathcal{B}}\llbracket F\rrbracket$. Consequently, $\mathcal{A}_{\Pi}\models\Gamma$ if $\mathcal{B}\models\Gamma$.

The main obstacle (and where $\sqsubseteq$ fails) is to ensure that $\precsim$ is compatible with applications, i.e. if $r\precsim_{\tau\to\rho}r^{\prime}$ and $s\precsim_{\tau}s^{\prime}$ then $r(s)\precsim_{\rho}r^{\prime}(s^{\prime})$. Therefore, we simply define it that way:

Definition 19**.**

We define a relation ${\precsim_{\sigma}}\subseteq{{\mathcal{F}}\llbracket\sigma\rrbracket\times{\mathcal{F}}\llbracket\sigma\rrbracket}$ as follows by recursion on the type $\sigma$:

[TABLE]

$\precsim$ is transitive but neither reflexive ((ii)) nor antisymmetric, in general, and coincides with the pointwise ordering $\sqsubseteq$ on the monotone frame $\mathcal{M}$ ((ii)).

Example 20**.**

1. (ii)

For all relational types $\rho$ and $s\in{\mathcal{F}}\llbracket\rho\rrbracket$, $\bot_{\rho}\precsim s\precsim\top_{\rho}$. 2. (ii)

$\operatorname{or}\precsim\operatorname{or}$, $\operatorname{and}\precsim\operatorname{and}$ and for argument types $\tau$, $\operatorname{exists}_{\tau}\precsim\operatorname{exists}_{\tau}$777the argument for the latter is not entirely trivial but similar as in (ii). 3. (ii)

Let $\mathcal{F}=\mathcal{S}$ be the standard frame and let $\operatorname{neg}\in{\mathcal{S}}\llbracket(\iota\to o)\to o\rrbracket$ as in Ex. 15. Recall that $\bot_{\iota\to o}\precsim\top_{\iota\to o}$. However, $\operatorname{neg}(\bot_{\iota\to o})=1>0=\operatorname{neg}(\top_{\iota\to o})$. This shows that $\precsim$ is not reflexive, in general.

Example 21**.**

For the structures $\mathcal{B}_{1}$ and $\mathcal{B}_{2}$ of Ex. 15 it holds that $\mathcal{B}_{1}=\mathcal{A}_{\Pi}$ and $\mathcal{B}_{1}\precsim\mathcal{B}_{2}$ because due to $\bot_{\iota\to o}\precsim\top_{\iota\to o}$, for any $s\precsim s^{\prime}$, $s(\bot_{\iota\to o})\leq s^{\prime}(\top_{\iota\to o})$ and therefore $R^{\mathcal{B}_{1}}(s)\leq R^{\mathcal{B}_{2}}(s^{\prime})$. In particular, the fact that $R^{\mathcal{B}_{1}}(\operatorname{neg})>R^{\mathcal{B}_{2}}(\operatorname{neg})$ is not a concern because $\operatorname{neg}\precsim\operatorname{neg}$ does not hold.

A simple induction (cf. Lemma 64)on the type $\sigma$ shows that $\precsim_{\sigma}$ is compatible with $\sqsubseteq_{\sigma}$. Furthermore,

Lemma 22**.**

Let $\mathcal{B}\precsim\mathcal{B}^{\prime}$ be expansions of $\mathcal{A}$, $\alpha\precsim\alpha^{\prime}$ be valuations and let $M$ be a positive existential term. Then ${\mathcal{B}}\llbracket M\rrbracket(\alpha)\precsim{\mathcal{B}^{\prime}}\llbracket M\rrbracket(\alpha^{\prime})$.

Consequently, the immediate consequence operator is quasi-monotone and we conclude:

Theorem 23**.**

If $\Gamma$ is $(\mathcal{A},\mathcal{F})$-satisfiable then $\mathcal{A}_{\Pi}\models\Gamma$.

IV Resolution Proof System

Our resolution proof system is remarkably simple, consisting of only three rules:

1. a higher-order version of the usual resolution rule [3] between a pair of goal and definite clauses (thus yielding a goal clause),

2. a rule for $\beta$-reductions on leftmost (outermost) positions of atoms in goal clauses and

3. a rule to refute certain goal clauses which are not satisfied by the model of the background theory (similar to [19]).

Resolution

G\lor\big{(}G^{\prime}[\overline{M}/\overline{x}]\big{)}\lx@proof@logical@and\neg R\,\overline{M}\lor GG^{\prime}\lor R\,\overline{x}

$\beta$-Reduction

$\neg L[M/x]\,\overline{N}\lor G\neg(\lambda x\ldotp L)M\,\overline{N}\lor G$

Constraint refutation

$\bot G\lor\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}$

provided that each atom in $G$ has the form888where $x$ is a variable $x\,\overline{M}$, each $\varphi_{i}$ is a background atom and there exists a valuation $\alpha$ such that $\mathcal{A},\alpha\models\varphi_{1}\land\cdots\land\varphi_{n}$.

Example 24** (Refutation proof).**

A refutation of the set of HoCHCs from Ex. 11 is given in Fig. 2. The last inference is admissible because for any valuation satisfying $\alpha(n)=\alpha(y)=1$ and $\alpha(x)=2$,

[TABLE]

Since variables are implicitly universally quantified, the rules have to be applied modulo the renaming of (free) variables; we write $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{G\}$ if $G$ can be thus derived from the clauses in $\Gamma^{\prime}$ using the above rules and $\vdash_{\mathcal{A}}^{*}$ for the reflexive, transitive closure of $\vdash_{\mathcal{A}}$.

Proposition 25** (Soundness).**

Let $\Gamma$ be a set of HoCHCs.

If $\Gamma\vdash_{\mathcal{A}}^{*}\Gamma^{\prime}\cup\{\bot\}$ (for some $\Gamma^{\prime}$) then $\Gamma$ is $(\mathcal{A},\mathcal{F})$-unsatisfiable, and this holds even if $\mathcal{F}$ is not complete.

Proof sketch.

The most interesting case occurs when the constraint refutation rule is applied to $G\coloneqq\bigvee_{i=1}^{m}\neg x_{i}\,\overline{M}_{i}\lor\bigvee_{j=1}^{n}\neg\varphi_{j}$. Being of relational type, each variable $x_{i}$ cannot occur in any $\varphi_{j}$. Thus, modifying witnesses $\alpha$ of $\mathcal{A},\alpha\models\varphi_{1}\land\cdots\land\varphi_{n}$ to satisfy $\alpha^{\prime}(x)=\top_{\rho}$ for $x:\rho\in\Delta$, we conclude $\mathcal{B},\alpha^{\prime}\not\models G$ for all expansions $\mathcal{B}$ of $\mathcal{A}$. ∎

Observe that the argument makes use of $\top_{\rho}\in{\mathcal{F}}\llbracket\rho\rrbracket$, which is a consequence of the comprehension axiom.

The following completeness theorem is significantly more difficult. In fact, we will not prove it until Sec. IV-D.

Theorem 26** (Completeness).**

If $\Gamma$ is $(\mathcal{A},\mathcal{F})$-unsatisfiable then $\Gamma\vdash_{\mathcal{A}}^{*}\{\bot\}\cup\Gamma^{\prime}$ for some $\Gamma^{\prime}$.

Consequently, the resolution proof system gives rise to a semi-decision procedure for the $(\mathcal{A},\mathcal{F})$-unsatisfiability problem provided it is (semi-)decidable whether a goal clause of background atoms is not satisfied by the background theory999i.e. whether there exists a valuation $\alpha$ such that $\mathcal{A},\alpha\models\varphi_{1}\land\cdots\land\varphi_{n}$.

Outline of the Completeness Proof

1. (S1)

First, we prove that some goal clause is not satisfied by the canonical structure already after a finite number of iterations if $\Gamma$ is $(\mathcal{A},\mathcal{F})$-unsatisfiable (Sec. IV-A). 2. (S2)

Consequently, there is a syntactic reason for $\Gamma$’s $(\mathcal{A},\mathcal{F})$-unsatisfiability (by “unfolding definitions”) (Sec. IV-B). 3. (S3)

Finally, we prove that the “unfolding” actually only needs to take place at the leftmost (outermost) positions of atoms (Sec. IV-C), which can be captured by the resolution proof system (Sec. IV-D).

Observe that Proof Step (S1) is model theoretic / semantic, whilst Proof Steps (S2) and (S3) are proof theoretic / syntactic.

IV-A Quasi-Continuity

Whilst in Sec. III we have shown that $\mathcal{A}_{\Pi}$ is a model of the definite clauses, we now examine the consequences of $\mathcal{A}_{\Pi}\not\models G$ for some goal clause $G\in\Gamma$. Unlike the 1st-order case [20], stage $\omega$ is not a fixed point of $T_{\Pi}$ in general, as the following example illustrates:

Example 27**.**

Consider the following program:

[TABLE]

where $\Sigma^{\prime}=\Sigma_{\operatorname{LIA}}\cup\{R:\iota\to o,U:((\iota\to o)\to o)\to o\}$, $\Delta(x_{R})=\iota$ and $\Delta(x_{U})=(\iota\to o)\to o$. Let $\mathcal{A}$ be the standard model of Linear Integer Arithmetic $\mathcal{A}_{\operatorname{LIA}}$ and let $\mathcal{F}=\mathcal{S}$ be the standard frame. For ease of notation, we introduce functions $r_{\alpha}:{\mathcal{S}}\llbracket\iota\rrbracket\to\mathbb{B}$ such that $r_{\alpha}(n)=1$ iff $0\leq n<\alpha$, and $\delta_{\alpha}:{\mathcal{S}}\llbracket\iota\to o\rrbracket\to\mathbb{B}$ such that $\delta_{\alpha}(r)=1$ iff $r=r_{\alpha}$, where $\alpha\in\omega\cup\{\omega\}$. Then it holds $R^{\mathcal{A}_{n}}=r_{n}$, $U^{\mathcal{A}_{0}}=\bot_{(\iota\to o)\to o}$ and $U^{\mathcal{A}_{n}}(s)=s(r_{n-1})$ for $n>0$. Therefore $R^{\mathcal{A}_{\omega}}=r_{\omega}$ and $U^{\mathcal{A}_{\omega}}(s)=1$ iff there exists $n<\omega$ satisfying $s(r_{n})=1$. In particular, $U^{\mathcal{A}_{\omega}}(\delta_{\omega})=0$. On the other hand, $U^{\mathcal{A}_{\omega+1}}(\delta_{\omega})={\mathcal{A}_{\omega}}\llbracket\lambda x_{U}\ldotp x_{U}\,R\rrbracket(\delta_{\omega})=1$. Consequently, $\mathcal{A}_{\omega}\neq\mathcal{A}_{\omega+1}$.

Nonetheless, there still exists a (finite) $n\in\omega$ satisfying $\mathcal{A}_{n}\not\models G$ if $\mathcal{A}_{\Pi}\not\models G$ (Thm. 32). We make use of a similar strategy to establishing the canonical model property: we introduce the notion of quasi-continuity, state a version of Kleene’s fixed point theorem and prove the immediate consequence operator to be quasi-continuous.

Definition 28**.**

Let ${\precsim}\subseteq L\times L$ be a relation.

1. (ii)

$\precsim$* is $\precsim$-directed if for every $a,b\in L$, $a\precsim a$ and there exists $c\in L$ satisfying $a,b\precsim c$.*

For $a\in L$ we write $\operatorname{dir}_{\precsim}(a)$ for the set of $\precsim$-directed subsets $D$ of $L$ satisfying $a\precsim\bigvee D$. 2. (ii)

$F$* is quasi-continuous if for all $a\in L$ and $D\in\operatorname{dir}_{\precsim}(a)$, $F(a)\precsim\bigvee_{b\in D}F(b)$.*

Thus, every quasi-continuous function is in particular quasi-monotone if $\precsim$ is reflexive.

Proposition 29**.**

*If $\precsim$ is compatible with $\leq$ and $F$ is quasi-continuous then

1. for all ordinals $\beta\leq\beta^{\prime}$, $a_{\beta}\precsim a_{\beta^{\prime}}$ and

2. $a_{F}\precsim a_{\omega}$.

Combined with Prop. 17 this yields Kleene’s fixed point theorem in the case of ${\precsim}\coloneqq{\leq}$.

Similarly as in Sec. III, we need relations ${\precsim_{\sigma}}\subseteq{\mathcal{F}}\llbracket\sigma\rrbracket\times{\mathcal{F}}\llbracket\sigma\rrbracket$ which behave well with applications in order for the immediate consequence operator to be quasi-continuous. Therefore, we stipulate (overloading the notation of Sec. III):

Definition 30**.**

We define ${\precsim_{\sigma}}\subseteq{{\mathcal{F}}\llbracket\sigma\rrbracket\times{\mathcal{F}}\llbracket\sigma\rrbracket}$ by recursion on the type $\sigma$:

[TABLE]

There is an elementary inductive argument (cf. Lemma 68) that each $\precsim_{\sigma}$ is compatible with $\sqsubseteq_{\sigma}$. We lift $\precsim$ to structures and valuations in a pointwise way, and abbreviate $\operatorname{dir}_{\precsim}$ as $\operatorname{dir}$.

Lemma 31**.**

Let $M$ be a positive existential term, $\mathcal{B}$ be an expansion of $\mathcal{A}$, $\mathfrak{B}^{\prime}\in\operatorname{dir}(\mathcal{B})$, $\alpha$ be a valuation and let $\mathfrak{a}^{\prime}\in\operatorname{dir}(\alpha)$. Then101010By (ii) the right-hand side is well-defined.

[TABLE]

Consequently, the immediate consequence operator is quasi-continuous. Moreover, by Prop. 29, for closed positive existential formulas $F$, ${\mathcal{A}_{\Pi}}\llbracket F\rrbracket\leq\max_{n\in\omega}{\mathcal{A}_{n}}\llbracket F\rrbracket$. Therefore, we get the following result, which is key for the refutational completeness of the proof system.

Theorem 32**.**

Let $G$ be a goal clause. If $\mathcal{A}_{\Pi}\not\models G$ then there exists $n\in\omega$ such that $\mathcal{A}_{n}\not\models G$.

IV-B Syntactic Unfolding

Having established Proof Step (S1), we study a functional relation $\rightarrow_{\parallel}$ on positive existential terms, which is a syntactic counterpart of the immediate consequence operator. Essentially111111For a formal definition refer to Fig. 5 in Sec. -C2., it holds $M\rightarrow_{\parallel}N$ if $N$ is obtained from $M$ by replacing all occurrences of symbols $R\in\Sigma^{\prime}\setminus\Sigma$ with $\lambda\overline{x}_{R}\ldotp F_{R}$, which is reminiscent of the definition of $R^{T_{\Pi}(\mathcal{B})}$. Therefore:

Proposition 33**.**

Let $\mathcal{B}$ be an expansion of $\mathcal{A}$ and let $M$ and $N$ be positive existential terms satisfying $M\rightarrow_{\parallel}N$. Then for all valuations $\alpha$, ${T_{\Pi}(\mathcal{B})}\llbracket M\rrbracket(\alpha)={\mathcal{B}}\llbracket N\rrbracket(\alpha)$.

A similar idea is exploited in [16].

Next, let $\upsilon\coloneqq\{(R,\lambda\overline{x}_{R}\ldotp F_{R})\mid R\in\Sigma^{\prime}\setminus\Sigma\}$ and $\beta\upsilon\coloneqq\beta\cup\upsilon$. Besides, let $\rightarrow_{\beta\upsilon}$ be the compatible closure [15, p. 51] of $\beta\upsilon$. It is easy to see that ${\rightarrow_{\parallel}}\subseteq{\twoheadrightarrow_{\beta\upsilon}}$, where $\twoheadrightarrow_{\beta\upsilon}$ is the reflexive, transitive closure of $\rightarrow_{\beta\upsilon}$.

IV-C Leftmost (Outermost) Reduction

There is an important mismatch between the relation $\rightarrow_{\beta\upsilon}$ and the rules of the proof system: in contrast to the former, the latter only take leftmost (outermost) positions of atoms into account. Fortunately, arbitrary sequences of $\beta\upsilon$-reductions can be mimicked by sequences which are standard in the sense that purely leftmost reductions are followed by purely non-leftmost ones (Cor. 35).

Fig. 3 defines \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[12.36115pt]{\scriptstyle\cdot}}}{\scriptstyle\ell\,}} and \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}, which formalise leftmost (outermost) and standard reductions, respectively. We write M\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N if M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N for some $m$, where $m$ corresponds to the number of leftmost $\beta\upsilon$-reductions having been performed. The idea is that L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N if for some $M$, L\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}M and we can obtain $N$ from $M$ by performing standard $\beta\upsilon$-reductions only on non-leftmost positions.

Lemma 34**.**

If K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M\rightarrow_{\beta\upsilon}N then K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N.

The proof of this proposition is very similar to the proof of the standardisation theorem in the $\lambda$-calculus as presented in [10] and relies on the insight that if all of \overline{K}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{M}, K^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M^{\prime} and O\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}Q hold then K^{\prime}[O/x]\,\overline{K}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M^{\prime}[Q/x]\,\overline{M}.

Corollary 35**.**

Let $M$ and $N$ be positive existential terms such that $M\twoheadrightarrow_{\beta\upsilon}N$. Then M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N.

Next, we consider the relation $\vartriangleright$ on positive existential formulas and valuations inductively defined by:

[TABLE]

Intuitively, $\alpha\vartriangleright F$ if for some $\alpha^{\prime}$ (agreeing with $\alpha$ on $\Delta^{-1}(\iota)$), $\mathcal{A}_{0},\alpha^{\prime}\models F$ and there are no $\lambda$-abstractions in relevant leftmost positions.

Remark 36**.**

If $G$ is a goal clause and $\alpha\vartriangleright\operatorname{posex}(G)$ (for some $\alpha$) then $G$ has the form $\bigvee_{i=1}^{m}\neg x_{i}\,\overline{M}_{i}\lor\bigvee_{j=1}^{n}\neg\varphi_{j}$ and $G$ can be refuted by the constraint refutation rule in one step.

Lemma 37**.**

Let $G$ be a goal clause, $F$ be a $\beta$-normal positive existential formula and $\alpha$ be a valuation such that $\mathcal{A}_{0},\alpha\models F$ and \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}F. Then there exists a positive existential formula $F^{\prime}$ satisfying \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}F^{\prime} and $\alpha\vartriangleright F^{\prime}$.

IV-D Concluding Refutational Completeness

Finally, we establish a connection between the (abstract) relation \mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}} on positive existential terms and the resolution proof system on clauses. We define a function $\mu$ assigning natural numbers or $\omega$ to positive existential formulas $E$ by

[TABLE]

which is extended to non-empty sets $\Gamma^{\prime}$ of HoCHCs by $\mu(\Gamma^{\prime})\coloneqq\min\{\mu(\operatorname{posex}(G))\mid G\in\Gamma\}$.

We can use the resolution proof system to derive a set of HoCHCs $\Gamma^{\prime\prime}$ with a strictly smaller measure by simulating a \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}-reduction step:

Proposition 38**.**

Let $\Gamma^{\prime}\supseteq\Gamma$ be a set of HoCHCs satisfying $0<\mu(\Gamma^{\prime})<\omega$. Then there exists $\Gamma^{\prime\prime}\supseteq\Gamma$ satisfying $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime\prime}$ and $\mu(\Gamma^{\prime\prime})<\mu(\Gamma^{\prime})$.

Example 39**.**

Consider the HoCHCs $\Gamma=\{\neg(x_{R}\geq 5)\lor R\,x_{R},\neg R\,(x_{R}-5)\lor R\,x_{R},\neg R\,5\}$. It holds that R\,5\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}(\lambda x_{R}\ldotp x_{R}\geq 5\lor R\,(x_{R}-5))\,5\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}5\geq 5\lor R\,(5-5) and $\mu(\Gamma)=2$. Furthermore, $\Gamma\vdash_{\mathcal{A}}\Gamma\cup\{\neg 5\geq 5\}$ and $\mu(\Gamma\cup\{\neg 5\geq 5\})=0$.

Combining everything, we finally obtain: See 26

Proof.

By Cor. 18, $\mathcal{A}_{\Pi}\models D$ for all definite clauses $D\in\Gamma$. Since $\Gamma$ is $(\mathcal{A},\mathcal{F})$-unsatisfiable there exists a goal clause $G\in\Gamma$ satisfying $\mathcal{A}_{\Pi}\not\models G$. By Thm. 32 there exists $n\in\omega$ such that $\mathcal{A}_{n}\not\models G$. Let $F_{n}$ be such that $\operatorname{posex}(G)\rightarrow_{\parallel}^{n}F_{n}$ (where $\rightarrow_{\parallel}^{n}$ is the $n$-fold composition of $\rightarrow_{\parallel}$). By Prop. 33, $\mathcal{A}_{0},\alpha\models F_{n}$ (for any $\alpha$ as $F_{n}$ is closed). Let $F_{n}^{\prime}$ be the $\beta$-normal form of $F_{n}$. By Corollary 35 and 37 there exists $F^{\prime}$ such that \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}F^{\prime} and $\alpha\vartriangleright F^{\prime}$. Consequently, $\mu(\Gamma)<\omega$. By Prop. 38 there exists $\Gamma^{\prime}\supseteq\Gamma$ satisfying $\Gamma\vdash_{\mathcal{A}}^{*}\Gamma^{\prime}$ and $\mu(\Gamma^{\prime})=0$.

Hence, there exists $G\in\Gamma^{\prime}$ and $\alpha$ such that \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 0}}}{\scriptstyle\ell\,}}F^{\prime} and $\alpha\vartriangleright F^{\prime}$. Clearly, this implies $F^{\prime}=\operatorname{posex}(G)$, and by Remark 36, $\Gamma\vdash_{\mathcal{A}}^{*}\Gamma^{\prime}\vdash_{\mathcal{A}}\{\bot\}\cup\Gamma^{\prime}$. ∎

IV-E Compactness of HoCHC

The reason why we restrict $\Gamma$ to be finite is to achieve correspondence with programs (Def. 13), which are finite expressions. If we simply extend programs with infinitary disjunctions (but keep HoCHCs finitary) we can carry out exactly the same reasoning to derive that also every infinite, $(\mathcal{A},\mathcal{F})$-unsatisfiable set of HoCHCs can be refuted in the proof system. Consequently:

Theorem 40** (Compactness).**

For every $(\mathcal{A},\mathcal{F})$-unsatisfiable set $\Gamma$ of HoCHCs there exists a finite subset $\Gamma^{\prime}\subseteq\Gamma$ which is $(\mathcal{A},\mathcal{F})$-unsatisfiable.

V Semantic Invariance

[1] details an explicit translation between standard and monotone models of HoCHCs, thus yielding the equivalence of $\mathcal{A}$-standard- and $\mathcal{A}$-monotone-satisfiability.

As a consequence of the Completeness Thm. 26 for the proof system, $(\mathcal{A},\mathcal{F})$-unsatisfiability for any complete frame $\mathcal{F}$ implies the existence of a refutation, which in turn entails $(\mathcal{A},\mathcal{F}^{\prime})$-unsatisfiability for any frame $\mathcal{F}^{\prime}$ by the Soundness Prop. 25.

Therefore, exploiting Ex. 5, we obtain an equivalence result encompassing a much wider class of semantics:

Theorem 41** (Semantic Invariance).**

Let $\Gamma$ be a set of HoCHCs. Then the following are equivalent:

1. (ii)

$\Gamma$* is $\mathcal{A}$-standard-satisfiable,* 2. (ii)

$\Gamma$* is $\mathcal{A}$-Henkin-satisfiable,* 3. (ii)

$\Gamma$* is $\mathcal{A}$-monotone-satisfiable,* 4. (ii)

$\Gamma$* is $\mathcal{A}$-continuous-satisfiable,* 5. (ii)

$\Gamma$* is $(\mathcal{A},\mathcal{F})$-satisfiable, where $\mathcal{F}$ is a complete frame expanding $\mathcal{A}$.*

Thus, we call a set of $\Gamma$ of HoCHCs $\mathcal{A}$-satisfiable if it satisfies any of the equivalent conditions of Thm. 41.

VI Compact Theories

In this section, we extend our results to background theories (over $\Sigma$) with a set $\mathfrak{A}$ of models (i.e. $\Sigma$-structures), calling a set of HoCHCs $\mathfrak{A}$-satisfiable if it is $\mathcal{A}$-satisfiable for some $\mathcal{A}\in\mathfrak{A}$. Otherwise it is $\mathfrak{A}$-unsatisfiable.

Observe that the Completeness Thm. 26 critically relies on the observation that $\mathcal{A}$-unsatisfiability can be traced back to the failure of a single goal clause of background atoms (manifested in the constraint refutation rule). Therefore, it is natural to generalise constraint refutation to a rule refuting sets of $\mathfrak{A}$-unsatisfiable121212Note that for a set $\Gamma$ of goal clauses of background atoms, $\mathcal{A}$-satisfiability is in essence not about the existence of $\mathcal{A}\in\mathfrak{A}$ and an expansion $\mathcal{B}$ of $\mathcal{A}$ such that $\mathcal{B}\models\Gamma$ but only about the existence of $\mathcal{A}\in\mathfrak{A}$ such that $\mathcal{A}\models\Gamma$. goal clauses of background atoms:

Comp. const. refutation

$\bot\lx@proof@logical@and G_{1}\lor\bigvee_{i=1}^{m_{1}}\neg\varphi_{1,i}\ldots G_{n}\lor\bigvee_{i=1}^{m_{n}}\neg\varphi_{n,i}$

provided that each atom in each $G_{i}$ has the form $x\,\overline{M}$, each $\varphi_{i,j}$ is a background atom and $\{\neg\varphi_{j,1}\lor\cdots\lor\neg\varphi_{j,m_{j}}\mid 1\leq j\leq n\}$ is $\mathfrak{A}$-unsatisfiable.

and let $\vdash_{\mathfrak{A}}$ be defined accordingly. However, to match the rule’s finitary nature, $\mathfrak{A}$ needs to be restricted a little:

Definition 42**.**

A set $\mathfrak{A}$ of 1st-order $\Sigma$-structures is compact if for all $\mathfrak{A}$-unsatisfiable sets $\Gamma$ of goal clauses of background atoms there exists a finite $\Gamma^{\prime}\subseteq\Gamma$ which is $\mathfrak{A}$-unsatisfiable.

In particular, every finite $\mathfrak{A}$ is compact. Then we obtain:

Theorem 43** (Soundness and Completeness).**

Let $\mathfrak{A}$ be a compact set of $\Sigma$-structures and $\Gamma$ be a set of HoCHCs. Then $\Gamma$ is $\mathfrak{A}$-unsatisfiable iff $\Gamma\vdash_{\mathfrak{A}}^{*}\Gamma^{\prime}\cup\{\bot\}$ for some $\Gamma^{\prime}$.

As an interesting special case, this shows that the proof system is also sound and complete in the unconstrained setting: by the compactness theorem for 1st-order logic the set of 1st-order $\Sigma$-structures (possibly interpreting (in-)equality symbols as (non-)identity) is compact. Consequently, there does not exist a $\Sigma^{\prime}$-structure $\mathcal{B}$ (interpreting (in-)equality as (non-)identity) satisfying $\mathcal{B}\models\Gamma$ iff $\Gamma$ is refutable.

VII 1st-order Translation

It is folklore that there is a 1st-order translation of higher-order logic which is sound and complete for Henkin semantics (see e.g. [21, 22, 23]). The essence of the technique is to replace all symbols by constants (of a base type) and encode application using dedicated binary function symbols.

For the reasons discussed in the introduction this translation is however not in general complete for standard semantics. In this section, we present a particularly simple 1st-order translation of HoCHC which is sound and complete even for standard semantics. Fortunately, the target fragment is still semi-decidable.

We do not need to consider HoCHCs containing $\lambda$-abstractions because they can be eliminated by a logical counterpart of $\lambda$-lifting [24] (i.e. introducing new relational symbols and adding appropriate “definitions” for them, see Sec. -E1 and 79). This constitutes a considerable generalisation of the “polarity-dependent renaming” for 1st-order logic [25, 26].

Therefore, the following is without loss of generality:

Assumption**.**

Henceforth, we fix a finite set $\Gamma$ of HoCHCs which does not contain $\lambda$-abstractions and a set $\mathfrak{A}$ of 1st-order $\Sigma$-structures.

Let $\mathfrak{I}=\{\iota\}\cup\{\lfloor\rho\rfloor\mid\rho\text{ relational}\}$ (and we set $\lfloor\iota^{n}\to\iota\rfloor\coloneqq\iota^{n}\to\iota$). Clearly, we can regard $\Sigma$ and each $\mathcal{A}\in\mathfrak{A}$ as a 1st-order signature and structure, respectively, over the extended set of types of individuals.

We assume a type environment $\lfloor\Delta\rfloor$ such that for $x:\tau\in\Delta$, $\lfloor\Delta\rfloor(x)=\lfloor\tau\rfloor$ and define $\lfloor\Sigma^{\prime}\rfloor$ to be the following 1st-order extension of $\Sigma$:

[TABLE]

To reduce clutter, we often omit the subscripts from $\operatorname{@}$.

Intuitively, $\operatorname{@}$ encodes application, relational symbols $R\in\Sigma^{\prime}\setminus\Sigma$ become constants $c_{R}$, $H$ maps the “bogus booleans“ $\lfloor o\rfloor$ to $o$ and the following comprehension axiom $\operatorname{Comp}_{\rho}$ (for relational $\rho=\tau_{1}\to\cdots\to\tau_{n}\to o$) asserts the existence of an element (the interpretation of $c_{\rho}$) corresponding to $\top_{\rho}$:

[TABLE]

where the $x_{i}$ are distinct variables of type $\lfloor\tau_{i}\rfloor$.

For a $\Sigma^{\prime}$-term $M$ containing neither logical symbols nor $\lambda$-abstractions, we define $\lfloor M\rfloor^{\prime}$ by structural recursion:

[TABLE]

Thus, terms of the background theory are unchanged by $\lfloor\cdot\rfloor^{\prime}$ and by Remark 2, for each $\Sigma^{\prime}$-term $\Delta\vdash M:\sigma$ which is not a background atom, $\lfloor\Delta\rfloor\vdash\lfloor M\rfloor^{\prime}:\lfloor\sigma\rfloor$. The following operator $\lfloor\cdot\rfloor$ ensures that also foreground atoms have type $o$ (not $\lfloor o\rfloor$)

[TABLE]

and we lift $\lfloor\cdot\rfloor$ to HoCHCs by

[TABLE]

Finally, for $\Gamma$ we set

[TABLE]

Note that $\lfloor\Gamma\rfloor$ is a finite set of 1st-order Horn clauses131313in the standard sense of the (1st-order) language of $\lfloor\Sigma^{\prime}\rfloor$.

Example 44** (1st-order translation $\lfloor\cdot\rfloor$).**

Consider again the set $\Gamma$ of HoCHCs from Ex. 11. Applying the translation $\lfloor\cdot\rfloor$ to $\Gamma$ we get the 1st-order clauses in Fig. 4.

For $\mathcal{A}\in\mathfrak{A}$ and a $\Sigma^{\prime}$-expansion $\mathcal{B}$ of $\mathcal{A}$, let $\lfloor\mathcal{B}\rfloor$ be the 1st-order $\lfloor\Sigma\rfloor$-expansion of $\mathcal{A}$ defined by

[TABLE]

for relational $\rho$ and $\tau\to\rho^{\prime}$, $R\in\Sigma^{\prime}\setminus\Sigma$, $r\in{\lfloor\mathcal{B}\rfloor}\llbracket\lfloor\tau\to\rho^{\prime}\rfloor\rrbracket$, $s\in{\lfloor\mathcal{B}\rfloor}\llbracket\lfloor\tau\rfloor\rrbracket$ and $b\in{\lfloor\mathcal{B}\rfloor}\llbracket\lfloor o\rfloor\rrbracket=\mathbb{B}$. It is easy to see that $\mathcal{B}\models\Gamma$ implies $\lfloor\mathcal{B}\rfloor\models\lfloor\Gamma\rfloor$. Consequently:

Proposition 45**.**

If $\Gamma$ is $\mathfrak{A}$-satisfiable then $\lfloor\Gamma\rfloor$ is $\mathfrak{A}$-satisfiable.

Conversely, applications of the (higher-order) resolution rule can be matched by 1st-order resolution inferences between the corresponding translated clauses. Besides, the 1st-order translation contains comprehension axioms $\operatorname{Comp}_{\rho}$, which complements the instantiation of relational variables with $\top_{\rho}$ in the proof of the Soundness Prop. 25. Therefore, we obtain:

Lemma 46**.**

Let $\Gamma^{\prime}$ be a set of HoCHCs not containing $\lambda$-abstractions and suppose $\Gamma^{\prime}\vdash_{\mathfrak{A}}\Gamma^{\prime}\cup\{G\}$. Then

1. (ii)

$G$* does not contain $\lambda$-abstractions* 2. (ii)

if $G\neq\bot$ then $\lfloor\Gamma^{\prime}\rfloor\models\lfloor\Gamma^{\prime}\cup\{G\}\rfloor$ 3. (ii)

if $G=\bot$ then $\lfloor\Gamma^{\prime}\rfloor$ is $\mathfrak{A}$-unsatisfiable.

By the Completeness Thm. 43 we conclude:

Corollary 47**.**

If $\mathfrak{A}$ is compact and $\Gamma$ is $\mathfrak{A}$-unsatisfiable then $\lfloor\Gamma\rfloor$ is $\mathfrak{A}$-unsatisfiable.

Theorem 48**.**

Assuming that $\mathfrak{A}$ is compact, $\Gamma$ is $\mathfrak{A}$-satisfiable iff $\lfloor\Gamma\rfloor$ is $\mathfrak{A}$-satisfiable.

It is remarkable that our translation does not require extensionality axioms and only a very restricted form of comprehension axioms (cf. [6]).

Finally, if $\mathfrak{A}$ is compact, definable141414or term-generated [19], i.e. for every $\mathcal{A}\in\mathfrak{A}$ and $a\in{\mathcal{A}}\llbracket\iota\rrbracket$ there exists a closed $\Sigma$-term $M$ such that ${\mathcal{A}}\llbracket M\rrbracket=a$ and $\mathfrak{A}$-unsatisfiability of goal clauses of background atoms is semi-decidable, then $\mathfrak{A}$-unsatisfiability of $\lfloor\Gamma\rfloor$ is also semi-decidable [19, Thm. 24].

VIII Decidable Fragments

Satisfiability of HoCHC is undecidable in general because already its 1st-order fragments are undecidable for Linear Integer Arithmetic [27, 28] or the unconstrained setting151515i.e. the background theory imposes no restriction at all [29].

Remark 49**.**

Despite these negative results, $\mathfrak{A}$-satisfiability of finite $\Gamma$ is decidable if $\mathfrak{A}$ is a finite set of $\Sigma$-structures such that for each $\mathcal{A}\in\mathfrak{A}$ and type $\sigma$, ${\mathcal{A}}\llbracket\sigma\rrbracket$ is finite. This is a consequence of Thm. 23 and the fact that we can compute each $\mathcal{A}_{\Pi_{\Gamma}}$ explicitly and check whether $\mathcal{A}_{\Pi_{\Gamma}}\models\Gamma$ holds.

Thanks to this insight, we have identified two decidable fragments of HoCHC, one of which is presented as follows; we leave the other (higher-order Datalog) to Sec. -F1.

VIII-A *Combining the Bernays-Schönfinkel-Ramsey Fragment of

HoCHC with Simple Linear Integer Arithmetic*

Some authors [30, 31] have studied 1st-order clauses without function symbols (the so-called Bernays-Schönfinkel-Ramsey class161616Precisely the set of sentences that, when written in prenex normal form, have a $\exists^{*}\forall^{*}$-quantifier prefix and contain no function symbols.) extended with a restricted form of Linear Integer Arithmetic. The fragment enjoys the attractive property that every clause set is equi-satisfiable with a finite set of its ground instances, which implies decidability [30, 31].

In this section, we transfer this result to our higher-order Horn setting.

Assumption**.**

Let $\Sigma$ be a (1st-order) signature extending $\Sigma_{\operatorname{LIA}}$ with constant symbols $c:\iota$, and let $\Sigma^{\prime}\supseteq\Sigma$ be a relational extension of $\Sigma$.

Definition 50**.**

1. (ii)

A $\Sigma$-atom is simple if it has the form $x\leq M$, $M\leq x$ or $x\leq y$, where $M$ is closed171717or ground because atoms do not contain (existential) quantifiers by definition*. * 2. (ii)

A HoCHC is a higher-order simple linear arithmetic Bernays-Schönfinkel-Ramsey Horn clause (HoBHC(SLA)) if it has the form $\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}\lor C$, where each $\varphi_{i}$ is a simple (linear arithmetic) background atom and $C$ is $\bot$ or it does not contain symbols from $\Sigma$.

Note that we could also have allowed background atoms of the form $M\triangleleft N$, $x\triangleleft M$ and $x\trianglelefteq y$, where $M,N$ are closed, $\triangleleft\in\{<,\leq,=,\neq,\geq,>\}$ and $\trianglelefteq\;\in\{\leq,=,\geq\}$ [31].

Example 51**.**

Let $\Sigma=\Sigma_{\operatorname{LIA}}\cup\{c,d:\iota\}$, $\Sigma^{\prime}=\Sigma\cup\{R:\iota\to o,U:(\iota\to o)\to\iota\to o\}$, $\Delta(x)=\Delta(y)=\Delta(z)=\iota$ and $\Delta(f)=\iota\to o$. The following is a set of HoBHC(SLA):

[TABLE]

Assumption**.**

Let $\mathfrak{A}$ be the set of $\Sigma$-expansions of $\mathcal{A}_{\operatorname{LIA}}$ and let $\Gamma$ be a finite set of HoBHC(SLA).

As in the 1st-order case, only the relations between ground terms are relevant. Therefore, we replace ground terms $M$ with (fresh) constant symbols $c_{M}$ and consider only structures in which “$\leq$” is interpreted consistently (with the meaning of the constants).

Formally, let $\mathrm{gt}_{\iota}(\Gamma)$ be the set of closed terms of type $\iota$ occurring in $\Gamma$ and we define

[TABLE]

For $\mathcal{A}\in\mathfrak{A}$, let $\mathcal{A}^{\flat}$ be the 1-order $\Sigma^{\flat}$-structure defined by

[TABLE]

for $M,N\in\mathrm{gt}_{\iota}(\Gamma)$, and let $\mathfrak{A}^{\flat}\coloneqq\{\mathcal{A}^{\flat}\mid\mathcal{A}\in\mathfrak{A}\}$.

Furthermore, for simple atoms $x\leq M$ and $M\leq x$, we set ${(x\leq M)^{\flat}}\coloneqq{x\leq c_{M}}$ and ${(M\leq x)^{\flat}}\coloneqq{c_{M}\leq x}$. For all other atoms $A$ (i.e. $x\leq y$ or foreground atoms) we set $A^{\flat}\coloneqq A$; we lift $\cdot^{\flat}$ in the obvious way to clauses181818i.e. ${(\neg A_{1}\lor\cdots\lor\neg A_{n}\lor(\neg)A)^{\flat}}\coloneqq\neg A_{1}^{\flat}\lor\cdots\lor\neg A_{n}^{\flat}\lor(\neg)A^{\flat}$ and define $\Gamma^{\flat}\coloneqq\{C^{\flat}\mid C\in\Gamma\}$. Note that $\Gamma^{\flat}$ is a set of HoCHCs for $\Sigma^{\flat}$ and $(\Sigma^{\prime})^{\flat}$, and that $\mathfrak{A}^{\flat}$ is finite.

Clearly, there is an inverse $\cdot^{\sharp}$ of $\cdot^{\flat}$ on formulas, e.g. satisfying $(x\leq c_{M})^{\sharp}=(x\leq M)$.

Now, suppose $\mathcal{A}\in\mathfrak{A}$. Then valuations $\alpha$ over (a frame induced by) ${\mathcal{A}^{\flat}}\llbracket\iota\rrbracket$ naturally correspond to valuations $\alpha^{\sharp}$ over ${\mathcal{A}}\llbracket\iota\rrbracket$ by evaluating ground terms191919precisely, $\alpha^{\sharp}(x)={\mathcal{A}}\llbracket\alpha(x)\rrbracket$ for $x:\iota\in\Delta$ and it holds ${\mathcal{A}}\llbracket\varphi\rrbracket(\alpha^{\sharp})={\mathcal{A}^{\flat}}\llbracket\varphi^{\flat}\rrbracket(\alpha)$ for simple background atoms $\varphi$.

Conversely, for valuations $\alpha$ and $\alpha^{\flat}$ (over ${\mathcal{A}}\llbracket\iota\rrbracket$ and ${\mathcal{A}^{\flat}}\llbracket\iota\rrbracket$, respectively) satisfying

[TABLE]

[TABLE]

for $x:\iota\in\Delta$, it holds ${\mathcal{A}}\llbracket\varphi\rrbracket(\alpha)\leq{\mathcal{A}^{\flat}}\llbracket\varphi^{\flat}\rrbracket(\alpha^{\flat})$ if $\mathrm{gt}_{\iota}(\varphi)\subseteq\mathrm{gt}_{\iota}(\Gamma)$. Therefore:

Lemma 52**.**

Let $\Gamma^{\prime}$ be a set of goal clauses of simple background atoms satisfying $\mathrm{gt}_{\iota}(\Gamma^{\prime})\subseteq\mathrm{gt}_{\iota}(\Gamma)$.

Then $\Gamma^{\prime}$ is $\mathfrak{A}$-satisfiable iff $(\Gamma^{\prime})^{\flat}$ is $\mathfrak{A}^{\flat}$-satisfiable.

Lemma 53**.**

Let $\Gamma^{\prime}$ be a set of HoBHC(SLA) satisfying $\mathrm{gt}_{\iota}(\Gamma^{\prime})\subseteq\mathrm{gt}_{\iota}(\Gamma)$. Then

1. (ii)

$\Gamma^{\prime}\vdash_{\mathfrak{A}}\Gamma^{\prime}\cup\{G\}$* implies $(\Gamma^{\prime})^{\flat}\vdash_{\mathfrak{A}^{\flat}}(\Gamma^{\prime})^{\flat}\cup\{G^{\flat}\}$* 2. (ii)

$(\Gamma^{\prime})^{\flat}\vdash_{\mathfrak{A}^{\flat}}(\Gamma^{\prime})^{\flat}\cup\{G\}$* implies $\Gamma^{\prime}\vdash_{\mathfrak{A}}\Gamma^{\prime}\cup\{G^{\sharp}\}$.*

The proof of the Completeness Thm. 43 can be strengthened (Thm. 87 in Sec. -F2) to yield:

Proposition 54**.**

If $\Gamma$ is $\mathfrak{A}$-unsatisfiable then $\Gamma\vdash_{\mathfrak{A}}^{*}\Gamma^{\prime}\cup\{\bot\}$ for some $\Gamma^{\prime}$.

Consequently, if $\Gamma$ is $\mathfrak{A}$-unsatisfiable then $\Gamma\vdash_{\mathfrak{A}}^{*}\Gamma^{\prime}\cup\{\bot\}$ for some $\Gamma^{\prime}$. It is easy to see that sets $\Gamma^{\prime}$ of HoBHC(SLA) satisfying $\mathrm{gt}_{\iota}(\Gamma^{\prime})\subseteq\mathrm{gt}_{\iota}(\Gamma)$ are closed under the rules of the proof system (Lemma 86). Hence, by (ii), $\Gamma^{\flat}\vdash_{\mathfrak{A}^{\flat}}^{*}(\Gamma^{\prime})^{\flat}\cup\{\bot\}$ and therefore by soundness (Prop. 25), $\Gamma^{\flat}$ is $\mathfrak{A}^{\flat}$-unsatisfiable.

The converse can be derived similarly and we conclude:

Proposition 55**.**

$\Gamma$* is $\mathfrak{A}$-satisfiable iff $\Gamma^{\flat}$ is $\mathfrak{A}^{\flat}$-satisfiable.*

Finally, $\mathfrak{A}^{\flat}$, which is finite, can be effectively obtained as a result of the decidability of Linear Integer Arithmetic (or Presburger arithmetic) [32]. Moreover, for every $\mathcal{A}^{\flat}\in\mathfrak{A}^{\flat}$ and type $\sigma$, ${\mathcal{A}^{\flat}}\llbracket\sigma\rrbracket$ is finite. Hence, by Remark 49, we obtain:

Theorem 56**.**

Let $\Gamma$ be a finite set of HoBHC(SLA). It is decidable if there is a $\Sigma^{\prime}$-expansion $\mathcal{B}$ of $\mathcal{A}_{\operatorname{LIA}}$ satisfying $\mathcal{B}\models\Gamma$.

IX Related Work

Higher-order Automated Theorem Proving

There is a long history of resolution-based procedures for higher-order logic without background theories which are refutationally complete for Henkin semantics e.g. [11, 12, 13, 14]. Furthermore, a tableau-style proof system has been proposed [33]. Their completeness proofs construct countable Henkin models out of terms in case the proof system is unable to refute a problem. Hence, these proofs do not seem to be extendable to provide standard models when restricted to HoCHCs.

Furthermore, there are efforts to extend SMT solvers to higher-order logic [34, 35] but the techniques seem to be incomplete even for Henkin semantics.

Theorem Proving for 1st-order Logic Modulo Theories

In the 1990s, superposition [36]—the basis of most state-of-the-art theorem provers [37, 38]—was extended to a setting with background theories [19, 39]. The proof system is sound and complete, assuming a compact background theory and some technical conditions. Abstractly, their proof system is very similar to ours: there is a clear separation between logical / foreground reasoning and reasoning in the background theory. Moreover, the search is directed purely by the former whilst the latter is only used in a final step to check satisfiability of a conjunction of theory atoms.

Defunctionalisation

Our translation to 1st-order logic (Sec. VII) resembles Reynolds’ defunctionalisation [40]. A whole-program transformation, defunctionalisation reduces higher-order functional programs to 1st-order ones. It eliminates higher-order features, such as partial applications and $\lambda$-abstractions, by storing arguments in data types and recovering them in an application function, which performs a matching on the data type.

Recently, the approach was adapted to the satisfiability problem for HoCHC [41] and implemented in the tool DefMono202020see http://mjolnir.cs.ox.ac.uk/dfhochc/: given a set of HoCHCs, it generates an equi-satisfiable set of 1st-order Horn clauses over the original background theory and additionally the theory of data types. By contrast, our translation is purely logical, directly yielding 1st-order Horn clauses, without recourse to inductive data types.

Extensional Higher-order Logic Programming

The aim of higher-order logic programming is not only to establish satisfiability of a set of Horn clauses without background theories but also to find (representatives of) “answers to queries”, i.e. witnesses that goal clauses are falsified in every model of the definite clauses. Thus, [16] proposes a rather complicated domain-theoretic semantics (equivalent to the continuous semantics [16, Prop. 5.14]). They design a resolution-based proof system that supports a strong notion of completeness ([16, Thm. 7.38]) with respect to this semantics.

Their proof system is more complicated because it operates on more general formulas (which are nonetheless translatable to clauses). Moreover it requires the instantiation of variables with certain terms, which we avoid by implicitly instantiating all remaining relational variables with $\top_{\rho}$ in the constraint refutation rule.

Refinement Type Assignments

[1] also introduces a refinement type system, the aim of which is to automate the search for models. In this respect, the approach is orthogonal to our resolution proof system, which can be used to refute all unsatisfiable problems (but might fail on satisfiable instances). However, for satisfiable clause sets the method by [1], which is implemented in the tool Horus212121see http://mjolnir.cs.ox.ac.uk/horus/, may also be unable to generate models.

X Conclusion and Future Directions

In sum, HoCHC lies at a “sweet spot” in higher-order logic, semantically robust and useful for algorithmic verification.

Future work

We expect that our proof system’s robustness on satisfiable instances can be improved by tightening the rules (cf. Sec. IX) or combining it with a search for models [1, 42, 43]. Crucially, soundness and completeness even for standard semantics can be retained thanks to HoCHC’s semantic invariance. To facilitate comparison of approaches, it would also be important to obtain an implementation of our techniques and conduct an empirical evaluation.

On the more theoretical side it would be interesting to identify extensions of HoCHC sharing its excellent properties.

Acknowledgments

We gratefully acknowledge support of EPSRC grants EP/N509711/1 and EP/M023974/1.

-A Supplementary Materials for Sec. II

-A1 Supplementary Materials for Sec. II-A

The following lemma is completely standard and can be proven by a routine structural induction (exploiting the variable convention).

Lemma 57** (Substitution).**

Let $\mathcal{F}$ be a pre-frame, $\mathcal{A}$ be a $(\Sigma,\mathcal{F})$-structure and $\alpha$ be a $(\Delta,\mathcal{F})$-valuation. Furthermore, let $x\in\operatorname{dom}(\Delta)$ and let $M$ and $N$ be terms such that $\Delta\vdash N:\Delta(x)$. Then ${\mathcal{A}}\llbracket M[N/x]\rrbracket(\alpha)={\mathcal{A}}\llbracket M\rrbracket(\alpha[x\mapsto{\mathcal{A}}\llbracket N\rrbracket(\alpha)])$.

The following lemma states that in frames, the denotation is stable under $\beta$- and $\eta$-conversion.

Lemma 58**.**

Let $\mathcal{F}$ be a frame, let $M$ and $M^{\prime}$ be $\Sigma$-terms, $\mathcal{A}$ be a $(\Sigma,\mathcal{F})$-structure and let $\alpha$ be a $(\Delta,\mathcal{F})$-valuation. Then

1. (ii)

if $M\rightarrow_{\beta}M^{\prime}$ then ${\mathcal{A}}\llbracket M\rrbracket(\alpha)={\mathcal{A}}\llbracket M^{\prime}\rrbracket(\alpha)$; 2. (ii)

if $M\rightarrow_{\eta}M^{\prime}$ then ${\mathcal{A}}\llbracket M\rrbracket(\alpha)={\mathcal{A}}\llbracket M^{\prime}\rrbracket(\alpha)$.

Proof.

We prove the lemma by induction on the compatible closure. The only interesting cases are the base cases $((\lambda x\ldotp N)N^{\prime},N[N^{\prime}/x])\in\beta$ and $(\lambda y\ldotp L\,y,L)\in\eta$, respectively. Then

[TABLE]

because of the fact that $\mathcal{F}$ is a frame and Lemma 57, and

[TABLE]

because $\mathcal{F}$ is a frame. ∎

-A2 Supplementary Materials for Sec. II-C

Let $\Gamma$ be a finite set of HoCHCs. W.l.o.g. we can assume that for each $R\in\Sigma^{\prime}\setminus\Sigma$ there is at least one Horn clause $G\lor R\,\overline{x}_{R}$ and each definite clause has this form.

For a goal clause $G=\neg A_{1}\lor\cdots\lor\neg A_{n}$ let $\operatorname{posex}(G,V)\coloneqq\exists y_{1},\ldots,y_{m}\ldotp A_{1}\land\cdots\land A_{n}$, where $\{y_{1},\ldots,y_{m}\}=\operatorname{fv}(G)\setminus V$ and $\operatorname{posex}(G)\coloneqq\operatorname{posex}(G,\emptyset)$. Clearly, $\operatorname{posex}(G)$ is a positive existential closed formula. Let $\Pi_{\Gamma}$ be the set of definite formulas

[TABLE]

where $G_{R,1}\lor R\,\overline{x}_{R},\ldots,G_{R,n}\lor R\,\overline{x}_{R}$ are the unnegated occurrences of $R\,\overline{x}_{R}$ in $\Gamma$ and $R\in\Sigma^{\prime}\setminus\Sigma$. Clearly, $\Pi_{\Gamma}$ is a program. Furthermore, the following is obvious by definition:

Lemma 59**.**

Let $\Gamma$ be a finite set of HoCHCs, $\mathcal{F}$ a frame and $\mathcal{B}$ a $(\Sigma^{\prime},\mathcal{F})$-expansion of $\mathcal{A}$.

Then $\mathcal{B}\models\{D\in\Gamma\mid D\text{ definite}\}$ iff $\mathcal{B}\models\Pi_{\Gamma}$.

-A3 $\mathcal{S}$, $\mathcal{M}$ and $\mathcal{C}$ are Complete Frames

First, note that $\precsim$ (as defined in Def. 30) and $\sqsubseteq$ coincide for the continuous frame.

Lemma 60**.**

Let $\sqsubseteq$ be the pointwise ordering on $\mathcal{C}$ and $\precsim$ be the relation defined in Def. 30. Then ${\precsim}={\sqsubseteq}$.

Proof.

We prove by induction on $\sigma$ that ${\precsim_{\sigma}}={\sqsubseteq_{\sigma}}$. For $\iota$ and $o$ this is obvious. Hence, suppose $\sigma=\tau\to\sigma^{\prime}$ and let $r,r^{\prime}\in{\mathcal{C}}\llbracket\tau\to\sigma^{\prime}\rrbracket$.

First, suppose $r\precsim r^{\prime}$. Let $s\in{\mathcal{C}}\llbracket\tau\rrbracket$ be arbitrary. By the inductive hypothesis, $s\precsim s$ ($\sqsubseteq$ is reflexive). Thus, $\{s\}\in\operatorname{dir}_{\precsim}(s)$ and therefore, $r(s)\precsim r^{\prime}(s)$. Again by the inductive hypothesis, $r(s)\sqsubseteq r^{\prime}(s)$. Consequently, $r\sqsubseteq r^{\prime}$.

Conversely, suppose $r\sqsubseteq r^{\prime}$. Let $s\in{\mathcal{C}}\llbracket\tau\rrbracket$ and $\mathfrak{S}^{\prime}\in\operatorname{dir}_{\precsim}(s)$ be arbitrary. By the inductive hypothesis, $s\sqsubseteq\bigsqcup\mathfrak{S}^{\prime}$ and $\mathfrak{S}^{\prime}$ is $\sqsubseteq$-directed. Hence,

[TABLE]

exploiting the monotonicity of $r$, the continuity of $r^{\prime}$ and the fact that $r\sqsubseteq r^{\prime}$. Again by the inductive hypothesis, $r(s)\precsim\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime}(s^{\prime})$. Therefore, $r\precsim r^{\prime}$. ∎

Lemma 61**.**

Let $\Sigma$ be a signature, $\Delta$ be a type environment and $\mathcal{B}$ be a $(\Sigma,\mathcal{C})$-structure. Then for any positive existential term $M$, $(\Delta,\mathcal{C})$-valuation $\alpha$ and $\mathfrak{a}^{\prime}\in\operatorname{dir}_{\precsim}(\alpha)$,

1. (ii)

if $M$ is a $\lambda$-abstraction $\Delta\vdash\lambda x\ldotp M^{\prime}:\tau\to\rho$ then for every $s\in{\mathcal{B}}\llbracket\tau\rrbracket$, ${\mathcal{B}}\llbracket M\rrbracket(\alpha)(s)={\mathcal{B}}\llbracket M^{\prime}\rrbracket(\alpha[x\mapsto s])$, and 2. (ii)

${\mathcal{B}}\llbracket M\rrbracket(\alpha)\precsim\bigsqcup_{\alpha^{\prime}\in\mathfrak{a}^{\prime}}{\mathcal{B}}\llbracket M\rrbracket(\alpha^{\prime})$.

Proof.

We prove both parts of the lemma simultaneously by induction on the structure of $M$. For all cases except $\lambda$-abstractions, Part (ii) is trivially true and Part (ii) is proven as in Lemma 31.

Hence, suppose $M$ is a $\lambda$-abstraction $\Delta\vdash\lambda x\ldotp M^{\prime}:\tau\to\rho$. We define $r\coloneqq\lambda s\in{\mathcal{B}}\llbracket\tau\rrbracket\ldotp{\mathcal{B}}\llbracket M^{\prime}\rrbracket(\alpha[x\mapsto s])$

Claim 1**.**

$r\in{\mathcal{B}}\llbracket\tau\to\rho\rrbracket={\mathcal{C}}\llbracket\tau\to\rho\rrbracket$.

Proof 1*.*

First, let $s,s^{\prime}\in{\mathcal{B}}\llbracket\tau\rrbracket$ be such that $s\sqsubseteq s^{\prime}$. By the reflexivity of $\sqsubseteq$ and Lemma 60, $\{\alpha[x\mapsto s^{\prime}]\}\in\operatorname{dir}_{\precsim}(\alpha[x\mapsto s])$. Hence, by the inductive hypothesis,

[TABLE]

Consequently by Lemma 60, $r(s)\sqsubseteq r(s^{\prime})$ and $r$ is monotone.

Next, suppose that $\mathfrak{S}\subseteq{\mathcal{B}}\llbracket\tau\rrbracket$ is $\sqsubseteq$-directed. Note that by Lemma 60 and the reflexivity of $\sqsubseteq$, $\{\alpha[x\mapsto s]\mid s\in\mathfrak{S}\}\in\operatorname{dir}_{\precsim}(\alpha[x\mapsto\bigsqcup\mathfrak{S}])$. Therefore, by the inductive hypothesis

[TABLE]

Again by Lemma 60, $r(\bigsqcup\mathfrak{S})\sqsubseteq\bigsqcup_{s\in\mathfrak{S}}r(s)$. Furthermore, by monotonicity of $r$, for every $s\in\mathfrak{S}$, $r(s)\sqsubseteq r(\bigsqcup\mathfrak{S})$. Consequently, by the antisymmetry of $\sqsubseteq$, $r(\bigsqcup\mathfrak{S})=\bigsqcup_{s\in\mathfrak{S}}r(s)$.

This concludes the proof of the claim that $r:{\mathcal{B}}\llbracket\tau\rrbracket\to{\mathcal{B}}\llbracket\rho\rrbracket$ is continuous.

As a consequence of Claim 1, for every $s\in{\mathcal{B}}\llbracket\tau\rrbracket$, ${\mathcal{B}}\llbracket M\rrbracket(\alpha)(s)={\mathcal{B}}\llbracket M^{\prime}\rrbracket(\alpha[x\mapsto s])$ and the same argument as in the proof of Lemma 31 can be used to demonstrate Part (ii) of the lemma. ∎

Similarly, we get the following for the monotone frame

Lemma 62**.**

1. (ii)

${\precsim}={\sqsubseteq}$, where $\sqsubseteq$ be the pointwise ordering on $\mathcal{M}$ and $\precsim$ is the relation defined in Def. 19; 2. (ii)

If $\Sigma$ is a signature, $\Delta$ is a type environment, $\mathcal{B}$ is a $(\Sigma,\mathcal{M})$-structure, $\alpha$ is a $(\Delta,\mathcal{M})$-valuation, $\Delta\vdash\lambda x\ldotp M:\tau\to\rho$ is a positive existential $\Sigma$-term and $s\in{\mathcal{B}}\llbracket\tau\rrbracket$ then

[TABLE]

Lemmas 62 and 61 immediately imply the following (completeness is trivial):

Proposition 63**.**

$\mathcal{S}$, $\mathcal{M}$ and $\mathcal{C}$ are complete frames.

-B Supplementary Materials for Sec. III

See 17

Proof.

Since, $L$ is a set (in contrast to $\operatorname{\mathbf{On}}$) there exists $\beta\in\operatorname{\mathbf{On}}$ satisfying $a_{F}=a_{\beta}$.

1. (ii)

Thus, $F(a_{F})=a_{\beta+1}\leq a_{F}$. 2. (ii)

By what we have just shown it suffices to prove by transfinite induction on $\beta$ that $a_{\beta}\precsim b$.

• •

First, suppose $\beta=\widetilde{\beta}+1$ is a successor ordinal. By the inductive hypothesis and quasi-monotonicity of $F$, $a_{\beta}=F(a_{\widetilde{\beta}})\precsim F(b)\leq b$. Consequently by (C1), $a_{\beta}\precsim b$.

• •

Otherwise, $\beta$ is a limit ordinal and by the inductive hypothesis, $a_{\widetilde{\beta}}\precsim b$ for all $\widetilde{\beta}<\beta$. Consequently, by (C2), $a_{\beta}\precsim b$.

∎

Lemma 64**.**

$\precsim$* is compatible with $\sqsubseteq$.*

Proof.

We prove by induction on the type $\sigma$ that $\precsim_{\sigma}$ is compatible with $\sqsubseteq_{\sigma}$. For $o$ and $\iota$ this is obvious. Hence, suppose that $\sigma=\tau\to\sigma^{\prime}$.

1. (i)

Let $r,r^{\prime},r^{\prime\prime}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ be such that $r\precsim_{\sigma}r^{\prime}\sqsubseteq_{\sigma}r^{\prime\prime}$. Besides, let $s,s^{\prime}\in{\mathcal{F}}\llbracket\tau\rrbracket$ be such that $s\precsim_{\tau}s^{\prime}$. Clearly, it holds that $r(s)\precsim_{\sigma^{\prime}}r^{\prime}(s^{\prime})\sqsubseteq_{\sigma^{\prime}}r^{\prime\prime}(s^{\prime})$ and by the inductive hypothesis, $r(s)\precsim_{\sigma^{\prime}}r^{\prime\prime}(s^{\prime})$. Hence, $r\precsim_{\sigma}r^{\prime\prime}$. 2. (ii)

Let $r^{\prime}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ and $\mathfrak{R}\subseteq\{r\in{\mathcal{F}}\llbracket\sigma\rrbracket\mid r\precsim_{\sigma}r^{\prime}\}$ be arbitrary. Suppose $s,s^{\prime}\in{\mathcal{F}}\llbracket\tau\rrbracket$ are such that $s\precsim_{\tau}s^{\prime}$. By definition, $\{r(s)\mid r\in\mathfrak{R}\}\subseteq\{t\in{\mathcal{F}}\llbracket\sigma^{\prime}\rrbracket\mid t\precsim_{\sigma^{\prime}}r^{\prime}(s^{\prime})\}$. Therefore, by the inductive hypothesis, $\left(\bigsqcup\mathfrak{R}\right)(s)=\bigsqcup_{r\in\mathfrak{R}}r(s)\precsim_{\sigma^{\prime}}r^{\prime}(s^{\prime})$. Consequently, $\bigsqcup\mathfrak{R}\precsim_{\sigma}r^{\prime}$.∎

See 22

Proof.

We prove the claim by induction on the structure of $M$.

• •

If $M$ is a variable $x$ then ${\mathcal{B}}\llbracket M\rrbracket(\alpha)=\alpha(x)\precsim\alpha^{\prime}(x)={\mathcal{B}^{\prime}}\llbracket M\rrbracket(\alpha^{\prime})$ because of $\alpha\precsim\alpha^{\prime}$.

• •

If $M$ is a logical symbol (other than $\neg$) then this is a consequence of (ii).

• •

If $M$ is a symbol $R\in\Sigma^{\prime}$ then ${\mathcal{B}}\llbracket M\rrbracket(\alpha)=R^{\mathcal{B}}\precsim R^{\mathcal{B}^{\prime}}={\mathcal{B}^{\prime}}\llbracket M\rrbracket(\alpha^{\prime})$ because of $\mathcal{B}\precsim\mathcal{B}^{\prime}$.

• •

If $M$ is an application $N\,N^{\prime}$ then by the inductive hypothesis ${\mathcal{B}}\llbracket N\rrbracket(\alpha)\precsim{\mathcal{B}^{\prime}}\llbracket N\rrbracket(\alpha^{\prime})$ and ${\mathcal{B}}\llbracket N^{\prime}\rrbracket(\alpha)\precsim{\mathcal{B}^{\prime}}\llbracket N^{\prime}\rrbracket(\alpha^{\prime})$. Therefore, by definition of $\precsim$,

[TABLE]

• •

Finally, suppose $M$ is an abstraction $\lambda x\ldotp N$. Let $s\precsim s^{\prime}$. By the inductive hypothesis ${\mathcal{B}}\llbracket N\rrbracket(\alpha[x\mapsto s])\precsim{\mathcal{B}^{\prime}}\llbracket N\rrbracket(\alpha^{\prime}[x\mapsto s^{\prime}])$ and hence,

[TABLE]

because $\mathcal{F}$ is a frame. Due to the fact that this holds for every $s\precsim s^{\prime}$, ${\mathcal{B}}\llbracket M\rrbracket(\alpha)\precsim{\mathcal{B}^{\prime}}\llbracket M\rrbracket(\alpha^{\prime})$.∎

-C Supplementary Materials for Sec. IV

Lemma 65**.**

Let $\varphi_{1},\ldots,\varphi_{n}$ be background atoms. Then $\neg x_{1}\,\overline{M}_{1}\lor\neg x_{m}\,\overline{M}_{m}\lor\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}\models\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}$.

Proof.

Let $\mathcal{F}$ be a frame and suppose $\mathcal{B}$ is an arbitrary $(\Sigma^{\prime},\mathcal{F})$-structure satisfying

[TABLE]

Let $\alpha$ be an arbitrary $(\Delta,\mathcal{F})$-valuation. We define another $(\Delta,\mathcal{F})$-valuation $\alpha^{\prime}$ by

[TABLE]

Clearly, $\mathcal{B},\alpha^{\prime}\not\models\neg x_{1}\,\overline{M}_{1}\lor\neg x_{m}\,\overline{M}_{m}$. Hence, by Eq. 2, $\mathcal{B},\alpha^{\prime}\models\neg\varphi_{i}$ for some $i$. Note that by Remark 2, $\varphi_{i}$ only contains variables of type $\iota$. Hence, also $\mathcal{B},\alpha\models\neg\varphi_{i}$. This proves, $\mathcal{B}\models\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}$. ∎

Now, Prop. 25 is a simple consequence of the following:

Lemma 66**.**

Let $\Gamma^{\prime}$ be a set of HoCHCs and suppose that $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{C\}$. Then

1. (ii)

if $C\neq\bot$ then $\Gamma^{\prime}\models C$; 2. (ii)

if $\mathcal{B}$ is an expansion of $\mathcal{A}$ and $\mathcal{B}\models\Gamma^{\prime}$ then $\mathcal{B}\models C$.

Proof.

1. (i)

Note that by assumption the constraint refutation rule cannot have been applied. Besides, for $\beta$-reduction this is a consequence of (ii). Finally, suppose that $\neg R\,\overline{M}\lor G$ and $G^{\prime}\lor R\,\overline{x}$ are in $\Gamma^{\prime}$ (modulo renaming of variables). The proof for this case uses the same ideas as the classic one for 1st-order logic (see e.g. [3, 44]): 2. (ii)

Let $\mathcal{B}$ be an expansion of $\mathcal{A}$ satisfying $\mathcal{B}\models\Gamma^{\prime}$. By Part (ii) it suffices to consider the case when the constraint refutation rule is applicable to some goal clause $\neg x_{1}\,\overline{M}_{1}\lor\neg x_{m}\,\overline{M}_{m}\lor\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}$, where each $\varphi_{i}$ is a background atom and there exists a valuation $\alpha$ such that $\mathcal{A},\alpha\models\varphi_{1}\land\cdots\land\varphi_{n}$. However, by Lemma 65, $\mathcal{B},\alpha\models\neg\varphi_{1}\lor\cdots\lor\neg\varphi_{n}$, which is clearly a contradiction to the fact that $\mathcal{B}$ is an expansion of $\mathcal{A}$.∎

-C1 Supplementary Materials for Sec. IV-A

Lemma 67**.**

If $\precsim$ is compatible with $\leq$ and $F$ is quasi-continuous then for all ordinals $\beta$, $a_{\beta}\precsim a_{\beta}$.

Proof.

• •

If $\beta=\widetilde{\beta}+1$ is a successor ordinal then by the inductive hypothesis, $\{a_{\widetilde{\beta}}\}\in\operatorname{dir}(a_{\widetilde{\beta}})$ and by quasi-continuity, $a_{\beta}=F(a_{\widetilde{\beta}})\precsim F(a_{\widetilde{\beta}})=a_{\beta}$.

• •

If $\beta$ is a limit ordinal then by the inductive hypothesis for all $\widetilde{\beta}<\beta$, $a_{\widetilde{\beta}}\precsim a_{\widetilde{\beta}}$, and by definition, $a_{\widetilde{\beta}}\leq a_{\beta}$. By (C1), $a_{\widetilde{\beta}}\precsim a_{\beta}$ (for all $\widetilde{\beta}<\beta$) and thus by (C2), $a_{\beta}\precsim a_{\beta}$.∎

See 29

Proof.

1. (ii)

We prove by transfinite induction on $\beta$ that for all $\beta^{\prime}\geq\beta$, $a_{\beta}\precsim a_{\beta^{\prime}}$.

• •

First, suppose $\beta=\widetilde{\beta}+1\leq\beta^{\prime}$ is a successor ordinal. If $\beta^{\prime}=\beta^{\prime\prime}+1$ is a successor ordinal, too, then $\widetilde{\beta}\leq\beta^{\prime\prime}$. Therefore, by the inductive hypothesis and Lemma 67, $\{a_{\beta^{\prime\prime}}\}\in\operatorname{dir}(a_{\widetilde{\beta}})$. By quasi-continuity of $F$, $a_{\beta}=F(a_{\widetilde{\beta}})\precsim F(a_{\beta^{\prime\prime}})=a_{\beta^{\prime}}$.

Otherwise, $\beta^{\prime}$ is a limit ordinal and $\beta<\beta^{\prime}$. By Lemma 67 and definition, $a_{\beta}\precsim a_{\beta}\leq a_{\beta^{\prime}}$. Hence, by (C1), $a_{\beta}\precsim a_{\beta^{\prime}}$.

• •

Finally, suppose $\beta$ is a limit ordinal. By the inductive hypothesis for every $\widetilde{\beta}<\beta$, $a_{\widetilde{\beta}}\precsim a_{\beta^{\prime}}$ and thus by (C2), $a_{\beta}\precsim a_{\beta^{\prime}}$. 2. (ii)

Next, we prove by transfinite induction that for every ordinal $\beta$, $a_{\beta}\precsim a_{\omega}$. Then the claim follows from (C2).

• •

First, suppose that $\beta=\beta^{\prime}+1$ is a successor ordinal. By the inductive hypothesis, $a_{\beta^{\prime}}\precsim a_{\omega}$. Therefore (also using the first part), $\{a_{n}\mid n\in\omega\}\in\operatorname{dir}_{\precsim}(a_{\beta^{\prime}})$. Thus, by quasi-continuity, $a_{\beta}=F(a_{\beta^{\prime}})\precsim\bigvee_{n\in\omega}F(a_{n})=a_{\omega}$.

• •

Next, suppose that $\beta$ is a limit ordinal. By the inductive hypothesis, $a_{\beta^{\prime}}\precsim a_{\omega}$ for every $\beta^{\prime}<\beta$. Therefore, by (C2), $a_{\beta}\precsim a_{\omega}$.∎

Lemma 68**.**

$\precsim$* is compatible with $\sqsubseteq$.*

Proof.

We prove by induction on the type $\sigma$ that $\precsim_{\sigma}$ is compatible with $\sqsubseteq_{\sigma}$. For $o$ and $\iota$ this is obvious. Hence, suppose that $\sigma=\tau\to\sigma^{\prime}$.

1. (i)

Let $r,r^{\prime},r^{\prime\prime}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ be such that $r\precsim_{\sigma}r^{\prime}\sqsubseteq_{\sigma}r^{\prime\prime}$. Besides let $s\in{\mathcal{F}}\llbracket\tau\rrbracket$ and $\mathfrak{S}^{\prime}\in\operatorname{dir}_{\precsim}(s)$ be arbitrary. Clearly, it holds that $r(s)\precsim_{\sigma^{\prime}}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime}(s^{\prime})\sqsubseteq_{\sigma^{\prime}}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime\prime}(s^{\prime})$. Hence, by the inductive hypothesis, $r(s)\precsim_{\sigma^{\prime}}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime\prime}(s^{\prime})$. Consequently, $r\precsim_{\sigma}r^{\prime\prime}$. 2. (ii)

Let $r^{\prime}\in{\mathcal{F}}\llbracket\sigma\rrbracket$ and $\mathfrak{R}\subseteq\{r\in{\mathcal{F}}\llbracket\sigma\rrbracket\mid r\precsim_{\sigma}r^{\prime}\}$ be arbitrary. Besides, suppose $s\in{\mathcal{F}}\llbracket\tau\rrbracket$ and $\mathfrak{S}^{\prime}\in\operatorname{dir}_{\precsim}(s)$. Clearly, $\{r(s)\mid r\in\mathfrak{R}\}\subseteq\{t\in{\mathcal{F}}\llbracket\sigma^{\prime}\rrbracket\mid t\precsim_{\sigma^{\prime}}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime}(s^{\prime})\}$ and hence by the inductive hypothesis, $\left(\bigsqcup\mathfrak{R}\right)(s)=\bigsqcup_{r\in\mathfrak{R}}r(s)\precsim_{\sigma^{\prime}}\bigsqcup_{s^{\prime}\in\mathfrak{S}^{\prime}}r^{\prime}(s^{\prime})$. Consequently, $\bigsqcup\mathfrak{R}\precsim_{\sigma}r^{\prime}$.∎

The relation $\precsim$ is transitive but neither reflexive ((ii)) nor antisymmetric and coincides with the pointwise ordering $\sqsubseteq$ on the continuous frame $\mathcal{C}$ (Lemma 60).

Example 69**.**

1. (ii)

For all relational types $\rho$ and $s\in{\mathcal{F}}\llbracket\rho\rrbracket$, $\bot_{\rho}\precsim s\precsim\top_{\rho}$. 2. (ii)

$\operatorname{or}\precsim\operatorname{or}$* and $\operatorname{and}\precsim\operatorname{and}$.* 3. (ii)

Next, suppose $r\in{\mathcal{F}}\llbracket\tau\to o\rrbracket$, $\mathfrak{R}^{\prime}\in\operatorname{dir}(r)$ and $s\in{\mathcal{F}}\llbracket\tau\rrbracket$ are such that $r(s)=1$. If $\tau=\iota$ then $r^{\prime}(s)=1$ for all $r^{\prime}\in\mathfrak{R}^{\prime}$. Otherwise, there exists $r^{\prime}\in\mathfrak{R}^{\prime}$ satisfying $r^{\prime}(\top_{\tau})=1$ because $\{\top_{\tau}\}\in\operatorname{dir}(s)$. Consequently, $\operatorname{exists}_{\tau}\precsim\operatorname{exists}_{\tau}$ holds as well. 4. (ii)

$\delta_{\omega}\precsim\delta_{\omega}$* does not hold (see Ex. 27): clearly $\{r_{n}\mid n\in\mathbb{N}\}\in\operatorname{dir}(r_{\omega})$ but $\delta_{\omega}(r_{\omega})=1>0=\max\{\delta_{\omega}(r_{n})\mid n\in\mathbb{N}\}$. This shows that $\precsim$ is not reflexive.*

See 31

Proof.

We prove that for all positive existential terms $M$, expansions $\mathcal{B}$ of $\mathcal{A}$, $\mathfrak{B}^{\prime}\in\operatorname{dir}(\mathcal{B})$, valuations $\alpha$ and $\mathfrak{a}^{\prime}\in\operatorname{dir}(\alpha)$ Eq. 1 holds by induction on the structure of $M$.

• •

If $M$ is a logical constant (other than $\neg$) then this is due to (ii) and (ii).

• •

If $M$ is a symbol in $\Sigma^{\prime}$ or a variable then this is by assumption.

• •

Next, suppose $M$ is an application $M_{1}\,M_{2}$. By the inductive hypothesis,

[TABLE]

Let $s\coloneqq{\mathcal{B}}\llbracket M_{2}\rrbracket(\alpha)$ and $\mathfrak{S}^{\prime}\coloneqq\{{\mathcal{B}_{2}}\llbracket M_{2}\rrbracket(\alpha_{2})\mid\mathcal{B}_{2}\in\mathfrak{B}^{\prime}\land\alpha_{2}\in\mathfrak{a}^{\prime}\}$.

Claim 1**.**

$\mathfrak{S}^{\prime}\in\operatorname{dir}(s)$.

Proof 2*.*

By Eq. 4, $s\precsim\bigsqcup\mathfrak{S}^{\prime}$. To prove that $\mathfrak{S}^{\prime}$ is directed, let $\mathcal{B}^{(1)},\mathcal{B}^{(2)}\in\mathfrak{B}^{\prime}$ and $\alpha^{(1)},\alpha^{(2)}\in\mathfrak{a}^{\prime}$. Since $\mathfrak{B}^{\prime}$ and $\mathfrak{a}^{\prime}$ are directed, $\{\mathcal{B}^{(1)}\}\in\operatorname{dir}(\mathcal{B}^{(1)})$, $\{\alpha^{(1)}\}\in\operatorname{dir}(\alpha^{(1)})$ and there are $\mathcal{B}^{\prime}\in\mathfrak{B}^{\prime}$ and $\alpha^{\prime}\in\mathfrak{a}^{\prime}$ such that $\{\mathcal{B}^{\prime}\}\in\operatorname{dir}(\mathcal{B}^{(1)})\cap\operatorname{dir}(\mathcal{B}^{(2)})$ and $\{\alpha^{\prime}\}\in\operatorname{dir}(\alpha^{(1)})\cap\operatorname{dir}(\alpha^{(2)})$. Hence, by the inductive hypothesis, ${\mathcal{B}^{(1)}}\llbracket M_{2}\rrbracket(\alpha^{(1)})\precsim{\mathcal{B}^{(1)}}\llbracket M_{2}\rrbracket(\alpha^{(1)})$ and for $j\in\{1,2\}$, ${\mathcal{B}^{(j)}}\llbracket M_{2}\rrbracket(\alpha^{(j)})\precsim{\mathcal{B}^{\prime}}\llbracket M_{2}\rrbracket(\alpha^{\prime})$.

Next, we define

[TABLE]

Claim 2**.**

$\bigsqcup\mathfrak{T}\precsim\bigsqcup\mathfrak{T}^{\prime}$.

Proof 3*.*

It suffices to prove that for every $t\in\mathfrak{T}$ there exists $t^{\prime}\in\mathfrak{T}^{\prime}$ satisfying $t\precsim t^{\prime}$. Then the claim is a consequence of (C1) and (C2).

Hence, let $\mathcal{B}_{1},\mathcal{B}_{2}\in\mathfrak{B}^{\prime}$ and $\alpha_{1},\alpha_{2}\in\mathfrak{a}^{\prime}$ be arbitrary. By directedness of $\mathfrak{B}^{\prime}$ and $\mathfrak{a}^{\prime}$, there are $\mathcal{B}^{\prime}\in\mathfrak{B}^{\prime}$ and $\alpha^{\prime}\in\mathfrak{a}^{\prime}$ such that $\{\mathcal{B}^{\prime}\}\in\operatorname{dir}(\mathcal{B}_{1})\cap\operatorname{dir}(\mathcal{B}_{2})$ and $\{\alpha^{\prime}\}\in\operatorname{dir}(\alpha_{1})\cap\operatorname{dir}(\alpha_{2})$. Therefore, again by the inductive hypothesis,

[TABLE]

Furthermore, due to $\{\mathcal{B}^{\prime}\}\in\operatorname{dir}(\mathcal{B}^{\prime})$, $\{\alpha^{\prime}\}\in\operatorname{dir}(\alpha^{\prime})$ and the inductive hypothesis, ${\mathcal{B}^{\prime}}\llbracket M_{2}\rrbracket(\alpha^{\prime})\precsim{\mathcal{B}^{\prime}}\llbracket M_{2}\rrbracket(\alpha^{\prime})$. Hence (by Eq. 6), $\{{\mathcal{B}^{\prime}}\llbracket M_{2}\rrbracket(\alpha^{\prime})\}\in\operatorname{dir}({\mathcal{B}_{2}}\llbracket M_{2}\rrbracket(\alpha_{2}))$. Therefore, by Eq. 5,

[TABLE]

Combining everything (Claims 1 and 2, Eq. 3 and [17, Prop. 2.1.4]), we obtain

[TABLE]

This concludes the proof of ${\mathcal{B}}\llbracket M_{1}M_{2}\rrbracket(\alpha)\precsim\bigsqcup_{\mathcal{B}^{\prime}\in\mathfrak{B}^{\prime},\alpha^{\prime}\in\mathfrak{a}^{\prime}}{\mathcal{B}^{\prime}}\llbracket M_{1}M_{2}\rrbracket(\alpha^{\prime})$ (because $\precsim$ is transitive).

• •

Finally, suppose $M$ is $\lambda x\ldotp M^{\prime}$. Let $s\in{\mathcal{F}}\llbracket\Delta(x)\rrbracket$ and $\mathfrak{S}^{\prime}\in\operatorname{dir}(s)$. Note that $\{\alpha^{\prime}[x\mapsto s^{\prime}]\mid\alpha^{\prime}\in\mathfrak{a}^{\prime}\land s^{\prime}\in\mathfrak{S}^{\prime}\}\in\operatorname{dir}(\alpha[x\mapsto s])$. Therefore by the inductive hypothesis,

[TABLE]

Consequently,

[TABLE]

using [17, Prop. 2.1.4] in the last step. This concludes the proof of ${\mathcal{B}}\llbracket\lambda x\ldotp M^{\prime}\rrbracket(\alpha)\precsim\bigsqcup_{\mathcal{B}^{\prime}\in\mathfrak{B}^{\prime},\alpha^{\prime}\in\mathfrak{a}^{\prime}}{\mathcal{B}^{\prime}}\llbracket\lambda x\ldotp M^{\prime}\rrbracket(\alpha^{\prime})$.

-C2 Supplementary Materials for Sec. IV-B

The relation $\rightarrow_{\parallel}$ is defined in Fig. 5.

See 33

Proof.

We prove the lemma by induction on $\rightarrow_{\parallel}$:

• •

For variables, symbols from $\Sigma$ and logical constants (other than $\neg$) this is trivial.

• •

If $M$ is a symbol $R\in\Sigma^{\prime}\setminus\Sigma$ then ${T_{\Pi}(\mathcal{B})}\llbracket R\rrbracket(\alpha)={\mathcal{B}}\llbracket\lambda\overline{x}_{R}\ldotp F_{R}\rrbracket(\alpha)$.

• •

Next, if $M$ is an application $M_{1}\,M_{2}$, $M_{1}\rightarrow_{\parallel}N_{1}$ and $M_{2}\rightarrow_{\parallel}N_{2}$ then

[TABLE]

using the inductive hypothesis in the second step.

• •

Finally, if $M$ is a $\lambda$-abstraction $\lambda x\ldotp M^{\prime}$ and $M^{\prime}\rightarrow_{\parallel}N^{\prime}$ then

[TABLE]

exploiting the fact that $\mathcal{F}$ is a frame and the inductive hypothesis.∎

Definition 70**.**

A positive existential formula $F$ is ex-normal if for all subterms $\exists M$ of $F$, $M$ is a $\lambda$-abstraction.

Lemma 71** (Basic properties of $\rightarrow_{\beta\upsilon}$).**

Suppose $M\rightarrow_{\beta\upsilon}N$. Then

1. (ii)

$\rightarrow_{\parallel}\;\subseteq\;\twoheadrightarrow_{\beta\upsilon}$, 2. (ii)

$\operatorname{fv}(N)\subseteq\operatorname{fv}(M)$, 3. (ii)

if $M$ is ex-normal then $N$ is ex-normal, too.

Proof.

1. (ii)

Straightforward induction on the definition of $\rightarrow_{\parallel}$. 2. (ii)

We prove the first part of the lemma by induction on the compatible closure of $\rightarrow_{\beta\upsilon}$. If $(M,N)\in\beta$ this is a standard fact of $\beta$-reduction. If $(M,N)\in\upsilon$ then $\operatorname{fv}(M)=\operatorname{fv}(N)=\emptyset$. In the inductive cases the claim immediately follows from the inductive hypothesis. 3. (ii)

We prove the claim by induction on the compatible closure of $\rightarrow_{\beta\upsilon}$.

• •

First, suppose that $(R,\lambda\overline{x}_{R}\ldotp F_{R})\in\upsilon$. Obviously, $F_{R}$ is ex-normal and hence, $\lambda\overline{x}_{R}\ldotp F_{R}$ is ex-normal, too.

• •

Next, suppose that $((\lambda x\ldotp M)M^{\prime},M[M^{\prime}/x])\in\beta$. Clearly, $M$ and $M^{\prime}$ must be ex-normal. We prove by induction on $M$ that $M[M^{\prime}/x]$ is ex-normal. If $M$ is a variable this is obvious (because $M^{\prime}$ is ex-normal). The cases for (logical) constants and $\lambda$-abstractions are straightforward.

Finally, suppose that $M$ is an application and let $\exists L$ be a subterm of

[TABLE]

By the inductive hypothesis, both $M_{1}[M^{\prime}/x]$ and $M_{2}[M^{\prime}/x]$ are ex-normal. Hence, if $\exists K$ is a subterm of either $M_{1}[M^{\prime}/x]$ or $M_{2}[M^{\prime}/x]$ then $K$ must be a $\lambda$-abstraction. Otherwise $M_{1}=\exists$ and $K=M_{2}[M^{\prime}/x]$. Then by assumption $M_{2}$ is a $\lambda$-abstraction and clearly, $M_{2}[M^{\prime}/x]$ is a $\lambda$-abstraction, too.

• •

Next, suppose that $M_{1}M_{2}\rightarrow_{\beta\upsilon}N_{1}M_{2}$ because $M_{1}\rightarrow_{\beta\upsilon}N_{1}$. Clearly, $M_{1}$ is ex-normal. Therefore, by the inductive hypothesis, $N_{1}$ is ex-normal. Note that $N_{1}=\exists$ is impossible. Therefore, any subterm $\exists L$ of $N_{1}M_{2}$ is either a subterm of $N_{1}$ or $M_{2}$, which are both ex-normal. Hence, $L$ is a $\lambda$-abstraction.

• •

Suppose $M_{1}M_{2}\rightarrow_{\beta\upsilon}M_{1}N_{2}$ because $M_{2}\rightarrow_{\beta\upsilon}N_{2}$. Clearly, $M_{2}$ is ex-normal. Therefore, by the inductive hypothesis, $N_{2}$ is ex-normal. Let $\exists L$ be a subterm of $M_{1}N_{2}$. If $\exists L$ is a subterm of $M_{1}$ or $N_{2}$ the argument is as in the previous case. Hence, suppose $M_{1}=\exists$ and $L=N_{2}[M^{\prime}/x]$. By assumption $M_{2}$ is a $\lambda$-abstraction. Due to $M_{2}\rightarrow_{\beta\upsilon}L$, $L$ is a $\lambda$-abstraction, too.

• •

Finally, suppose that $\lambda x\ldotp M\rightarrow_{\beta\upsilon}\lambda x\ldotp N$ because $M\rightarrow_{\beta\upsilon}N$. Clearly, $M$ is ex-normal and hence by the inductive hypothesis $N$ is ex-normal. Let $\exists L$ be a subterm of $\lambda x\ldotp N$. Obviously, $\exists L$ must be a subterm of $M$, which is ex-normal. Hence, $L$ is a $\lambda$-abstraction.∎

Lemma 72** (Subject Reduction).**

Let $\Delta\vdash M:\sigma$ be a term such that $M\rightarrow_{\beta\upsilon}N$. Then

1. (ii)

$\Delta\vdash N:\sigma$* and* 2. (ii)

$\sigma$* is a relational type.*

Proof.

1. (ii)

We prove the lemma by induction on the compatible closure of $\beta\upsilon$. For $(M,N)\in\beta$ this is [45, Proposition 1.2.6]. If $(R,\lambda\overline{x}_{R}\ldotp F_{R})\in\upsilon$ and $R:\overline{\tau}\to o\in\Sigma^{\prime}\setminus\Sigma$ then by convention $\Delta(\overline{x}_{R})=\overline{\tau}$ and hence, $\Delta\vdash\lambda\overline{x}_{R}\ldotp F_{R}:\overline{\tau}\to o$, too. The proofs for the recursive cases are exactly as in the proof of [45, Proposition 1.2.6]. 2. (ii)

Clearly, it suffices to prove by induction on the compatible closure of $\beta\upsilon$ that $M\rightarrow_{\beta\upsilon}N$ implies $\Delta\not\vdash M:\iota^{n}\to\iota$ for all $n\in\mathbb{N}$.

• •

If $(M,N)\in\beta\upsilon$ then clearly $\Delta\not\vdash M:\iota^{n}\to\iota$ for all $n\in\mathbb{N}$.

• •

Next, suppose $M_{1}M_{2}\rightarrow_{\beta\upsilon}N_{1}N_{2}$ due to $M_{1}\rightarrow_{\beta\upsilon}N_{1}$. Then by the inductive hypothesis $\Delta\not\vdash M_{1}:\iota^{n}\to\iota$ for all $n\in\mathbb{N}$. Hence, clearly $\Delta\not\vdash M_{1}M_{2}:\iota^{m}\to\iota$ for all $m\in\mathbb{N}$.

• •

Suppose $M_{1}M_{2}\rightarrow_{\beta\upsilon}N_{1}N_{2}$ due to $M_{2}\rightarrow_{\beta\upsilon}N_{2}$ and assume towards contradiction that $\Delta\vdash M_{1}M_{2}:\iota^{n}\to\iota$. Then $\Delta\vdash M_{1}:\sigma\to\iota^{n}\to\iota$ and $\Delta\vdash M_{2}:\sigma$ for some $\sigma$. However, by the definition of types this implies $\sigma=\iota$, which contradicts the inductive hypothesis.

• •

Finally, if $\lambda x\ldotp M^{\prime}\rightarrow_{\beta\upsilon}\lambda x\ldotp N$ then clearly $\Delta\not\vdash\lambda x\ldotp M^{\prime}:\iota^{n}\to\iota$ for all $n\in\mathbb{N}$.∎

-C3 Supplementary Materials for Sec. IV-C

Lemma 73** (Basic Properties of \mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}).**

Let $L,M,N$ and $Q$ be terms. Then

1. (ii)

\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}* is reflexive and transitive;* 2. (ii)

\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\;\subseteq\;\twoheadrightarrow_{\beta\upsilon}; 3. (ii)

if M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 0}}}{\scriptstyle\ell\,}}N then $M=N$; 4. (ii)

if L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[25.1945pt]{\scriptstyle m+1}}}{\scriptstyle\ell\,}}N then there exists $M$ satisfying L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N; 5. (ii)

if $M\,Q$ is a term and M\,\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N then M\,Q\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N\,Q; 6. (ii)

if $M[Q/z]$ is a term and M\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N then M[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N[Q/z].

Proof.

1. (ii)

Completely trivial. 2. (ii)

Straightforward induction on the definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}} 3. (ii)

Straightforward induction on the definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 0}}}{\scriptstyle\ell\,}} 4. (ii)

Straightforward induction on the definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[25.1945pt]{\scriptstyle m+1}}}{\scriptstyle\ell\,}} 5. (ii)

Straightforward induction on the definition of M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N noting that for $\circ\in\{\land,\lor\}$ the cases M_{1}\circ M_{2}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[31.52785pt]{\scriptstyle m_{1}+m_{2}}}}{\scriptstyle\ell\,}}N_{1}\circ N_{2} and \exists x\ldotp M^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}\exists x\ldotp N^{\prime} cannot occur because $(M_{1}\circ M_{2})\,Q$ and $(\exists x\ldotp M^{\prime})\,Q$ are not terms. 6. (ii)

We prove by induction on M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N that M[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N[Q/z].

• •

If $M=N$ and $m=0$ then also M[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 0}}}{\scriptstyle\ell\,}}N[Q/z].

• •

If there exist $L$, $m_{1}$ and $m_{2}$ such that M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[18.25005pt]{\scriptstyle m_{1}}}}{\scriptstyle\ell\,}}L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[18.25005pt]{\scriptstyle m_{2}}}}{\scriptstyle\ell\,}}N and $m=m_{1}+m_{2}$ then by the inductive hypothesis M[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[18.25005pt]{\scriptstyle m_{1}}}}{\scriptstyle\ell\,}}L[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[18.25005pt]{\scriptstyle m_{2}}}}{\scriptstyle\ell\,}}N[Q/z]. Consequently, M[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N[Q/z].

• •

Next, suppose that $M$ is $M_{1}\circ M_{2}$ for $\circ\in\{\land,\lor\}$ and that there exist $m_{1}$ and $m_{2}$ such that $m=m_{1}+m_{2}$ and M_{j}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[17.47227pt]{\scriptstyle m_{j}}}}{\scriptstyle\ell\,}}N_{j} for $j\in\{1,2\}$. By the inductive hypothesis, M_{j}[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[17.47227pt]{\scriptstyle m_{j}}}}{\scriptstyle\ell\,}}N_{j}[Q/z]. Consequently,

[TABLE]

• •

Suppose that $M$ is $\exists x\ldotp M^{\prime}$ and that \exists x\ldotp M^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}\exists x\ldotp N^{\prime}. By the inductive hypothesis, M^{\prime}[Q/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}N^{\prime}[Q/z]. By the variable convention, $x\neq z$. Hence,

[TABLE]

• •

Suppose that $M$ is $R\,\overline{M}^{\prime}$ for $R\in\Sigma^{\prime}\setminus\Sigma$ and that R\,\overline{M}^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}(\lambda\overline{x}_{R}\ldotp F_{R})\overline{M}^{\prime}. Clearly,

[TABLE]

using the variable convention and the fact that $\lambda\overline{x}_{R}\ldotp F_{R}$ is closed.

• •

Finally, suppose that $M$ is $(\lambda x\ldotp M^{\prime})M^{\prime\prime}\overline{M}^{\prime\prime\prime}$ and that

[TABLE]

By the variable convention $x\neq z$. Hence

[TABLE]

using the Nested Substitution Lemma from [15, 2.1.16. Substitution Lemma].∎

Besides, the following Inversion Lemma is immediate by definition.

Lemma 74** (Inversion).**

1. (ii)

If \exists\overline{x}\ldotp E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}F then there exists $F^{\prime}$ such that $F^{\prime}=\exists\overline{x}\ldotp F^{\prime}$ and E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}F^{\prime}. 2. (ii)

If E_{1}\circ\cdots\circ E_{n}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}F, where $\circ\in\{\land,\lor\}$, then there exist $F_{1},\ldots,F_{n}$ and $m_{1},\ldots,m_{n}$ satisfying $F=F_{1}\circ\cdots\circ F_{n}$, $m=\sum_{i=1}^{n}m_{i}$ and E_{j}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[17.47227pt]{\scriptstyle m_{j}}}}{\scriptstyle\ell\,}}F_{j} for each $1\leq j\leq n$. 3. (ii)

If \exists\overline{x}\ldotp A_{1}\land\cdots\land A_{n}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}F then there exist $F_{1},\ldots,F_{n}$ and $m_{1},\ldots,m_{n}$ satisfying $F=\exists\overline{x}\ldotp F_{1}\land\cdots\land F_{n}$, $m=\sum_{i=1}^{n}m_{i}$ and A_{j}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[17.47227pt]{\scriptstyle m_{j}}}}{\scriptstyle\ell\,}}F_{j} for each $1\leq j\leq n$. 4. (ii)

If (\lambda x\ldotp K)L\overline{M}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}N then $N=K[L/x]\overline{M}$.

Lemma 75** (Basic Properties of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}).**

1. (ii)

\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}* is reflexive (on positive existential terms).* 2. (ii)

\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\;\subseteq\;\twoheadrightarrow_{\beta\upsilon}. 3. (ii)

If L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N and \overline{O}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{Q} then L\overline{O}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N\,\overline{Q}. 4. (ii)

If K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N then K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N. 5. (ii)

If L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N and O\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}Q then L[O/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N[Q/z].

Proof.

1. (ii)

We prove by structural induction on $M$ that M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M. $M$ has the form $M_{1}\cdots M_{n}$, where $M_{1}$ is either a variable, a symbol from $\Sigma^{\prime}\cup\{\land,\lor\exists_{\tau}\}$ or a $\lambda$-abstraction. In any case the inductive hypothesis and the reflexivity of \mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}} immediately yield that M_{1}\cdots M_{n}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M_{1}\cdots M_{n}.

We prove the remaining four parts by induction on the definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}. We only show the detailed proof for the case L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,\overline{N} due to L\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,\overline{M} and \overline{M}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{N} for some $\overline{M}$ (the other cases are analogous).

1. (i)

By (ii) and the inductive hypothesis, $L\twoheadrightarrow_{\beta\upsilon}x\,\overline{M}$ and $\overline{M}\twoheadrightarrow_{\beta\upsilon}\overline{N}$. Therefore clearly, $L\twoheadrightarrow_{\beta\upsilon}x\,\overline{M}\twoheadrightarrow_{\beta\upsilon}x\,\overline{N}$ and hence also, $L\twoheadrightarrow_{\beta\upsilon}x\,\overline{N}$. 2. (i)

By (ii), L\overline{O}\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,\overline{M}\,\overline{O} and hence by definition L\overline{O}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,\overline{N}\,\overline{Q}. 3. (i)

By transitivity of \mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}} ((ii)), K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,\overline{M} and hence by definition K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,\overline{N}. 4. (i)

By the inductive hypothesis, \overline{M}[O/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{N}[Q/z] and by assumption or Part (ii), x[O/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x[Q/z]. Therefore by Part (ii) and (ii),

[TABLE]

which proves L[O/z]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}(x\,\overline{N})[Q/z] by Part (ii).∎

Lemma 76** (Inversion).**

Let $E$ be an ex-normal formula.

1. (i)

If E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,\overline{N} then there exists $\overline{M}$ such that E\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,\overline{M}. 2. (i)

If E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}c\,\overline{N}, where $c\in\Sigma^{\prime}\cup\{\land,\lor,\exists_{\tau}\}$, then there exists $\overline{M}$ such that E\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}c\,\overline{M} and \overline{M}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{N}. 3. (i)

If E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\exists N then there exist $x$, $N^{\prime}$ and $M$ such that $N=(\lambda x\ldotp N^{\prime})$, E\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\exists x\ldotp M and M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N^{\prime}.

Proof.

The first two parts are obvious by definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}. Hence, suppose that E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\exists N.

By (ii) and (ii), $N$ has the form $\lambda x\ldotp N^{\prime}$ for some $N^{\prime}$. Furthermore, by Part (i) there exists $L$ such that E\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\exists_{\tau}L and L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\lambda x\ldotp N^{\prime}. Again, by (ii) and (ii), $L$ has the form $\lambda y\ldotp L^{\prime}$. By definition of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}, (\lambda y\ldotp L^{\prime})\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}(\lambda x\ldotp N^{\prime}) implies that there exists $M$ such that (\lambda y\ldotp L^{\prime})\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}(\lambda x\ldotp M) and M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N^{\prime}. However, (\lambda y\ldotp L^{\prime})\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}(\lambda x\ldotp M) clearly implies $y=x$ and $L^{\prime}=M$. Consequently, E\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\exists x\ldotp M and M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N^{\prime}. ∎

See 34

Proof.

We prove the lemma by induction on K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M.

• •

First, suppose K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,M_{1}\cdots M_{n} because for some $L_{1},\ldots,L_{n}$, K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,L_{1}\cdots L_{n} and L_{i}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M_{i} for each $i$. Clearly, $x\,M_{1}\cdots M_{n}\rightarrow_{\beta\upsilon}x\,N_{1}\cdots N_{n}$, because of $M_{j}\rightarrow_{\beta\upsilon}N_{j}$ for some $j$ and $M_{i}=N_{i}$ for $i\neq j$ are the only possible $\beta\upsilon$-reductions. By the inductive hypothesis, L_{j}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N_{j} and therefore by definition, L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,N_{1}\cdots N_{n}.

• •

Next, suppose K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}c\,\overline{M} because for some $\overline{L}$, K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}c\,\overline{L} and \overline{L}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{M}. If $c=R\in\Sigma^{\prime}\setminus\Sigma$ and $R\,\overline{M}\rightarrow_{\beta\upsilon}(\lambda\overline{x}_{R}\ldotp F_{R})\overline{M}$ then K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}R\,\overline{L}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}(\lambda\overline{x}_{R}\ldotp F_{R})\overline{L}. Therefore, by reflexivity of \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}} ((ii)), K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}(\lambda\overline{x}_{R}\ldotp F_{R})\overline{M}.

Otherwise, $\overline{M}$ is reduced and the argument is analogous to the case for K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}x\,\overline{M}.

• •

Finally, suppose K\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}(\lambda x\ldotp M^{\prime})\overline{M} because for some $L^{\prime}$ and $\overline{L}$, K\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}(\lambda x\ldotp L^{\prime})\overline{L}, L^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M^{\prime} and \overline{L}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{M}. Let $\overline{L}=(L_{1},\ldots,L_{n})$ and $\overline{M}=(M_{1},\ldots,M_{n})$.

First, suppose $(\lambda x\ldotp M^{\prime})\overline{M}\rightarrow_{\beta\upsilon}(\lambda x\ldotp N^{\prime})\overline{M}$, where $M^{\prime}\rightarrow_{\beta\upsilon}N^{\prime}$. By the inductive hypothesis, L^{\prime}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N^{\prime}. Therefore, by definition, (\lambda x\ldotp K^{\prime})\overline{K}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}(\lambda x\ldotp N^{\prime})\overline{M}.

The argument for the case $(\lambda x\ldotp M^{\prime})M_{1}\cdots M_{n}\rightarrow_{\beta\upsilon}(\lambda x\ldotp M^{\prime})N_{1}\cdots N_{n}$, where for some $j$, $M_{j}\rightarrow_{\beta\upsilon}N_{j}$ and $M_{k}=N_{k}$ for all $k\neq j$, is very similar.

Finally, assume that $n\geq 1$ and $(\lambda x\ldotp M^{\prime})M_{1}\cdots M_{n}\rightarrow_{\beta\upsilon}M^{\prime}[M_{1}/x]M_{2}\cdots M_{n}$. Then

[TABLE]

which proves L\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}M^{\prime}[M_{1}/x]M_{2}\cdots M_{n} by (ii) and (ii).∎

See 37

Proof.

We prove the lemma by induction on the structure of $F$. Note that the case $(\lambda x\ldotp N^{\prime})\overline{N}$ cannot occur for otherwise $F$ is not in $\beta$-normal form or does not have type $o$. If $F$ has the form $x\,\overline{N}$ then by the Inversion Lemma 76 there exists $\overline{M}$ such that \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}x\,\overline{M}, and clearly, $\alpha\vartriangleright x\,\overline{M}$.

Hence, the only remaining case is that $F$ has the form $c\,\overline{N}$. By the Inversion Lemma 76 there exist $\overline{M}$ such that \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}c\,\overline{M} and \overline{M}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}\overline{N}. Note that $c\in\Sigma^{\prime}$ implies $c:\iota^{n}\to o\in\Sigma$ for otherwise $\mathcal{A}_{0},\alpha\not\models c\,\overline{N}$. By (ii) and (ii), $M=N$ and thus $\mathcal{A}_{0},\alpha\models c\,\overline{M}$. Consequently, $\alpha\vartriangleright c\,\overline{M}$.

Next, suppose that $c$ is $\land$. Then $F$ is $N_{1}\land N_{2}$ and $c\,\overline{M}$ has the form $M_{1}\land M_{2}$. By (ii) and the Subject Reduction Lemma 72, $M_{j}$ is a positive existential formula and clearly, by assumption, $N_{j}$ is in $\beta$-normal form and $\mathcal{A}_{0},\alpha\models N_{j}$ for all $j\in\{1,2\}$. By the inductive hypothesis, there are $N_{1}^{\prime}$ and $N_{2}^{\prime}$ satisfying M_{j}\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N_{j}^{\prime} and $\alpha\vartriangleright N_{j}^{\prime}$. Consequently, $\alpha\vartriangleright N_{1}^{\prime}\land N_{2}^{\prime}$ and by definition, \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N_{1}^{\prime}\land N_{2}^{\prime}.

The case where $c$ is $\lor$ is very similar.

Finally, suppose that $c$ is $\exists_{\tau}$ and that $F$ is $\exists_{\tau}N_{1}$. By the Inversion Lemma 76 there exist $x$, $N^{\prime}$ and $M$ such that $N_{1}=(\lambda x\ldotp N^{\prime})$, \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\exists x\ldotp M and M\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[10.26112pt]{\scriptstyle}}}{\scriptstyle s\,}}N^{\prime}. By (ii) and the Subject Reduction Lemma 72, $M$ is a positive existential formula and clearly $N^{\prime}$ is in $\beta$-normal form and $\mathcal{A}_{0},\alpha[x\mapsto r]\models N^{\prime}$ for some $r\in{\mathcal{F}}\llbracket\tau\rrbracket$. By the inductive hypothesis, there exists $N^{\prime\prime}$ satisfying M\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}N^{\prime\prime} and $\alpha[x\mapsto r]\vartriangleright N^{\prime\prime}$. Consequently, $\alpha\vartriangleright\exists x\ldotp N^{\prime\prime}$ and by definition, \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow[]{\makebox[10.4167pt]{\scriptstyle}}\mathrel{\mkern-14.0mu}\rightarrow}{\scriptstyle\ell\,}}\exists x\ldotp N^{\prime\prime}. ∎

-C4 Supplementary Materials for Sec. IV-D

The proof of the following lemma is a straightforward induction on the definition of $\vartriangleright$:

Lemma 77**.**

Let $\alpha,\alpha^{\prime}$ be valuations and $F$ be positive existential formulas satisfying $\alpha\vartriangleright F$. If $\alpha(x)=\alpha^{\prime}(x)$ for all $x\in\operatorname{fv}(F)$ then $\alpha^{\prime}\vartriangleright F$.

See 38

Proof.

Let $G\in\Gamma^{\prime}$ be a goal clause, $F$ be a (closed) positive existential formula, $\alpha$ be a valuation and let $m=\mu(G)>0$ be such that \operatorname{posex}(G)\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[16.25005pt]{\scriptstyle m}}}{\scriptstyle\ell\,}}F and $\alpha\vartriangleright F$. W.l.o.g. we can assume that

[TABLE]

(Otherwise, rename all variables occurring in $G$ to obtain $\widetilde{G}$ satisfying Eq. 7 and clearly, by definition of $\vdash_{\mathcal{A}}$, $\Gamma^{\prime}\cup\{\widetilde{G}\}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{\widetilde{G},G^{\prime}\}$ implies $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{G^{\prime}\}$.)

Furthermore, suppose that $G=\neg A_{1}\lor\cdots\lor\neg A_{n}$ and $\operatorname{posex}(G)=\exists\overline{x}\ldotp\bigwedge_{i=1}^{n}A_{i}$. By the Inversion Lemma 74, there exist $F_{1},\ldots,F_{n}$ and $m_{1},\ldots,m_{n}$ such that $F=\exists\overline{x}\ldotp\bigwedge_{i=1}^{n}F_{i}$, $m=\sum_{i=1}^{n}m_{i}$ and A_{j}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[17.47227pt]{\scriptstyle m_{j}}}}{\scriptstyle\ell\,}}F_{j} for each $1\leq j\leq m$. Note that due to $\alpha\vartriangleright F$ we can assume w.l.o.g. that also $\alpha\vartriangleright F_{j}$ for each $1\leq j\leq n$, and furthermore we can assume that $m_{1}>0$. By (ii), there exists $E$ such that A_{1}\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}}E\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[24.08337pt]{\scriptstyle m_{1}-1}}}{\scriptstyle\ell\,}}F_{1}. Since $A_{1}$ is an atom there are exactly two cases:

1. (i)

$A_{1}=(\lambda y\ldotp L)M\,\overline{N}$ and $E=L[M/y]\overline{N}$ or 2. (i)

$A_{1}=R\,\overline{M}$ and $E=(\lambda\overline{x}_{R}\ldotp F_{R})\overline{M}$.

The first case is easy because for $G^{\prime}=\neg L[M/y]\overline{N}\lor\bigvee_{i=2}^{n}\neg A_{i}$, $\Gamma^{\prime}\cup\{G\}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{G,G^{\prime}\}$ and $\operatorname{posex}(G^{\prime})=\exists\overline{x}\ldotp L[M/y]\overline{N}\land\bigwedge_{i=2}^{n}A_{i}$.

In the second case, note that \mathrel{\stackunder[0pt]{\xrightarrow{\makebox[13.9167pt]{\scriptstyle 1}}}{\scriptstyle\ell\,}} is functional on applied $\lambda$-abstractions (by the Inversion Lemma 74). Hence, we can assume that

[TABLE]

where $m^{*}_{1}\leq m_{1}-1$ for otherwise $\alpha\vartriangleright F_{1}$ would clearly not hold.

$F_{R}$ has the form $\operatorname{posex}(G_{R,1},\overline{x}_{R})\lor\cdots\lor\operatorname{posex}(G_{R,k},\overline{x}_{R})$, where each $G_{R,j}$ is a goal clause and $G_{R,j}\lor R\,\overline{x}_{R}\in\Gamma^{\prime}$. Let $\overline{y}_{1},\ldots,\overline{y}_{k}$ and $E^{\prime}_{1},\ldots,E^{\prime}_{k}$ be such that for each $j$, $\operatorname{posex}(G_{R,j},\overline{x}_{R})=\exists\overline{y}_{j}\ldotp E_{j}^{\prime}$. Note that by Eq. 7, $\operatorname{posex}(G_{R},\overline{x}_{R})[\overline{M}/\overline{x}_{R}]=\exists\overline{y}_{j}\ldotp E^{\prime}_{j}[\overline{M}/\overline{x}_{R}]$ for each $j$ and by the Inversion Lemma 74, there exist $F_{1}^{\prime},\ldots,F^{\prime}_{k}$ and $m^{\prime}_{1},\ldots,m^{\prime}_{k}$ such that $F_{1}=\bigvee_{j=1}^{k}(\exists\overline{y}_{j}\ldotp F_{j}^{\prime})$, E^{\prime}_{j}[\overline{M}/\overline{x}_{R}]\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[19.41672pt]{\scriptstyle m_{j}^{\prime}}}}{\scriptstyle\ell\,}}F^{\prime}_{j} and $m^{\prime}_{j}\leq m_{1}^{*}$ for each $j$.

Next, because of $\alpha\vartriangleright F_{1}$ there exists $1\leq j\leq k$ and $\overline{r}\in{\mathcal{F}}\llbracket\Delta(\overline{y}_{j})\rrbracket$ satisfying $\alpha[\overline{y}_{j}\mapsto\overline{r}]\vartriangleright F^{\prime}_{j}$. Furthermore, because of Eqs. 7, (ii) and 77, $\alpha[\overline{y}_{j}\mapsto\overline{r}]\vartriangleright F_{i}$ for all $2\leq i\leq n$. Therefore,

[TABLE]

Clearly, it holds that

[TABLE]

and $\operatorname{fv}(G^{\prime})\subseteq\overline{x}\cup\overline{y}$. Let $\overline{x}^{\prime}\subseteq\overline{x}$ and $\overline{y}^{\prime}\subseteq\overline{y}$ be such that $\operatorname{fv}(G^{\prime})=\overline{x}^{\prime}\cup\overline{y}^{\prime}$. Hence, $\operatorname{posex}(G^{\prime})=\exists\overline{x}^{\prime},\overline{y}^{\prime}\ldotp E_{j}^{\prime}[\overline{M}/\overline{x}_{R}]\land\bigwedge_{i=2}^{n}A_{2}$. We define

[TABLE]

By Eqs. 8, 9 and 10, it holds that

1. $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime}\cup\{G^{\prime}\}$,

2. \operatorname{posex}(G^{\prime})\mathrel{\stackunder[0pt]{\xrightarrow{\makebox[18.19449pt]{\scriptstyle m^{\prime}}}}{\scriptstyle\ell\,}}F^{\prime},

3. $\alpha\vartriangleright F^{\prime}$and

4. $m^{\prime}\leq m_{1}^{*}+\sum_{i=2}^{n}m_{i}<\sum_{i=1}^{n}m_{i}=m$.

Consequently, also $\mu(\Gamma^{\prime}\cup\{G^{\prime}\})<\mu(\Gamma^{\prime})$ ∎

frame). By the inductive hypothesis and Lemma 22,

-D Supplementary Materials for Sec. VI

See 43

Proof.

The “if”-direction is straightforward. For the converse, suppose that $\Gamma$ is $\mathfrak{A}$-unsatisfiable. By the Completeness Thm. 26, for each $\mathcal{A}\in\mathfrak{A}$ there exist $G_{\mathcal{A}}$, every atom of which has the form $x\,\overline{M}$, and background atoms $\varphi_{\mathcal{A},i}$ and $\Gamma_{\mathcal{A}}$ such that $\mathcal{A}\not\models\neg\varphi_{\mathcal{A},1}\lor\cdots\lor\neg\varphi_{\mathcal{A},m_{\mathcal{A}}}$ and $\Gamma\vdash_{\mathcal{A}}^{*}\Gamma_{\mathcal{A}}\cup\{G_{\mathcal{A}}\lor\neg\varphi_{\mathcal{A},1}\lor\cdots\lor\neg\varphi_{\mathcal{A},m_{\mathcal{A}}}\}=\Gamma^{\prime}_{\mathcal{A}}$. Hence, $\{\neg\varphi_{\mathcal{A},1}\lor\cdots\lor\neg\varphi_{\mathcal{A},m_{\mathcal{A}}}\mid\mathcal{A}\in\mathfrak{A}\}$ is $\mathfrak{A}$-unsatisfiable and by compactness of $\mathfrak{A}$ there exists finite $\mathfrak{A}^{\prime}\subseteq\mathfrak{A}$ such that $\{\neg\varphi_{\mathcal{A},1}\lor\cdots\lor\neg\varphi_{\mathcal{A},m_{\mathcal{A}}}\mid\mathcal{A}\in\mathfrak{A}^{\prime}\}$ is $\mathfrak{A}$-unsatisfiable. Consequently, $\Gamma\vdash_{\mathfrak{A}}^{*}\{\Gamma^{\prime}_{\mathcal{A}}\mid\mathcal{A}\in\mathfrak{A}^{\prime}\}\vdash_{\mathfrak{A}}\{\bot\}\cup\{\Gamma^{\prime}_{\mathcal{A}}\mid\mathcal{A}\in\mathfrak{A}^{\prime}\}$. ∎

-E Supplementary Materials for Sec. VII

-E1 $\lambda$-lifting

In this section, we examine how to eliminate $\lambda$-abstractions. We make use of the notion of terms with holes (cf. [15, p. 29], [45]).

Let $\lambda y\ldotp M$ be a positive existential $\Sigma^{\prime}$-term not containing logical symbols with free variables $\overline{x}$ such that $\Delta\vdash M:\overline{\tau}\to o$, let $\widetilde{\Gamma}[-]$ be a set of terms with a hole of type $\Delta(y)\to\overline{\tau}\to o$ such that $\Gamma[\lambda y\ldotp M]$ is a set of HoCHCs.

Let $\overline{z}$ be distinct variables (different from $\overline{x},y$) satisfying $\Delta(\overline{z})=\overline{\tau}$. We define a signature $\Sigma^{\prime\prime}\coloneqq\Sigma^{\prime}\cup\{R_{M}:\Delta(\overline{x})\to\Delta(y)\to\overline{\tau}\to o\}$ and

[TABLE]

These are sets of HoCHCs.

Proposition 78**.**

Let $\mathcal{A}\in\mathfrak{A}$. Then $\Gamma$ is $\mathcal{A}$-monotone-satisfiable iff $\Gamma^{\prime}$ is $\mathcal{A}$-monotone-satisfiable.

Proof.

• •

First, suppose that there exists a $(\Sigma^{\prime},\mathcal{M})$-expansion $\mathcal{B}$ of $\mathcal{A}$ satisfying $\mathcal{B}\models\Gamma$. We define a $(\Sigma^{\prime\prime},\mathcal{M})$-expansion $\mathcal{B}^{\prime}$ of $\mathcal{A}$ by setting $R^{\mathcal{B}^{\prime}}\coloneqq R^{\mathcal{B}}$ for $R\in\Sigma^{\prime}\setminus\Sigma$ and $R_{M}^{\mathcal{B}^{\prime}}\coloneqq{\mathcal{B}}\llbracket\lambda\overline{x},y,\overline{z}\ldotp M\,\overline{z}\rrbracket$. By definition, $\mathcal{B}^{\prime}\models\neg M\,\overline{z}\lor R_{M}\,\overline{x}\,y\,\overline{z}$. Furthermore for every positive existential $\Sigma^{\prime}$-formula $E$ and valuation $\alpha$, ${\mathcal{B}}\llbracket E[\lambda y\ldotp M]\rrbracket(\alpha)={\mathcal{B}^{\prime}}\llbracket E[R_{M}\,\overline{x}]\rrbracket(\alpha)$. Consequently, $\mathcal{B}^{\prime}\models\Gamma^{\prime}$.

• •

Conversely, suppose $\Gamma^{\prime}$ is $\mathcal{A}$-monotone-satisfiable. Let $\mathcal{B}\coloneqq\mathcal{A}_{\Pi_{\Gamma^{\prime}}}$. By Thm. 23, $\mathcal{B}\models\Gamma^{\prime}$. Furthermore, by (ii) and 17, $\mathcal{B}=T_{\Pi_{\Gamma^{\prime}}}(\mathcal{B})$. Thus, $R_{M}^{\mathcal{B}}={\mathcal{B}}\llbracket\lambda\overline{x},y,\overline{z}\ldotp M\,\overline{z}\rrbracket$ and therefore, by Lemma 58, ${\mathcal{B}}\llbracket R_{M}\,\overline{x}\rrbracket(\alpha)={\mathcal{B}}\llbracket\lambda y\ldotp M\rrbracket(\alpha)$ for every valuation $\alpha$. Consequently, $\mathcal{B}\models\Gamma$. ∎

Hence, we conclude:

Corollary 79**.**

Let $\mathfrak{A}$ be a set of 1st-order $\Sigma$-structures and $\Gamma$ be a finite set of HoCHCs. Then there exists a set of HoCHCs (over an extended signature) which does not contain $\lambda$-abstractions and which is $\mathfrak{A}$-satisfiable iff $\Gamma$ is $\mathfrak{A}$-satisfiable.

-E2 Proof of Lemma 46

Before turning to Lemma 46, we prove the following auxiliary lemma:

Lemma 80**.**

Let $M,M_{1},\ldots,M_{n}$ and $\overline{L}$ be terms neither containing logical symbols nor $\lambda$-abstractions. Then:

1. (i)

If $R\in\Sigma^{\prime}\setminus\Sigma$, $R\,M_{1}\cdots M_{n}$ and $R\,x_{1}\cdots x_{n}$ are terms such that $\operatorname{fv}(R\,M_{1}\cdots M_{n})\cap\operatorname{fv}(R\,x_{1}\cdots x_{n})=\emptyset$ then

[TABLE]

is a unifier of $\lfloor RM_{1}\cdots M_{n}\rfloor^{\prime}$ and $\lfloor Rx_{1}\cdots x_{n}\rfloor^{\prime}$. 2. (i)

If $\Delta(y)=\rho=\tau_{1}\to\cdots\to\tau_{n}\to o$ and $y\,M_{1}\cdots M_{n}$ is a formula such that $\operatorname{fv}(\operatorname{Comp}_{\rho})\cap\operatorname{fv}(y\,M_{1}\cdots M_{n})$ then

[TABLE]

is a unifier of $\operatorname{Comp}_{\rho}$ and $\lfloor y\,M_{1}\cdots M_{n}\rfloor$. 3. (i)

If $M$ is a term neither containing logical symbols nor $\lambda$-abstractions then

[TABLE] 4. (i)

If $G$ is a goal clause then $\lfloor G[M_{1}/x_{1},\ldots,M_{n}/x_{n}]\rfloor=\lfloor G\rfloor[\lfloor M_{1}\rfloor^{\prime}/x_{1},\ldots,\lfloor M_{n}\rfloor^{\prime}/x_{n}]$.

Proof.

1. (i)

We prove Part (i) by induction on $n$. For $n=0$ this is trivial. Hence, suppose $n\geq 0$. By the inductive hypothesis,

[TABLE]

Consequently,

[TABLE]

using that $x_{i}\not\in\operatorname{fv}(M_{j})$ in the second and (i) in the third step. 2. (i)

Similar to Part (i). 3. (i)

We prove the claim by structural induction. For variables, and symbols from $\Sigma^{\prime}\setminus\Sigma$ this is obvious. Next, consider a term of the form $c\overline{N}$, where $c\in\Sigma$. By Remark 2, $c\overline{N}$ only contains variables $y:\iota$ and for each term $\Delta\vdash K:\iota^{n}\to\iota$, $\lfloor K\rfloor^{\prime}=K$. Hence,

[TABLE]

Finally, consider a term of the form $M\overline{N}\,N^{\prime}$, where $M\not\in\Sigma$. Then,

[TABLE]

using the inductive hypothesis in the third step. 4. (i)

Immediate from Part (i).∎

See 46

Proof.

1. (i)

Obvious. 2. (i)

Note that by assumption the $\beta$-reduction rule is not applicable. Next, let $\neg R\,\overline{M}\lor G_{1}$ and $G_{2}\lor R\,\overline{x}$ be clauses in $\Gamma^{\prime}$ modulo renaming of variables (such that they are variable-disjoint) and suppose $G=G_{1}\lor(G_{2}[\overline{M}/\overline{x}])$. By (i), $\lfloor R\,\overline{M}\rfloor[\lfloor\overline{M}\rfloor^{\prime}/\overline{x}]=\lfloor R\,\overline{x}\rfloor[\lfloor\overline{M}\rfloor^{\prime}/\overline{x}]$, by soundness of 1st-order resolution [3, 44],

[TABLE]

and by (i),

[TABLE]

Furthermore, $\operatorname{vars}(G)\subseteq\operatorname{vars}(\neg R\,\overline{M}\lor G_{1})\cup\operatorname{vars}(G_{2})$ and therefore $\lfloor\Gamma^{\prime}\cup\{G\}\rfloor=\lfloor\Gamma^{\prime}\rfloor\cup\{\lfloor G\rfloor\}$. 3. (i)

Finally, suppose that there exists $\{\bigvee_{i=1}^{m_{j}^{\prime}}\neg x_{j,i}\,M_{j,i}\lor\bigvee_{i=1}^{m_{j}}\neg\varphi_{j,i}\mid 1\leq j\leq n\}\subseteq\Gamma^{\prime}$ such that $\{\bigvee_{i=1}^{m_{j}}\neg\varphi_{j,i}\mid 1\leq j\leq n\}$ is $\mathfrak{A}$-unsatisfiable. Note that each $x_{j,i}$ does not occur in any of the $\varphi_{j^{\prime},i^{\prime}}$. Therefore, by (i), the fact that $\operatorname{Comp}_{\Delta(x_{j,i})}\in\lfloor\Gamma^{\prime}\rfloor$ and the soundness of 1st-order resolution, $\lfloor\Gamma^{\prime}\rfloor\models\{\bigvee_{i=1}^{m_{j}}\neg\varphi_{j,i}\mid 1\leq j\leq n\}$. Hence, by assumption $\lfloor\Gamma^{\prime}\rfloor$ is $\mathfrak{A}$-unsatisfiable.∎

-F Supplementary Materials for Sec. VIII

-F1 Higher-order Datalog

First consider the higher-order extension of Datalog.

Assumption**.**

Let $\Sigma\supseteq\{{\approx},{\not\approx}:\iota\to\iota\to o,c_{0}:\iota\}$ be a finite 1st-order signature containing ${\approx},{\not\approx}$ and symbol(s) of type $\iota$ (but nothing else); let $\Sigma^{\prime}$ be a relational extension of $\Sigma$ and $\Gamma$ be a finite set of HoCHCs.

Besides, let $\mathfrak{A}$ be the set of (1st-order) $\Sigma$-structures $\mathcal{A}$ satisfying ${\approx}^{\mathcal{A}}(a)(b)=1$ iff ${\not\approx}^{\mathcal{A}}(a)(b)=0$ iff $a=b$, for $a,b\in{\mathcal{A}}\llbracket\iota\rrbracket$.

In this setting we refer to HoCHCs as higher-order Datalog clauses (HoDC). For $\mathcal{A}\in\mathfrak{A}$ we define $\mathcal{A}^{\flat}$ by

[TABLE]

for $c,d:\iota\in\Sigma$ and we set $\mathfrak{A}^{\flat}\coloneqq\{\mathcal{A}^{\flat}\mid\mathcal{A}\in\mathfrak{A}\}$. Clearly, $\mathfrak{A}^{\flat}$ is finite and for each $\mathcal{A}\in\mathfrak{A}$ and type $\sigma$, ${\mathcal{A}^{\flat}}\llbracket\sigma\rrbracket$ is finite.

Lemma 81**.**

Let $\varphi$ be a background atom and $\alpha$ be a valuation satisfying $\mathcal{A}^{\flat},\alpha\models\varphi$ then $\mathcal{A},\alpha^{\sharp}\models\varphi$, where $\alpha^{\sharp}$ is a valuation such that for each $x:\iota\in\Delta$, $\alpha^{\sharp}(x)={\mathcal{A}}\llbracket\alpha(x)\rrbracket$.

Corollary 82**.**

Let $\Gamma^{\prime}$ be a set of goal clauses of background atoms. $\Gamma^{\prime}$ is $\mathfrak{A}^{\flat}$-satisfiable if $\Gamma^{\prime}$ is $\mathfrak{A}$-satisfiable.

Lemma 83**.**

Let $\Gamma^{\prime}$ be a set of goal clauses of background atoms. $\Gamma^{\prime}$ is $\mathfrak{A}$-satisfiable if $\Gamma^{\prime}$ is $\mathfrak{A}^{\flat}$-satisfiable.

Proof.

Let $\mathcal{A}^{\flat}\in\mathfrak{A}^{\flat}$ be such that $\mathcal{A}^{\flat}\models\Gamma^{\prime}$. Consider the element $\mathcal{A}^{\flat}/{\approx}$ of $\mathfrak{A}$ with domain

[TABLE]

i.e. the quotient of ${\mathcal{A}^{\flat}}\llbracket\iota\rrbracket$ over $\approx^{\mathcal{A}^{\flat}}$. It is easy to see that $\mathcal{A}^{\flat}/{\approx}\models\Gamma^{\prime}$. ∎

Note that both $\mathfrak{A}$ and $\mathfrak{A}^{\flat}$ are compact. Hence, by soundness and completeness of the proof system (Theorems 26 and 25) we obtain:

Proposition 84**.**

$\Gamma$* is $\mathfrak{A}$-satisfiable iff $\Gamma$ is $\mathfrak{A}^{\flat}$-satisfiable.*

Consequently, by Remark 49, we conclude:

Theorem 85**.**

It is decidable whether there exists a $\Sigma^{\prime}$-structure $\mathcal{B}$ satisfying $\mathcal{B}\models\Gamma$ and ${\approx}^{\mathcal{B}}(a)(b)=1$ iff ${\not\approx}^{\mathcal{B}}(a)(b)=0$ iff $a=b$, for $a,b\in{\mathcal{B}}\llbracket\iota\rrbracket$.

-F2 Supplementary Materials for Sec. VIII-A

Lemma 86**.**

*Let $\Gamma^{\prime}$ be a set of HoBHC(SLA). If $\Gamma^{\prime}\vdash_{\mathfrak{A}}\Gamma^{\prime}\cup\{G\}$ then $G$ is a HoBHC(SLA) and $\mathrm{gt}_{\iota}(G)\subseteq\mathrm{gt}_{\iota}(\Gamma^{\prime})$. *

Proof.

For the compact constraint refutation rule this is trivial.

Next, if $\neg(\lambda x\ldotp L)\,M\,\overline{N}\lor G$ is a HoBHC(SLA) then neither $(\lambda x\ldotp L)\,M\,\overline{N}$ nor $L[M/x]\,\overline{N}$ contain symbols from $\Sigma$ and $\mathrm{gt}_{\iota}((\lambda x\ldotp L)\,M\,\overline{N})=\mathrm{gt}_{\iota}(L[M/x]\,\overline{N})=\emptyset$. Hence, $\neg L[M/x]\,\overline{N}\lor G$ is a HoBHC(SLA) and $\mathrm{gt}_{\iota}(\neg L[M/x]\,\overline{N}\lor G)=\mathrm{gt}_{\iota}(\neg(\lambda x\ldotp L)\,M\,\overline{N}\lor G)$.

Finally, suppose $\neg R\,\overline{M}\lor G$ and $G^{\prime}\lor R\,\overline{x}$ are HoBHC(SLA)s. Note that all terms in $\overline{M}$ of type $\iota$ must be variables. Therefore $G\lor G^{\prime}[\overline{M}/\overline{x}]$ is a HoBHC(SLA) and $\mathrm{gt}_{\iota}(G\lor G^{\prime}[\overline{M}/\overline{x}])=\mathrm{gt}_{\iota}(\neg R\,\overline{M}\lor G)\cup\mathrm{gt}_{\iota}(G^{\prime}\lor R\,\overline{x})$. ∎

See 53

Proof.

For the rule compact constraint refutation this is due to Lemma 52 and for the $\beta$-reduction rule this is obvious because $((\lambda x\ldotp L)\,M\,\overline{N})^{\flat}=(\lambda x\ldotp L)\,M\,\overline{N}$.

Finally, suppose that $\{\neg R\,\overline{M}\lor G,G^{\prime}\lor R\,\overline{x}\}\subseteq\Gamma^{\prime}$. It holds that $(R\,\overline{M})^{\flat}=R\,\overline{M}$, $(R\,\overline{x})^{\flat}=R\,\overline{x}$ and for every atom $A$, $A^{\flat}[\overline{M}/\overline{x}]=(A[\overline{M}/\overline{x}])^{\flat}$. Consequently, $(G^{\prime})^{\flat}[\overline{M}/\overline{x}]=(G^{\prime}[\overline{M}/\overline{x}])^{\flat}$ and the lemma also holds for applications of the resolution rule. ∎

Theorem 87**.**

Let $\Phi$ be a predicate on atoms222222which is lifted to clauses by setting $\Phi(\neg A_{1}\lor\cdots\lor\neg A_{n}\lor(\neg)A)\coloneqq\min\{\Phi(A_{1}),\ldots,\Phi(A_{n}),\Phi(A)\}$ and to sets of HoCHCs $\Gamma^{\prime}$ by setting $\Phi(\Gamma^{\prime})=\min\{\Phi(C)\mid C\in\Gamma^{\prime}\}$ satisfying

1. (i)

$\Phi(\Gamma)=1$, 2. (i)

if $\Gamma^{\prime}\vdash_{\mathcal{A}}\Gamma^{\prime\prime}$ then $\Phi(\Gamma^{\prime\prime})\geq\Phi(\Gamma^{\prime})$ and 3. (i)

if $\Gamma^{\prime}$ is an $\mathfrak{A}$-unsatisfiable set of HoCHCs satisfying $\Phi(\Gamma^{\prime})=1$ then there exists a finite subset $\Gamma^{\prime\prime}\subseteq\Gamma^{\prime}$ which is $\mathfrak{A}$-unsatisfiable.

Then $\Gamma$ is $\mathfrak{A}$-unsatisfiable iff $\Gamma\vdash_{\mathfrak{A}}^{*}\Gamma^{\prime}\cup\{\bot\}$ for some $\Gamma^{\prime}$.

Proof.

Similar to the proof of Thm. 43. ∎

See 54

Proof.

Define $\Phi(A)=1$ just if $\mathrm{gt}_{\iota}(A)\subseteq\mathrm{gt}_{\iota}(\Gamma)$ and $\neg A$ is a HoBHC(SLA). By Lemmas 86 and 52, Thm. 87 is applicable, which yields the theorem. ∎