# Superposition for Higher-Order Logic

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović

► To cite this version:

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović. Superposition for Higher-Order Logic. Journal of Automated Reasoning, 2023, 67 (1), pp.10. 10.1007/s10817-022-09649-9. hal-04298616

HAL Id: hal-04298616

https://inria.hal.science/hal-04298616v1

Submitted on 21 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Superposition for Higher-Order Logic

Alexander Bentkamp · Jasmin Blanchette ·

Sophie Tourret · Petar Vukmirović

Received: date / Accepted: date

**Abstract** We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

**Keywords** superposition calculus · higher-order logic · refutational completeness

## 1 Introduction

Superposition is a leading calculus for first-order logic with equality. We have been wondering for some years whether it would be possible to gracefully generalize it to extensional higher-order logic and use it as the basis of a strong higher-order automatic theorem prover. Towards this goal, we have, together with colleagues, designed superposition-like calculi for three intermediate logics between first-order and higher-order logic. Now we are finally

Alexander Bentkamp (✉)

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, No. 4, South Fourth Street, Zhong Guan Cun, Beijing, 100190, China

E-mail: bentkamp@ios.ac.cn

Alexander Bentkamp · Jasmin Blanchette · Petar Vukmirović

Vrije Universiteit Amsterdam, Department of Computer Science, Section of Theoretical Computer Science, De Boelelaan 1111, 1081 HV Amsterdam, the Netherlands

E-mail: {a.bentkamp,j.c.blanchette}@vu.nl, petar.vukmirovic2@gmail.com

Sophie Tourret

Université de Lorraine, CNRS, Inria, LORIA, 615, rue du Jardin Botanique, 54600 Villers-lès-Nancy, France

E-mail: sophie.tourret@loria.fr

Jasmin Blanchette · Sophie Tourret

Max-Planck-Institut für Informatik, Saarland Informatics Campus E1 4, 66123 Saarbrücken, Germany

E-mail: {jblanche,stourret}@mpi-inf.mpg.de
ready to assemble a superposition calculus for full higher-order logic. The filiation of our new calculus from Bachmair and Ganzinger's standard first-order superposition is as follows:

<figure><img src="image_2.png" /></figure>

Our goal was to devise an efficient calculus for higher-order logic. To achieve it, we pursued two objectives. First, the calculus should be refutationally complete. Second, the calculus should coincide as much as possible with its predecessors oSup and λSup on the respective fragments of higher-order logic (which in turn essentially coincide with Sup on first-order logic). Achieving these objectives is the main contribution of this article. We made an effort to keep the calculus simple, but often the refutational completeness proof forced our hand to add conditions or special cases.

Like oSup, our calculus oλSup operates on clauses that can contain Boolean subterms, and it interleaves clausification with other inferences. Like λSup, oλSup eagerly βη-normalizes terms, employs full higher-order unification, and relies on a fluid subterm superposition rule (FLUIDSUP) to simulate superposition inferences below applied variables—i.e., terms of the form $y t_1 \dots t_n$ for $n \ge 1$.

In addition to the issues discussed previously and the complexity of combining the two approaches, we encountered the following main challenges.

First, because oSup contains several superposition-like inference rules for Boolean subterms, our completeness proof requires dedicated *fluid Boolean subterm hoisting rules* (FLUIDBOOLHOIST, FLUIDLOOBOHOIST), which simulate Boolean inferences below applied variables, in addition to FLUIDSUP, which simulates superposition inferences.

Second, due to restrictions related to the term order that parameterizes superposition, it is difficult to handle variables bound by unclausified quantifiers if these variables occur applied or in arguments of applied variables. We solve the issue by replacing such quantified terms $\forall y.t$ or $\exists y.t$ by equivalent terms $(\lambda y.t) \approx (\lambda y.\mathbf{T})$ or $(\lambda y.t) \not\approx (\lambda y.\perp)$ in a preprocessing step. We leave all other quantified terms intact so that we can process them more efficiently.

Third, like other higher-order calculi that support Booleans, our calculus must include some form of primitive substitution [1, 11, 21, 34]. For example, given the clauses $a \not\approx b$ and $z a \approx \perp \lor z b \approx \mathbf{T}$, it is crucial to find the substitution $\{z \mapsto \lambda v.v \approx a\}$, which does not arise through unification. Primitive substitution accomplishes this by blindly substituting logical connectives and quantifiers; here it would apply $\{z \mapsto \lambda v.v \approx y'v\}$ to the second clause, where $y$ and $y'$ are fresh variables. In the context of superposition, this is problematic because the instantiated clause is subsumed by the original clause and could be discarded. Our solution is to immediately clausify the introduced logical symbol, yielding a clause that is no longer subsumed.
The core of this article is the proof of refutational completeness. To keep it manageable, we structure it in three levels. The first level proves completeness of a calculus in first-order logic with Booleans, essentially relying on the completeness of oSup. The second level lifts this result to a ground version of our calculus by transforming the first-order model constructed in the first level into a higher-order model, closely following $\Lambda$Sup. The third level lifts this result further to the nonground level by showing that each ground inference on the second level corresponds to an inference of our calculus or is redundant. This establishes refutational completeness of our calculus.

We implemented our calculus in the Zipperposition prover and evaluated it on TPTP and Sledgehammer benchmarks. The new Zipperposition outperforms all other higher-order provers and is on a par with an ad hoc implementation of Booleans in the same prover by Vukmirović and Nummelin [39].

This article is structured as follows. Section 2 introduces syntax and semantics of higher-order logic and other preliminaries of this article. Section 3 presents our calculus, proves it sound, and discusses its redundancy criterion. Section 4 contains the detailed proof of refutational completeness. Section 5 discusses our implementation in Zipperposition. Section 6 presents our evaluation results.

An earlier version of this article is contained in Bentkamp's PhD thesis [7], and parts of it were presented at CADE-28 [9]. This article extends the conference paper with more explanations and detailed soundness and completeness proofs. We phrase the redundancy criterion in a slightly more general way to make it more convenient to use in our completeness proof. However, we are not aware of any concrete examples where this additional generality would be useful in practice. We also present a concrete term order fulfilling our abstract requirements as well as additional evaluation results.

## 2 Logic

Our logic is higher-order logic (simple type theory) with rank-1 polymorphism, Hilbert choice, Henkin semantics, and functional and Boolean extensionality. It closely resembles Gordon and Melham's HOL [20] and the TPTP TH1 standard [25].

Although standard semantics is commonly considered the foundation of the HOL systems, also Henkin semantics is compatible with the notion of provability employed by the HOL systems. By admitting nonstandard models, Henkin semantics is not subject to Gödel's first incompleteness theorem, allowing us to claim refutational completeness of our calculus.

On top of the standard higher-order terms, we install a clausal structure that allows us to formulate calculus rules in the style of first-order superposition. It does not restrict the flexibility of the logic because an arbitrary term $t$ of Boolean type can be written as the clause $t \approx \Gamma$.

### 2.1 Syntax

We use the notation $\tilde{a}_n$ or $\tilde{a}$ to stand for the tuple $(a_1, \dots, a_n)$ or product $a_1 \times \dots \times a_n$, where $n \ge 0$. We abuse notation by applying an operation on a tuple when it must be applied elementwise; thus, $f(\tilde{a}_n)$ can stand for $(f(a_1), \dots, f(a_n))$, $f(a_1) \times \dots \times f(a_n)$, or $f(a_1, \dots, a_n)$, depending on the operation $f$.

As a basis for our logic's types, we fix an infinite set $V_{ty}$ of type variables. A set $\Sigma_{ty}$ of type constructors with associated arities is a *type signature* if it contains at least one nullary
Boolean type constructor o and a binary function type constructor $\to$. A type, usually denoted by $\tau$ or $v$, is inductively defined to either be a type variable $\alpha \in \mathcal{V}_{\text{ty}}$ or have the form $\kappa(\bar{\tau}_n)$ for an $n$-ary type constructor $\kappa \in \Sigma_{\text{ty}}$ and types $\bar{\tau}_n$. We write $\kappa$ for $\kappa(\bar{\tau}_n)$ and $\tau \to v$ for $\to(\tau, v)$. A type declaration is an expression $\Pi \tilde{\alpha}_m. \tau$ (or simply $\tau$ if $m=0$), where all type variables occurring in $\tau$ belong to $\tilde{\alpha}_m$.

To define our logic's terms, we fix a type signature $\Sigma_{\text{ty}}$ and a set $\mathcal{V}$ of term variables with associated types, written as $x : \tau$ or $x$. We require that there are infinitely many variables for each type.

A term signature is a set $\Sigma$ of (function) symbols, usually denoted by $a, b, c, f, g, h$, each associated with a type declaration, written as $f : \Pi \tilde{\alpha}_m. \tau$. We require the presence of the logical symbols $\mathbf{T}, \mathbf{L} : o; \neg : o \to o; \mathbf{A}, \mathbf{V}, \to : o \to o \to o; \forall, \exists : \Pi \alpha. (\alpha \to o) \to o$; and $\approx, \not\approx : \Pi \alpha. \alpha \to \alpha \to o$. Moreover, we require the presence of the Hilbert choice operator $\varepsilon : \Pi \alpha. (\alpha \to o) \to \alpha$. The logical symbols are printed in bold to distinguish them from the notation used for clauses below. Although $\varepsilon$ is interpreted in our semantics, we do not consider it to be a logical symbol. The reason is that our calculus will enforce the semantics of $\varepsilon$ by an axiom, whereas the semantics of the logical symbols will be enforced by inference rules. In the following, we also fix a term signature $\Sigma$. A type signature and a term signature form a *signature*.

We will define terms in three layers of abstraction: raw $\lambda$-terms, $\lambda$-terms, and terms; where $\lambda$-terms will be $\alpha$-equivalence classes of raw $\lambda$-terms and terms will be $\beta\eta$-equivalence classes of $\lambda$-terms.

We write $t : \tau$ for a raw lambda term $t$ of type $\tau$. The set of raw $\lambda$-terms and their associated types is defined inductively as follows. Every $x : \tau \in \mathcal{V}$ is a raw $\lambda$-term of type $\tau$. If $f : \Pi \tilde{\alpha}_m. \tau \in \Sigma$ and $\bar{v}_m$ is a tuple of types, called *type arguments*, then $f(\langle \bar{v}_m \rangle)$ (or simply $f$ if $m=0$) is a raw $\lambda$-term of type $\tau(\tilde{\alpha}_m \mapsto \bar{v}_m)$. If $x : \tau$ and $t : v$, then the $\lambda$-expression $\lambda x.t$ is a raw $\lambda$-term of type $\tau \to v$. If $s : \tau \to v$ and $t : \tau$, then the *application* $st$ is a raw $\lambda$-term of type $v$. Using the spine notation [17], raw $\lambda$-terms can be decomposed in a unique way as a nonapplication *head* $t$ applied to zero or more arguments: $t s_1 \dots s_n$ or $t \bar{s}_n$ (abusing notation). For the symbols $\approx$ and $\not\approx$, we will typically use infix notation and omit the type argument.

A raw $\lambda$-term $s$ is a *subterm* of a raw $\lambda$-term $t$, written $t = t[s]$, if $t = s$, if $t = (\lambda x. u[s])$, if $t = (u[s])v$, or if $t = u(v[s])$ for some raw $\lambda$-terms $u$ and $v$. A proper subterm of a raw $\lambda$-term $t$ is any subterm of $t$ that is distinct from $t$ itself. A variable occurrence is *free* in a raw $\lambda$-term if it is not bound by a $\lambda$-expression. A raw $\lambda$-term is *ground* if it is built without using type variables and contains no free term variables.

The $\alpha$-renaming rule is defined as $(\lambda x.t) \to_{\alpha} (\lambda y.t\{x \mapsto y\})$, where $y$ does not occur free in $t$ and is not captured by a $\lambda$-binder in $t$. Two terms are $\alpha$-equivalent if they can be made equal by repeatedly $\alpha$-renaming their subterms. Raw $\lambda$-terms form equivalence classes modulo $\alpha$-equivalence, called *$\lambda$-terms*. We lift the above notions on raw $\lambda$-terms to $\lambda$-terms.

A substitution $\rho$ is a function from type variables to types and from term variables to $\lambda$-terms such that it maps all but finitely many variables to themselves. We require that it is type-correct—i.e., for each $x : \tau \in \mathcal{V}$, $x\rho$ is of type $\tau\rho$. The letters $\theta, \rho, \sigma$ are reserved for substitutions. Substitutions $\alpha$-rename $\lambda$-terms to avoid capture; for example, $(\lambda x. y)\{y \mapsto x\} = (\lambda x'. x)$. The composition $\rho\sigma$ applies $\rho$ first: $t\rho\sigma = (t\rho)\sigma$. The notation $\sigma[\bar{x}_n \mapsto \bar{s}_n]$ denotes the substitution that replaces each $x_i$ by $s_i$ and that otherwise coincides with $\sigma$.

The $\beta$- and $\eta$-reduction rules are specified on $\lambda$-terms as $(\lambda x.t) u \to_{\beta} t\{x \mapsto u\}$ and $(\lambda x.t x) \to_{\eta} t$. For $\beta$, bound variables in $t$ are implicitly renamed to avoid capture; for $\eta$, the variable $x$ may not occur free in $t$. Two terms are $\beta\eta$-equivalent if they can be made equal by
repeatedly $\beta$- and $\eta$-reducing their subterms. The $\lambda$-terms form equivalence classes modulo $\beta\eta$-equivalence, called $\beta\eta$-equivalence classes or simply terms.

We use the following nonstandard normal form: The $\beta\eta Q\eta$-normal form $t_{\downarrow\beta\eta Q\eta}$ of a $\lambda$-term $t$ is obtained by applying $\rightarrow_{\beta}$ and $\rightarrow_{\eta}$ exhaustively on all subterms and finally applying the following rewrite rule $Q\eta$ exhaustively on all subterms:

$$Q\langle\tau\rangle t \rightarrow_{Q\eta} Q\langle\tau\rangle (\lambda x.t x)$$

where $t$ is not a $\lambda$-expression. Here and elsewhere, $Q$ stands for either $\forall$ or $\exists$.

We lift all of the notions defined on $\lambda$-terms to terms:

**Convention 1** When defining operations that need to analyze the structure of terms, we use the $\beta\eta Q\eta$-normal representative as the default representative of a $\beta\eta$-equivalence class. Nevertheless, we will sometimes write $\downarrow_{\beta\eta Q\eta}$ for clarity.

Many authors prefer the $\eta$-long $\beta$-normal form [22, 24, 29], but in a polymorphic setting it has the drawback that instantiating a type variable with a functional type can lead to $\eta$-expansion. Below quantifiers, however, we prefer $\eta$-long form, which is enforced by the $Q\eta$-rule. The reason is that our completeness theorem requires arguments of quantifiers to be $\lambda$-expressions.

A literal is an equation $s \approx t$ or a disequation $s \not\approx t$ of terms $s$ and $t$. In both cases, the order of $s$ and $t$ is not fixed. We write $s \approx t$ for a literal that can be either an equation or a disequation. A clause $L_1 \lor \dots \lor L_n$ is a finite multiset of literals $L_j$. The empty clause is written as $\perp$.

Our calculus does not allow nonequational literals. These must be encoded as $t \approx \mathbf{T}$ or $t \approx \bot$. We even considered excluding negative literals by encoding them as $(s \approx t) \approx \bot$, following $\leftrightarrow$Sup [19]. However, this approach would make the conclusion of the equality factoring rule (EFACT) too large for our purposes. Regardless, the simplification machinery will allow us to reduce negative literals of the form $t \not\approx \bot$ and $t \not\approx \mathbf{T}$ to $t \approx \mathbf{T}$ and $t \approx \bot$, thereby eliminating redundant representations of literals.

A complete set of unifiers on a set $X$ of variables for two terms $s$ and $t$ is a set $U$ of unifiers of $s$ and $t$ such that for every unifier $\theta$ of $s$ and $t$ there exists a member $\sigma \in U$ and a substitution $\rho$ such that $x\sigma\rho = x\theta$ for all $x \in X$. We let $CSU_X(s,t)$ denote an arbitrary (preferably, minimal) complete set of unifiers on $X$ for $s$ and $t$. We assume that all $\sigma \in CSU_X(s,t)$ are idempotent on $X$—i.e., $x\sigma\sigma = x\sigma$ for all $x \in X$. The set $X$ will consist of the free variables of the clauses in which $s$ and $t$ occur and will be left implicit. To compute $CSU(s,t)$, Huet-style preunification [21] is not sufficient, and we must resort to full unification procedures [23, 38].

## 2.2 Semantics

A type interpretation $J_{ty} = (U, J_{ty})$ is defined as follows. The universe $U$ is a collection of nonempty sets, called *domains*. We require that $\{0, 1\} \in U$. The function $J_{ty}$ associates a function $J_{ty}(\kappa) : U^n \rightarrow U$ with each $n$-ary type constructor $\kappa$, such that $J_{ty}(0) = \{0, 1\}$ and for all domains $D_1, D_2 \in U$, the set $J_{ty}(\rightarrow)(D_1, D_2)$ is a subset of the function space from $D_1$ to $D_2$. The semantics is *standard* if $J_{ty}(\rightarrow)(D_1, D_2)$ is the entire function space for all $D_1, D_2$. A type valuation $\xi$ is a function that maps every type variable to a domain. The *denotation* of a type for a type interpretation $J_{ty}$ and a type valuation $\xi$ is recursively defined by $[[\alpha]]_{J_{ty}}^{\xi} = \xi(\alpha)$ and $[[\kappa(\bar{\tau})]]_{J_{ty}}^{\xi} = J_{ty}(\kappa)([[\bar{\tau}]]_{J_{ty}}^{\xi})$.

A type valuation $\xi$ can be extended to be a *valuation* by additionally assigning an element $\xi(x) \in [[\tau]]_{J_{ty}}^{\xi}$ to each variable $x : \tau$. An *interpretation function* $J$ for a type interpretation $J_{ty}$
associates with each symbol $f: \Pi\tilde{\alpha}_m \cdot \tau$ and domain tuple $\tilde{D}_m \in \mathcal{U}^m$ a value $\mathcal{J}(f, \tilde{D}_m) \in [[\tau]]_{\mathcal{J}_{\text{ty}}}^{\xi}$, where $\xi$ is a type valuation that maps each $\alpha_i$ to $\mathcal{D}_i$. We require that

$$
(\mathbb{I}) \quad \mathcal{J}(\mathbf{T}) = 1
$$

$$
(\mathbb{I}2) \quad \mathcal{J}(\perp) = 0
$$

$$
(\mathbb{I}3) \quad \mathcal{J}(\mathbf{A})(a, b) = \min \{a, b\}
$$

$$
(\mathbb{I}4) \quad \mathcal{J}(\mathbf{V})(a, b) = \max \{a, b\}
$$

$$
(\mathbb{I}5) \quad \mathcal{J}(\neg)(a) = 1 - a
$$

$$
(\mathbb{I}6) \quad \mathcal{J}(\rightarrow)(a, b) = \max \{1 - a, b\}
$$

$$
(\mathbb{I}7) \quad \mathcal{J}(\approx, \mathcal{D})(c, d) = 1 \text{ if } c = d \text{ and } 0 \text{ otherwise}
$$

$$
(\mathbb{I}8) \quad \mathcal{J}(\not\approx, \mathcal{D})(c, d) = 0 \text{ if } c = d \text{ and } 1 \text{ otherwise}
$$

$$
(\mathbb{I}9) \quad \mathcal{J}(\forall, \mathcal{D})(f) = \min \{f(a) \mid a \in \mathcal{D}\}
$$

$$
(\mathbb{I}10) \quad \mathcal{J}(\exists, \mathcal{D})(f) = \max \{f(a) \mid a \in \mathcal{D}\}
$$

$$
(\mathbb{I}11) \quad f(\mathcal{J}(\varepsilon, \mathcal{D})(f)) = \max \{f(a) \mid a \in \mathcal{D}\}
$$

for all $a,b \in \{0,1\}$, $\mathcal{D} \in \mathcal{U}$, $c,d \in \mathcal{D}$, and $f \in \mathcal{J}_{\text{ty}}(\rightarrow)(\mathcal{D}, \{0,1\})$.

The comprehension principle states that every function designated by a $\lambda$-expression is contained in the corresponding domain. Loosely following Fitting [18, Sect. 2.4], we initially allow $\lambda$-expressions to designate arbitrary elements of the domain, to be able to define the denotation of a term. We impose restrictions afterwards using the notion of a proper interpretation, enforcing comprehension.

A *$\lambda$-designation function* $\mathcal{L}$ for a type interpretation $\mathcal{I}_{\text{ty}}$ is a function that maps a valuation $\xi$ and a $\lambda$-expression of type $\tau$ to an element of $[[\tau]]_{\mathcal{J}_{\text{ty}}}^{\xi}$. A type interpretation, an interpretation function, and a $\lambda$-designation function form an *interpretation* $\mathcal{I} = (\mathcal{I}_{\text{ty}}, \mathcal{J}, \mathcal{L})$.

For an interpretation $\mathcal{I}$ and a valuation $\xi$, the denotation of a term is defined as $[[x]]_{\mathcal{J}}^{\xi} = \xi(x)$,
$[[f(\tilde{\tau}_m)]_{\mathcal{J}}^{\xi} = \mathcal{J}(f, [[\tilde{\tau}_m]]_{\mathcal{J}_{\text{ty}}}^{\xi})$, $[[s t]]_{\mathcal{J}}^{\xi} = [[s]]_{\mathcal{J}}^{\xi}([[[t]]_{\mathcal{J}}^{\xi})$, and $[[\lambda x. t]]_{\mathcal{J}}^{\xi} = \mathcal{L}(\xi, \lambda x. t)$. For ground terms $t$, the denotation does not depend on the choice of the valuation $\xi$, which is why we sometimes write $[[t]]_{\mathcal{J}}$ for $[[t]]_{\mathcal{J}}^{\xi}$.

An interpretation $\mathcal{I}$ is proper if $[[\lambda x. t]]_{\mathcal{J}}^{\xi}(a) = [[t]]_{\mathcal{J}}^{\xi[x \to a]}$ for all $\lambda$-expressions $\lambda x. t$ and all valuations $\xi$. If a type interpretation $\mathcal{I}_{\text{ty}}$ and an interpretation function $\mathcal{J}$ can be extended by a $\lambda$-designation function $\mathcal{L}$ to a proper interpretation $(\mathcal{I}_{\text{ty}}, \mathcal{J}, \mathcal{L})$, then this $\mathcal{L}$ is unique [18, Proposition 2.18]. Given an interpretation $\mathcal{I}$ and a valuation $\xi$, an equation $s \approx t$ is true if $[[s]]_{\mathcal{J}}^{\xi}$ and $[[t]]_{\mathcal{J}}^{\xi}$ are equal and it is false otherwise. A disequation $s \not\approx t$ is true if $s \approx t$ is false. A clause is true if at least one of its literals is true. A clause set is true if all its clauses are true. A proper interpretation $\mathcal{I}$ is a *model* of a clause set $N$, written $\mathcal{I} \models N$, if $N$ is true in $\mathcal{I}$ for all valuations $\xi$.

2.3 Skolem-Aware Interpretations

Some of our calculus rules introduce Skolem symbols—i.e., symbols representing objects mandated by existential quantification. We define a Skolem-extended signature that contains all Skolem symbols that could possibly be needed by the calculus rules.

**Definition 2** Given a term signature $\Sigma$, let the *Skolem-extended term signature* $\Sigma_{\text{sk}}$ the smallest signature that contains all symbols from $\Sigma$ and a symbol $\text{sk}_{\Pi\tilde{\alpha}, \forall\bar{x}, \exists\bar{x}, t z : \Pi\tilde{\alpha}. \bar{\tau} \to \upsilon}$ for all types $\upsilon$, variables $z : \upsilon$, terms $t : \upsilon \to \emptyset$ over the signature $(\Sigma_{\text{ty}}, \Sigma_{\text{sk}})$, where $\tilde{\alpha}$ are the free type variables occurring in $t$ and $\bar{x} : \bar{\tau}$ are the free term variables occurring in $t$ in order of first occurrence.
Interpretations as defined above can interpret the Skolem symbols arbitrarily. For example, an interpretation $\mathcal{J}$ does not necessarily interpret the symbol $sk_{\exists z, z \approx a}$ as $[[a]]_J$. Therefore, an inference producing $(sk_{\exists z, z \approx a} \approx a) \approx \mathbf{T}$ from $\exists \langle t \rangle (\lambda z. z \approx a) \approx \mathbf{T}$ is unsound w.r.t. $\models$. As a remedy, we define Skolem-aware interpretations as follows:

**Definition 3** We call a proper interpretation over a Skolem-extended signature $\mathcal{Skolem-aware}$ if for all Skolem symbols $\mathcal{J} \models (\exists \langle v \rangle (\lambda z. t z)) \approx t (sk_{\sqcap \bar{a}, \forall \bar{x}, \exists z, t z} \langle \bar{a} \rangle \bar{x})$, where $\bar{a}$ are the free type variables and $\bar{x}$ are the free term variables occurring in $t$ in order of first occurrence. An interpretation is a *Skolem-aware model* of a clause set $N$, written $\mathcal{J} \models_N$, if $\mathcal{J}$ is Skolem-aware and $\mathcal{J} \models N$.

### 3 The Calculus

The inference rules of our calculus $o\lambda\text{Sup}$ have many complex side conditions that may appear arbitrary at first sight. They are, however, directly motivated by our completeness proof and are designed to restrict inferences as much as possible without compromising refutational completeness.

The $o\lambda\text{Sup}$ calculus closely resembles $\lambda\text{Sup}$, augmented with rules for Boolean reasoning that are inspired by $o\text{Sup}$. As in $\lambda\text{Sup}$, superposition-like inferences are restricted to certain first-order-like subterms, the green subterms. Our completeness proof allows for this restriction because it is based on a reduction to first-order logic.

**Definition 4 (Green subterms and positions)** A green position of a $\lambda$-term is a finite sequence of natural numbers defined inductively as follows. For any $\lambda$-term $t$, the empty sequence $\varepsilon$ is a green position of $t$. For all symbols $f \in \Sigma \setminus \{\forall, \exists\}$, types $\bar{\tau}$, and $\lambda$-terms $\bar{u}$, if $p$ is a green position of $u_i$, then $i.p$ is a green position of $f(\bar{\tau}) \bar{u}$.

The green subterm of a $\lambda$-term at a given green position is defined inductively as follows. For any $\lambda$-term $t$, $t$ itself is the green subterm of $t$ at green position $\varepsilon$. For all symbols $f \in \Sigma \setminus \{\forall, \exists\}$, types $\bar{\tau}$, and $\lambda$-terms $\bar{u}$, if $t$ is a green subterm of $u_i$ at some green position $p$ for some $i$, then $t$ is the green subterm of $f(\bar{\tau}) \bar{u}$ at green position $i.p$.

For positions in clauses, natural numbers are not appropriate because clauses and literals are unordered. A green position in a clause C is a tuple $L.s.p$ where $L = s \approx t$ is a literal in C and $p$ is a green position in $s$. The green subterm of $C$ at green position $L.s.p$ is the green subterm of $s$ at green position $p$. A green position is *top level* if it is of the form $L.s.\varepsilon$.

We write $s|_p$ to denote the green subterm at position $p$ in $s$. A position $p$ is *at or below* a position $q$ if $q$ is a prefix of $p$. A position $p$ is *below* a position $q$ if $q$ is a proper prefix of $p$.

For example, the green subterms of $f(g(\neg p))(\forall \tau)(\lambda x. q)(ya)(\lambda x. h b)$ are the term itself, $g(\neg p)$, $\neg p$, $p$, $\forall \tau(\lambda x. q)$, $ya$, and $\lambda x. h b$.

**Definition 5 (Green contexts)** We write $s\langle u \rangle_p$ to denote a $\lambda$-term $s$ with the green subterm $u$ at position $p$ and call $s\langle \rangle_p$ a *green context*; We omit the subscript $p$ if there are no ambiguities.

The notions of green positions, subterms, and context are lifted to $\beta\eta$-equivalence classes via the $\beta\eta Q_\eta$-normal representative.
## 3.1 Preprocessing

Our completeness theorem requires that quantified variables do not appear in certain higher-order contexts. Quantified variables in these higher-order contexts are problematic because they have no clear counterpart in first-order logic and our completeness proof is based on a reduction to first-order logic. We use preprocessing to eliminate such problematic occurrences of quantifiers.

**Definition 6** The rewrite rules $\forall \approx$ and $\exists \approx$, which we collectively denote by $Q_{\approx}$, are defined on $\lambda$-terms as

$$ \forall \langle \tau \rangle \rightarrow \forall_{\approx} \lambda y. y \approx (\lambda x. T) $$

$$ \exists \langle \tau \rangle \rightarrow \exists_{\approx} \lambda y. y \not\approx (\lambda x. \perp) $$

where the rewritten occurrence of $Q\langle\tau\rangle$ is unapplied, has an argument that is not a $\lambda$-expression, or has an argument of the form $\lambda x. v$ such that $x$ occurs free in a nongreen position of $v$.

If either of these rewrite rules can be applied to a given term, the term is $Q_{\approx}$-reducible; otherwise, it is $Q_{\approx}$-normal. We lift this notion to $\beta\eta$-equivalence classes via the $\beta\eta Q_{\eta}$-normal representative. A clause or clause set is $Q_{\approx}$-normal if all contained terms are $Q_{\approx}$-normal.

For example, the term $\lambda y. \exists \langle t \to i \rangle (\lambda x. g x y (z y) (f x))$ is $Q_{\approx}$-normal. A term may be $Q_{\approx}$-reducible because a quantifier appears unapplied (e.g., $g \exists \langle i \rangle$); a quantified variable occurs applied (e.g., $\forall \langle t \to i \rangle (\lambda x. x a)$); a quantified variable occurs inside a nested $\lambda$-expression (e.g., $\forall \langle t \rangle (\lambda x. f (\lambda y. x))$); or a quantified variable occurs in the argument of a variable, either a free variable (e.g., $\forall \langle i \rangle (\lambda x. z x)$) or a bound variable (e.g., $\lambda y. \exists \langle i \rangle (\lambda x. y x)$).

We can also characterize $Q_{\approx}$-normality as follows:

**Lemma 7** Let $t$ be a term with spine notation $t = s \bar{u}_n$. Then $t$ is $Q_{\approx}$-normal if and only if $\bar{u}_n$ are $Q_{\approx}$-normal and

(i) $s$ is of the form $Q\langle\tau\rangle$, $n = 1$, and $u_1$ is of the form $\lambda y. u'$ such that $y$ occurs free only in green positions of $u'$; or

(ii) $s$ is a $\lambda$-expression whose body is $Q_{\approx}$-normal; or

(iii) $s$ is neither of the form $Q\langle\tau\rangle$ nor a $\lambda$-expression.

*Proof* This follows directly from Definition 6. □

In the following lemmas, our goal is to show that $Q_{\approx}$-normality is invariant under $\beta\eta Q_{\eta}$-normalization—i.e., if a $\lambda$-term $t$ is $Q_{\approx}$-normal, then so is $t \downarrow_{\beta\eta Q_{\eta}}$. However, $Q_{\approx}$-normality is not invariant under arbitrary $\beta\eta$-conversions. Clearly, a $\beta$-expansion can easily introduce $Q_{\approx}$-reducible terms, e.g., $c \leftarrow \beta (\lambda x. c) (\forall \langle i \rangle)$.

**Lemma 8** If $t$ and $v$ are $Q_{\approx}$-normal $\lambda$-terms, then $tv$ is a $Q_{\approx}$-normal $\lambda$-term.

*Proof* We prove this by induction on the structure of $t$. Let $s \bar{u}_n = t$ be the spine notation of $t$. By Lemma 7, $\bar{u}_n$ are $Q_{\approx}$-normal and one of the lemma's three cases applies. Since $t$ is of functional type and $Q_{\approx}$-normal, $s$ cannot be of the form $Q\langle\tau\rangle$, excluding case (i). Cases (ii) and (iii) are independent of $\bar{u}_n$, and hence appending $v$ to that tuple does not affect the $Q_{\approx}$-normality of $t$. □

**Lemma 9** If $t$ is a $Q_{\approx}$-normal $\lambda$-term and $\rho$ is a substitution such that $x\rho$ is $Q_{\approx}$-normal for all $x$, then $t\rho$ is $Q_{\approx}$-normal.
**Proof** We prove this by induction on the structure of $t$. Let $s\bar{u}_n = t$ be its spine notation. Since $t$ is $Q\asymp$-normal, by Lemma 7, $u_n$ are $Q\asymp$-normal and one of the following cases applies:

Case (i): $s$ is of the form $Q\langle\tau\rangle$, $n = 1$, and $u_1$ is of the form $\lambda y. u'$ such that $y$ occurs free only in green positions of $u'$. Since our substitutions avoid capture, $y\rho = y$ and $y$ does not appear in $x\rho$ for all other variables $x$. It is clear from the definition of green positions (Definition 4) that since $y$ occurs free only in green positions of $u'$, $y$ also occurs free only in green positions of $u'\rho$. Moreover, by the induction hypothesis, $u_1\rho$ is $Q\asymp$-normal. Hence, $t\rho = Q\langle\tau\rho\rangle (u_1\rho) = Q\langle\tau\rho\rangle (\lambda y. u'\rho)$ is also $Q\asymp$-normal.

Case (ii): $s$ is a $\lambda$-expression whose body is $Q\asymp$-normal. Then $t\rho = (\lambda y. s'\rho)(\bar{u}_n\rho)$ for some $Q\asymp$-normal $\lambda$-term $s'$. By the induction hypothesis, $s'\rho$ and $\bar{u}_n\rho$ are $Q\asymp$-normal. Therefore, $t\rho$ is also $Q\asymp$-normal.

Case (iii): $s$ is neither of the form $Q\langle\tau\rangle$ nor a $\lambda$-expression. If $s$ is of the form $f\langle\bar{\tau}\rangle$ for some $f \notin \{\forall, \exists\}$, then $t\rho = f\langle\bar{\tau}\rho\rangle(\bar{u}_n\rho)$. By the induction hypothesis, $\bar{u}_n\rho$ are $Q\asymp$-normal, and therefore $t\rho$ is also $Q\asymp$-normal. Otherwise, $s$ is a variable $x$ and hence $t\rho = x\rho(\bar{u}_n\rho)$. Since $x\rho$ is $Q\asymp$-normal by assumption and $\bar{u}_n\rho$ are $Q\asymp$-normal by the induction hypothesis, it follows from (repeated application of) Lemma 8 that $t\rho$ is also $Q\asymp$-normal. $\square$

**Lemma 10** Let $t$ be a $\lambda$-term of functional type that does not contain the variable $x$. If $\lambda x.t x$ is $Q\asymp$-normal, then $t$ is $Q\asymp$-normal.

**Proof** Since $\lambda x.t x$ is $Q\asymp$-normal, $t x$ is also $Q\asymp$-normal. Let $s\bar{u}_n = t$. Since $t x$ is $Q\asymp$-normal and $x$ is not a $\lambda$-expression, $s$ cannot be a quantifier by Lemma 7. Cases (ii) and (iii) are independent of $\bar{u}_n$, and hence removing $x$ from that tuple does not affect $Q\asymp$-normality. Thus, $t x$ being $Q\asymp$-normal implies that $t$ is $Q\asymp$-normal. $\square$

**Lemma 11** Let $t$ be a $\lambda$-term and $x$ a variable occurring free only in green positions of $t$. Let $t'$ be a term obtained via a $\beta\eta Q_\eta$-normalization step from $t$. Then $x$ occurs free only in green positions of $t'$.

**Proof** By induction on the structure of $t$. If $x$ does not occur free in $t$, the claim is obvious. If $t = x$, there is no possible $\beta\eta Q_\eta$-normalization step because for these steps the head of the rewritten term must be either a $\lambda$-expression or a quantifier. So we now assume that $x$ does occur free in $t$ and that $t \neq x$. Then, by the assumption that $x$ occurs free only in green positions, $t$ must be of the form $f\langle\bar{\tau}\rangle \bar{u}$ for some $f \in \Sigma \setminus \{\forall, \exists\}$, some types $\bar{\tau}$ and some $\lambda$-terms $\bar{u}$. The $\beta\eta Q_\eta$-normalization step must take place in one of the $\bar{u}$, yielding $\bar{u}'$ such that $t' = f\langle\bar{\tau}\rangle \bar{u}'$. By the induction hypothesis, $x$ occurs free only in green positions of $\bar{u}'$ and therefore only in green positions of $t'$. $\square$

**Lemma 12** Let $t$ be $Q\asymp$-normal and let $t'$ be obtained from $t$ by a $\beta\eta Q_\eta$-normalization step. If it is an $\eta$-reduction step, we assume that it happens not directly below a quantifier. Then $t'$ is also $Q\asymp$-normal.

**Proof** By induction on the structure of $t$. Let $s\bar{u}_n = t$. By Lemma 7, $\bar{u}_n$ are $Q\asymp$-normal, and one of the following cases applies:

Case (i): $s$ is of the form $Q\langle\tau\rangle$, $n = 1$, and $u_1$ is of the form $\lambda y. v$ such that $y$ occurs free only in green positions of $v$. Then the normalization cannot happen at $t$, because $s$ is of the form $Q\langle\tau\rangle$ and $u_1$ is a $\lambda$-expression already. It cannot happen at $u_1$ by the assumption of this lemma. So it must happen in $v$, yielding some $\lambda$-term $v'$. Then $t = s(\lambda y. v')$. The $\lambda$-term $v'$ is $Q\asymp$-normal by the induction hypothesis and hence $(\lambda y. v')$ is $Q\asymp$-normal. Since $y$ occurs free only in green positions of $v$, by Lemma 11, $y$ occurs free only in green positions of $v'$. Thus, $t'$ is $Q\asymp$-normal.
Cases (ii) and (iii): *s* is a *λ*-expression whose body is Q<sub>≈</sub>-normal; or *s* is neither of the form Q⟨τ⟩ nor a *λ*-expression.

If the $\beta\eta Q_{\eta}$-normalization step happens in some $u_i$, yielding some $\lambda$-term $u_i'$, then $u_i'$ is $Q_{\approx}^-$-normal by the induction hypothesis. Thus, $t' = s u_1 \cdots u_{i-1} u_i' u_{i+1} \cdots u_n$ is also $Q_{\approx}^-$-normal.

Otherwise, if $s = \lambda x.v$ and the $\beta\eta Q_{\eta}$-normalization step happens in $v$, yielding some
$\lambda$-term $v'$, then $v'$ is $Q_{\approx}^-$-normal by the induction hypothesis. Thus, $t' = (\lambda x.v') \bar{u}_n$ is also
$Q_{\approx}^-$-normal.

Otherwise, the $\beta\eta Q_{\eta}$-normalization step happens at $s \bar{u}_m$ for some $m \le n$, yielding some $\lambda$-term $v'$. Then $t' = v' u_{m+1} \cdots u_n$. The $\lambda$-terms $s$ and $\bar{u}_m$ are $Q_{\approx}^-$-normal and by repeated application of Lemma 8, $s \bar{u}_m$ is also $Q_{\approx}^-$-normal. The $\lambda$-term $v'$ is $Q_{\approx}^-$-normal by Lemma 9 (for $\beta$-reductions) or Lemma 10 (for $\eta$-reductions). The normalization step cannot be a $Q_{\eta}$-normalization because $s$ is not a quantifier. Since $\bar{u}_n$ are also $Q_{\approx}^-$-normal, by repeated application of Lemma 8, $t[v'] = v' u_{m+1} \cdots u_n$ is also $Q_{\approx}^-$-normal. $\square$

A direct consequence of this lemma is that $Q_{\approx}^-$-normality is invariant under $\beta\eta Q_{\eta}$-
normalization, as we wanted to show:

**Corollary 13** If *t* is a *Q<sub>∞</sub>*-normal *λ*-term, then *t*↓<sub>βηQ<sub>η</sub></sub> is also *Q<sub>∞</sub>*-normal.

As mentioned above, the converse does not hold. Therefore, following our convention, $Q_{\approx}$-normality is defined on terms (i.e., $\beta\eta$-equivalence classes) via $\beta\eta Q_{\eta}$-normal forms. It follows that $Q_{\approx}$-normality is well-behaved under applications of terms as well:

**Lemma 14** If *t* and *v* are $Q_{\approx}$-normal terms where *t* is of functional type, then *tv* is also $Q_{\approx}$-normal.

*Proof* Since $\mathcal{Q}_{\approx}$-normality is defined via $\beta\eta Q_{\eta}$-normal forms, we must show that if $t \downarrow_{\beta\eta Q_{\eta}}$ and $v \downarrow_{\beta\eta Q_{\eta}}$ are $\mathcal{Q}_{\approx}$-normal, then $tv \downarrow_{\beta\eta Q_{\eta}}$ is $\mathcal{Q}_{\approx}$-normal. By Lemma 8, $(t \downarrow_{\beta\eta Q_{\eta}}) (v \downarrow_{\beta\eta Q_{\eta}})$ is $\mathcal{Q}_{\approx}$-normal. By Corollary 13, $((t \downarrow_{\beta\eta Q_{\eta}}) (v \downarrow_{\beta\eta Q_{\eta}})) \downarrow_{\beta\eta Q_{\eta}} = (tv) \downarrow_{\beta\eta Q_{\eta}}$ is $\mathcal{Q}_{\approx}$-normal. $\square$

A preprocessor $\mathcal{Q}_{\approx}$-normalizes the input problem. It clearly terminates because each
$\mathcal{Q}_{\approx}$-step reduces the number of quantifiers. The $\mathcal{Q}_{\approx}$-normality of the initial clause set of a
derivation will be a precondition of the completeness theorem. Although inferences may
produce $\mathcal{Q}_{\approx}$-reducible clauses, we do not $\mathcal{Q}_{\approx}$-normalize during the derivation process itself.
Instead, $\mathcal{Q}_{\approx}$-reducible ground instances of clauses will be considered redundant by the
redundancy criterion. Thus, clauses whose ground instances are all $\mathcal{Q}_{\approx}$-reducible can be
deleted. However, there are $\mathcal{Q}_{\approx}$-reducible clauses, such as $x \forall \langle i \rangle \approx a$, that nevertheless have
$\mathcal{Q}_{\approx}$-normal ground instances. Such clauses must be kept because the completeness proof
relies on their $\mathcal{Q}_{\approx}$-normal ground instances.

In principle, we could omit the side condition of the $\mathcal{Q}_{\approx}$-rewrite rules and eliminate all quantifiers. However, the calculus (especially, the redundancy criterion) performs better with quantifiers than with $\lambda$-expressions, which is why we restrict $\mathcal{Q}_{\approx}$-normalization as much as the completeness proof allows. Extending the preprocessing to eliminate all Boolean terms as in Kotelnikov et al. [27] does not work for higher-order logic because Boolean terms can contain variables bound by enclosing $\lambda$-expressions.

3.2 Term Orders and Selection Functions

The calculus is parameterized by a strict and a nonstrict term order, a literal selection function,
and a Boolean subterm selection function. These concepts are defined below.
**Definition 15 (Strict ground term order)** A well-founded strict total order $\succ$ on ground terms is a *strict ground term order* if it satisfies the following criteria, where $\succeq$ denotes the reflexive closure of $\succ$:

(O1) compatibility with green contexts: $s' \succ s$ implies $t<s' \succ t<s$;

(O2) green subterm property: $t<s \succeq s$;

(O3) $u \succ \bot \succ T$ for all terms $u \neq T, \bot$;

(O4) $Q\langle\tau\rangle t \succ tu$ for all types $\tau$, terms $t$, and terms $u$ such that $Q\langle\tau\rangle t$ and $u$ are $Q\approx$-normal and the only Boolean green subterms of $u$ are $T$ and $\bot$.

Given a strict ground term order, we extend it to literals and clauses via the multiset extensions in the standard way [2, Sect. 2.4].

**Remark 16** The property $Q\langle\tau\rangle t \succ tu$ from (O4) cannot be achieved in general—a fact that Christoph Benzmüller made us aware about. Without further restrictions, it would imply that $Q\langle\tau\rangle(\lambda x. x) \succ (\lambda x. x)(Q\langle\tau\rangle(\lambda x. x)) = Q\langle\tau\rangle(\lambda x. x)$, contradicting irreflexivity of $\succ$. Restricting the Boolean green subterms of $u$ to be only $T$ and $\bot$ resolves this issue. A second issue is that (O4) without further restrictions would imply $Q\langle\tau\rangle (\lambda y. y a) \succ (\lambda y. y a)(\lambda x. Q\langle\tau\rangle (\lambda y. y a)) = Q\langle\tau\rangle (\lambda y. y a)$, again contradicting irreflexivity. The restriction on the Boolean green subterms of $u$ does not apply here because the Boolean subterms of $\lambda x. Q\langle\tau\rangle (\lambda y. y a)$ are not green. The restriction to $Q\approx$-normal terms resolves this second issue, but it forces us to preprocess the input problem.

**Definition 17 (Strict term order)** A *strict term order* is a relation $\succ$ on terms, literals, and clauses such that its restriction to ground entities is a strict ground term order and such that it is stable under grounding substitutions (i.e., $t \succ s$ implies $t\theta \succ s\theta$ for all substitutions $\theta$ grounding the entities $t$ and $s$).

**Definition 18 (Nonstrict term order)** Given a strict term order $\succ$ and its reflexive closure $\succeq$, a *nonstrict term order* is a relation $\succeq$ on terms, literals, and clauses such that $t \succeq s$ implies $t\theta \succeq s\theta$ for all $\theta$ grounding the entities $t$ and $s$.

Although we call them orders, a strict term order $\succ$ is not required to be transitive on nonground entities, and a nonstrict term order $\succeq$ does not need to be transitive at all. Normally, $t \succeq s$ should imply $t \succeq s$, but this is not required either. A nonstrict term order $\succeq$ allows us to be more precise than the reflexive closure $\succeq$ of $\succ$. For example, we cannot have $yb \succeq ya$, because $yb \neq ya$ and $yb \nsucc ya$ by stability under grounding substitutions (with $\{y \mapsto \lambda x. c\}$). But we can have $yb \succeq ya$ if $b \succ a$. In practice, the strict and the nonstrict term order should be chosen so that they can compare as many pairs of terms as possible while being computable and reasonably efficient.

**Definition 19 (Maximality)** An element $x$ of a multiset $M$ is $\Delta$-maximal for some relation $\Delta$ if for all $y \in M$ with $y \Delta x$, we have $y = x$. It is strictly $\Delta$-maximal if it is $\Delta$-maximal and occurs only once in $M$.

**Definition 20 (Literal selection function)** A literal selection function is a mapping from each clause to a subset of its literals. The literals in this subset are called *selected*. The following restrictions apply:

- A literal must not be selected if it is positive and neither side is $\bot$.

- A literal $L\langle y \rangle$ must not be selected if $y \bar{u}_n$, with $n \ge 1$, is a $\succeq$-maximal term of the clause.
**Definition 21 (Boolean subterm selection function)** A Boolean subterm selection function is a function mapping each clause C to a subset of the green positions with Boolean subterms in C. The positions in this subset are called *selected* in C. Informally, we also say that the Boolean subterms at these positions are selected. The following restrictions apply:

- A subterm $s\langle y\rangle$ must not be selected if $y\bar{u}_n$, with $n \ge 1$, is a $\ge$-maximal term of the clause.

- A subterm must not be selected if it is $\mathbf{T}$ or $\mathbf{\perp}$ or a variable-headed term.

- A subterm must not be selected if it is at the top-level position on either side of a positive literal.

### 3.3 The Core Inference Rules

Let $\succ$ be a strict term order, let $\succeq$ be a nonstrict term order, let $HLitSel$ be a literal selection function, and let $HBoolSel$ be a Boolean subterm selection function. The calculus rules depend on the following auxiliary notions.

**Definition 22 (Eligibility)** A literal *L* is (*strictly*) $\sqsupset$-eligible w.r.t. a substitution $\sigma$ in *C* for some relation $\sqsupset$ if it is selected in *C* or there are no selected literals and no selected Boolean subterms in *C* and *L*~$\sigma$ is (*strictly*) $\sqsupset$-maximal in *C*~$\sigma$.

The $\sqsupset$-eligible positions of a clause *C* w.r.t. a substitution $\sigma$ are inductively defined as follows:

(E1) Any selected position is $\sqsupset$-eligible.

(E2) If a literal $L = s \approx t$ with $s\sigma \triangleleft t\sigma$ is either $\sqsupset$-eligible and negative or strictly $\sqsupset$-eligible and positive, then $L.s.\epsilon$ is $\sqsupset$-eligible.

(E3) If the position *p* is $\sqsupset$-eligible and the head of $C|_p$ is not $\approx$ or $\not\approx$, the positions of all direct green subterms are $\sqsupset$-eligible.

(E4) If the position *p* is $\sqsupset$-eligible and $C|_p$ is of the form $s \approx t$ or $s \not\approx t$, then the position of *s* is $\sqsupset$-eligible if $s\sigma \triangleleft t\sigma$ and the position of *t* is $\sqsupset$-eligible if $s\sigma \not\sqsupset t\sigma$.

If $\sigma$ is the identity substitution, we leave it implicit.

We define deeply occurring variables as in $\lambda$Sup, but exclude $\lambda$-expressions directly below quantifiers:

**Definition 23 (Deep occurrences)** A variable *occurs deeply* in a clause *C* if it occurs free inside an argument of an applied variable or inside a $\lambda$-expression that is not directly below a quantifier.

For example, *x* and *z* occur deeply in $fxy \approx yx \lor z \not\approx (\lambda w. z a) \lor \forall l\langle l \rangle (\lambda u. p y) \approx \mathbf{T}$, whereas *y* does not occur deeply. Intuitively, deep occurrences are occurrences of variables that can be caught in $\lambda$-expressions by grounding.

Fluid terms are defined as in $\lambda$Sup, using the $\beta\eta Q\eta$-normal form:

**Definition 24 (Fluid terms)** A term *t* is called *fluid* if (1) $t \downarrow_{\beta\eta Q_\eta}$ is of the form $y\bar{u}_n$ where $n \ge 1$, or (2) $t \downarrow_{\beta\eta Q_\eta}$ is a $\lambda$-expression and there exists a substitution $\sigma$ such that $t\sigma \downarrow_{\beta\eta Q_\eta}$ is not a $\lambda$-expression (due to $\eta$-reduction).

Case (2) can arise only if *t* contains an applied variable. Intuitively, fluid terms are terms whose $\eta$-short $\beta$-normal form can change radically as a result of instantiation. For example, $\lambda x. y a (z x)$ is fluid because applying $\{z \mapsto \lambda x. x\}$ makes the $\lambda$ vanish: $(\lambda x. y a x) = y a$.
Similarly, $\lambda x.f(yx)x$ is fluid because $(\lambda x.f(yx)x)\{y\mapsto\lambda x.a\} = (\lambda x.fax) = fa$. In Section 5, we will discuss how fluid terms can be overapproximated in an implementation.

The rules of our calculus are stated as follows. The superposition rule strongly resembles the one of $\lambda Sup$ but uses our new notion of eligibility, and the new conditions 9 and 10 stem from the $SUP$ rule of $oSup$:

$$ \frac{\overbrace{D' \vee t \approx t'}^{D} C\langle u \rangle}{(D' \vee C\langle t' \rangle)\sigma}^{SUP} $$

1. $u$ is not fluid;

2. $u$ is not a variable deeply occurring in $C$;

3. *variable condition*: if $u$ is a variable $y$, there must exist a grounding substitution $\theta$ such that $t\sigma\theta \succ t'\sigma\theta$ and $C\sigma\theta \prec C''\sigma\theta$, where $C'' = C\{y\mapsto t'\}$;

4. $\sigma \in \text{CSU}(t, u)$;

5. $t\sigma \preceq t'\sigma$;

6. the position of $u$ is $\succeq$-eligible in $C$ w.r.t. $\sigma$;

7. $C\sigma \preceq D\sigma$;

8. $t \approx t'$ is strictly $\succeq$-eligible in $D$ w.r.t. $\sigma$;

9. $t\sigma$ is not a fully applied logical symbol;

10. if $t'\sigma = \bot$, the position of the subterm $u$ is at the top level of a positive literal.

The second rule is a variant of $SUP$ that focuses on fluid green subterms. It stems from $\lambda Sup$.

$$ \frac{\overbrace{D' \vee t \approx t'}^{D} C\langle u \rangle}{(D' \vee C\langle zt' \rangle)\sigma}^{FLUIDSUP} $$

with the following side conditions, in addition to $SUP$'s conditions 5 to 10:

1. $u$ is a variable deeply occurring in $C$ or $u$ is fluid;

2. $z$ is a fresh variable;

3. $\sigma \in \text{CSU}(zt, u)$;

4. $(zt')\sigma \neq (zt)\sigma$.

The $ERES$ and $EFACT$ rules are copied from $\lambda Sup$. As a minor optimization, we replace the $\succeq$-eligibility condition of $\lambda Sup$'s $EFACT$ by a $\succeq$-maximality condition and a condition that nothing is selected. The new conditions are not equivalent to the old one because positive literals of the form $u \approx \bot$ can be selected.

$$ \frac{\overbrace{C' \vee u \approx u'}^{C} ERES}{C'\sigma} $$

$$ \frac{\overbrace{C' \vee u' \approx v' \vee u \approx v}^{C} EFACT}{(C' \vee v \approx v' \vee u \approx v')\sigma} $$

For $ERES$: $\sigma \in \text{CSU}(u, u')$ and $u \not\approx u'$ is $\succeq$-eligible in $C$ w.r.t. $\sigma$. For $EFACT$: $\sigma \in \text{CSU}(u, u')$, $u\sigma \preceq v\sigma$, $(u \approx v)\sigma$ is $\succeq$-maximal in $C\sigma$, and nothing is selected in $C$.

Argument congruence—the property that $t \approx s$ entails $tz \approx sz$—is embodied by the rule $ARGCONG$, which is identical with the rule of $\lambda Sup$:

$$ \frac{\overbrace{C' \vee s \approx s'}^{C} ARGCONG}{C'\sigma \vee s\sigma \bar{x}_n \approx s'\sigma \bar{x}_n} $$

where $n > 0$ and $\sigma$ is the most general type substitution that ensures well-typedness of the conclusion. In particular, if $s$ accepts $k$ arguments, then $ARGCONG$ will yield $k$ conclusions—one for each $n \in \{1, \dots, k\}$—where $\sigma$ is the identity substitution. If the result type of $s$ is a type variable, $ARGCONG$ will yield infinitely many additional conclusions—one for each $n > k$—where $\sigma$ instantiates the result type of $s$ with $\alpha_1 \to \dots \to \alpha_{n-k} \to \beta$ for fresh $\bar{\alpha}_{n-k}$
and $\beta$. Moreover, the literal $s \approx s'$ must be strictly $\gtrsim$-eligible in C w.r.t. $\sigma$, and $\bar{x}_n$ is a tuple of distinct fresh variables.

The following rules are concerned with Boolean reasoning and originate from oSup. They have been adapted to support polymorphism and applied variables.

$$ \frac{C<u>}{(C<\perp> \lor u \approx \mathbf{T})\sigma} \text{BOOLHOIST} $$

1. $\sigma$ is a type unifier of the type of $u$ with the Boolean type o (i.e., the identity if $u$ is Boolean or $\alpha \mapsto o$ if $u$ is of type $\alpha$ for some type variable $\alpha$);

2. $u$ is neither variable-headed nor a fully applied logical symbol;

3. the position of $u$ is $\gtrsim$-eligible in C;

4. the occurrence of $u$ is not at the top level of a positive literal.

$$ \frac{\overbrace{C' \lor s \approx s'}^{C}}{C'\sigma} \text{FALSEELIM} $$

1. $\sigma \in \text{CSU}(s \approx s', \perp \approx \mathbf{T})$;

2. $s \approx s'$ is strictly $\gtrsim$-eligible in C w.r.t. $\sigma$.

$$ \frac{\frac{C<u>}{(C<\perp> \lor x \approx y)\sigma} \text{EQHOIST}}{C<u>}{\text{FORALLHOIST}} \quad \frac{C<u>}{(C<\mathbf{T}> \lor y x \approx \mathbf{T})\sigma} \text{NEQHOIST} $$

$$ \frac{C<u>}{(C<\mathbf{T}> \lor x \approx y)\sigma} \text{NEQHOIST} $$ $$ \frac{C<u>}{(C<\mathbf{T}> \lor y x \approx \perp)\sigma} \text{EXISTSHOIST} $$

1. $\sigma \in \text{CSU}(u, x \approx y)$, $\sigma \in \text{CSU}(u, x \not\approx y)$, $\sigma \in \text{CSU}(u, \forall\langle\alpha\rangle y)$, or $\sigma \in \text{CSU}(u, \exists\langle\alpha\rangle y)$, respectively;

2. $x, y$, and $\alpha$ are fresh variables;

3. the position of $u$ is $\gtrsim$-eligible in C w.r.t. $\sigma$;

4. if the head of $u$ is a variable, it must be applied and the affected literal must be of the form $u \approx \mathbf{T}$, $u \approx \perp$, or $u \approx v$ where $v$ is a variable-headed term.

$$ \frac{C<u>}{C<t'>\sigma} \text{BOOLRW} $$

1. $\sigma \in \text{CSU}(t, u)$ and $(t, t')$ is one of the following pairs:

$$ \begin{array}{llll} (\neg\perp, \mathbf{T}) & (\perp\wedge\perp, \perp) & (\perp\vee\perp, \perp) & (\perp \to \perp, \mathbf{T}) \\ (\neg\mathbf{T}, \perp) & (\mathbf{T}\wedge\perp, \perp) & (\mathbf{T}\vee\perp, \mathbf{T}) & (\mathbf{T} \to \perp, \perp) \\ (y \approx y, \mathbf{T}) & (\perp\wedge\mathbf{T}, \perp) & (\perp\vee\mathbf{T}, \mathbf{T}) & (\perp \to \mathbf{T}, \mathbf{T}) \\ (y \not\approx y, \perp) & (\mathbf{T}\wedge\mathbf{T}, \mathbf{T}) & (\mathbf{T}\vee\mathbf{T}, \mathbf{T}) & (\mathbf{T} \to \mathbf{T}, \mathbf{T}) \end{array} $$

where $y$ is a fresh variable;

2. $u$ is not a variable;

3. the position of $u$ is $\gtrsim$-eligible in C w.r.t. $\sigma$;

4. if the head of $u$ is a variable, it must be applied and the affected literal must be of the form $u \approx \mathbf{T}$, $u \approx \perp$, or $u \approx v$ where $v$ is a variable-headed term.
$$ \frac{C<u>}{C<y(\mathfrak{sk}_{\Pi\bar{a}. \forall \bar{x}. \exists z. \neg y \sigma z \langle\bar{\alpha}\rangle \bar{x})>\sigma}} \text{FORALLRW} $$ $$ \frac{C<u>}{C<y(\mathfrak{sk}_{\Pi\bar{a}. \forall \bar{x}. \exists z. y \sigma z \langle\bar{\alpha}\rangle \bar{x})>\sigma}} \text{EXISTSRW} $$

1. $\sigma \in \text{CSU}(\forall\langle\beta\rangle y, u)$ and $\sigma \in \text{CSU}(\exists\langle\beta\rangle y, u)$, respectively, where $\beta$ is a fresh type variable, $y$ is a fresh term variable, $\bar{a}$ are the free type variables and $\bar{x}$ are the free term variables occurring in $y\sigma$ in order of first occurrence;

2. $u$ is not a variable;

3. the position of $u$ is $\gtrsim$-eligible in C w.r.t. $\sigma$;

4. if the head of $u$ is a variable, it must be applied and the affected literal must be of the form $u \approx \mathbf{T}$, $u \approx \bot$, or $u \approx \nu$ where $\nu$ is a variable-headed term;

5. for FORALLRW, the indicated occurrence of $u$ is not in a literal $u \approx \mathbf{T}$, and for EXISTSRW, the indicated occurrence of $u$ is not in a literal $u \approx \bot$.

In principle, the subscript of the Skolems above could be normalized using Boolean tautologies to share as many Skolem symbols as possible. This is an extension of our calculus that we did not investigate any further.

Like SUP, also the Boolean rules must be simulated in fluid terms. The following rules are Boolean counterparts of FLUIDSUP:

$$ \frac{C<u>}{(C<z\bot> \lor x \approx \mathbf{T})\sigma} \text{FLUIDBOOLHOIST} $$

1. $u$ is fluid;

2. $z$ and $x$ are fresh variables;

3. $\sigma \in \text{CSU}(zx, u)$;

4. $(z\bot)\sigma \neq (zx)\sigma$;

5. $x\sigma \neq \mathbf{T}$ and $x\sigma \neq \bot$;

6. the position of $u$ is $\gtrsim$-eligible in C w.r.t. $\sigma$.

$$ \frac{C<u>}{(C<z\mathbf{T}> \lor x \approx \bot)\sigma} \text{FLUIDLOOBHOIST} $$

Same conditions as FLUIDBOOLHOIST, but $\bot$ is replaced by $\mathbf{T}$ in condition 4.

In addition to the inference rules, our calculus relies on two axioms, below. Axiom (EXT), from $\lambda\text{Sup}$, embodies functional extensionality; the expression $\text{diff}(\alpha, \beta)$ abbreviates $\mathfrak{sk}_{\Pi\alpha\beta. \forall z. \exists x. z \neq y} \langle\alpha, \beta\rangle$. Axiom (CHOICE) characterizes the Hilbert choice operator $\varepsilon$.

$$ z(\text{diff}(\alpha, \beta)zy) \not\approx y(\text{diff}(\alpha, \beta)zy) \lor z \approx y \quad (\text{EXT}) $$

$$ yx \approx \bot \lor y(\varepsilon\langle\alpha\rangle y) \approx \mathbf{T} \quad (\text{CHOICE}) $$

### 3.4 Rationale for the Rules

Most of the calculus's rules are adapted from its precursors. SUP, ERES, and EFACT are already present in Sup, with slightly different side conditions. Notably, as in $\lambda\text{fSup}$ and $\lambda\text{Sup}$, SUP inferences are required only into green contexts. Other subterms are accessed indirectly via ARGCONG and (EXT).

The rules BOOLHOIST, EQHOIST, NEQHOIST, FORALLHOIST, EXISTSHOIST, FALSE-ELIM, BOOLRW, FORALLRW, and EXISTSRW, concerned with Boolean reasoning, stem
from oSup, which was inspired by $↔Sup$. Except for BOOLHOIST and FALSEELIM, these rules have a condition stating that “if the head of $u$ is a variable, it must be applied and the affected literal must be of the form $u \approx \mathbf{T}$, $u \approx \bot$, or $u \approx \nu$ where $\nu$ is a variable-headed term.” The inferences at variable-headed terms permitted by this condition are our form of primitive substitution [1, 21], a mechanism that blindly substitutes logical connectives and quantifiers for variables $z$ with a Boolean result type.

**Example 25** Our calculus can prove that Leibniz equality implies equality (i.e., if two values behave the same for all predicates, they are equal) as follows:

$$ \frac{\frac{za \approx \bot \lor zb \approx \mathbf{T}}{(xa \approx ya) \approx \bot \lor \bot \approx \mathbf{T} \lor xb \approx yb}}{\mathbf{T} \approx \bot \lor \bot \approx \mathbf{T} \lor wabb \approx wbab} \begin{array}{l} \text{EQHOIST} \\ \text{BOOLRW} \\ \text{FALSEELIM} \end{array} \quad \frac{\frac{\bot \approx \mathbf{T} \lor wabb \approx wbab}{wabb \approx wbab} \text{FALSEELIM}}{a \not\approx b} \quad \frac{a \not\approx a}{\bot} \text{ERES} $$

The clause $za \approx \bot \lor zb \approx \mathbf{T}$ describes Leibniz equality of a and b; if a predicate $z$ holds for a, it also holds for b. The clause $a \not\approx b$ is the negated conjecture. The EQHOIST inference, applied on $zb$, illustrates how our calculus introduces logical symbols without a dedicated primitive substitution rule. Although $\approx$ does not appear in the premise, we still need to apply EQHOIST on $zb$ with $CSU(zb, x_0 \approx y_0) = \{{z \mapsto \lambda v. xv \approx yv, x_0 \mapsto xb, y_0 \mapsto yb}\}$. Other calculi [1, 11, 21, 34] would apply an explicit primitive substitution rule instead, yielding essentially $(xa \approx ya) \approx \bot \lor (xb \approx yb) \approx \mathbf{T}$. However, in our approach this clause is subsumed and could be discarded immediately. By hoisting the equality to the clausal level, we bypass the redundancy criterion.

Next, BOOLRW can be applied to $xa \approx ya$ with $CSU(xa \approx ya, y_0 \approx y_0) = \{{x \mapsto \lambda v. wavv, y \mapsto \lambda v. wvav, y_0 \mapsto waaa}\}$. The two FALSEELIM steps remove the $\bot \approx \mathbf{T}$ literals. Then $SUP$ is applicable with the unifier $\{w \mapsto \lambda x_1 x_2 x_3. x_2\} \in \text{CSU}(b, wabb)$, and $ERES$ derives the contradiction.

This mechanism resembling primitive substitution is not the only way our calculus can instantiate variables with logical symbols. Often, the correct instantiation can also be found by unification with a logical symbol that is already present:

**Example 26** The following derivation shows that there exists a function $y$ that is equivalent to the conjunction of $p \land x$ and $q \land x$ for all arguments $x$:

$$ \frac{\frac{\exists \langle \iota \rangle (\lambda y. \forall \langle \iota \rangle (\lambda x. y x \approx (p x \wedge q x))) \approx \bot}{\mathbf{T} \approx \bot \lor \forall \langle \iota \rangle (\lambda x. y' x \approx (p x \wedge q x)) \approx \bot} \begin{array}{l} \text{EXISTSHOIST} \\ \text{FORALLRW} \end{array} \quad \frac{\frac{\mathbf{T} \approx \bot \lor (y' (sk y') \approx (p (sk y') \wedge q (sk y'))) \approx \bot}{\mathbf{T} \approx \bot \lor \mathbf{T} \approx \bot} \text{FALSEELIM} \quad \frac{\mathbf{T} \approx \bot}{\bot} \text{FALSEELIM} \end{array} $$
the unifier {$y \mapsto a, x''' \mapsto \lambda u. a$} ∈ CSU(y ≈ y, a ≈ x''' b). Finally, applying ERES twice and FALSEELIM once yields the empty clause.

Remarkably, none of the provers that participated in the CASC-J10 competition can solve this two-clause problem within a minute. Satallax finds a proof after 72 s and LEO-II after over 7 minutes. The CASC-28 version of our new Zipperposition implementation solves it in 3 s.

## 3.5 Soundness

All of our inference rules and axioms are sound w.r.t. $≈$ and the ones that do not introduce Skolem symbols are also sound w.r.t. $|=$. Any derivation using our inference rules and axioms is satisfiability-preserving w.r.t. both $|=$ and $≈$ if the initial clause set does not contain sk symbols. The preprocessing is sound w.r.t. both $|=$ and $≈$:

**Theorem 28 (Soundness and completeness of Q<sub>≈</sub>-normalization)** $Q<sub>≈</sub>-normalization preserves denotations of terms and truth of clauses w.r.t. proper interpretations.

*Proof* It suffices to show that

$$[\forall \langle \tau \rangle]_J^\xi = [[\lambda y. y \approx (\lambda x. \mathbf{T})]]_J^\xi \quad \text{and} \quad [\exists \langle \tau \rangle]_J^\xi = [[\lambda y. y \not\approx (\lambda x. \perp)]]_J^\xi$$

for all types $\tau$, proper interpretations $\mathcal{J} = (\mathcal{J}_{ty}, \mathcal{J}, \mathcal{L})$, and all valuations $\xi$.
Let $f$ be a function from $[[\tau]]_{\mathcal{J}_{ty}}^\xi$ to $\{0, 1\}$. Then

$$[\forall \langle \tau \rangle]_J^\xi(f) = \mathcal{J}(\forall, [[\tau]]_{\mathcal{J}_{ty}}^\xi)(f) = \min \{f(a) \mid a \in [[\tau]]_{\mathcal{J}_{ty}}^\xi\} = \begin{cases} 1 & \text{if } f \text{ is constantly } 1 \\ 0 & \text{otherwise} \end{cases}$$

By the definition of proper interpretations (Sect. 2.2), we have

$$[[\lambda y. y \approx (\lambda x. \mathbf{T})]]_J^\xi(f) = [[y \approx (\lambda x. \mathbf{T})]]_J^\xi[y \to f] = \begin{cases} 1 & \text{if } [[y]]_J^{\xi[y \to f]} = [[\lambda x. \mathbf{T}]]_J^{\xi[y \to f]} \\ 0 & \text{otherwise} \end{cases}$$

Thus, it remains to show that $[[y]]_J^{\xi[y \to f]} = [[\lambda x. \mathbf{T}]]_J^{\xi[y \to f]}$ if and only if $f$ is constantly 1. This holds because by the definition of term denotation, $[[y]]_J^{\xi[y \to f]} = f$ and because $[[\lambda x. \mathbf{T}]]_J^{\xi[y \to f]}(a) = [[\mathbf{T}]]_J^{\xi[x \to a, y \to f]} = 1$ by properness of the interpretation, for all $a \in [[\tau]]_{\mathcal{J}_{ty}}^\xi$. The case of $\exists$ is analogous. □

To show soundness of the inferences, we need the substitution lemma for our logic:

**Lemma 29 (Substitution lemma)** Let $\mathcal{J} = (\mathcal{J}_{ty}, \mathcal{J}, \mathcal{L})$ be a proper interpretation. Then

$$[[\tau \rho]]_{\mathcal{J}_{ty}}^{\xi} = [[\tau]]_{\mathcal{J}_{ty}}^{\xi'} \quad \text{and} \quad [[t \rho]]_{\mathcal{J}}^{\xi} = [[t]]_{\mathcal{J}}^{\xi'}$$

for all terms $t$, all types $\tau$, and all substitutions $\rho$, where $\xi'(\alpha) = [[\alpha \rho]]_{\mathcal{J}_{ty}}^{\xi}$ for all type variables $\alpha$ and $\xi'(x) = [[x \rho]]_{\mathcal{J}}^{\xi}$ for all term variables $x$.

*Proof* Analogous to Lemma 18 of $\lambda\text{Sup}$ [10]. □

It follows that a model of a clause is also a model of its instances:
**Lemma 30** If $\mathcal{J} \models C$ for some interpretation $\mathcal{J}$ and some clause $C$, then $\mathcal{J} \models C_{\rho}$ for all substitutions $\rho$.

*Proof* Analogous to Lemma 19 of $\lambda$Sup [10], using Lemma 29. □

With this lemma in place, we can prove the soundness of our calculus. Some of the rules and axioms are only sound w.r.t. $\models$.

**Theorem 31 (Soundness) Axiom (CHOICE) and all of our inference rules, except for FORALLRW and EXISTSRW, are sound w.r.t. $\models$. All of our axioms and inference rules are sound w.r.t. $\models$. Both of these claims hold even without the variable condition and the side conditions on fluidity, deeply occurring variables, order, and eligibility.**

*Proof* Analogous to Lemma 20 of $\lambda$Sup [10]. For the Boolean rules, we make use of the special requirements on interpretations of logical symbols.

We elaborate on the soundness of FORALLRW, EXISTSRW, and EXT w.r.t. $\models$.

For FORALLRW: Let $\mathcal{J}$ be a Skolem-aware model of $C<u>$. By Lemma 29, $\mathcal{J}$ is a model of $C<u>\sigma$ as well. Since $\sigma \in \text{CSU}(\forall\langle\beta\rangle y, u)$, we have $C<u>\sigma = C<\forall\langle\beta\rangle y>\sigma$. Thus, to show that $\mathcal{J}$ is also a model of the conclusion $C<y(\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, \neg y\sigma z}\langle\tilde{\alpha}\rangle\tilde{x})>\sigma$, it suffices to show that $\mathcal{J} \models \forall\langle\beta\sigma\rangle(y\sigma) \approx y\sigma(\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, \neg y\sigma z}\langle\tilde{\alpha}\rangle\tilde{x})$. This follows directly from the definition of Skolem-awareness (Definition 3), which states that

$$ \mathcal{J} \models (\exists\langle\beta\sigma\rangle (\lambda z. \neg y\sigma z)) \approx \neg y\sigma (\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z. \neg y\sigma z}\langle\tilde{\alpha}\rangle\tilde{x}) $$

For EXISTSRW, we can argue analogously.

For (EXT), we must show that any Skolem-aware model $\mathcal{J}$ is a model of axiom (EXT) $z(\text{diff}(\alpha,\beta)zy) \not\approx y(\text{diff}(\alpha,\beta)zy) \lor z \approx y$. By the definition of Skolem-awareness, we have $\mathcal{J} \models (\exists\langle\alpha\rangle (\lambda x. z x \not\approx y x)) \approx (\lambda x. z x \not\approx y x) (\text{diff}(\alpha,\beta)zy)$. Thus, if the first literal of (EXT) is false in $\mathcal{J}$ for some valuation $\xi$, then

$$ \begin{aligned} 0 &= \llbracket (\lambda x. z x \not\approx y x) (\text{diff}(\alpha,\beta) z y) \rrbracket_{\mathcal{J}}^{\xi} \\ &= \llbracket \exists\langle\alpha\rangle (\lambda x. z x \not\approx y x) \rrbracket_{\mathcal{J}}^{\xi} \\ &= \max\{ \llbracket \lambda x. z x \not\approx y x \rrbracket_{\mathcal{J}}^{\xi}(a) \mid a \in \llbracket \alpha \rrbracket_{\mathcal{J}}^{\xi} \} \\ &= \max\{ \llbracket z x \not\approx y x \rrbracket_{\mathcal{J}}^{\xi}[x \to a] \mid a \in \llbracket \alpha \rrbracket_{\mathcal{J}}^{\xi} \} \end{aligned} $$

It follows that there exists no $a \in \llbracket \alpha \rrbracket_{\mathcal{J}}^{\xi}$ such that $\llbracket z x \rrbracket_{\mathcal{J}}^{\xi}[x \to a] = \llbracket z \rrbracket_{\mathcal{J}}^{\xi}(a)$ and $\llbracket y x \rrbracket_{\mathcal{J}}^{\xi}[x \to a] = \llbracket y \rrbracket_{\mathcal{J}}^{\xi}(a)$ are different. Thus, $\llbracket z \rrbracket_{\mathcal{J}}^{\xi} = \llbracket y \rrbracket_{\mathcal{J}}^{\xi}$ and hence the second literal of (EXT) must be true under $\mathcal{J}$ and $\xi$. □

To prove satisfiability preservation w.r.t. $\models$, we need the following lemma:

**Lemma 32** Let $N \subseteq C_H$ be a clause set that does not contain any sk symbols. Then $N$ is satisfiable w.r.t. $\models$ if and only if it is satisfiable w.r.t. $\models$.

*Proof* If $N$ is satisfiable w.r.t. $\models$, then it is satisfiable w.r.t. $\models$ by definition. For the other direction, we assume that $N$ has a model $\mathcal{J}$, and we must show that there exists a Skolem-aware model $\mathcal{J}'$ of $N$.

To transform the model $\mathcal{J} = (\mathcal{J}_{\text{ty}}, \mathcal{J}', \mathcal{L})$ into a skolem-aware model $\mathcal{J}' = (\mathcal{J}'_{\text{ty}}, \mathcal{J}', \mathcal{L}')$, we redefine the interpretation of the Skolem symbol $\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, t z}$: $\Pi\tilde{\alpha}. \tilde{\tau} \to v$ as follows. Given some domains $\tilde{D}$, let $\xi(\tilde{\alpha}) = \tilde{D}$. Then define $\mathcal{J}'(\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, t z}, \tilde{D}) = \llbracket \lambda\tilde{x}. \varepsilon\langle\nu\rangle t \rrbracket_{\mathcal{J}}^{\xi}$ and $\mathcal{L}'(\xi, \lambda x.s) = \mathcal{L}(\xi, \lambda x.s')$ where $s'$ is obtained from $s$ by replacing each occurrence of a
subterm $sk_{Π\tilde{a}, \forall\tilde{x}. \exists z. t z} \langle \tilde{v} \rangle$ by $(\lambda\tilde{x}. \varepsilon \langle v \rangle t)\{\tilde{a} \mapsto \tilde{v}\}$. This modification of $J$ yields a new interpretation $J'$, which is still a model of $N$ because $N$ does not contain any sk symbols. Moreover, it is a Skolem-aware model of $N$ because our redefinition ensures $J' \models (\exists \langle v \rangle (\lambda z. t z)) \approx t (sk_{Π\tilde{a}, \forall\tilde{x}. \exists z. t z} \langle \tilde{a} \rangle \tilde{x})$. $\square$

**Theorem 33 (Satisfiability preservation)** Any derivation using our inference rules and axioms is satisfiability-preserving w.r.t. both $\models$ and $\Vdash$ if the initial clause set does not contain sk symbols.

*Proof* By Theorem 31, all of our inference rules and axioms are sound w.r.t. $\Vdash$. Thus, they clearly preserve satisfiability w.r.t. $\Vdash$.

If the initial clause set of a derivation does not contain sk symbols and is satisfiable w.r.t. $\models$, it is also satisfiable w.r.t. $\Vdash$ by Lemma 32. By satisfiability preservation w.r.t. $\Vdash$, any clauses derived from this initial clause set are then satisfiable w.r.t. $\Vdash$. By definition of $\Vdash$ (Definition 3), the derived clauses are therefore also satisfiable w.r.t. $\models$. This proves satisfiability preservation w.r.t. $\models$. $\square$

## 3.6 The Redundancy Criterion

As in $\lambda$Sup and $\lambda$Sup, the redundancy criterion and the completeness proof distinguish three levels of logics. We have a higher-order level H, a $Q\approx$-normal ground higher-order level GH, and a ground monomorphic first-order level GF with an interpreted Boolean type. We use $\mathcal{T}_H$, $\mathcal{T}_{GH}$, and $\mathcal{T}_{GF}$ to denote the respective sets of terms, $\mathcal{T}_{y_H}$, $\mathcal{T}_{y_{GH}}$, and $\mathcal{T}_{y_{GF}}$ to denote the respective sets of types, and $C_H$, $C_{GH}$, and $C_{GF}$ to denote the respective sets of clauses. We will define a grounding function $G$ that connects levels H and GH and an encoding $\mathcal{F}$ that connects levels GH and GF. Schematically, the three levels are connected as follows:

<figure><img src="image_3.png" /></figure>

### 3.6.1 Redundancy of Clauses

In first-order superposition, a clause is considered redundant if all its ground instances are entailed by $\leftarrow$-smaller ground instances of other clauses. In essence, this will also be our definition, but we will use a special grounding function $G$ and the entailment notion of the GF level.

Let $(\Sigma_{ty}, \Sigma)$ be the signature of level H. The level GH has the same signature but is restricted to ground $Q\approx$-normal terms and clauses. For the GF level, we employ the logic of oSup [31]. Its signature $(\Sigma_{ty}, \Sigma_{GF})$ is defined as follows. The type constructors $\Sigma_{ty}$ are the same in both signatures, but $\rightarrow$ is an uninterpreted type constructor on GF and not to be confused with the arrow used for type declarations in the logic of oSup [31], which we will avoid in this article due to the ambiguity. For each ground instance $f \langle \tilde{v} \rangle : \tau_1 \rightarrow \dots \rightarrow \tau_n \rightarrow \tau$ of a symbol $f \in \Sigma$, we introduce a first-order symbol $f_j^{\tilde{v}} \in \Sigma_{GF}$ with argument types $\tilde{\tau}_j$ and result type $\tau_{j+1} \rightarrow \dots \rightarrow \tau_n \rightarrow \tau$, for each $j$. This is done for both logical and nonlogical symbols. Moreover, for each ground term $\lambda x.t$, we introduce a symbol $lam_{\lambda x.t} \in \Sigma_{GF}$ of the same type. The symbols $\perp_0$, $\mathcal{T}_0$, $\neg_1$, $\Lambda_2$, $\mathcal{V}_2$, $\rightarrow_2$, $\approx_2^T$, and $\not\approx_2^T$ are identified with the corresponding first-order logical symbols.
**Definition 34 (The grounding function $G$ on terms and clauses)** Given a clause $C \in C_H$, let its ground instances $G(C)$ be the set of all clauses in $C_{GH}$ of the form $C\theta$ for some grounding substitution $\theta$ such that for all free variables $x$ occurring in $C$, the only Boolean green subterms of $x\theta$ are $\mathbf{T}$ and $\mathbf{\perp}$.

Restricting the grounding to the Boolean terms $\mathbf{T}$ and $\mathbf{\perp}$ allows condition O4 to consider only terms $u$ with Boolean subterms $\mathbf{T}$ and $\mathbf{\perp}$. This is crucial because without the restriction no suitable term order would exist. The approach resembles basic superposition [4] where the redundancy criterion only considers ground instances that are irreducible w.r.t. an arbitrary term rewriting system. A disadvantage of basic superposition is that its redundancy criterion severely restricts the simplification machinery because the irreducible terms are unknown during a derivation. In our setting, however, we know that $\mathbf{T}$ and $\mathbf{\perp}$ will be normal forms of the term rewriting system used in the completeness proof. Thus we can restrict grounding to the Boolean terms $\mathbf{T}$ and $\mathbf{\perp}$ without compromising the simplification machinery.

Since we have defined all clauses in $C_{GH}$ to be $Q\approx$-normal, the ground instances $G(C)$ of a clause are $Q\approx$-normal as well. The clauses in $C_{GH}$ being $Q\approx$-normal allow us to define the encoding $\mathcal{F}$ as follows:

**Definition 35 (The encoding $\mathcal{F}$ on terms and clauses)** The encoding $\mathcal{F}: \mathcal{T}_{GH} \to \mathcal{T}_{GF}$ is recursively defined by

$$ \begin{array}{l} \mathcal{F}(\forall\langle\tau\rangle (\lambda x.t)) = \forall x. \mathcal{F}(t) \qquad \mathcal{F}(\exists\langle\tau\rangle (\lambda x.t)) = \exists x. \mathcal{F}(t) \\ \mathcal{F}(x) = x \qquad \mathcal{F}(\lambda x.t) = \mathbf{\Gamma}\mathbf{m}_{\lambda x.t} \qquad \mathcal{F}(f\langle\bar{\nu}\rangle \bar{s}_j) = f_j^{\bar{\nu}}(\mathcal{F}(\bar{s}_j)) \end{array} $$

using $\downarrow_{\beta\eta Q_n}$ representatives of terms. The encoding $\mathcal{F}$ is extended to map from $C_{GH}$ to $C_{GF}$ by mapping each literal and each side of a literal individually.

Although we define $\mathcal{F}$ only on ground terms, the encoding of variables $\mathcal{F}(x) = x$ is necessary for variables bound by $\forall$ and $\exists$. Since the terms $\mathcal{T}_{GH}$ are $Q\approx$-normal, these variables occur neither applied nor inside $\lambda$-expressions.

The mapping $\mathcal{F}$ is clearly bijective. Using the inverse mapping, the order $\succ$ can be transferred from $\mathcal{T}_{GH}$ to $\mathcal{T}_{GF}$ and from $C_{GH}$ to $C_{GF}$ by defining $t \succ s$ as $\mathcal{F}^{-1}(t) \succ \mathcal{F}^{-1}(s)$ and $C \succ D$ as $\mathcal{F}^{-1}(C) \succ \mathcal{F}^{-1}(D)$. The property that $\succ$ on clauses is the multiset extension of $\succ$ on literals, which in turn is the multiset extension of $\succ$ on terms, is maintained because $\mathcal{F}^{-1}$ maps the multiset representations elementwise.

A key property of $\mathcal{F}$ is that there is a bijection between green subterms on GH and subterms on GF that are not below quantifiers:

**Lemma 36** Let $s, t \in \mathcal{T}_{GH}$. If $p$ is a green position in $t$ or a position in $\mathcal{F}(t)$ that is not below a quantifier, we have $\mathcal{F}(t\langle s \rangle_p) = \mathcal{F}(t)[\mathcal{F}(s)]_p$. In other words, $s$ is a green subterm of $t$ at position $p$ if and only if $\mathcal{F}(s)$ is a subterm of $\mathcal{F}(t)$ at position $p$ that is not below a quantifier.

*Proof* Analogous to Lemma 3.17 of $\lambda f\text{Sup}$ [8]. □

**Lemma 37** The relation $\succ$ on $\mathcal{T}_{GF}$ is a term order in the sense of $o\text{Sup}$. That is, it is a well-founded strict order $\succ$ on ground terms such that

1. compatibility with contexts holds, but not necessarily below quantifiers;

2. the subterm property holds, but not necessarily below quantifiers;

3. totality holds;

4. $u \succ \perp_0 \succ \mathbf{T}_0$ for any term $u \in \mathcal{T}_{GF}$ that is not $\mathbf{T}_0$ or $\mathbf{\perp}_0$; and
5. $Qx.t \succ t\{x \mapsto u\}$ for any term $u \in \mathcal{T}_{\text{GF}}$ whose only Boolean subterms are $\mathcal{T}$ and $\perp$.

*Proof* Transitivity and irreflexivity follow directly from transitivity and irreflexivity of $\succ$ on $\mathcal{T}_{\text{GH}}$. Well-foundedness, compatibility with contexts, subterm property and totality can be shown analogously to Lemma 3.19 of $\lambda f \text{Sup}$ [8], using Lemma 36. That $\mathcal{T}$ or $\perp$ are the smallest terms follows from (O3) of Definition 15. Finally, $Qx.t \succ t\{x \mapsto u\}$ follows from (O4) of Definition 15. □

Each of the three levels has an entailment relation $|\models$. A clause set $N_1$ entails a clause set $N_2$, denoted by $N_1 \models N_2$, if all models of $N_1$ are also a models of $N_2$. For H and GH, we use higher-order models; for GF, we use first-order models with interpreted Booleans as defined by oSup [31]. We write $N_1 \models_f N_2$ to abbreviate $\mathcal{F}(N_1) \models \mathcal{F}(N_2)$ and $N_1 \models_g N_2$ to abbreviate $\mathcal{G}(N_1) \models \mathcal{G}(N_2)$. On the H level, we additionally define Skolem-aware entailment, denoted by $N_1 \asymp N_2$, to hold if all Skolem-aware models of a clause set $N_1 \subseteq C_H$ are also models of a clause set $N_2 \subseteq C_H$.

We define the sets of redundant clauses w.r.t. a clause set as follows:

- Given $C \in C_{\text{GF}}$ and $N \subseteq C_{\text{GF}}$, let $C \in \text{GFRed}_C(N)$ if $\{D \in N \mid D \prec C\} \models C$.

- Given $C \in C_{\text{GH}}$ and $N \subseteq C_{\text{GH}}$, let $C \in \text{GHRed}_C(N)$ if $\mathcal{F}(C) \in \text{GFRed}_C(\mathcal{F}(N))$.

- Given $C \in C_H$ and $N \subseteq C_H$, let $C \in \text{HRed}_C(N)$ if for every $D \in \mathcal{G}(C)$, we have $D \in \text{GHRed}_C(\mathcal{G}(N))$ or there exists $C' \in N$ such that $C \sqsupset C'$ and $D \in \mathcal{G}(C')$.

The tiebreaker $\sqsupset$ can be an arbitrary well-founded partial order on $C_H$, natural candidates being restrictions of (ill-founded) strict subsumption [10, Sect. 3.4].

### 3.6.2 Redundancy of Inferences

Standard simplification rules and most other optimizations can be justified by clause redundancy. For a few other prover optimizations (e.g., simultaneous superposition [6]), a notion of inference redundancy is required. For first-order superposition, an inference is considered redundant if for each of its ground instances, a premise is redundant or the conclusion is entailed by clauses smaller than the main premise. For most inference rules, our definition follows this idea, using specific ground instances and $|\models_f$ for entailment; other rules need nonstandard notions of inference redundancy.

Each of the three levels has an associated inference system *HInf*, *GHInf*, and *GFInf*. For H, it is the inference system *HInf* consisting of the rules described above. We view axioms (EXT) and (CHOICE) as premiseless inference rules EXT and CHOICE, respectively. We fix the selection functions *HLitSel* and *HBoolSel* globally.

The system *GHInf* is parameterized by selection functions and a witness function, which are defined as follows.

**Definition 38 (GH level selection functions)** A GH level literal selection function $GHLitSel$ maps each clause $C \in C_{\text{GH}}$ to a subset of its literals. A GH level Boolean subterm selection function $GHBoolSel$ maps each clause $C \in C_{\text{GH}}$ to a subset of its green positions with Boolean subterms.

We require these selection functions to have the property that for every $C \in C_{\text{GH}}$, there exists a $D \in C_H$ with $C \in \mathcal{G}(D)$ for which the selections $HLitSel(D)$, $HBoolSel(D)$ and the selections $GHLitSel(C)$, $GHBoolSel(C)$ correspond in the following sense: A literal $K$ is selected in $C$ if and only if there exists a selected literal $L$ in $D$ with $L\theta = K$; a green position $C.K.p$ is selected in $C$ if and only if there exists a literal $L$ in $D$ with $L\theta = K$ such that $D.L.p$ is selected.
**Definition 39 (Witness function)** A witness function GHWit maps a clause $C \in \mathcal{C}_{GH}$ and a green position of a quantifier-headed term in $C$ to a term $GHWit(C, p) \in \mathcal{T}_{GH}$ such that $Q\langle\tau\rangle t \succ t GHWit(C, p)$ if $C|_p = Q\langle\tau\rangle t$.

The witness function will be used to provide appropriate Skolem terms that witness the existence of terms fulfilling the given predicate.

In our completeness proof, the choice of the GH level selection and witness functions will depend on the saturated clause set in the limit of the derivation. Since we do not know this clause set during the derivation, we need to consider all possible parameters in our redundancy criterion:

**Definition 40 (Set of parameter triples $Q$)** Let $Q$ be the set of parameters triples $(GHLitSel, GHBoolSel, GHWit)$ where $GHLitSel$ and $GHBoolSel$ are GH level selection functions and $GHWit$ is a witness function.

We write $GHInf^q$ with $q = (GHLitSel, GHBoolSel, GHWit) \in Q$ to specify the inference system for a given set of parameters. The rules of $GHInf^q$ include $SUP$, $ERES$, $EFACT$, $BOOLHOIST$, $FALSEELIM$, $EQHOIST$, $NEQHOIST$, and $BOOLRW$ with the restriction that all references to $\succeq$ are replaced by $\succeq$.

In addition, $GHInf^q$ contains the rules $GFORALLHOIST$, $GEXISTSHOIST$, $GARGCONG$, $GEXT$, and $GCHOICE$, which enumerate ground terms in the conclusion where their $HInf$ counterparts use fresh variables. They enumerate all terms $u \in \mathcal{T}_{GH}$ such that the only Boolean green subterms of $u$ are $\mathbf{T}$ and $\mathbf{\perp}$. Let $\mathcal{T}_{GH}^*$ be the set of all such terms $u$. Then these rules are stated as follows:

$$ \frac{C\langle\forall\langle\tau\rangle v\rangle_p}{C\langle\perp\rangle \lor vu \approx \mathbf{T}} \quad \text{GFORALLHOIST} \qquad \frac{C\langle\exists\langle\tau\rangle v\rangle_p}{C\langle\mathbf{T}\rangle \lor vu \approx \mathbf{\perp}} \quad \text{GEXISTSHOIST} $$

where $p$ is $\succeq$-eligible in $C$ and $u \in \mathcal{T}_{GH}^*$.

$$ \frac{C' \lor t \approx s}{C' \lor t \bar{u} \approx s \bar{u}} \quad \text{GARGCONG} $$

where $t \approx s$ is strictly $\succeq$-eligible in $C' \lor t \approx s$ and $u_i \in \mathcal{T}_{GH}^*$.

The rules $GEXT$ and $GCHOICE$ are premiseless and their conclusions are the infinitely many $G$-instances of $(EXT)$ and $(CHOICE)$, respectively.

Moreover, $GHInf^q$ contains the following two rules, which use the witness function $GHWit$ instead of Skolem terms:

$$ \frac{C\langle\forall\langle\tau\rangle v\rangle_p}{C\langle v \text{GHWit}(C, p)\rangle_p} \quad \text{GFORALLRW} \qquad \frac{C\langle\exists\langle\tau\rangle v\rangle_p}{C\langle v \text{GHWit}(C, p)\rangle_p} \quad \text{GEXISTSRW} $$

where $p$ is $\succeq$-eligible in $C$; for $GFORALLRW$, $\mathcal{F}(C\langle\mathbf{T}\rangle_p)$ is not a tautology; and for $GEXISTSRW$, $\mathcal{F}(C\langle\perp\rangle_p)$ is not a tautology.

The inference systems $GHInf^q$ are indeed inference systems on $\mathcal{C}_{GH}$—i.e., if the premises are in $\mathcal{C}_{GH}$, the conclusions are in $\mathcal{C}_{GH}$, too. The conclusions are obviously ground. They are also $Q\mathcal{R}$-normal:

**Lemma 41** If the premises of a $GHInf^q$ inference are $Q\mathcal{R}$-normal, then the conclusion is also $Q\mathcal{R}$-normal.
**Proof** The conclusions of GEXT and GCHOICE are $Q_{\sim}$-normal because $\mathcal{G}$ maps into $C_{GH}$, which is restricted to $Q_{\sim}$-normal clauses.

The definition of $Q_{\sim}$-normality (Definition 6) clearly only depends on the contained quantifier-headed subterms. As long as no new quantifier-headed subterms are added, a clause set cannot become $Q_{\sim}$-reducible.

The inference rules ERES, EFACT, and FALSEELIM do not introduce any subterms that were not already present in the premises. The inference rules SUP, BOOLHOIST, EQHOIST, NEQHOIST, BOOLRW only introduce new subterms by replacing a green subterm of a $Q_{\sim}$-normal term by another $Q_{\sim}$-normal term. Since green positions are never below quantifiers, these rules also do not add new quantifier-headed subterms.

For the inference rules GFORALLHOIST, GEXISTSHOIST, GARGCONG, GFORALLRW, and GEXISTSRW, we can use Lemma 14 to show that the conclusions are $Q_{\sim}$-normal. $\square$

The inference system $GInf$ is parameterized by an analogous parameter triple $(GFLitSel, GFBoolSel, GFWit)$. Using the bijection $\mathcal{F}$, we can translate a parameter triple $q$ of $GHInf$ to a parameter triple $\mathcal{F}(q)$ of $GInf$. Let $GInf^{\mathcal{F}(q)}$ be the inference system containing the inferences isomorphic to $GHInf^q$ obtained by $\mathcal{F}$, except for GARGCONG, GEXT, and GCHOICE. This is essentially identical to the ground inference system of oSup [31].

We extend the functions $\mathcal{F}$ and $\mathcal{G}$ to inferences:

**Notation 42** Given an inference $\iota$, we write $prems(\iota)$ for the tuple of premises, $mprem(\iota)$ for the main (i.e., rightmost) premise, and $concl(\iota)$ for the conclusion.

**Definition 43 (The encoding $\mathcal{F}$ on inferences)** Given an inference $\iota \in GHInf$ that is not a GARGCONG, GEXT, or GCHOICE inference, let $\mathcal{F}(\iota) \in GInf$ denote the inference defined by $prems(\mathcal{F}(\iota)) = \mathcal{F}(prems(\iota))$ and $concl(\mathcal{F}(\iota)) = \mathcal{F}(concl(\iota))$.

**Definition 44 (The grounding function $\mathcal{G}$ on inferences)** Given a parameter triple $q \in Q$ and an inference $\iota \in HInf$, we define the set $\mathcal{G}^q(\iota)$ of ground instances of $\iota$ to be all inferences $\iota' \in GHInf^q$ such that $prems(\iota') = prems(\iota)\theta$ and $concl(\iota') = concl(\iota)\theta$ for some grounding substitution $\theta$.

Thus, $\mathcal{G}$ maps FLUIDSUP to SUP, FLUIDBOOLHOIST to BOOLHOIST, FORALLRW to GFORALLRW, EXISTSRW to GEXISTSRW, FORALLHOIST to GFORALLHOIST, EXISTSHOIST to GEXISTSHOIST, ARGCONG to GARGCONG, EXT to GEXT, CHOICE to GCHOICE, and inferences of other $HInf$ rules to inferences of the identically named rules in $GHInf$. For FLUIDLOOBHOIST, which needs not be grounded to prove refutational completeness, we let $\mathcal{G}^q(\iota) = \text{undef}$. Although the rules FLUIDBOOLHOIST and FLUIDLOOBHOIST are dual to each other, their redundancy criteria are asymmetric because only FLUIDBOOLHOIST has a counterpart in $GHInf$, namely BOOLHOIST.

We define the sets of redundant inferences w.r.t. a given clause set as follows:

- Given $\iota \in GInf^q$ and $N \subseteq C_{GF}$, let $\iota \in GFRed_1^q(N)$ if $prems(\iota) \cap GFRed_c(N) \neq \emptyset$ or $\{D \in N | D \prec mprem(\iota)\} \models concl(\iota)$.

- Given $\iota \in GHInf^q$ and $N \subseteq C_{GH}$, let $\iota \in GHRed_1^q(N)$ if

- $\iota$ is GARGCONG, GEXT, or GCHOICE and $concl(\iota) \in N \cup GHRed_c(N)$; or

- $\iota$ is any other inference and $\mathcal{F}(\iota) \in GFRed_1^{\mathcal{F}(q)}(\mathcal{F}(N))$.

- Given $\iota \in HInf$ and $N \subseteq C_H$, let $\iota \in HRed_1(N)$ if

- $\iota$ is a FLUIDLOOBHOIST inference and $\mathcal{G}(concl(\iota)) \subseteq \mathcal{G}(N) \cup GHRed_c(\mathcal{G}(N))$ or

- $\iota$ is any other inference and $\mathcal{G}^q(\iota) \subseteq GHRed_1(\mathcal{G}(N))$ for all $q \in Q$.
Some authors prefer not to define inferences with a redundant premise as redundant, but in our proof of refutational completeness, this will be crucial for the lifting lemma of FORALLRw and EXISTSRw.

A clause set $N$ is saturated w.r.t. an inference system and the inference component $Red_I$ of a redundancy criterion if every inference from clauses in $N$ is in $Red_I(N)$.

## 3.7 Simplification Rules

The redundancy criterion ($HRed_I$, $HRed_C$) is strong enough to support most simplification rules implemented in Schulz's first-order prover E [33, Sects. 2.3.1 and 2.3.2], although some require minor adaptions. To describe the adaptions, we introduce the notion of blue subterms, which include all green subterms but also some subterms below quantifiers.

**Definition 45 (Blue subterms and positions)** Blue subterms and positions are inductively defined as follows. A blue position is a tuple of natural numbers. For any $\lambda$-term $t$, the empty tuple $\varepsilon$ is a blue position of $t$, and $t$ is the blue subterm of $t$ at position $\varepsilon$. For all symbols $f \in \Sigma \setminus \{\forall, \exists\}$, if $t$ is a blue subterm of $u_i$ at position $p$, then $i.p$ is a blue position of $f \langle \bar{\tau} \rangle \bar{u}$, and $t$ is the blue subterm of $f \langle \bar{\tau} \rangle \bar{u}$ at position $i.p$. If $t$ is a blue subterm of $u$ at position $p$, then $1.p$ is a blue position of $Q \langle \tau \rangle (\lambda x. u)$ and $t$ is the blue subterm of $Q \langle \tau \rangle (\lambda x. u)$ at position $1.p$.

For example, the blue subterms of $f(g(\neg p)) (\forall \langle \tau \rangle (\lambda x. q)) (y a) (\lambda x. h b)$ are all of the green subterms and $q$. The notions of blue positions and subterms are lifted to $\beta\eta$-equivalence classes via the $\beta\eta Q\eta$-normal representative.

Deletion of duplicated literals, deletion of resolved literals, syntactic tautology deletion, negative simplify-reflect, and clause subsumption adhere to our redundancy criterion. Positive simplify-reflect and equality subsumption are supported by our criterion if they are applied on blue subterms. Semantic tautology deletion can be applied as well, but we must use the entailment relation $\models$. Rewriting of positive and negative literals (demodulation) can only be applied on blue subterms. Moreover, for positive literals, the rewriting clause must be smaller than the rewritten clause—a condition that is also necessary with the standard first-order redundancy criterion but not always fulfilled by Schulz's rule. As for destructive equality resolution, even in first-order logic the rule cannot be justified with the standard redundancy criterion, and it is unclear whether it preserves refutational completeness.

As a representative example, we show how demodulation into green contexts can be justified. Demodulation into blue contexts and the other simplification rules can be justified similarly.

**Lemma 46 Demodulation into green contexts is a simplification:**

$$ \frac{\begin{array}{c} t \approx t' \\ \hline t \approx t' \end{array}}{\begin{array}{c} \overbrace{s \langle t \sigma \rangle \approx s' \vee C'}^{C} \\ \hline s \langle t' \sigma \rangle \approx s' \vee C' \end{array}} \text{DEMOD} $$

where $t\sigma \succ t'\sigma$ and $C \succ (t \approx t')\sigma$. It adheres to our redundancy criterion—i.e., the deleted premise $C$ is redundant w.r.t. the conclusions.

*Proof* Let $N$ be the set consisting of the two conclusions. We must show that $C \in HRed_C(N)$. Let $C\theta$ be a ground instance of $C$. By the definition of $HRed_C$, it suffices to show that $C\theta \in GHRed_C(G(N))$. By the definition of $GHRed_C$, it thus suffices to show that $\mathcal{F}(C\theta) \in$
$GF_{Red_C}(\mathcal{F}(G(N)))$. By the definition of $GF_{Red_C}$, this is equivalent to proving that the clauses in $\mathcal{F}(G(N))$ that are smaller than $\mathcal{F}(C\theta)$ entail $\mathcal{F}(C\theta)$.

By compatibility with green contexts and stability under substitutions of $>$, the condition $t\sigma \succ t'\sigma$ implies that $D = \mathcal{F}((s<t's') \approx s' \lor C')\theta$ is a clause in $\mathcal{F}(G(N))$ that is smaller than $\mathcal{F}(C\theta)$. By stability under substitutions, $C \succ (t \approx t')\sigma$ implies that $E = \mathcal{F}((t \approx t')\sigma\theta)$ is another clause in $\mathcal{F}(G(N))$ that is smaller than $\mathcal{F}(C\theta)$. By Lemma 36, green subterms on the GH level correspond to subterms on the GF level. Thus, $\{D, E\} \models \mathcal{F}(C\theta)$ by congruence. $\square$

All of $\lambda$Sup's extensions [10, Sect. 5] can also be used in our setting. DEMODEXT and PRUNEARG are sound w.r.t. both $\models$ and $\cong$. NEGEXT, EXTINST, and $\lambda$SUP are sound w.r.t. $\cong$ if the appropriate sk symbols are reused. As shown in the proof of Theorem 33, this implies that these rules are satisfiability-preserving w.r.t. $\models$, provided that the initial clause set does not contain sk symbols. If fresh Skolem symbols are used, the rules are satisfiability-preserving w.r.t. both $\models$ and $\cong$. DUPSUP and FLEXSUP are sound w.r.t. both $\models$ and $\cong$.

Under some circumstances, certain inference rules of our calculus can be applied as simplifications—i.e., a premise can be deleted after performing them. The FALSEELIM and BOOLRW rules can be applied as a simplification if $\sigma$ is the identity. If the head of $u$ is $\forall$, FORALLHOIST and FORALLRW can both be applied and, together, serve as one simplification rule. If the head of $u$ is $\forall$ and FORALLRW cannot be applied due to its condition 5, FORALLHOIST alone serves as a simplification rule. The same holds for EXISTS- HOIST and EXISTSRW if the head of $u$ is $\exists$. For all of these simplifications, the eligibility conditions can be ignored.

If $\sigma$ is the identity, the rule BOOLHOIST can also be applied as a simplification in combination with the following rule to the same subterm $u$:

$$ \frac{C<u>}{C<T> \lor u \approx \bot} \text{ LOOBHOIST} $$

Again, the eligibility condition can be ignored, and $u$ can even be a fully applied logical symbol as long as it is not $T$ or $\bot$.

## 3.8 Clausification

Like $o$Sup, our calculus does not require the input problem to be clausified during the preprocessing, and it supports higher-order analogs of the three inprocessing clausification methods introduced by Nummelin et al. *Inner delayed clausification* relies on our core calculus rules to destruct logical symbols. *Outer delayed clausification* adds the following clausification rules to the calculus:

$$ \begin{array}{l} \frac{s \approx T \lor C}{oc(s, C)} \quad \text{POSOUTERCLAUS} \qquad \frac{s \approx \bot \lor C}{oc(\neg s, C)} \quad \text{NEGOUTERCLAUS} \\ \frac{s \approx \bot \lor C}{s \approx \bot \lor t \approx T \lor C} \quad \frac{s \approx T \lor t \approx \bot \lor C}{s \approx \bot \lor t \approx T \lor C} \quad \text{EQOUTERCLAUS} \\ \frac{s \approx \bot \lor t \approx \bot \lor C}{s \approx \bot \lor t \approx T \lor C} \quad \frac{s \approx t \lor C}{s \approx \bot \lor t \approx T \lor C} \quad \text{NEQOUTERCLAUS} \end{array} $$
The double bars identify simplification rules (i.e., the conclusions make the premise redundant and can replace it). The first two rules require that *s* has a logical symbol as its head, whereas the last two require that *s* and *t* are Boolean terms other than **T** and **⊥**. The function *oc* distributes the logical symbols over the clause *C*—e.g., *oc*(*s* → *t*, *C*) = {*s* ≈ **⊥** ∨ *t* ≈ **T** ∨ *C*}, and *oc*(*¬*(*s* ∨ *t*), *C*) = {*s* ≈ **⊥** ∨ *C*, *t* ≈ **⊥** ∨ *C*}. It is easy to check that our redundancy criterion allows us to replace the premise of the OUTERCLAUS rules with their conclusion. Nonetheless, we apply EQOUTERCLAUS and NEQOUTERCLAUS as inferences because the premises might be useful in their original form.

Besides the two delayed clausification methods, a third inprocessing clausification method is *immediate* clausification. This clausifies the input problem’s outer Boolean structure in one swoop, resulting in a set of higher-order clauses. If unclausified Boolean terms rise to the top during saturation, the same algorithm is run to clausify them. This method can be made to adhere to our redundancy criterion as well, although advanced clausification techniques such as the Tseitin transformation [36] and miniscoping [30] sometimes violate the criterion. The observations described for oSup [31, Sect. 6] essentially apply to our calculus as well.

Unlike delayed clausification, immediate clausification is a black box and is unaware
of the proof state other than the Boolean term it is applied to. Delayed clausification, on
the other hand, clausifies the term step by step, allowing us to interleave clausification with
the strong simplification machinery of superposition provers. It is especially powerful in
higher-order contexts: Examples such as ypq̸<sub>≈</sub> (pVq) can be refuted directly by equality
resolution, rather than via more explosive rules on the clausified form.

3.9 A Concrete Term Order

We define a concrete order ≽_λ that fulfills the properties of a strict term order as defined in
Definition 17 to show that the requirements can indeed be fulfilled and to provide a concrete
order for implementations of our calculus.

Given a signature $(\Sigma_{ty}, \Sigma)$, we encode types and terms as terms over the untyped first-order signature $\Sigma_{ty} \uplus \{f_k \mid f \in \Sigma, k \in \mathbb{N}\} \uplus \{\text{lam}, \forall^i, \exists^j \mid \text{db}_k^i \mid i, k \in \mathbb{N}\}$. The encoding introduces an identically named first-order (term) variable $\alpha$ for each higher-order type variable $\alpha$, a first-order variable $z_x$ for each higher-order variable $x$, and a first-order variable $z_t$ for each fluid higher-order term $t$. We define the encoding in two parts. The first part is the encoding $O$, resembling the one defined for $\Lambda$Sup. The auxiliary function $\mathcal{B}_x(t)$ replaces each free occurrence of the variable $x$ by a De Bruijn index—that is, a symbol $db^i$ where $i$ is the number of $\lambda$-expressions surrounding the variable occurrence. The encoding $O$ recursively encodes higher-order types into untyped first-order terms as follows: $O(\alpha) = \alpha$ and $O(\kappa(\bar{\tau})) = \kappa(O(\bar{\tau}))$. Using $\beta\eta Q_\eta$-normal representatives, it recursively encodes higher-order terms into untyped first-order terms as follows:

$$
O(t) = \begin{cases}
z_t & \text{if } t = x \text{ or } t \text{ is fluid} \\
\text{lam}(O(\tau), O(\mathcal{B}_x(u))) & \text{if } t = (\lambda x : \tau. u) \text{ and } t \text{ is not fluid} \\
f_k(O(\bar{\tau}), O(\bar{u}_k)) & \text{if } t = f(\bar{\tau}) \bar{u}_k \text{ and either } f \notin \{\forall, \exists\} \text{ or } k = 0 \\
Q_1(O(\tau), O(\mathcal{B}_x(u))) & \text{if } t = Q(\tau)(\lambda x : \tau. u)
\end{cases}
$$

Via this encoding, the term order conditions (O1), (O2), and (O3) can be easily achieved.
For (O4), however, we need to transform the encoded term further to ensure that the symbols
∀₁ and ∃₁ occur only as translations of fully applied quantifiers in green contexts. Then we
can achieve (O4) by assigning them a large weight. The function P transforms the result of O
in this way by applying a function $p$ to all subterms below $\lambda m$ symbols. It maps untyped first-order terms to untyped first-order terms as follows:

$$ \mathcal{P}(t) = \begin{cases} \alpha & \text{if } t = \alpha \\ z_u & \text{if } t = z_u \\ \lambda m(\tau, p(u)) & \text{if } t = \lambda m(\tau, u) \\ f(\mathcal{P}(\bar{\tau})) & \text{if } t = f(\bar{\tau}) \text{ and } f \neq \lambda m \end{cases} $$

In particular, for any higher-order type $\tau$, we have $\mathcal{P}(O(\tau)) = O(\tau)$ because $\lambda$-expressions do not occur in types.

The function $p$ replaces $\forall_1$ by $\forall'_1$, $\exists_1$ by $\exists'_1$, and $z_u$ by a fresh variable $z'_u$.

$$ p(t) = \begin{cases} \alpha & \text{if } t = \alpha \\ z'_u & \text{if } t = z_u \\ \forall'_1(\tau, p(u)) & \text{if } t = \forall_1(\tau, u) \\ \exists'_1(\tau, p(u)) & \text{if } t = \exists_1(\tau, u) \\ f(p(\bar{\tau})) & \text{if } t = f(\bar{\tau}) \text{ and } f \notin \{\forall_1, \exists_1\} \end{cases} $$

Again, for any higher-order type $\tau$, we have $p(O(\tau)) = O(\tau)$ because the variables $z_u$ and the constants $\forall_1$ and $\exists_1$ never occur in the result of applying $O$ to types.

For example, $O$ encodes the term $\forall \langle t \rangle (\lambda x. p y (\lambda u. f y (\forall \langle t \rangle (\lambda v. u))))$ into the first-order term $\forall_1 (t, p_3(z_y, z_y, \lambda m(o, f_3(z_y, z_y, \forall_1 (t, db^1)))))$ and $\mathcal{P}$ transforms it further into $\forall_1 (t, p_3(z_y, z_y, \lambda m(o, f_3(z'_y, z'_y, \forall'_1 (t, db^1)))))$.

Using the encoding $O$ and the function $\mathcal{P}$, we define our term order $\succ_\lambda$. Let $\succ_{kb}$ be the transfinite Knuth-Bendix order [28] on first-order terms. The weight of $\forall_1$ and $\exists_1$ must be $\omega$, the weight of $T_0$ and $\bot_0$ must be 1, and the weights of all other symbols must be smaller than $\omega$. The precedence $\succ$ must be total and $\bot_0 > T_0$ must be the symbols of lowest precedence. We do not use subterm coefficients (i.e., all coefficients are 1), nor a symbol of weight 0. Let $\succ_p$ be the order induced by $\mathcal{P}$ from $\succ_{kb}$, meaning $t \succ_p s$ if and only if $\mathcal{P}(t) \succ_{kb} \mathcal{P}(s)$. Let $\succ_\lambda$ be the order induced by $O$ from $\succ_p$, meaning $t \succ_\lambda s$ if and only if $O(t) \succ_p O(s)$. We extend $\succ_\lambda$ to literals and clauses in the usual way. We will show that $\succ_\lambda$ fulfills the properties of a strict term order:

**Lemma 47** The restriction of $\succ_\lambda$ to ground terms is a strict ground term order, as defined in Definition 15.

*Proof* We follow the proof of Lemma 31 of Bentkamp et al. The transfinite Knuth-Bendix order $\succ_{kb}$ has been shown to enjoy irreflexivity, transitivity, well-foundedness, totality on ground terms, the subterm property, and compatibility with contexts [28]. Transitivity and irreflexivity of $\succ_{kb}$ imply transitivity and irreflexivity of $\succ_\lambda$, respectively.

**WELL-FOUNDEDNESS:** If there existed an infinite chain $t_1 \succ_\lambda t_2 \succ_\lambda \dots$ of ground terms, there would also be the chain $\mathcal{P}(O(t_1)) \succ_{kb} \mathcal{P}(O(t_2)) \succ_{kb} \dots$, contradicting the well-foundedness of $\succ_{kb}$.

**TOTALITY:** For any ground terms $t$ and $s$ we have $\mathcal{P}(O(t)) \succ_{kb} \mathcal{P}(O(s))$, $\mathcal{P}(O(t)) \prec_{kb} \mathcal{P}(O(s))$, or $\mathcal{P}(O(t)) = \mathcal{P}(O(s))$ by ground totality of $\succ_{kb}$. In the first two cases, it follows that $t \succ_\lambda s$ or $t \prec_\lambda s$ respectively. In the last case, it follows that $t = s$ because $O$ and $\mathcal{P}$ are clearly injective.
(O1): By induction on the depth of the context, it suffices to show that $t \succcurlyeq \lambda s$ implies $f(\langle \bar{\tau} \rangle) \bar{u} t \bar{v} \succcurlyeq \lambda f(\langle \bar{\tau} \rangle) \bar{u} s \bar{v}$ for all $t, s, f \in \Sigma \setminus \{\forall, \exists\}, \bar{\tau}, \bar{u}, \bar{v}$. This amounts to showing that $\mathcal{P}(O(t)) \succcurlyeq_{kb} \mathcal{P}(O(s))$ implies

$$ 
\begin{aligned}
\mathcal{P}(O(f(\langle \bar{\tau} \rangle) \bar{u} t \bar{v})) &= \mathcal{P}(f_k(O(\bar{\tau})), O(\bar{u}), O(t), O(\bar{v}))) = \\
&\quad f_k(\mathcal{P}(O(\bar{\tau})), \mathcal{P}(O(\bar{u})), \mathcal{P}(O(t)), \mathcal{P}(O(\bar{v}))) \succcurlyeq_{kb} f_k(\mathcal{P}(O(\bar{\tau})), \mathcal{P}(O(\bar{u})), \mathcal{P}(O(s)), \mathcal{P}(O(\bar{v}))) \\
&= \mathcal{P}(f_k(O(\bar{\tau})), O(\bar{u}), O(s), O(\bar{v}))) = \mathcal{P}(O(f(\langle \bar{\tau} \rangle) \bar{u} s \bar{v}))
\end{aligned}
$$

which follows directly from compatibility of $\succcurlyeq_{kb}$ with contexts and the induction hypothesis.

(O2): Let $s$ be a term. We show that $s \succeq_{\lambda} s|_p$ by induction on $p$, where $s|_p$ denotes the green subterm at position $p$. If $p = \varepsilon$, this is trivial. If $p = p'.i$, we have $s \succeq_{\lambda} s|_{p'}$ by the induction hypothesis. Hence, it suffices to show that $s|_{p'} \succeq_{\lambda} s|_{p'.i}$. From the existence of the position $p'.i$, we know that $s|_{p'}$ must be of the form $s|_{p'} = f(\langle \bar{\tau} \rangle) \bar{u}_k$ for some $f \in \Sigma \setminus \{\forall, \exists\}$. Then $s|_{p'.i} = u_i$. The encoding yields $\mathcal{P}(O(s|_{p'})) = \mathcal{P}(f_k(O(\bar{\tau})), O(\bar{u}_k))) = f_k(\mathcal{P}(O(\bar{\tau})), \mathcal{P}(O(\bar{u}_k)))$ and hence $\mathcal{P}(O(s|_{p'})) \succeq_{kb} \mathcal{P}(O(s|_{p'.i}))$ by the subterm property of $\succcurlyeq_{kb}$. Hence, $s|_{p'} \succeq_{\lambda} s|_{p'.i}$ and thus $s \succeq_{\lambda} s|_p$.

(O3): Since we do not have a symbol of weight 0, and $T_0$ and $\perp_0$ have weight 1, there cannot be any term of smaller weight. Since moreover $T_0$ and $\perp_0$ have the lowest precedence, they are the smallest terms w.r.t. $\succcurlyeq_{kb}$. We have $\perp_0 \succcurlyeq_{kb} T_0$ because $\perp_0$ has higher precedence. Since $\mathcal{P}(O(T)) = T_0$ and $\mathcal{P}(O(T)) = \perp_0$, it follows that $T$ and $\perp$ are the smallest ground terms w.r.t. $\succcurlyeq_{\lambda}$ and that $\perp \succcurlyeq_{\lambda} T$.

(O4): Let $Q(\langle \tau \rangle) t$ and $u$ be $Q$-normal ground terms. We assume that the Boolean green subterms of $u$ are $T$ and $\perp$. We must show $Q(\langle \tau \rangle) t \succcurlyeq \lambda tu$, which is equivalent to $\mathcal{P}(O(Q(\langle \tau \rangle) t)) \succcurlyeq_{kb} \mathcal{P}(O(tu))$.

All symbols except $\forall_1$ and $\exists_1$ have finite weight. Only $\forall_1$ and $\exists_1$ have weight $\omega$. Since all subterm coefficients are 1, the coefficient of $\omega$ in the weight of a given term indicates the number of occurrences of the symbols $\forall_1$ and $\exists_1$ in that term.

In $\eta$-expanded form, we have $t = \lambda x. s$ for some $s$. Then we have $\mathcal{P}(O(Q(\langle \tau \rangle) t)) = Q_1(\mathcal{P}(O(\tau)), \mathcal{P}(O(B_x(s))))$ and $\mathcal{P}(O(tu)) = \mathcal{P}(O(s\{x \mapsto u\}))$. By $Q$-normality, $x$ occurs free only in green positions of $s$. Therefore, replacing $x$ by $u$ in $s$ does not trigger any $\beta\eta Q$-normalizations. Thus, $\mathcal{P}(O(B_x(s)))$ and $\mathcal{P}(O(s\{x \mapsto u\}))$ are almost identical, except that $\mathcal{P}(O(B_x(s)))$ contains $db^i$ where $\mathcal{P}(O(s\{x \mapsto u\}))$ contains $\mathcal{P}(O(u))$. Since the only Boolean green subterms of $u$ are $T$ and $\perp$, $\mathcal{P}(O(u))$ does not contain $\forall_1$ or $\exists_1$. So $\mathcal{P}(O(B_x(s)))$ and $\mathcal{P}(O(s\{x \mapsto u\}))$ contain the same number of $\forall_1$ and $\exists_1$ symbols. Hence, $\mathcal{P}(O(Q(\langle \tau \rangle) t))$ contains exactly one more of these symbols than $\mathcal{P}(O(tu))$. This means that the weight of the former is larger than the weight of the latter and thus $\mathcal{P}(O(Q(\langle \tau \rangle) t)) \succcurlyeq_{kb} \mathcal{P}(O(tu))$. $\square$

**Lemma 48** The relation $\succcurlyeq_{\lambda}$ is a strict term order as defined in Definition 17.

*Proof* Given Lemma 47, it remains to show that $\succcurlyeq_{\lambda}$ is stable under grounding substitutions. Assume $s \succcurlyeq_{\lambda} s'$ for some terms $s$ and $s'$. Let $\theta$ be a higher-order substitution grounding $s$ and $s'$. We must show $s\theta \succcurlyeq_{\lambda} s'\theta$. We will define a first-order substitution $\rho$ grounding $\mathcal{P}(O(s))$ and $\mathcal{P}(O(s'))$ such that $\mathcal{P}(O(s))\rho = \mathcal{P}(O(s\theta))$ and $\mathcal{P}(O(s'))\rho = \mathcal{P}(O(s'\theta))$. Since $s \succcurlyeq_{\lambda} s'$, we have $\mathcal{P}(O(s)) \succcurlyeq_{kb} \mathcal{P}(O(s'))$. The transfinite Knuth-Bendix order $\succcurlyeq_{kb}$ has been shown to be stable under substitutions [28]. Hence, $\mathcal{P}(O(s))\rho \succcurlyeq_{kb} \mathcal{P}(O(s'))\rho$ and therefore $\mathcal{P}(O(s\theta)) \succcurlyeq_{kb} \mathcal{P}(O(s'\theta))$ and $s\theta \succcurlyeq_{\lambda} s'\theta$.

We define the first-order substitution $\rho$ as $\alpha\rho = \alpha\theta$ for type variables $\alpha, z_u\rho = \mathcal{P}(O(u\theta))$, and $z'_u\rho = p(O(u\theta))$ for terms $u$. Strictly speaking, the domain of a substitution must be finite,
so we restrict this definition of $\rho$ to the finitely many variables that occur in the computation of $\mathcal{P}(O(s))$ and $\mathcal{P}(O(s'))$.

Clearly, we have $\mathcal{P}(O(\tau))\rho = \mathcal{P}(O(\tau\theta))$ and $p(O(\tau))\rho = p(O(\tau\theta))$ for all types $\tau$ occurring in the computation of $\mathcal{P}(O(s))$ and $\mathcal{P}(O(s'))$. Moreover, $\mathcal{P}(O(t))\rho = \mathcal{P}(O(t\theta))$ and $p(O(t))\rho = p(O(t\theta))$ for all terms $t$ occurring in the computation of $\mathcal{P}(O(s))$ and $\mathcal{P}(O(s'))$, which we show by induction on the structure of $t$.

If $t = x$ or if $t$ is fluid, $\mathcal{P}(O(t))\rho = z_t\rho = \mathcal{P}(O(t\theta))$.

If $t = f(\bar{\tau})\bar{u}$ for $f \notin \{\forall, \exists\}$, then

$$ \begin{align*} \mathcal{P}(O(t))\rho &= f_k(\mathcal{P}(O(\bar{\tau})), \mathcal{P}(O(\bar{u})))\rho \\ &\stackrel{\text{IIH}}{=} f_k(\mathcal{P}(O(\bar{\tau}\theta)), \mathcal{P}(O(\bar{u}\theta))) = \mathcal{P}(O(f(\bar{\tau}\theta)(\bar{u}\theta))) = \mathcal{P}(O(t\theta)) \end{align*} $$

If $t = Q(\tau) (\lambda x. u)$, then

$$ \begin{align*} \mathcal{P}(O(t))\rho &= Q_1(\mathcal{P}(O(\tau))\rho, \mathcal{P}(O(\mathcal{B}_x(u)))\rho) \\ &\stackrel{\text{IIH}}{=} Q_1(\mathcal{P}(O(\tau\theta)), \mathcal{P}(O(\mathcal{B}_x(u)\theta))) \\ &= Q_1(\mathcal{P}(O(\tau\theta)), \mathcal{P}(O(\mathcal{B}_x(u\theta[x \mapsto x])))) \\ &= \mathcal{P}(O(Q(\tau) (\lambda x. (u\theta[x \mapsto x])))) = \mathcal{P}(O(Q(\tau) ((\lambda x. u)\theta))) = \mathcal{P}(O(t\theta)) \end{align*} $$

If $t = (\lambda x. \tau. u)$ and $t$ is not fluid, then

$$ \begin{align*} \mathcal{P}(O(t))\rho &= \text{lam}(O(\tau)\rho, p(O(\mathcal{B}_x(u)))\rho) \\ &= \text{lam}(\mathcal{P}(O(\tau))\rho, p(O(\mathcal{B}_x(u)))\rho) \\ &\stackrel{\text{IIH}}{=} \text{lam}(\mathcal{P}(O(\tau\theta)), p(O(\mathcal{B}_x(u)\theta))) \\ &= \text{lam}(\mathcal{P}(O(\tau\theta)), p(O(\mathcal{B}_x(u\theta[x \mapsto x])))) \\ &= \mathcal{P}(O(\lambda x. \tau\theta. (u\theta[x \mapsto x])))) = \mathcal{P}(O((\lambda x. \tau. u)\theta)) = \mathcal{P}(O(t\theta)) \end{align*} $$

For $p$, we can argue analogously, using $Q'_1$ instead of $Q_1$ and $z'_t$ instead of $z_t$. $\square$

<figure><img src="image_4.png" /></figure>

## 4 Refutational Completeness

We present a proof of refutational completeness for our higher-order logic superposition calculus. The literature contains two different notions of refutational completeness: static and dynamic. They are defined as follows. For the precise definitions of inference systems and redundancy criteria, we refer to Waldmann et al. [40].

**Definition 49 (Static refutational completeness)** Let $|\models|$ be an entailment relation, let Inf be an inference system, and let (Red<sub>1</sub>, Red<sub>C</sub>) be a redundancy criterion. The inference system Inf is statically refutationally complete w.r.t. $|\models|$ and (Red<sub>1</sub>, Red<sub>C</sub>) if we have $N \models \perp$ if and only if $\perp \in N$ for every clause set $N$ that is saturated w.r.t. Inf and Red<sub>1</sub>.

**Definition 50 (Dynamic refutational completeness)** Let $|\models|$ be an entailment relation, let Inf be an inference system, and let (Red<sub>1</sub>, Red<sub>C</sub>) be a redundancy criterion. Let $(N_i)_i$ be a finite or infinite sequence over sets of clauses. Such a sequence is a *derivation* if $N_i \setminus N_{i+1} \subseteq Red_C(N_{i+1})$ for all $i$. It is *fair* if all Inf-inferences from clauses in the limit inferior $\bigcup_i \bigcap_{j \ge t} N_j$ are contained in $\bigcup_i Red_1(N_i)$. The inference system Inf is *dynamically refutationally complete* w.r.t. $|\models|$ and (Red<sub>1</sub>, Red<sub>C</sub>) if for every fair derivation $(N_i)_i$ such that $N_0 \models \perp$, we have $\perp \in N_i$ for some $i$.
We have introduced three different notions of entailment on the H level: $|\models_G|$, $|=$, and $|\cong|$. With respect to $|\models_G|$, static and dynamic completeness hold unconditionally. For the other two notions of entailment, we will need to add an additional precondition that ensure that the initial clause set is $Q_{\sim}$-normal, which can only be stated for dynamic completeness. For $|\cong|$, we need to require in addition that the initial clause set does not contain any sk symbols.

## 4.1 Outline of the Proof

Following the completeness proof of $\lambda$Sup and $\lambda$Sup, our proof proceeds in three steps, corresponding to the three levels defined above:

1. We prove static refutational completeness of $GFInf$.

2. We show static refutational completeness of $GHInf$ by transforming the model constructed on the GF level into a higher-order interpretation.

3. We lift the result to the H level by invoking the saturation framework of Waldmann et al. [40].

For the first step, since $GFInf$ is essentially identical with $oSup$, we can rely on Nummelin et al.'s completeness theorem for $oSup$. The refutational completeness result holds for any tuple of parameters $q \in \mathcal{F}(Q)$. In addition to the refutational completeness of $GFInf$, the subsequent steps also depend on some properties of the constructed model, which we can easily derive from lemmas proved by Nummelin et al.

For the second step, we fix a parameter triple $q \in Q$ and a set $N \subseteq C_{GH}$ saturated w.r.t. $GHInf^q$ and not containing the empty clause. Then the first step guarantees us a model of $\mathcal{F}(N)$. Based on this model, we construct a higher-order interpretation that we show to be a model of $N$. In essence, the proof is analogous to the one of $\lambda$Sup, but additionally, we need to consider $Q_{\sim}$-normality and the logical symbols.

For the third step, the main proof obligation the saturation framework leaves to us is to show that nonredundant $GHInf^q$ inferences can be lifted to corresponding $HInf$ inferences. For this lifting, we must choose a suitable parameter triple $q \in Q$, given a clause set $N \subseteq C_H$ saturated w.r.t. $HInf$ and the H selection functions. In particular, we must specify the witness function to produce Skolem terms according to the given set $N$. Then the saturation framework guarantees static refutational completeness w.r.t. $|\models_G|$. We show that this implies dynamic refutational completeness w.r.t. $|=$ for $Q_{\sim}$-normal initial clause sets.

## 4.2 The Ground First-Order Level

The inference system $GFInf$ is essentially identical with Nummelin et al.'s ground $oSup$ calculus, with the following caveats:

- The conditions of EFACT superficially appear different but are equivalent.

- $GFInf$'s last condition of FORALLRW and EXISTSRW is weaker than $oSup$'s to simplify our presentation. Where $oSup$ tests for general tautologies, $GFInf$ only tests for a certain form of tautological literal. Clearly, this does not compromise the refutational completeness of $GFInf$.

- The redundancy criterion of $oSup$ requires that a finite subset of $\{D \in N \mid D \prec C\}$ entails $C$, whereas $GFRed_C$ requires that $\{D \in N \mid D \prec C\}$ entails $C$. Since first-order logic with Booleans is compact, the two criteria are equivalent.
Similar to Bachmair and Ganzinger's construction for Sup, Nummelin et al. define the model via a term rewriting system $R_M^*$. As they explain in Definition 16 and Lemma 17, such a term rewriting system $R_M^*$ can be viewed as an interpretation in GF's logic with the property that $t \leftrightarrow_R^{R_M^*} s$ if and only if $[[t]]_{R_M^*} = [[s]]_{R_M^*}$ for any two ground terms $t$ and $s$. The interpretation $R_M^*$ fulfills the following property:

**Lemma 51** Let $C = C' \lor s \approx t \in C_{GF}$ produce a rule $s \rightarrow t \in R_M^*$ (i.e., the rule $s \rightarrow t$ is introduced into $R_M^*$ because of C). Then $s \approx t$ is strictly $\succeq$-eligible in C and $C'$ is false in $R_M^*$.

*Proof* The literal $s \approx t$ is $\succeq$-eligible in C by (C3) of oSup. It is even strictly $\succeq$-eligible by (C6). The subclause $C'$ is false in $R_M^*$ by Lemma 26 of oSup. $\square$

Since Nummelin et al. prove refutational completeness, but do not explicitly state that $R_{N \setminus GFRed_C(N)}^*$ is the model witnessing the completeness, we retrace the last step of their completeness proof in the proof of the following theorem. This also allows us to circumvent the mismatch between the redundancy criteria. Adapted to the context of this article, their completeness theorem can be restated as follows:

**Theorem 52 (Ground first-order static refutational completeness)** Let $q \in \mathcal{F}(Q)$ be a parameter triple. Then the inference system $GFinf^q$ is statically refutationally complete w.r.t. $|=$ and $(GFRed_1, GFRed_C)$. More precisely, if $N \subseteq C_{GF}$ is a clause set saturated w.r.t. $GFinf^q$ and $GFRed_I^q$ such that $\perp \notin N$, then $R_{N \setminus GFRed_C(N)}^*$ is a model of $N$.

*Proof* This proof is inspired by the one of Theorem 4.9 of Bachmair and Ganzinger [3].

By Lemma 31 of oSup, $GFinf^q$ fulfills the reduction property of counterexamples w.r.t. $\succ$. This means that for any clause set $M$ where $C$ is the smallest clause in $M$ that is false in $R_M^*$, there exists an inference from $M$ with

- main premise $C$,

- side premises that are true in $R_M^*$, and

- a conclusion that is smaller than $C$ and false in $R_M^*$.

To derive a contradiction, we assume that $R_{N \setminus GFRed_C(N)}^* \not\models N$. Then there must be a smallest clause in $C \in N$ that is false in $R_{N \setminus GFRed_C(N)}^*$. Using $M = N \setminus GFRed_C(N)$, we obtain an inference $\iota$ with the above properties. Since $N$ is saturated w.r.t. $GFinf^q$ and $GFRed_I^q$ and prems($\iota$) $\subseteq M \subseteq N$, we have $\iota \in GFRed_I^q(N)$. By definition, this means prems($\iota$) $\cap GFRed_C(N) \neq \emptyset$ or $\{D \in N \mid D \prec C\} \models concl(\iota)$. Since prems($\iota$) $\subseteq M = N \setminus GFRed_C(N)$, it must be the latter. Then $R_M^* \not\models \{D \in N \mid D \prec C\}$ because $R_M^* \not= concl(\iota)$. This contradicts the minimality of $C$. $\square$

## 4.3 The Ground Higher-Order Level

In this subsection, let $q = (GHLitSel, GHBoolSel, GHWit) \in Q$ be a parameter triple and let $N \subseteq C_{GH}$. Since all terms on the GH level are $Q$-normal, in particular $N$ is $Q$-normal. We assume that $N$ is saturated w.r.t. $GHInf^q$ and $GHRed_I^q$, and that $\perp \notin N$. Clearly, $\mathcal{F}(N)$ is then saturated w.r.t. $GFinf^{\mathcal{F}(sel)}$ and $GFRed_I^{\mathcal{F}(sel)}$ and $R_{\mathcal{F}(N) \setminus GFRed_C(N)}^*$ is a model of $\mathcal{F}(N)$ by Theorem 52.

In the following, we abbreviate $R_{\mathcal{F}(N) \setminus GFRed_C(N)}^*$ as $R$. Given two terms $s, t \in \mathcal{T}_{GH}$, we write $s \sim t$ to abbreviate $R \models \mathcal{F}(s) \approx \mathcal{F}(t)$, which is equivalent to $[[\mathcal{F}(s)]_R = [[\mathcal{F}(t)]_R]$.

**Lemma 53** For all terms $t, s : \tau \to \upsilon$ in $\mathcal{T}_{GH}$, these statements are equivalent:
1. $t \sim s$;

2. $t(\text{diff } t s) \sim s(\text{diff } t s)$;

3. $tu \sim su$ for all $u \in \mathcal{T}_{\text{GH}}$.

*Proof* Analogous to Lemma 38 of $\lambda$Sup, using Lemma 51 and the $\beta\eta Q_\eta$-normal form. $\square$

**Lemma 54** Let $s \in \mathcal{T}_H$ and let $\theta, \theta'$ be grounding substitutions such that $s\theta$ and $s\theta'$ are $Q_\eta$-normal, $x\theta \sim x\theta'$ for all variables $x$, and $\alpha\theta = \alpha\theta'$ for all type variables $\alpha$. Then $s\theta \sim s\theta'$.

*Proof* This proof is almost identical to the one of Lemma 39 of $\lambda$Sup [10]. The only difference lies in Case 4.1 that must deal with quantifiers. What follows is a copy of the beginning of this previous proof that introduces the notions relevant to deal with the extra case here.

In this proof, we work directly on $\lambda$-terms. To prove the lemma, it suffices to prove it for any $\lambda$-term $s$. Here, for $\lambda$-terms $t_1$ and $t_2$, the notation $t_1 \sim t_2$ is to be read as $t_1 \downarrow_{\beta\eta Q_\eta} \sim t_2 \downarrow_{\beta\eta Q_\eta}$ because $\mathcal{F}$ is only defined on $\beta\eta Q_\eta$-normal terms.

**DEFINITION** We extend the syntax of $\lambda$-terms with a new polymorphic function symbol $\oplus : \Pi\alpha. \alpha \rightarrow \alpha \rightarrow \alpha$. We will omit its type argument. It is equipped with two reduction rules: $\oplus t s \rightarrow t$ and $\oplus t s \rightarrow s$. A $\beta$-$\oplus$-reduction step is either a rewrite step following one of these rules or a $\beta$-reduction step.

The computability path order $\succ_{CPO}$ [14] guarantees that

- $\oplus t s \succ_{CPO} s$ by applying rule @▷;

- $\oplus t s \succ_{CPO} t$ by applying rule @▷ twice;

- $(\lambda x.t) s \succ_{CPO} t[x \mapsto s]$ by applying rule @β.

Since this order is moreover monotone, it decreases with $\beta \oplus$-reduction steps. The order is also well-founded; thus, $\beta \oplus$-reductions terminate. And since the $\beta \oplus$-reduction steps describe a finitely branching term rewrite system, by Kőnig's lemma [26], there is a maximal number of $\beta \oplus$-reduction steps from each $\lambda$-term.

**DEFINITION** A $\lambda$-term is *term-ground* if it does not contain free term variables. It may contain polymorphic type arguments.

**DEFINITION** We introduce an auxiliary function $\mathcal{S}$ that essentially measures the size of a $\lambda$-term but assigns a size of 1 to term-ground $\lambda$-terms.

$$ \mathcal{S}(s) = \begin{cases} 1 & \text{if } s \text{ is term-ground or is a bound or free variable or a symbol} \\ 1 + \mathcal{S}(t) & \text{if } s \text{ is not term-ground and has the form } \lambda x.t \\ \mathcal{S}(t) + \mathcal{S}(u) & \text{if } s \text{ is not term-ground and has the form } tu \end{cases} $$

We prove $s\theta \sim s\theta'$ by well-founded induction on $s$, $\theta$, and $\theta'$ using the left-to-right lexicographic order on the triple $(n_1(s), n_2(s), n_3(s)) \in \mathbb{N}^3$, where

- $n_1(s)$ is the maximal number of $\beta \oplus$-reduction steps starting from $s\sigma$, where $\sigma$ is the substitution mapping each term variable $x$ to $\oplus x\theta x\theta'$;

- $n_2(s)$ is the number of free term variables occurring more than once in $s$;

- $n_3(s) = \mathcal{S}(s)$.

In Case 4.1 of the proof of Lemma 39 of $\lambda$Sup [10], we consider a $\lambda$-term $s$ that contains exactly one free term variable that occurs exactly once in $s$ and $s$ is of the form $f(\tilde{\tau})\tilde{t}$, for some symbol $f$, some types $\tilde{\tau}$, and some $\lambda$-terms $\tilde{t}$. For any $f \notin \{\forall, \exists\}$ the proof proceeds as
before, because then the definition of the encoding $\mathcal{F}$ coincides with the one of $\lambda$Sup. The remaining case to handle is thus when $s$ is of the form $Q\langle\tau\rangle (\lambda z.t)$.

In that case, we have $\llbracket \mathcal{F}(s\theta) \rrbracket_R = \llbracket \mathcal{Qz.} \mathcal{F}(t\theta) \rrbracket_R$ where $Q \in \{\forall, \exists\}$, but $\theta$ and $\theta'$ are not necessarily grounding for $t$ since $t$ may contain the variable $z$ that is bound in $s$. Thus, we cannot apply our induction hypothesis directly on $t$. Instead we want to apply it on $t\{z \mapsto u\}$, which we denote $t_u$, where $u \in \mathcal{T}_{GH}$. It is possible to apply the induction hypothesis to obtain $t_u\theta \sim t_u\theta'$ because

- $n_1(s) = n_1(t_u)$ since all $\beta \oplus$-reductions in $s$ are also in $t_u$;

- $n_2(s) = 0 = n_2(t_u)$ since the same unique free term variable occurs in $s$ and in $t_u$; and

- $n_3(t_u) < n_3(s)$ because $S(z) = S(u) = 1$ implies $n_3(t_u) = n_3(t)$ and hence $n_3(s) = S(Q) + S(\lambda z.t) = 1 + 1 + S(t) = 1 + 1 + S(t_u)$.

Moreover, since $\theta$ and $\theta'$ do not capture $z$, and since $u$ is $Q\approx$-normal, $t_u\theta = (t\theta)\{z \mapsto u\}$ is $Q\approx$-normal by Lemma 9 and similarly for $\theta'$. Thus, we obtain $(t\theta)\{z \mapsto u\} \sim (t\theta')\{z \mapsto u\}$.

Now, let us consider the case where $Q = \forall$: By the definition of interpretations on the GF level, by Lemma 6 (substitution lemma) of oSup, and $R$ being term-generated, we have

$$ \begin{aligned} \llbracket \forall z. \mathcal{F}(t\theta) \rrbracket_R^\xi &= \min\{\llbracket \mathcal{F}(t\theta) \rrbracket_R^{\xi[z \to a]} \mid a \in \mathcal{U}_\tau\} \\ &= \min\{\llbracket \mathcal{F}(t\theta) \{z \mapsto v\} \rrbracket_R^\xi \mid v \in \mathcal{T}_{GF}\} \\ &= \min\{\llbracket \mathcal{F}(t\theta\{z \mapsto u\}) \rrbracket_R^\xi \mid u \in \mathcal{T}_{GH}\} \end{aligned} $$

The same holds for $\theta'$. Moreover, above we deduced $(t\theta)\{z \mapsto u\} \sim (t\theta')\{z \mapsto u\}$ from the induction hypothesis. Thus, $s\theta \sim s\theta'$, as desired in the case $Q = \forall$. The case $Q = \exists$ is analogous, with max instead of min. $\square$

We proceed by defining a higher-order interpretation $\mathcal{J}^{GH} = (\mathcal{U}^{GH}, \mathcal{J}_{ty}^{GH}, \mathcal{J}^{GH}, \mathcal{L}^{GH})$ derived from $R$. We call this interpretation $\mathcal{J}^{GH}$ because we use it to show refutational completeness of GHInf; it is a higher-order interpretation as defined in Section 2, which can interpret ground as well as nonground terms. Let $(\mathcal{U}, \mathcal{J}) = R$, meaning that $\mathcal{U}_\tau$ is the universe of $R$ for type $\tau$ and $\mathcal{J}$ is the interpretation function of $R$.

To illustrate the construction, we will employ the following running example. Let $\Sigma_{ty} = \{\iota, o, \to\}$ and let $\Sigma$ contain $f: \iota \to \iota$ and $a: \iota$, as well as the logical symbols and the choice constant $\varepsilon$. Then, on the GF level, the type signature is also $\Sigma_{ty}$, and the term signature is the set $\Sigma_{GF}$, which contains $f_0, f_1, a_0$, subscripted versions of all logical symbols, such as $\mathcal{T}_0, \perp_0, \neg_0$, and $\neg_1$, as well as symbols $\varepsilon_i^T$ for each $\tau \in \mathcal{T}_{GH}$, and a symbol $\mathrm{lam}_{\lambda x.t}$ for each $\lambda x.t \in \mathcal{T}_{GH}$. We write $[i]$ for the equivalence class of $t \in \mathcal{T}_{GF}$ modulo $R$. The universes $\mathcal{U}_\tau$ are sets of such equivalence classes; for instance $[f_1(a_0)] \in \mathcal{U}_\iota, [\neg_0] \in \mathcal{U}_{o \to o},$ and $[\mathrm{lam}_{\lambda x.a}] \in \mathcal{U}_{\iota \to i}$. We assume that $R$ is such that $[a_0], [f_1(a_0)], [f_1(f_1(a_0))], \dots$ are all different from each other, and therefore that $\mathcal{U}_\iota$ is infinite.

When defining the universe $\mathcal{U}^{GH}$ of the higher-order interpretation, we need to ensure that it contains subsets of function spaces, since $\mathcal{J}_{ty}^{GH}(\to)(\mathcal{D}_1, \mathcal{D}_2)$ must be a subset of the function space from $\mathcal{D}_1$ to $\mathcal{D}_2$ for all $\mathcal{D}_1, \mathcal{D}_2 \in \mathcal{U}^{GH}$. However, the first-order universes $\mathcal{U}_\tau$ consist of equivalence classes of terms from $\mathcal{T}_{GF}$ w.r.t. the rewriting system $R$, not of functions.

To repair this mismatch, we will define a family of functions $\mathcal{E}_\tau$ that give a meaning to the elements of the first-order universes $\mathcal{U}_\tau$. We will define a domain $\mathcal{D}_\tau$ for each ground type $\tau$ and then let $\mathcal{U}^{GH}$ be the set of all these domains $\mathcal{D}_\tau$. Thus, there will be a one-to-one correspondence between ground types and domains. Since the higher-order and first-order type signatures are identical (including $\to$, which is uninterpreted in GF's logic), we can identify higher-order and first-order types.
We define $\mathcal{E}_\tau$ and $\mathcal{D}_\tau$ in a mutual recursion. To ensure well definedness, we must simultaneously show that $\mathcal{E}_\tau$ is bijective. We start with nonfunctional types $\tau$: Let $\mathcal{D}_\tau = \mathcal{U}_\tau$ and let $\mathcal{E}_\tau: \mathcal{U}_\tau \to \mathcal{D}_\tau$ be the identity. Clearly, the identity is bijective. For functional types, we define

$$ \begin{aligned} \mathcal{D}_{\tau \to \nu} &= \{ \varphi : \mathcal{D}_{\tau} \to \mathcal{D}_{\nu} \mid \exists s : \tau \to \nu. \forall u : \tau. \varphi(\mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}})) = \mathcal{E}_{\nu}(\llbracket \mathcal{F}(su) \rrbracket_{\mathcal{R}}) \} \\ \mathcal{E}_{\tau \to \nu} : \mathcal{U}_{\tau \to \nu} &\to \mathcal{D}_{\tau \to \nu} \\ \mathcal{E}_{\tau \to \nu}(\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}})(\mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}})) &= \mathcal{E}_{\nu}(\llbracket \mathcal{F}(su) \rrbracket_{\mathcal{R}}) \end{aligned} $$

To verify that this equation is a valid definition of $\mathcal{E}_{\tau \to \nu}$, we must show that

- every element of $\mathcal{U}_{\tau \to \nu}$ is of the form $\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}}$ for some $s \in \mathcal{T}_{\text{GH}}$;

- every element of $\mathcal{D}_{\tau}$ is of the form $\mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}})$ for some $u \in \mathcal{T}_{\text{GH}}$;

- the definition does not depend on the choice of such $s$ and $u$;

- $\mathcal{E}_{\tau \to \nu}(\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}}) \in \mathcal{D}_{\tau \to \nu}$ for all $s \in \mathcal{T}_{\text{GH}}$.

The first claim holds because $R$ is term-generated and $\mathcal{F}$ is a bijection. The second claim holds because $R$ is term-generated and $\mathcal{F}$ and $\mathcal{E}_\tau$ are bijections. To prove the third claim, we assume that there are other ground terms $t \in \mathcal{T}_{\text{GH}}$ and $v \in \mathcal{T}_{\text{GH}}$ such that $\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}} = \llbracket \mathcal{F}(t) \rrbracket_{\mathcal{R}}$ and $\mathcal{E}_\tau(\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}}) = \mathcal{E}_\tau(\llbracket \mathcal{F}(v) \rrbracket_{\mathcal{R}})$. Since $\mathcal{E}_\tau$ is bijective, we have $\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}} = \llbracket \mathcal{F}(v) \rrbracket_{\mathcal{R}}$. Using the $\sim$-notation, we can write this as $u \sim v$. The terms $s, t, u$, and $v$ are in $\mathcal{T}_{\text{GH}}$, and thus $\mathcal{Q}$ normal, allowing us to apply Lemma 54 to the term $xy$ and the substitutions $\{x \mapsto s, y \mapsto u\}$ and $\{x \mapsto t, y \mapsto v\}$. Thus, we obtain $su \sim tv$—i.e., $\llbracket \mathcal{F}(su) \rrbracket_{\mathcal{R}} = \llbracket \mathcal{F}(tv) \rrbracket_{\mathcal{R}}$, indicating that the definition of $\mathcal{E}_{\tau \to \nu}$ above does not depend on the choice of $s$ and $u$. The fourth claim is obvious from the definition of $\mathcal{D}_{\tau \to \nu}$ and the third claim.

It remains to show that $\mathcal{E}_{\tau \to \nu}$ is bijective. For injectivity, we fix two terms $s, t \in \mathcal{T}_{\text{GH}}$ such that for all $u \in \mathcal{T}_{\text{GH}}$, we have $\llbracket \mathcal{F}(su) \rrbracket_{\mathcal{R}} = \llbracket \mathcal{F}(tu) \rrbracket_{\mathcal{R}}$. By Lemma 53, it follows that $\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}} = \llbracket \mathcal{F}(t) \rrbracket_{\mathcal{R}}$, which shows that $\mathcal{E}_{\tau \to \nu}$ is injective. For surjectivity, we fix an element $\varphi \in \mathcal{D}_{\tau \to \nu}$. By definition of $\mathcal{D}_{\tau \to \nu}$, there exists a term $s$ such that $\varphi(\mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_{\mathcal{R}})) = \mathcal{E}_{\nu}(\llbracket \mathcal{F}(su) \rrbracket_{\mathcal{R}})$ for all $u$. Hence, $\mathcal{E}_{\tau \to \nu}(\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{R}}) = \varphi$, proving surjectivity and therefore bijectivity of $\mathcal{E}_{\tau \to \nu}$. Below, we will usually write $\mathcal{E}$ instead of $\mathcal{E}_\tau$ since the type $\tau$ is determined by $\mathcal{E}_\tau$'s first argument.

In our running example, we have $\mathcal{D}_t = \mathcal{U}_t = \{[\mathbf{a}_0], [f_1(\mathbf{a}_0)], [f_1(f_1(\mathbf{a}_0))], \dots\}$ and $\mathcal{E}_t$ is the identity $\mathcal{U}_t \to \mathcal{D}_t$, $c \mapsto c$. The function $\mathcal{E}_{t \to t}$ maps $[\mathbf{a} \mathbf{m}_{\lambda x.x}]$ to the identity $\mathcal{D}_t \to \mathcal{D}_t$, $c \mapsto c$; it maps $[\mathbf{a} \mathbf{m}_{\lambda x.a}]$ to the constant function $\mathcal{D}_t \to \mathcal{D}_t$, $c \mapsto [\mathbf{a}_0]$; it maps $[f_0]$ to the function $\mathcal{D}_t \to \mathcal{D}_t$, $[t] \mapsto [f_1(t)]$; and it maps $[\mathcal{E}_1^{t \to t}(\mathbf{a} \mathbf{m}_{\lambda z.z}(f_1) \approx \mathbf{a})]$ to the function $\mathcal{D}_t \to \mathcal{D}_t$, $[t] \mapsto [\mathcal{E}_2^{t \to t}(\mathbf{a} \mathbf{m}_{\lambda z.z}(f_1) \approx \mathbf{a}, t)]$. There are many more functions in $\mathcal{D}_{t \to t} = \mathcal{E}_{t \to t}(\mathcal{U}_{t \to t})$, but still $\mathcal{D}_{t \to t}$ is a proper subset of the function space $\mathcal{U}_t \to \mathcal{U}_t$ because the function space is uncountably infinite, whereas $\mathcal{T}_{\text{GF}}$ and hence $\mathcal{D}_{t \to t}$ is countable. Thus, the construction works only because we allow nonstandard Henkin models.

We define the higher-order universe as $\mathcal{U}^{\text{GH}} = \{\mathcal{D}_\tau | \tau \text{ ground}\}$. In particular, this implies that $\mathcal{D}_o = \{0, 1\} \in \mathcal{U}^{\text{GH}}$ as needed, where $0$ is identified with $[\mathbf{L}_0]$ and $1$ with $[\mathbf{T}_0]$. Moreover, we define $\mathcal{J}^{\text{GH}}(\kappa)(\mathcal{D}_{\bar{\tau}}) = \mathcal{U}_{\kappa(\bar{\tau})}$ for all $\kappa \in \mathcal{S}_{\text{ty}}$, completing the type interpretation of $\mathcal{J}^{\text{GH}}_{\text{ty}} = (\mathcal{U}^{\text{GH}}, \mathcal{J}^{\text{GH}}_{\text{ty}})$ and ensuring that $\mathcal{J}^{\text{GH}}_{\text{ty}}(o) = \mathcal{U}_o = \{0, 1\}$.

We define the interpretation function $\mathcal{J}^{\text{GH}}$ for nonquantifier symbols $f: \Pi \bar{\alpha}_m. \tau$ by $\mathcal{J}^{\text{GH}}(f, \mathcal{D}_{\bar{\tau}}) = \mathcal{E}(\mathcal{J}(\bar{f}_0^{\bar{\alpha}_m}))$, and for quantifiers by $\mathcal{J}^{\text{GH}}(\forall, \mathcal{D}_\tau)(f) = \min\{f(a) \mid a \in \mathcal{D}_\tau\}$ and $\mathcal{J}^{\text{GH}}(\exists, \mathcal{D}_\tau)(f) = \max\{f(a) \mid a \in \mathcal{D}_\tau\}$ for all $f \in \mathcal{J}^{\text{GH}}_{\text{ty}}(\to)(\mathcal{D}_\tau, \{0, 1\})$.

In our example, we thus have $\mathcal{J}^{\text{GH}}(f) = \mathcal{E}([f_0])$, which is the function $[t] \mapsto [f_1(t)]$.

We must show that this definition indeed fulfills the requirements of an interpretation function (Section 2.2). By definition, we have
(11) $\mathcal{J}^{\text{GH}}(\mathbf{T}) = \mathcal{E}(\llbracket \mathbf{T}_0 \rrbracket_R) = \llbracket \mathbf{T}_0 \rrbracket_R = 1$; and

(12) $\mathcal{J}^{\text{GH}}(\perp) = \mathcal{E}(\llbracket \perp_0 \rrbracket_R) = \llbracket \perp_0 \rrbracket_R = 0$.

Let $a, b \in \{0, 1\}, u_0 = \perp$, and $u_1 = \mathbf{T}$. Then

(13) $\mathcal{J}^{\text{GH}}(\mathbf{\Lambda})(a, b) = \mathcal{E}(\llbracket \mathcal{F}(\mathbf{\Lambda}) \rrbracket_R)(\llbracket \mathcal{F}(u_a) \rrbracket_R, \llbracket \mathcal{F}(u_b) \rrbracket_R) = \mathcal{E}(\llbracket \mathcal{F}(u_a \mathbf{\Lambda} u_b) \rrbracket_R) = \min\{a, b\}$;

(14) $\mathcal{J}^{\text{GH}}(\mathbf{V})(a, b) = \mathcal{E}(\llbracket \mathcal{F}(u_a \mathbf{V} u_b) \rrbracket_R) = \max\{a, b\}$;

(15) $\mathcal{J}^{\text{GH}}(\neg)(a) = \mathcal{E}(\llbracket \neg_0 \rrbracket_R)(\llbracket \mathcal{F}(u_a) \rrbracket_R) = \mathcal{E}(\llbracket \mathcal{F}(\neg u_a) \rrbracket_R) = \llbracket \mathcal{F}(\neg u_a) \rrbracket_R = 1-a$; and

(16) $\mathcal{J}^{\text{GH}}(\rightarrow)(a, b) = \mathcal{E}(\llbracket \mathcal{F}(u_a \rightarrow u_b) \rrbracket_R) = \max\{1-a, b\}$.

Let $\mathcal{D} \in \mathcal{U}^{\text{GH}}$ and $a', b' \in \mathcal{D}$.

(17) Since $\mathcal{E}$ is bijective and $R$ is term-generated, there exist ground terms $u$ and $v$ such that $\mathcal{E}(\llbracket \mathcal{F}(u) \rrbracket_R) = a'$ and $\mathcal{E}(\llbracket \mathcal{F}(v) \rrbracket_R) = b'$. Then

$$ \mathcal{J}^{\text{GH}}(\approx)(a', b') = \mathcal{E}(\llbracket \mathcal{F}(\approx) \rrbracket_R)(\mathcal{E}(\llbracket \mathcal{F}(u) \rrbracket_R), \mathcal{E}(\llbracket \mathcal{F}(v) \rrbracket_R)) = \mathcal{E}(\llbracket \mathcal{F}(u \approx v) \rrbracket_R) $$

which is 1 if $a' = b'$ and 0 otherwise.

(18) Similarly $\mathcal{J}^{\text{GH}}(\not\approx)(a', b') = 0$ if $a' = b'$ and 1 otherwise.

(19) The requirement for $\forall$ holds by definition of $\mathcal{J}^{\text{GH}}$.

(110) The requirement for $\exists$ holds by definition of $\mathcal{J}^{\text{GH}}$.

(111) Let $\mathcal{D}_{\tau} \in \mathcal{U}^{\text{GH}}$ and $f \in \mathcal{J}_{\text{ty}}(\rightarrow)(\mathcal{D}_{\tau}, \{0, 1\})$. For the requirement on $\mathcal{E}$, we must show that $f(\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f)) = \max\{f(a) \mid a \in \mathcal{D}_{\tau}\}$.

First, we assume that $f(\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f)) = 0$. We want to show that $\max\{f(a) \mid a \in \mathcal{D}_{\tau}\} = 0$. Let $a \in \mathcal{D}_{\tau}$. We have $f = \mathcal{E}(\llbracket \mathcal{F}(p) \rrbracket_R)$ for some $p : \tau \to 0$ and $a = \mathcal{E}(\llbracket \mathcal{F}(u) \rrbracket_R)$ for some $u : \tau \in \mathcal{T}_{\text{GH}}$ because $\mathcal{E}$ and $\mathcal{F}$ are bijective and $R$ is term-generated. Since $N$ is saturated, all conclusions of GCHOICE belong to $N$. In particular, we have $(pu \approx \perp \lor p(\varepsilon\langle\tau\rangle p) \approx \mathbf{T}) \in N$ and hence $\llbracket \mathcal{F}(pu \approx \perp \lor p(\varepsilon\langle\tau\rangle p) \approx \mathbf{T}) \rrbracket_R = 1$. Thus, we have $\max\{\llbracket \mathcal{F}(pu \approx \perp) \rrbracket_R, \llbracket \mathcal{F}(p(\varepsilon\langle\tau\rangle p) \approx \mathbf{T}) \rrbracket_R\} = 1$. Since we have $f(\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f)) = \llbracket \mathcal{F}(p(\varepsilon\langle\tau\rangle p) \approx \mathbf{T}) \rrbracket_R$, our assumption implies that $\llbracket \mathcal{F}(pu \approx \perp) \rrbracket_R = 1$. Moreover,

$$ \begin{align*} \llbracket \mathcal{F}(pu \approx \perp) \rrbracket_R = 1 &\Leftrightarrow \llbracket (\mathcal{F}(pu)) \approx \perp_0 \rrbracket_R = 1 \\ &\Leftrightarrow \llbracket \mathcal{F}(pu) \rrbracket_R = 0 \\ &\Leftrightarrow \mathcal{E}(\llbracket \mathcal{F}(pu) \rrbracket_R) = 0 \\ &\Leftrightarrow \mathcal{E}(\llbracket \mathcal{F}(p) \rrbracket_R)(\mathcal{E}(\llbracket \mathcal{F}(u) \rrbracket_R)) = 0 \\ &\Leftrightarrow f(a) = 0 \end{align*} $$

Since our choice of $a$ was arbitrary, this shows that $\max\{f(a) \mid a \in \mathcal{D}_{\tau}\} = 0$.

For the other direction, we assume that $\max\{f(a) \mid a \in \mathcal{D}_{\tau}\} = 0$. Then, by definition of max, and since $\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f) \in \mathcal{D}_{\tau}$, we have in particular $f(\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f)) = 0$. Thus, we have $f(\mathcal{J}^{\text{GH}}(\varepsilon\langle\tau\rangle)(f)) = \max\{f(a) \mid a \in \mathcal{D}_{\tau}\}$ as required.

This concludes the proof that $\mathcal{J}^{\text{GH}}$ is an interpretation function.

Finally, we need to define the designation function $\mathcal{L}^{\text{GH}}$, which takes a valuation $\xi$ and a $\lambda$-expression $\lambda x.t$ as arguments. Given $\xi$ and $\lambda x.t$, we choose a grounding substitution $\theta$ such that $\mathcal{D}_{\alpha\theta} = \xi(\alpha)$ and $\mathcal{E}(\llbracket \mathcal{F}(y\theta) \rrbracket_R) = \xi(y)$ for all type variables $\alpha$ and all variables $y$ in $\lambda x.t$. Such a substitution can be constructed as follows: We can fulfill the first equation in a unique way because there is a one-to-one correspondence between ground types and domains. Since $\mathcal{E}^{-1}(\xi(y))$ is an element of a first-order universe and $R$ is term-generated, there exists a ground term $s$ such that $\llbracket s \rrbracket_R^\xi = \mathcal{E}^{-1}(\xi(y))$. Choosing one such $s$ and defining $y\theta = \mathcal{F}^{-1}(s)$ gives us a grounding substitution $\theta$ with the desired property.
We define $\mathcal{L}^{\text{GH}}(\xi, (\lambda x. t)) = \mathcal{E}(\llbracket \mathcal{F}((\lambda x. t)\theta) \rrbracket_R)$ if $\lambda x. t$ is $\mathcal{Q}\tilde{\approx}$-normal, and otherwise $\mathcal{L}^{\text{GH}}(\xi, (\lambda x. t)) = \mathcal{L}^{\text{GH}}(\xi, (\lambda x. t) \downarrow_{\mathcal{Q}\tilde{\approx}})$. Since $\mathcal{F}$ is only defined on $\mathcal{Q}\tilde{\approx}$-normal terms, we need to show that $(\lambda x. t)\theta$ is $\mathcal{Q}\tilde{\approx}$-normal if $\lambda x. t$ is $\mathcal{Q}\tilde{\approx}$-normal. This holds because by construction of $\theta$ all $y\theta$ are $\mathcal{Q}\tilde{\approx}$-normal and thus so is $(\lambda x. t)\theta$ according to Lemma 9. Moreover we need to show that our definition does not depend on the choice of $\theta$. We assume that there exists another substitution $\theta'$ with the properties $\mathcal{D}_{\alpha\theta'} = \xi(\alpha)$ for all $\alpha$ and $\mathcal{E}(\llbracket \mathcal{F}(y\theta') \rrbracket_R) = \xi(y)$ for all variables $y$ in $\lambda x. t$. Then we have $\alpha\theta = \alpha\theta'$ for all $\alpha$ due to the one-to-one correspondence between domains and ground types. We have $\llbracket \mathcal{F}(y\theta) \rrbracket_R = \llbracket \mathcal{F}(y\theta') \rrbracket_R$ for all free variables $y$ in $\lambda x. t$ because $\mathcal{E}$ is injective. By Lemma 54 it follows that $\llbracket \mathcal{F}((\lambda x. t)\theta) \rrbracket_R = \llbracket \mathcal{F}((\lambda x. t)\theta') \rrbracket_R$, which proves that $\mathcal{L}^{\text{GH}}$ is well defined.

In our running example, for all $\xi$ we have $\mathcal{L}^{\text{GH}}(\xi, \lambda x. x) = \mathcal{E}(\llbracket \text{lam}_{\lambda x. x} \rrbracket)$, which is the identity. If $\xi(y) = [\mathbf{a}_0]$, then $\mathcal{L}^{\text{GH}}(\xi, \lambda x. y) = \mathcal{E}(\llbracket \text{lam}_{\lambda x. y} \rrbracket)$, which is the constant function $c \mapsto [\mathbf{a}_0]$.

This concludes the definition of the interpretation $\mathcal{J}^{\text{GH}} = (\mathcal{U}^{\text{GH}}, \mathcal{J}_{\text{ty}}^{\text{GH}}, \mathcal{J}^{\text{GH}}, \mathcal{L}^{\text{GH}})$. It remains to show that $\mathcal{J}^{\text{GH}}$ is proper. We need a lemma:

**Lemma 55** Let $\mathcal{J}$ be an interpretation such that $\llbracket \lambda x. t \rrbracket_{\mathcal{J}}^{\xi}(a) = \llbracket t \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi[x \to a]}$ for all $\lambda$-terms $t$ and all valuations $\xi$. Then $\mathcal{Q}\tilde{\approx}$-normalization preserves denotations of terms and truth of clauses w.r.t. $\mathcal{J}$.

*Proof* We must show $\llbracket t \rrbracket_{\mathcal{J}}^{\xi} = \llbracket t \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi}$ for all $\lambda$-terms $t$ and all valuations $\xi$. We cannot work with $\beta\eta$-equivalence classes here because that would require the interpretation to be proper and thus result in a circular argument. We proceed by induction on the structure of $t$.

If $t = \lambda x. u$, by applying our assumption on $\mathcal{J}$ twice and because $\mathcal{Q}\tilde{\approx}$-normalization is idempotent, we have for all $a$

$$ \begin{aligned} \llbracket t \rrbracket_{\mathcal{J}}^{\xi}(a) &= \llbracket \lambda x. u \rrbracket_{\mathcal{J}}^{\xi}(a) = \llbracket u \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi[x \to a]} = \llbracket u \downarrow_{\mathcal{Q}\tilde{\approx}} \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi[x \to a]} = \llbracket \lambda x. (u \downarrow_{\mathcal{Q}\tilde{\approx}}) \rrbracket_{\mathcal{J}}^{\xi}(a) \\ &= \llbracket (\lambda x. u) \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi}(a) = \llbracket t \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi}(a) \end{aligned} $$

Otherwise, if $t = s\bar{u}$, where $s$ is a head that is not of the form $Q\langle\tau\rangle$,

$$ \llbracket t \rrbracket_{\mathcal{J}}^{\xi} = \llbracket s\bar{u} \rrbracket_{\mathcal{J}}^{\xi} = \llbracket s \rrbracket_{\mathcal{J}}^{\xi}(\llbracket \bar{u} \rrbracket_{\mathcal{J}}^{\xi}) \stackrel{\text{IH}}{=} \llbracket s \downarrow_{\mathcal{Q}\tilde{\approx}} \bar{u} \rrbracket_{\mathcal{J}}^{\xi}(\llbracket \bar{u} \downarrow_{\mathcal{Q}\tilde{\approx}} \bar{u} \rrbracket_{\mathcal{J}}^{\xi}) = \llbracket (s\bar{u}) \downarrow_{\mathcal{Q}\tilde{\approx}} \bar{u} \rrbracket_{\mathcal{J}}^{\xi} = \llbracket t \downarrow_{\mathcal{Q}\tilde{\approx}} \bar{u} \rrbracket_{\mathcal{J}}^{\xi} $$

If $t = Q\langle\tau\rangle u$, where $t$ is not $\mathcal{Q}\tilde{\approx}$-reducible at its head, then

$$ \llbracket t \rrbracket_{\mathcal{J}}^{\xi} = \llbracket Q\langle\tau\rangle u \rrbracket_{\mathcal{J}}^{\xi} = \llbracket Q\langle\tau\rangle \rrbracket_{\mathcal{J}}^{\xi}(\llbracket u \rrbracket_{\mathcal{J}}^{\xi}) \stackrel{\text{IH}}{=} \llbracket Q\langle\tau\rangle \rrbracket_{\mathcal{J}}^{\xi}(\llbracket u \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi}) = \llbracket (Q\langle\tau\rangle u) \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi} = \llbracket t \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi} $$

Otherwise we have $t = Q\langle\tau\rangle$ or $t = Q\langle\tau\rangle u$ such that $t$ is $\mathcal{Q}\tilde{\approx}$-reducible at its head. In these cases, it suffices to show that $\llbracket \forall\langle\tau\rangle \rrbracket_{\mathcal{J}}^{\xi} = \llbracket \lambda y. y \approx (\lambda x. \mathbf{T}) \rrbracket_{\mathcal{J}}^{\xi}$ and $\llbracket \exists\langle\tau\rangle \rrbracket_{\mathcal{J}}^{\xi} = \llbracket \lambda y. y \not\approx (\lambda x. \perp) \rrbracket_{\mathcal{J}}^{\xi}$ for all types $\tau$ and all valuations $\xi$. The argument we use here resembles the proof of Lemma 28, but here we cannot assume $\mathcal{J}$ to be proper.

Let $f$ be a function from $\llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}^{\xi}$ to $\{0, 1\}$. Then

$$ \llbracket \forall\langle\tau\rangle \rrbracket_{\mathcal{J}}^{\xi}(f) = \mathcal{J}(\forall, \llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}^{\xi})(f) = \min\{f(a) \mid a \in \llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}^{\xi}\} = \begin{cases} 1 & \text{if } f \text{ is constantly } 1 \\ 0 & \text{otherwise} \end{cases} $$

By our assumption on $\mathcal{J}$, we have

$$ \begin{aligned} \llbracket \lambda y. y \approx (\lambda x. \mathbf{T}) \rrbracket_{\mathcal{J}}^{\xi}(f) &= \llbracket (y \approx (\lambda x. \mathbf{T})) \downarrow_{\mathcal{Q}\tilde{\approx}} \rrbracket_{\mathcal{J}}^{\xi[y \to f]} = \llbracket y \approx (\lambda x. \mathbf{T}) \rrbracket_{\mathcal{J}}^{\xi[y \to f]} \\ &= \begin{cases} 1 & \text{if } \llbracket y \rrbracket_{\mathcal{J}}^{\xi[y \to f]} = \llbracket \lambda x. \mathbf{T} \rrbracket_{\mathcal{J}}^{\xi[y \to f]} \\ 0 & \text{otherwise} \end{cases} \end{aligned} $$
Thus, it remains to show that $[y]_J^{\xi^{[y \to f]}} = [\lambda x. T]_J^{\xi^{[y \to f]}}$ if and only if $f$ is constantly 1. This holds because $[y]_J^{\xi^{[y \to f]}}(a) = f(a)$ and, by our assumption on $\mathcal{J}$, $[\lambda x. T]_J^{\xi^{[y \to f]}}(a) = [T]_J^{\xi^{[x \to a, y \to f]}} = 1$ for all $a \in [\tau]_{\mathcal{J}_{ty}}$. The case of $\exists$ is analogous. $\square$

**Corollary 56** Let $\mathcal{J}$ be an interpretation such that $[\lambda x. t]_J^{\xi}(a) = [t \downarrow_{\mathcal{Q}\approx}]_J^{\xi^{[x \to a]}}$ for all $\lambda$-terms $t$ and all valuations $\xi$. Then $\mathcal{J}$ is proper.

Thus, to show that $\mathcal{J}^{GH}$ is proper, it suffices to prove that $[\lambda x. t]_{\mathcal{J}^{GH}}^{\xi}(a) = [t \downarrow_{\mathcal{Q}\approx}]_{\mathcal{J}^{GH}}^{\xi^{[x \to a]}}$. For quantifiers, we have the following relation between the higher-order interpretation $\mathcal{J}^{GH}$ and the first-order interpretation $\mathcal{R}$:

**Lemma 57** Let $\mathcal{Q} \in \{\forall, \exists\}$ and $f \in \mathcal{J}_{ty}^{GH}(\to)(\mathcal{D}_{\tau}, \{0, 1\})$. Then, for any term $p$ such that $\mathcal{Q}\langle\tau\rangle(\lambda x. p)$ is $\mathcal{Q}\approx$-normal and such that $f = \mathcal{E}(\llbracket\mathcal{F}(\lambda x. p)\rrbracket_R)$,

$$ \mathcal{J}^{GH}(\mathcal{Q}, \mathcal{D}_{\tau})(f) = \mathcal{E}(\llbracket \mathcal{F}(\mathcal{Q}\langle\tau\rangle(\lambda x. p)) \rrbracket_R) $$

*Proof* Let $\mathcal{Q}, f$, and $p$ be as in the preconditions of the lemma. If $\mathcal{Q} = \forall$, then

$$
\begin{align*}
\mathcal{J}^{GH}(\forall, \mathcal{D}_{\tau})(f) &= \min\{f(a) \mid a \in \mathcal{D}_{\tau}\} \\
&= \min\{\mathcal{E}_{\tau \to o}(\llbracket \mathcal{F}(\lambda x. p) \rrbracket_R)(\mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_R)) \mid \mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_R) \in \mathcal{D}_{\tau}\} \\
&= \min\{\mathcal{E}_o(\llbracket \mathcal{F}((\lambda x. p)u) \rrbracket_R) \mid \mathcal{E}_{\tau}(\llbracket \mathcal{F}(u) \rrbracket_R) \in \mathcal{D}_{\tau}\} \\
&= \min\{\llbracket \mathcal{F}((\lambda x. p)u) \rrbracket_R \mid \llbracket \mathcal{F}(u) \rrbracket_R \in \mathcal{U}_{\tau}\} \\
&= \min\{\llbracket \mathcal{F}(p\{x \mapsto u\}) \rrbracket_R \mid \llbracket \mathcal{F}(u) \rrbracket_R \in \mathcal{U}_{\tau}\} \\
&= \min\{\llbracket \mathcal{F}(p)\{x \mapsto \mathcal{F}(u)\} \rrbracket_R \mid \llbracket \mathcal{F}(u) \rrbracket_R \in \mathcal{U}_{\tau}\} \\
&\text{since, by Lemma 7, } x \text{ never occurs free under a } \lambda \text{ in } p \\
&= \min\{\llbracket \mathcal{F}(p) \rrbracket_R^{\xi^{[x \to a']}} \mid a' \in \mathcal{U}_{\tau}\} \\
&\text{by Lemma 6 (substitution lemma) of oSup} \\
&= \llbracket \forall x. \mathcal{F}(p) \rrbracket_R = \mathcal{E}_o(\llbracket \mathcal{F}(\forall \langle\tau\rangle (\lambda x. p)) \rrbracket_R)
\end{align*}
$$

If $\mathcal{Q} = \exists$, the proof is analogous, but uses max instead of min. $\square$

A similar relation holds on all $\mathcal{Q}\approx$-normal terms:

**Lemma 58** Given a ground $\mathcal{Q}\approx$-normal $\lambda$-term $t$, we have

$$ [t]_{\mathcal{J}^{GH}} = \mathcal{E}(\llbracket \mathcal{F}(t \downarrow_{\beta\eta\mathcal{Q}_{\eta}}) \rrbracket_R) $$

*Proof* The proof is analogous to that of Lemma 40 of $\lambda$Sup, using the $\beta\eta\mathcal{Q}_{\eta}$-normal form instead of the $\beta\eta$-normal form and with a special case for quantifier-headed terms. We proceed by induction on $t$. Assume that $[s]_{\mathcal{J}^{GH}} = \mathcal{E}(\llbracket \mathcal{F}(s \downarrow_{\beta\eta\mathcal{Q}_{\eta}}) \rrbracket_R)$ for all proper subterms $s$ of $t$. If $t$ is of the form $f\langle\bar{\tau}\rangle$, then it cannot be a quantifier since $t$ is $\mathcal{Q}\approx$-normal. Thus,

$$
\begin{align*}
[\bar{t}]_{\mathcal{J}^{GH}} &= \mathcal{J}^{GH}(f, \mathcal{D}_{\bar{\tau}}) \\
&= \mathcal{E}(\mathcal{J}(f_0, \mathcal{U}_{\mathcal{F}(\bar{\tau})})) \\
&= \mathcal{E}(\llbracket f_0 \langle \mathcal{F}(\bar{\tau}) \rangle \rrbracket_R) \\
&= \mathcal{E}(\llbracket \mathcal{F}(f \langle \bar{\tau} \rangle) \rrbracket_R) \\
&= \mathcal{E}(\llbracket \mathcal{F}(f \langle \bar{\tau} \rangle \downarrow_{\beta\eta\mathcal{Q}_{\eta}}) \rrbracket_R) = \mathcal{E}(\llbracket \mathcal{F}(t \downarrow_{\beta\eta\mathcal{Q}_{\eta}}) \rrbracket_R)
\end{align*}
$$
If $t$ is of the form $t = \mathbb{Q}\langle\tau\rangle u$, then $u = \lambda x.v$ since $t$ is $\mathbb{Q}\mathbb{R}$-normal, and

$$ \begin{aligned} [\mathbb{Q}\langle\tau\rangle (\lambda x.v)]_{\mathbb{Q}\mathbb{H}} &= [\mathbb{Q}\langle\tau\rangle]_{\mathbb{Q}\mathbb{H}} [\lambda x.v]_{\mathbb{Q}\mathbb{H}} \\ &= \mathcal{E}_o([\mathcal{F}(\mathbb{Q}\langle\tau\rangle (\lambda x.v))]_R) \quad \text{by Lemma 57} \\ &= \mathcal{E}_o([\mathcal{F}((\mathbb{Q}\langle\tau\rangle (\lambda x.v))\downarrow\beta\eta Q_\eta)]_R) \quad \text{by the definition of } \mathcal{F} \end{aligned} $$

If $t$ is an application $t = t_1 t_2$, where $t_1$ is of type $\tau \to \upsilon$ and $t_1$ is not a quantifier, then

$$ \begin{aligned} [t_1 t_2]_{\mathbb{Q}\mathbb{H}} &= [t_1]_{\mathbb{Q}\mathbb{H}} ([t_2]_{\mathbb{Q}\mathbb{H}}) \\ &\stackrel{\text{IH}}{=} \mathcal{E}_{\tau \to \upsilon} ([\mathcal{F}(t_1 \downarrow \beta\eta Q_\eta)]_R) (\mathcal{E}_{\tau} ([\mathcal{F}(t_2 \downarrow \beta\eta Q_\eta)]_R)) \\ &= \mathcal{E}_{\upsilon} ([\mathcal{F}((t_1 t_2) \downarrow \beta\eta Q_\eta)]_R) \end{aligned} $$

If $t$ is a $\lambda$-expression, then

$$ \begin{aligned} [\lambda x.u]_{\mathbb{Q}\mathbb{H}}^{\xi} &= \mathcal{L}^{\text{GH}}(\xi, (\lambda x.u)) \\ &= \mathcal{E}([\mathcal{F}((\lambda x.u)\theta\downarrow\beta\eta Q_\eta)]_R) \\ &= \mathcal{E}([\mathcal{F}((\lambda x.u)\downarrow\beta\eta Q_\eta)]_R) \end{aligned} $$

where $\theta$ is a substitution such that $\mathcal{D}_{\alpha\theta} = \xi(\alpha)$ and $\mathcal{E}([\mathcal{F}(x\theta)]_R) = \xi(x)$. $\square$

<figure><img src="image_5.png" /></figure>

We also need to employ the following lemma, which is very similar to the substitution lemma, but we must prove it here for our particular interpretation $\mathbb{J}^{\text{GH}}$ because we have not shown that $\mathbb{J}^{\text{GH}}$ is proper yet.

**Lemma 59 (Substitution lemma)** We have $[\tau\rho]_{\mathbb{Q}\mathbb{H}}^{\xi} = [\tau]_{\mathbb{Q}\mathbb{H}}^{\xi'}$ and $[t\rho]_{\mathbb{Q}\mathbb{H}}^{\xi} = [t]_{\mathbb{Q}\mathbb{H}}^{\xi'}$ for all $\mathbb{Q}\mathbb{R}$-normal $\lambda$-terms $t$, all $\tau \in \mathcal{T}_{\mathbb{H}}$ and all grounding substitutions $\rho$, where $\xi'(\alpha) = [\alpha\rho]_{\mathbb{Q}\mathbb{H}}^{\xi'}$ for all type variables $\alpha$ and $\xi'(x) = [xp]_{\mathbb{Q}\mathbb{H}}^{\xi'}$ for all term variables $x$.

*Proof* Analogous to Lemma 41 of $\lambda$Sup, using the $\beta\eta Q_\eta$-normal form instead of the $\beta\eta$-normal form. $\square$

<figure><img src="image_6.png" /></figure>

**Lemma 60** The interpretation $\mathbb{J}^{\text{GH}}$ is proper.

*Proof* By Corollary 56, it is enough to show that $[\lambda x.t]_{\mathbb{Q}\mathbb{H}}^{\xi}(a) = [t \downarrow_{\mathbb{Q}\mathbb{R}}]_{\mathbb{Q}\mathbb{H}}^{\xi[x \to a]}$. First, we show it for all $\mathbb{Q}\mathbb{R}$-normal $\lambda$-expressions $\lambda x.t$, all valuations $\xi$, and all values $a$:

$$ \begin{aligned} [\lambda x.t]_{\mathbb{Q}\mathbb{H}}^{\xi}(a) &= \mathcal{L}^{\text{GH}}(\xi, \lambda x.t)(a) && \text{by the definition of } [\quad]_{\mathbb{Q}\mathbb{H}} \\ &= \mathcal{E}([\mathcal{F}((\lambda x.t)\theta\downarrow\beta\eta Q_\eta)]_R)(a) && \text{by the definition of } \mathcal{L}^{\text{GH}} \text{ for some } \theta \\ && \text{such that } \mathcal{E}([\mathcal{F}(z\theta)]_R) = \xi(z) \text{ for all } z \\ && \text{and } \mathcal{D}_{\alpha\theta} = \xi(\alpha) \text{ for all } \alpha \\ &= \mathcal{E}([\mathcal{F}((\lambda x.t)\theta s)\downarrow\beta\eta Q_\eta]]_R) && \text{by the definition of } \mathcal{E} \\ && \text{where } \mathcal{E}([\mathcal{F}(s)]_R) = a \\ &= \mathcal{E}([\mathcal{F}(t(\theta[x \mapsto s]))\downarrow\beta\eta Q_\eta]]_R) && \text{by } \beta\text{-reduction} \\ &= [t(\theta[x \mapsto s])]_{\mathbb{Q}\mathbb{H}} && \text{by Lemma 58} \\ &= [t]_{\mathbb{Q}\mathbb{H}}^{\xi[x \to a]} && \text{by Lemma 59} \\ &= [t \downarrow_{\mathbb{Q}\mathbb{R}}]_{\mathbb{Q}\mathbb{H}}^{\xi[x \to a]} && \text{because } t \text{ is } \mathbb{Q}\mathbb{R}\text{-normal by definition} \end{aligned} $$

The case where $\lambda x.t$ is not $\mathbb{Q}\mathbb{R}$-normal is reduced to the previous case because then $[\lambda x.t]_{\mathbb{Q}\mathbb{H}}^{\xi}(a) = \mathcal{L}^{\text{GH}}(\xi, (\lambda x.t) \downarrow_{\mathbb{Q}\mathbb{R}})(a)$ and $(\lambda x.t) \downarrow_{\mathbb{Q}\mathbb{R}} = \lambda x.t'$ where $t' = t \downarrow_{\mathbb{Q}\mathbb{R}}$ by definition. $\square$

<figure><img src="image_7.png" /></figure>
**Lemma 61** $\mathcal{J}^{\text{GH}}$ is a model of $\mathcal{N}$.

*Proof* Because all terms in $\mathcal{N}$ are $\mathbb{Q}$-normal, by Lemma 58, $\llbracket t \rrbracket_{\mathcal{J}^{\text{GH}}} = \mathcal{E}(\llbracket \mathcal{F}(t) \rrbracket_{\mathcal{R}})$ for all $t \in \mathcal{J}^{\text{GH}}$. Since $\mathcal{E}$ is a bijection, it follows that any literal $s \approx t \in \mathcal{C}_{\text{GH}}$ is true in $\mathcal{J}^{\text{GH}}$ if and only if $\mathcal{F}(s \approx t)$ is true in $\mathcal{R}$. Hence, a clause $C \in \mathcal{C}_{\text{GH}}$ is true in $\mathcal{J}^{\text{GH}}$ if and only if $\mathcal{F}(C)$ is true in $\mathcal{R}$. By Theorem 52 and the assumption that $\perp \notin \mathcal{N}$, $\mathcal{R}$ is a model of $\mathcal{F}(\mathcal{N})$—that is, for all clauses $C \in \mathcal{N}$, $\mathcal{F}(C)$ is true in $\mathcal{R}$. Hence, all clauses $C \in \mathcal{N}$ are true in $\mathcal{J}^{\text{GH}}$ and therefore $\mathcal{J}^{\text{GH}}$ is a model of $\mathcal{N}$. $\square$

We summarize the results of this subsection in the following theorem:

**Theorem 62 (Ground static completeness)** Let $q \in \mathcal{Q}$ be some parameter triple. Then $\text{GHInf}^q$ is statically refutationally complete w.r.t. $\models$ and $(\text{GHRed}_1^q, \text{GHRed}_\mathcal{C})$. In other words, if $\mathcal{N} \subseteq \mathcal{C}_{\text{GH}}$ is a clause set saturated w.r.t. $\text{GHInf}^q$ and $\text{GHRed}_1^q$, then $\mathcal{N} \models \perp$ if and only if $\perp \in \mathcal{N}$.

The construction of $\mathcal{J}^{\text{GH}}$ relies on the specific properties of $\mathcal{R}$. It would not work with an arbitrary interpretation. In the other direction, transforming a higher-order model into a first-order model with interpreted Booleans is easier, as the following lemma shows:

**Lemma 63** Given a proper higher-order interpretation $\mathcal{J}$ on GH, there exists an interpretation $\mathcal{J}^{\text{GF}}$ on GF such that for any clause $C \in \mathcal{C}_{\text{GH}}$ the truth values of $C$ in $\mathcal{J}$ and of $\mathcal{F}(C)$ in $\mathcal{J}^{\text{GF}}$ coincide.

*Proof* Let $\mathcal{J} = (\mathcal{J}_{\text{ty}}, \mathcal{J}, \mathcal{L})$ be a proper higher-order interpretation on GH. Let $\mathcal{U}_{\tau}^{\text{GF}} = \llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}$ be the GF universe for the ground type $\tau$. For a symbol $f_j^{\tilde{v}} \in \Sigma_{\text{GF}}$, let $\mathcal{J}^{\text{GF}}(f_j^{\tilde{v}}) = \llbracket f \langle \tilde{v} \rangle \rrbracket_{\mathcal{J}}$ (up to currying). For a symbol $\text{la}_{\lambda x, t} \in \Sigma_{\text{GF}}$, let $\mathcal{J}^{\text{GF}}(\text{la}_{\lambda x, t}) = \llbracket \lambda x. t \rrbracket_{\mathcal{J}}$.

The requirements on the GF-interpretation of logical symbols are fulfilled because we have similar requirements on H: $\mathcal{U}_{\tau}^{\text{GF}} = \mathcal{J}_{\text{ty}}(o) = \{0, 1\}$; $\mathcal{J}^{\text{GF}}(\mathbf{T}_0) = \mathcal{J}(\mathbf{T}) = 1$; $\mathcal{J}^{\text{GF}}(\neg \mathbf{1})(a) = \mathcal{J}(\neg)(a) = 1 - a$; and similarly for the other logical symbols. Thus, this defines an interpretation $\mathcal{J}^{\text{GF}} = (\mathcal{U}^{\text{GF}}, \mathcal{J}^{\text{GF}})$ on GF.

We need to show that for any $C \in \mathcal{C}_{\text{GH}}$, $\mathcal{J} \models C$ if and only if $\mathcal{J}^{\text{GF}} \models \mathcal{F}(C)$. It suffices to show that $\llbracket t \rrbracket_{\mathcal{J}^{\text{GF}}} = \llbracket \mathcal{F}(t) \rrbracket_{\mathcal{J}^{\text{GF}}}$ for all terms $t \in \mathcal{T}_{\text{GH}}$. We prove this by induction on the structure of the $\beta\eta\text{Q}_\eta$-normal form of $t$. If $t$ is a $\lambda$-expression, this is obvious. If $t$ is of the form $f \langle \tilde{v} \rangle \tilde{s}_j$, then $\mathcal{F}(t) = f_j^{\tilde{v}}(\mathcal{F}(\tilde{s}_j))$ and hence

$$ \llbracket \mathcal{F}(t) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi} = \mathcal{J}^{\text{GF}}(f_j^{\tilde{v}})(\llbracket \mathcal{F}(\tilde{s}_j) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi}) = \llbracket f \langle \tilde{v} \rangle \rrbracket_{\mathcal{J}^{\xi}}^{\xi}(\llbracket \mathcal{F}(\tilde{s}_j) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi}) \stackrel{\text{IH}}{=} \llbracket f \langle \tilde{v} \rangle \rrbracket_{\mathcal{J}^{\xi}}^{\xi}(\llbracket \tilde{s}_j \rrbracket_{\mathcal{J}^{\xi}}^{\xi}) = \llbracket t \rrbracket_{\mathcal{J}^{\xi}}^{\xi} $$

If $t$ is of the form $\forall \langle \tau \rangle (\lambda x. s)$, then $\mathcal{F}(t) = \forall x. \mathcal{F}(s)$ and hence

$$ \llbracket \mathcal{F}(t) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi} = \min\{\llbracket \mathcal{F}(s) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi}[x \to a] \mid a \in \mathcal{U}_{\tau}^{\text{GF}}\} \stackrel{\text{IH}}{=} \min\{\llbracket s \rrbracket_{\mathcal{J}^{\xi}}^{\xi}[x \to a] \mid a \in \llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}\} \\ = \min\{\llbracket \lambda x. s \rrbracket_{\mathcal{J}^{\xi}}^{\xi}(a) \mid a \in \llbracket \tau \rrbracket_{\mathcal{J}_{\text{ty}}}\} = \llbracket t \rrbracket_{\mathcal{J}^{\xi}}^{\xi} $$

A similar argument applies for $\exists$. Since the definition of $\mathcal{F}$ recurses into subterms below quantifiers, we finally need to consider the case where $t$ is a variable $x$. In that case, we have $\mathcal{F}(x) = x$ and hence $\llbracket \mathcal{F}(t) \rrbracket_{\mathcal{J}^{\text{GF}}}^{\xi} = \xi(x) = \llbracket t \rrbracket_{\mathcal{J}^{\xi}}^{\xi}$. $\square$
4.4 The Nonground Higher-Order Level

To lift the result to the nonground level, we employ the saturation framework of Waldmann
et al. [40]. Clearly, the entailment relation $|\models$ on GH qualifies as a consequence relation in
the sense of the framework. We need to show that our redundancy criterion on GH qualifies
as a redundancy criterion and that $\mathcal{G}$ qualifies as a grounding function:

**Lemma 64** The pair $(GHRed_1^q, GHRed_c)$ is a redundancy criterion in the sense of the saturation framework.

*Proof* We must prove the conditions (R1) to (R4) of the saturation framework. Adapted to
our context, they state the following for all clause sets $N, N' \subseteq C_{GH}$:

(R1) if $N \models \bot$, then $N \setminus GHRed_c(N) \models \bot$;

(R2) if $N \subseteq N'$, then $GHRed_c(N) \subseteq GHRed_c(N')$ and $GHRed_1(N) \subseteq GHRed_1(N')$;

(R3) if $N' \subseteq GHRed_c(N)$, then we have $GHRed_c(N) \subseteq GHRed_c(N \setminus N')$ and $GHRed_1(N) \subseteq GHRed_1(N \setminus N')$;

(R4) if $\iota \in GHInf$ and concl($\iota$) $\in N$, then $\iota \in GHRed_1(N)$.

For (R1), it suffices to show that $N \setminus GHRed_c(N) \models N$. Let $\mathcal{J}$ be a model of $N \setminus GHRed_c(N)$. By Lemma 63, there exists a model $\mathcal{J}^{GF}$ of $\mathcal{F}(N \setminus GHRed_c(N)) = \mathcal{F}(N) \setminus GFRed_c(\mathcal{F}(N))$. We show that $\mathcal{J}^{GF} \models C$ for each clause $C \in \mathcal{F}(N)$ by well-founded induction on $C$ w.r.t. $>$. If $C \notin GFRed_c(\mathcal{F}(N))$, we have already shown that $\mathcal{J}^{GF} \models C$. Otherwise, $C \in GFRed_c(\mathcal{F}(N))$ and hence $\{D \in \mathcal{F}(N) \mid D \prec C\} \models C$. By the induction hypothesis, it follows that $\mathcal{J}^{GF} \models C$. Thus, we have shown that $\mathcal{J}^{GF} \models \mathcal{F}(N)$. By Lemma 63, this implies $\mathcal{J} \models N$.

For the first part of (R2), let $N \subseteq N'$ and $C \in GHRed_c(N)$, i.e., $\{D \in \mathcal{F}(N) \mid D \prec \mathcal{F}(C)\} \models \mathcal{F}(C)$. We must show that $\{D \in \mathcal{F}(N') \mid D \prec \mathcal{F}(C)\} \models \mathcal{F}(C)$. This is obvious because $\{D \in \mathcal{F}(N) \mid D \prec \mathcal{F}(C)\} \subseteq \{D \in \mathcal{F}(N') \mid D \prec \mathcal{F}(C)\}$.

For the second part of (R2), let $N \subseteq N'$ and $\iota \in GHRed_1(N)$. We must show that
$\iota \in GHRed_1(N')$. If $\iota$ is a GARGCONG, GEXT, or GCHOICE inference, we have concl($\iota$) $\in$
$N \cup GHRed_c(N)$. Using the first part of (R2), it follows that $N \cup GHRed_c(N) \subseteq N' \cup$
$GHRed_c(N')$, which implies $\iota \in GHRed_1(N')$. If $\iota$ is some other kind of inference, we have
prems($\mathcal{F}(\iota) \cap GFRed_c(\mathcal{F}(N)) \neq \emptyset$ or $\{D \in \mathcal{F}(N) \mid D \prec mprem(\mathcal{F}(\iota))\} \models$ concl($\mathcal{F}(\iota)$). In
the first case, prems($\mathcal{F}(\iota) \cap GFRed_c(\mathcal{F}(N')) \neq \emptyset$ because by the first part of (R2), we
have $GFRed_c(\mathcal{F}(N)) \subseteq GFRed_c(\mathcal{F}(N'))$. In the second case, we have $\{D \in \mathcal{F}(N') \mid D \prec$
$mprem(\mathcal{F}(\iota))\} \models$ concl($\mathcal{F}(\iota)$) because $N \subseteq N'$ implies $\{D \in \mathcal{F}(N) \mid D \prec$ mprem($\mathcal{F}(\iota)$)) $\subseteq$
$\{D \in \mathcal{F}(N') \mid D \prec$ mprem($\mathcal{F}(\iota)$))}.

For the first part of (R3), let $N' \subseteq GHRed_c(N)$ and $C \in GHRed_c(N)$, i.e., $\{D \in \mathcal{F}(N) \mid D \prec \mathcal{F}(C)\} \models \mathcal{F}(C)$. We must show that $\{D \in \mathcal{F}(N \setminus N') \mid D \prec \mathcal{F}(C)\} \models \mathcal{F}(C)$. Let $\mathcal{J}$ be a model of $\{D \in \mathcal{F}(N \setminus N') \mid D \prec \mathcal{F}(C)\}$. It suffices to show that $\mathcal{J} \models \{D \in \mathcal{F}(N) \mid D \prec \mathcal{F}(C)\}$, meaning $\mathcal{J} \models E$ for every $E \in \mathcal{F}(N)$ such that $E \prec \mathcal{F}(C)$. We prove this by well-founded induction on $E$ w.r.t. $>$. If $E \in \mathcal{F}(N \setminus N')$, the claim holds by assumption. Otherwise, $E \in \mathcal{F}(N') \subseteq GFRed_c(\mathcal{F}(N))$; hence $\{D \in \mathcal{F}(N) \mid D \prec E\} \models E$ and therefore $\mathcal{J} \models E$ by the induction hypothesis.

For the second part of (R3), let $N' \subseteq GHRed_c(N)$ and $\iota \in GHRed_1(N)$. We must show that $\iota \in GHRed_1(N \setminus N')$. If $\iota$ is a GARGCONG, GEXT, or GCHOICE inference, we have concl($\iota) \in N \cup GHRed_c(N)$. Using $N' \subseteq GHRed_c(N)$, and by the first part of (R3), it follows that concl($\iota) \in N \cup GHRed_c(N) = (N \setminus N') \cup GHRed_c(N) \subseteq (N \setminus N') \cup GHRed_c(N \setminus N')$ and therefore $\iota \in GHRed_1(N \setminus N')$. If $\iota$ is some other kind of inference, we have prems($\mathcal{F}(\iota) \cap GFRed_c(\mathcal{F}(N)) \neq \emptyset$ or $\{D \in \mathcal{F}(N) \mid D \prec mprem(\mathcal{F}(\iota))\} \models$ concl($\mathcal{F}(\iota)$). In
the first case, $\mathit{prems}(\mathcal{F}(\iota)) \cap \mathit{GFRed}_C(\mathcal{F}(N \setminus N')) \neq \emptyset$ because by the first part of (R3), we have $\mathit{GFRed}_C(\mathcal{F}(N)) \subseteq \mathit{GFRed}_C(\mathcal{F}(N \setminus N'))$. In the second case, it suffices to show that $\{D \in \mathcal{F}(N \setminus N') | D \prec \mathit{mprem}(\mathcal{F}(\iota))\} \models \{D \in \mathcal{F}(N) | D \prec \mathit{mprem}(\mathcal{F}(\iota))\}$, which can be shown analogously to the induction used for the first part of (R3).

For (R4), let $\iota \in \mathit{GHInf}$ and $\mathit{concl}(\iota) \in N$. We must show that $\iota \in \mathit{GHRed}_1(N)$. If $\iota$ is a GARGCONG, GEXT, or GCHOICE inference, we must show $\mathit{concl}(\iota) \in N \cup \mathit{GHRed}_C(N)$, which obviously holds by assumption. If $\iota$ is some other kind of inference, it suffices to show $\{D \in \mathcal{F}(N) | D \prec \mathit{mprem}(\mathcal{F}(\iota))\} \models \mathit{concl}(\mathcal{F}(\iota)) \in \mathcal{F}(N)$ and $\mathit{concl}(\mathcal{F}(\iota)) \prec \mathit{mprem}(\mathcal{F}(\iota))$. $\square$

**Lemma 65** For every $q \in Q$, the function $G^q$ is a grounding function in the sense of the saturation framework.

*Proof* We must prove the conditions (G1), (G2), and (G3) of the saturation framework. Adapted to our context, they state the following:

(G1) $G(\perp) = \{\perp\}$;

(G2) for every $C \in C_H$, if $\perp \in G(C)$, then $C = \perp$;

(G3) for every $\iota \in \mathit{HInf}$, $G^q(\iota) \subseteq \mathit{GHRed}_1^q(G(\mathit{concl}(\iota)))$.

Clearly, $C = \perp$ if and only if $\perp \in G(C)$ if and only if $G(C) = \{\perp\}$, proving (G1) and (G2). For every $\iota \in \mathit{HInf}$, by the definition of $G^q$ (Definition 44) and by Lemma 41, we have $\mathit{concl}(G^q(\iota)) \subseteq G(\mathit{concl}(\iota))$, and thus (G3) by (R4). $\square$

To lift the completeness result of the previous subsection to the nonground calculus $\mathit{HInf}$, we employ Theorem 14 of the saturation framework, which, adapted to our context, is stated as follows.

**Theorem 66 (Lifting theorem)** If, for every parameter triple $q \in Q$, $\mathit{GHInf}^q$ is statically refutationally complete w.r.t. $(\mathit{GHRed}_1^q, \mathit{GHRed}_C)$, and if for every $N \subseteq C_H$ that is saturated w.r.t. $\mathit{HInf}$ and $\mathit{HRed}_1$ there exists a $q \in Q$ such that $\mathit{GHInf}^q(G(N)) \subseteq G^q(\mathit{HInf}(N)) \cup \mathit{GHRed}_1^q(G(N))$, then also $\mathit{HInf}$ is statically refutationally complete w.r.t. $(\mathit{HRed}_1, \mathit{HRed}_C)$ and $\models_G$.

*Proof* This is almost an instance of Theorem 14 of the saturation framework. We take $C_H$ for $\mathbf{F}$, $C_{GH}$ for $\mathbf{G}$. Clearly, the entailment relation $\models_G$ on $\mathbf{GH}$ is a consequence relation in the sense of the framework. By Lemma 64 and 65, $(\mathit{GHRed}_1^q, \mathit{GHRed}_C)$ is a redundancy criterion in the sense of the framework, and $G^q$ are grounding functions in the sense of the framework, for all $q \in Q$. The redundancy criterion $(\mathit{HRed}_1, \mathit{HRed}_C)$ matches exactly the intersected lifted redundancy criterion $\mathit{Red}^{\mathcal{G}, \sqsupset}$ of the saturation framework. Theorem 14 of the saturation framework applies only when $\sqsupset = \emptyset$. By Lemma 16 of the saturation framework, it also holds if $\sqsupset \neq \emptyset$. $\square$

Let $N \subseteq C_H$ be a clause set saturated w.r.t. $\mathit{HInf}$ and $\mathit{HRed}_1$. For the above theorem to apply, we need to show that there exists a $q \in Q$ such that all inferences $\iota \in \mathit{GHInf}^q$ with $\mathit{prems}(\iota) \in G(N)$ are liftable or redundant. Here, $\iota$ being *liftable* means that $\iota$ is a $G^q$-ground instance of an $\mathit{HInf}$-inference from $N$; $\iota$ being *redundant* means that $\iota \in \mathit{GHRed}_1^q(G(N))$.

To choose the right $q = (\mathit{GHLitSel}, \mathit{GHBoolSel}, \mathit{GHWit}) \in Q$, we observe that each ground clause $C \in G(N)$ must have at least one corresponding clause $D \in N$ such that $C$ is a ground instance of $D$. We choose one of them for each $C \in G(N)$, which we denote by $G^{-1}(C)$. Then we choose $\mathit{GHLitSel}$ and $\mathit{GHBoolSel}$ such that the selections in $C$ correspond to those in $G^{-1}(C)$ in the sense of Definition 38.
To choose the witness function GHWit, let $C \in \mathcal{C}_{GH}$ and let $p$ be a green position of a quantifier-headed term $C|_p = Q\langle\tau\rangle t$. Let $D = G^{-1}(C)$ and let $\theta$ be the grounding substitution such that $D\theta = C$. Let $p'$ be the green position corresponding to $p$ in $D$. If there exists no such position $p'$, we define $GHWit(C, p)$ to be some arbitrary term that fulfills the order requirements of a witness function. Otherwise, let $\beta$ and $y$ be fresh variables and we extend $\theta$ to a substitution $\theta'$ by defining $\beta' = \tau$ and $y\theta' = t$. Then $\theta'$ is a unifier of $Q\langle\beta\rangle y$ and $D|_{p'}$ and hence there exists an idempotent $\sigma \in \text{CSU}(Q\langle\beta\rangle y, D|_{p'})$ such that for some substitution $\rho$ and for all free variables $x$ in $D$ and for $x \in \{y, \beta\}$, we have $x\sigma\rho = x\theta'$. We let $GHWit(C, p)$ be $\text{sk}_{\Pi_{\tilde{\alpha}}. \forall \tilde{x}. \exists z. \neg(y\sigma z)\langle\tilde{\alpha}\rangle \tilde{x}\theta}$ if the quantifier-headed term is a $\forall$-term and $\text{sk}_{\Pi_{\tilde{\alpha}}. \forall \tilde{x}. \exists z. (y\sigma z)\langle\tilde{\alpha}\rangle \tilde{x}\theta}$ if the quantifier-headed term is an $\exists$-term where $\tilde{\alpha}$ are the free type variables and $\tilde{x}$ are the free variables occurring in $D|_{p'}$ in order of first occurrence.

By definition of $\mathcal{G}$ (Definition 34), for all free variables $x$ occurring in $D$ the only Boolean green subterms of $x\theta$ are $\mathbf{T}$ and $\mathbf{\perp}$. The term $Q\langle\tau\rangle t$ must be $\mathcal{Q}\mathcal{G}$-normal because it occurs in $C \in \mathcal{C}_{GH}$. Hence $Q\langle\tau\rangle t \succ t \text{ GHWit}(C, p)$ by order condition O4.

With respect to this parameter triple $q = (\text{GHLitSel}, \text{GHBoolSel}, \text{GHWit})$, we can show that all inferences from $\mathcal{G}(N)$ are liftable or redundant:

**Lemma 67** Let $C\theta \in \mathcal{C}_{GH}$ and $C = G^{-1}(C\theta)$. Let $\sigma$ and $\rho$ be substitutions such that $x\sigma\rho = x\theta$ for all free variables in $C$. (This holds for example if $\sigma$ is an element of a CSU corresponding to a unifier $\theta$.) If a literal in a clause $C\theta$ is (strictly) $\succeq$-eligible w.r.t. $\text{GHLitSel}$, then a corresponding literal in $C$ is (strictly) $\succeq$-eligible w.r.t. $\sigma$ and $\text{HLitSel}$. If a green position in a clause $C\theta$ is $\succeq$-eligible w.r.t. $\text{GHBoolSel}$ and there exists a corresponding green position in $C$, then the corresponding position in $C$ is $\succeq$-eligible w.r.t. $\sigma$ and $\text{HBoolSel}$.

*Proof* **LITERALS:** If the literal in $C\theta$ is selected w.r.t. $\text{GHLitSel}$, then the corresponding literal is also selected in $C = G^{-1}(C\theta)$ w.r.t. $\text{HLitSel}$ by definition of $\text{GHLitSel}$ (Definition 38). If $L\theta$ is (strictly) $\succeq$-maximal in $C\theta$, then $L\sigma$ is (strictly) $\succeq$-maximal in $C\sigma$.

**POSITIONS:** Let $p$ be the position in $C\theta$ and let $p'$ be the corresponding position in $C$. We proceed by induction over the definition of eligible positions (Definition 22). If $p$ is selected in $C\theta$ w.r.t. $\text{GHBoolSel}$, then $p'$ is selected in $C = G^{-1}(C\theta)$ w.r.t. $\text{HBoolSel}$ by definition of $\text{GHBoolSel}$ (Definition 38). Otherwise, if $p$ is at the top level of a literal $L\theta = s\theta \approx t\theta$, then $s\theta \not\leq t\theta$ implies $s\sigma \not\leq t\sigma$, (strict) $\succeq$-eligibility of $L\theta$ implies (strict) $\succeq$-eligibility of $L$ w.r.t. $\sigma$ (as shown above), and hence $p'$ is eligible in $C$ w.r.t. $\sigma$. Otherwise, the position $p$ is neither selected nor at the top level. Let $q$ be the position directly above $p$ and $q'$ be the position directly above $p'$. By the induction hypothesis, $q$ and $q'$ are eligible. If the head of $C\theta_p$ is not $\approx$ or $\nparallel$, then the head of $C_{p'}$ cannot be $\approx$ or $\nparallel$ either. If the head $C\theta_p$ is $\approx$ or $\nparallel$, then $C_{p'}$ must also be $\approx$ or $\nparallel$ because the position $p'$ is green. Hence, $p'$ is eligible because $s\theta \not\leq t\theta$ implies $s\sigma \not\succeq t\sigma$. $\square$

In some edge cases, it is ambiguous what “the corresponding” literal is. When $C\theta$ contains multiple occurrences of a literal that correspond to different literals in $C$, we must choose a selected literal if available, or else a $\succeq$-maximal literal to make the lemma above work. In the following, we will implicitly assume that the correct literal is chosen when we refer to “the corresponding” literal.

**Lemma 68** All ERES, EFACT, GARGCONG, GEXT, GCHOICE, BOOLHOIST, and FALSE-ELIM inferences are liftable.

*Proof* For ERES, EFACT, GARGCONG, and GEXT, the proof is as in Lemma 50 of $\lambda\text{Sup}$ [10]. For GCHOICE, the proof is analogous to GEXT.
**BOOLHOIST:** Let $\iota \in GHInf$ be a BOOLHOIST inference with $prems(\iota) \in \mathcal{G}(N)$. Then $\iota$ is of the form

$$ \frac{C\theta\langle u \rangle_p}{C\theta\langle \perp \rangle_p \lor u \approx \mathbf{T}} \text{BOOLHOIST} $$

where $\mathcal{G}^{-1}(C\theta) = C$.

If $p$ corresponds to a position at or below an unapplied variable in $C$, $u$ could only be $\mathbf{T}$ or $\perp$, contradicting the condition of BOOLHOIST that $u$ is not a fully applied logical symbol.

If $p$ corresponds to a position at or below a fluid term in $C$, we will lift to a FLUIDBOOL-HOIST inference. Let $p = p_1 \cdot p_2$ such that $p_1$ is the longest prefix of $p$ that corresponds to a green position $p'_1$ in $C$. Let $v = C|_{p'_1}$. Then $v$ is fluid. Let $z$ and $x$ be fresh variables. Define a substitution $\theta'$ that maps the variable $z$ to $\lambda y.(v\theta)\langle y \rangle_{p_2}$, the variable $x$ to $v\theta|_{p_2}$, and all other variables $w$ to $w\theta$. Then $(zx)\theta' = (v\theta)\langle v\theta|_{p_2} \rangle_{p_2} = v\theta = v\theta'$. So $\theta'$ is a unifier of $zx$ and $v$, and thus there exists an idempotent $\sigma \in \text{CSU}(zx, v)$ such that for some substitution $\rho$, for all free variables $y$ in $C$, and for $y \in \{x, z\}$, we have $y\sigma\rho = y\theta'$. By the conditions of BOOLHOIST, $u \neq \mathbf{T}$ and $u \neq \perp$. Then $x\sigma \neq \mathbf{T}$ and $x\sigma \neq \perp$ because $u = v\theta|_{p_2} = x\theta' = x\sigma\rho$. Hence, we have $(z\perp)\theta' = (v\theta)\langle\perp\rangle_{p_2} \neq (v\theta)\langle x\theta' \rangle_{p_2} = (zx)\theta'$ and thus $(z\perp)\sigma \neq (zx)\sigma$. The position $p_1$ must be eligible in $C\theta$ because $p$ is eligible in $C\theta$ and $p_1$ is the longest prefix of $p$ that corresponds to a green position $p'_1$ in $C$. Eligibility of $p_1$ in $C\theta$ implies eligibility of $p'_1$ in $C$ by Lemma 67. Thus, there exists the following FLUIDBOOLHOIST inference $\iota'$:

$$ \frac{C\langle v \rangle_{p'_1}}{(C\langle z \perp \rangle_{p'_1} \lor x \approx \mathbf{T})\sigma} \text{FLUIDBOOLHOIST} $$

The inference $\iota$ is the $\sigma\rho$-ground instance of $\iota'$ and is therefore liftable.

Otherwise, we will lift to a BOOLHOIST inference. Since $u$ is not at or below a variable-headed term, there is a subterm $u'$ of $C$ at position $p'$ corresponding to the subterm $u$ of $C\theta$ at position $p$. Since $u$ is a Boolean term, there is a type unifier $\sigma$ of the type of $u'$ with the Boolean type. Eligibility of $u$ in $C\theta$ implies eligibility of $u'$ in $C$ by Lemma 67. Since the occurrence of $u$ in $C\theta$ is not at the top level of a positive literal, the corresponding occurrence of $u'$ in $C$ is not at the top level of a positive literal either. Thus, there exists the following BOOLHOIST inference $\iota'$:

$$ \frac{C\langle u' \rangle_{p'}}{(C\langle \perp \rangle_{p'} \lor u' \approx \mathbf{T})\sigma} \text{BOOLHOIST} $$

Then $\iota$ is a ground instance of $\iota'$ and is therefore liftable.

**FALSEELIM:** Let $\iota \in GHInf$ be an FALSEELIM inference with $prems(\iota) \in \mathcal{G}(N)$. Then $\iota$ is of the form

$$ \frac{C\theta = C'\theta \lor s\theta \approx s'\theta}{C'\theta} \text{FALSEELIM} $$

where $\mathcal{G}^{-1}(C\theta) = C = C' \lor s \approx s'$ and the literal $s\theta \approx s'\theta$ is strictly $\succeq$-eligible w.r.t. GHLitSel. Since $s\theta \approx s'\theta$ and $\perp \approx \mathbf{T}$ are unifiable and ground, we have $s\theta = \perp$ and $s'\theta = \mathbf{T}$. Thus, there exists an idempotent $\sigma \in \text{CSU}(s \approx s', \perp \approx \mathbf{T})$ such that for some substitution $\rho$ and for all free variables $x$ in $C$, we have $x\sigma\rho = x\theta$. Then $s \approx s'$ is strictly $\succeq$-eligible in $C$ w.r.t. $\sigma$. Hence, the following inference $\iota' \in HInf$ is applicable:

$$ \frac{C' \lor s \approx s'}{C'\sigma} \text{FALSEELIM} $$

Then $\iota$ is the $\sigma\rho$-ground instance of $\iota'$ and is therefore liftable. $\square$
**Lemma 69** All SUP inferences are *liftable* or *redundant*.

*Proof* The proof is as for Lemmas 52 and 53 of λSup [10]. The proof works with the altered definition of deeply occurring variables (Definition 23) because congruence holds below quantifiers on the GF level. □

**Lemma 70** All EQHOIST, NEQHOIST, GFORALLHOIST, GEXISTSHOIST, GFORALLRW, GEXISTSRW, and BOOLRW inferences from $\mathcal{G}(N)$ are *liftable* or *redundant*.

*Proof* Let $\iota \in GHInf$ be a EQHOIST, NEQHOIST, GFORALLHOIST, GEXISTSHOIST, GFORALLRW, GEXISTSRW, or BOOLRW inference from $\mathcal{G}(N)$. Let $C\theta = \text{prems}(\iota)$ where $C = \mathcal{G}^{-1}(C\theta) \in N$. Let $p$ be the position of the affected subterm in $C\theta$.

We distinguish two cases. We will show that $\iota$ is *liftable* if

(A) $p$ corresponds to a position in $C$ that is not at or below a fluid term, or

(B) $p$ is the position of a term $v$ in a literal $v \approx \mathbf{T}$ or $v \approx \bot$ in $C\theta$.

Otherwise, we will show that $\iota$ is *redundant*.

**LIFTABLE CASES:** If condition A or B holds, $p$ corresponds to some position $p'$ in $C$. Let $u = C|_{p'}$. By the definition of the grounding function $\mathcal{G}$ (Definition 34), for all free variables $x$ occurring in $C$, the only Boolean green subterms of $x\theta$ are $\mathbf{T}$ and $\bot$. Since $u\theta$ is a fully applied logical symbol different from $\mathbf{T}$ and $\bot$, the term $u$ cannot be a variable. Eligibility of $p$ in $C\theta$ implies eligibility of $p'$ in $C$ by Lemma 67. If $u$ is a fluid term, by conditions A and B, it must be in a literal $u \approx \mathbf{T}$ or $u \approx \bot$ or $u \approx \varnothing$ of $C$, for some variable-headed term $v$.

- **BOOLRW:** Let $(t, t')$ be the pair used among the ones listed for BOOLRW. Then we can extend $\theta$ to the free variables in $t$ such that the resulting substitution $\theta'$ is a unifier of $t$ and $u$. Therefore, there exists an idempotent $\sigma \in \text{CSU}(t, u)$ such that for some substitution $\rho$ and for all free variables $x$ in $C$, we have $x\sigma\rho = x\theta'$. Thus, there is the following BOOLRW inference $\iota' \in HInf$:

$$ \frac{C\langle u \rangle}{C\langle t' \rangle \sigma} \text{BOOLRW} $$

In this case, $\iota$ is the $\sigma\rho$-ground instance of $\iota'$ and is therefore *liftable*.

- **GFORALLRW:** Then $u\theta = \forall\langle\tau\rangle v$ and the inference $\iota$ is of the form

$$ \frac{C\theta\langle\forall\langle\tau\rangle v\rangle_p}{C\theta\langle v \text{GHWit}(C\theta, p)\rangle_p} \text{GFORALLRW} $$

for some term $v$ and some type $\tau$.

Let $\beta$ be a type variable and $y$ a variable of type $\beta \to \alpha$. We define a substitution $\theta'$ mapping $y$ to $v$, $\beta$ to $\tau$, and all other variables $x$ to $x\theta$. Then $(\forall\langle\beta\rangle y)\theta' = \forall\langle\tau\rangle v = u\theta = u\theta'$ and hence $\theta'$ is a unifier of $\forall\langle\beta\rangle y$ and $u$. Hence, there exists an idempotent $\sigma \in \text{CSU}(\forall\langle\beta\rangle y, u)$ such that for some substitution $\rho$, for all free variables $x$ in $C$, and for $x \in \{\beta, y\}$, we have $x\sigma\rho = x\theta'$. Since the affected literal in $C\theta$ is not of the form $u\theta \approx \mathbf{T}$, the affected literal in $C$ cannot be of the form $u \approx \mathbf{T}$. Thus, there exists the following inference $\iota' \in HInf$:

$$ \frac{C\langle u \rangle}{C\langle y (\text{sk}_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, \neg(y\sigma z)}\langle\tilde{\alpha}\rangle \tilde{x}) \rangle} \text{FORALLRW} $$

We have GHWit($C\theta, p$) = sk$_{\Pi\tilde{\alpha}, \forall\tilde{x}, \exists z, \neg(y\sigma z)}\langle\tilde{\alpha}\rangle \tilde{x}\theta$ by definition of the witness function, where $\tilde{\alpha}$ are the free type variables and $\tilde{x}$ are the free variables occurring in $y\sigma$ in order of first occurrence. Hence, $\iota$ is the $\sigma\rho$-ground instance of $\iota'$ and is therefore *liftable*.
- GEXISTSRW: Analogous to GFORALLRW.

- EQHOIST: Let $x$ and $y$ be fresh variables. Then we can extend $\theta$ to a $x$ and $y$ such that the resulting substitution $\theta'$ is a unifier of $u$ and $x \rightsquigarrow y$. Thus, there exists an idempotent $\sigma \in \text{CSU}(u, x \rightsquigarrow y)$ such that for some substitution $\rho$, for all free variables $z$ in $C$, and for $z \in \{x, y\}$, we have $z\sigma\rho = z\theta'$. Hence, there is the following EQHOIST inference $l' \in \text{HInf}$:

$$ \frac{C\langle u \rangle}{(C\langle \perp \rangle \lor x \approx y)\sigma} \text{EQHOIST} $$

Then $l$ is the $\sigma\rho$-ground instance of $l'$ and is therefore liftable.

- NEQHOIST: Analogous to EQHOIST.

- GFORALLHOIST: Let $\alpha$ be a fresh type variable and $y$ be a fresh variable. Then we can extend $\theta$ to $y$ such that the resulting substitution $\theta'$ is a unifier of $u$ and $\forall\langle\alpha\rangle y$. Thus, there exists an idempotent $\sigma \in \text{CSU}(u, \forall\langle\alpha\rangle y)$ such that for some substitution $\rho$, for all free variables $x$ in $C$, and for $x = y$, we have $x\sigma\rho = x\theta'$. Thus, there is the following FORALLHOIST inference $l' \in \text{HInf}$:

$$ \frac{C\langle u \rangle}{(C\langle \perp \rangle \lor y x \approx \mathbf{T})\sigma} \text{FORALLHOIST} $$

Then $l$ is the $\sigma\rho$-ground instance of $l'$ and is therefore liftable.

- GEXISTSHOIST: Analogous to GFORALLHOIST.

REDUNDANT CASE: Neither condition A nor B holds. Then $p$ corresponds to a position in $C$ at or below a fluid term, but $p$ is not the position of $v$ in a literal $v \approx \mathbf{T}$ or $v \approx \perp$. Let $p = p_1 \cdot p_2$ such that $p_1$ is the longest prefix of $p$ that corresponds to a green position $p'_1$ in $C$. Let $u = C|_{p'_1}$. Let $z$ and $x$ be fresh variables. Define a substitution $\theta'$ that maps the variable $z$ to $\lambda y.(u\theta)\langle y \rangle_{p_2}$, the variable $x$ to $u\theta|_{p_2}$, and all other variables $w$ to $w\theta$. Then $(zx)\theta' = (u\theta)\langle u\theta|_{p_2} \rangle_{p_2} = u\theta = u\theta'$. So $\theta'$ is a unifier of $zx$ and $u$. Thus, there exists an idempotent $\sigma \in \text{CSU}(zx, u)$ such that for some substitution $\rho$, for all free variables $y$ in $C$, and for $y \in \{z, x\}$, we have $y\sigma\rho = y\theta'$. For all of the inference rules, $C\theta|_p = u\theta|_{p_2}$ cannot be $\perp$ or $\mathbf{T}$. Thus, $x\theta' \neq \perp$, $\mathbf{T}$ and therefore $x\sigma \neq \perp$, $\mathbf{T}$. Hence, we have $(z\perp)\theta' = (u\theta)\langle \perp \rangle_{p_2} \neq (u\theta)\langle x\theta' \rangle_{p_2} = (zx)\theta' \text{ and therefore } (z\perp)\sigma \neq (zx)\sigma$. Analogously, we have $(z\mathbf{T})\sigma \neq (zx)\sigma$. The position $p_1$ must be eligible in $C\theta$ because $p$ is eligible in $C\theta$ and $p_1$ is the longest prefix of $p$ that corresponds to a green position $p'_1$ in $C$. Eligibility of $p_1$ in $C\theta$ implies eligibility of $p'_1$ in $C$ by Lemma 67. Then there are the following inferences $\iota_{bool}$ and $\iota_{loob}$ from $C$:

$$ \frac{C\langle u \rangle_{p'_1}}{(C\langle z \perp \rangle_{p'_1} \lor x \approx \mathbf{T})\sigma} \text{FLUIDBOOLHOIST} $$

$$ \frac{C\langle u \rangle_{p'_1}}{(C\langle z \mathbf{T} \rangle_{p'_1} \lor x \approx \perp)\sigma} \text{FLUIDLOOBHOIST} $$

Since $N$ is saturated w.r.t. $\text{HInf}$ and $\text{HRed}_1$, these inferences are in $\text{HRed}_1(N)$. We have

$$ \mathcal{F}((C\langle z \perp \rangle_{p'_1} \lor x \approx \mathbf{T})\theta') = \mathcal{F}(C\theta\langle \perp \rangle_p \lor C\theta|_p \approx \mathbf{T}) $$

$$ \text{and } \mathcal{F}((C\langle z \mathbf{T} \rangle_{p'_1} \lor x \approx \perp)\theta') = \mathcal{F}(C\theta\langle \mathbf{T} \rangle_p \lor C\theta|_p \approx \perp) $$
These two clauses entail $\mathcal{F}(C\theta)$. Since $p$ is not the position of $v$ in a literal $v \approx \mathbf{T}$ or $v \approx \bot$, the two clauses are also smaller than $\mathcal{F}(C\theta)$. Since $\iota_{bool} \in \mathit{HRed}_1(N)$, we have $\mathcal{G}^q(\iota_{bool}) \subseteq \mathit{GHRed}_1(\mathcal{G}(N))$ and therefore the clauses $\mathcal{F}(\mathcal{G}(N))$ that are smaller than $\mathcal{F}(C\theta') = \mathcal{F}(C\theta)$ entail $\mathcal{F}((C<z\bot>p_1') \lor x \approx \mathbf{T})\theta'$. Similarly, since $\iota_{loob} \in \mathit{HRed}_1(N)$, we have $\mathcal{G}(\mathit{concl}(\iota_{loob})) \subseteq \mathcal{G}(N) \cup \mathit{GHRed}_c(\mathcal{G}(N))$. Therefore $\mathcal{F}((C<z\mathbf{T}>p_1') \lor x \approx \bot)\theta'$ is entailed by clauses in $\mathcal{G}(N)$ that are smaller than or equal to itself. Thus, $C\theta$ is redundant and therefore $\iota$ is redundant. Here, it is crucial that we consider inferences with a redundant premise as redundant. $\square$

By the above lemmas, every *HInf* inference is liftable or redundant. Using these lemmas, we can apply Theorem 66 to lift ground refutational completeness to nonground refutational completeness.

**Lemma 71 (Static refutational completeness w.r.t. $|\models_G)$** The inference system *HInf* is statically refutationally complete w.r.t. $|\models_G$ and $(HRed_1, HRed_C)$. In other words, if $N \subseteq C_H$ is a clause set saturated w.r.t. *HInf* and *HRed*₁, then $N |\models_G \perp$ if and only if $\perp \in N$.

*Proof* We want to apply Theorem 66. $GHInf^q$ is statically refutationally complete for all $q \in Q$ by Theorem 62. By Lemmas 68, 69, and 70, for every saturated $N \subseteq C_H$, there exists $q \in \mathcal{G}(Q)$ such that all inferences $\iota \in GHInf^q$ with $\mathit{prems}(\iota) \in \mathcal{G}(N)$ either are $\mathcal{G}^q$-ground instances of *HInf*-inferences from $N$ or belong to $GHRed_1^q(\mathcal{G}(N))$. Thus, Theorem 66 applies. $\square$

<figure><img src="image_8.png" /></figure>

Dynamic refutational completeness is easy to derive from static refutational completeness:

**Lemma 72 (Dynamic refutational completeness w.r.t. $|\models_G)$** The inference system *HInf* is dynamically refutationally complete w.r.t. $|\models_G$ and $(HRed_1, HRed_C)$, as per Definition 50.

*Proof* By Theorem 17 of the saturation framework, this follows from Lemma 71. $\square$

<figure><img src="image_9.png" /></figure>

To derive a corresponding result for the entailment relation $|\models$, we employ the following lemma, which states equivalence of Herbrand entailment $|\models_G$ and Tarski entailment $|\models$ on $Q\mathcal{R}$-normal clauses.

**Lemma 73** Let $N \subseteq C_H$ be $Q\mathcal{R}$-normal. Then we have $N |\models_G \perp$ if and only if $N |\models$.

*Proof* By Lemma 30, any model of $N$ is also a model of $\mathcal{G}(N)$. So $N |\models_G \perp$ implies $N |\models$.

For the other direction, let $\mathcal{J}$ be a model of $\mathcal{G}(N)$. We must show that there exists a model of $N$. Let $\mathcal{J}'$ be the interpretation obtained from $\mathcal{J}$ by removing all domains that cannot be expressed as $[[\tau]]_{\mathcal{J}}$ for some ground type $\tau$ and by removing all domain elements that cannot be expressed as $[[t]]_j$ for some ground term $t$. We restrict the type interpretation function $\mathcal{J}_{ty}$, the interpretation function $\mathcal{J}$, and the $\lambda$-designation function $\mathcal{L}$ of $\mathcal{J}$ accordingly.

The restriction $\mathcal{J}'$ of $\mathcal{J}$ still maps the logical symbols correctly: For most logical symbols, this is obvious. Only $\forall$ and $\exists$ deserve some further explanations. For all domains $\mathcal{D}$ of $\mathcal{J}$, we have $\mathcal{J}(\exists, \mathcal{D})(f) = \max\{f(a) \mid a \in \mathcal{D}\}$. For the corresponding domain $\mathcal{D}' \subseteq \mathcal{D}$, if it has not been removed entirely, we have just defined $\mathcal{J}'(\exists, \mathcal{D}')(f) = \mathcal{J}(\exists, \mathcal{D})(f)$. We must show that $\mathcal{J}'(\exists, \mathcal{D}')(f) = \max\{f(a) \mid a \in \mathcal{D}'\}$ for all $f$ that can be expressed as $[[t]]_j$ for some ground term $t$. This claim can only be violated if there exist $a \in \mathcal{D}$ with $f(a) = 1$ and if all of them have been removed in $\mathcal{D}'$. But we have not removed all such elements $a$ because one of them can be expressed as $[[\varepsilon t]]_j$ where $t$ is the ground term such that $f = [[t]]_j$. We can argue similarly for $\forall$.
Clearly, all terms have the same denotation in $J'$ as in $J$. Thus, the truth values of ground clauses are identical in $J$ and $J'$. Since $J$ is proper, $J'$ is also proper. Hence, $J \models G(N)$ implies $J' \models G(N)$.

It remains to show that $J' \models N$. Let $C \in N$ and let $\xi$ be a valuation for $J'$. We must show that $C$ is true in $J'$ under $\xi$. By assumption, $C$ is $Q\mathcal{R}\mathcal{S}$-normal.

By the construction of $J'$, there is a grounding substitution $\theta$ such that for all type variables $\alpha$ and all free term variables $x$ occurring in $C$, we have $\xi(\alpha) = [[\alpha\theta]]_{J'}$ and $\xi(x) = [[x\theta]]_{J'}$. Then, by Lemma 29, $[[t\theta]]_{J'} = [[t]]_{J'}^\xi$ for all subterms $t$ of $C$. Moreover, we can choose $\theta$ such that for all variables $x$, the only Boolean green subterms of $x\theta$ are $\mathbf{T}$ and $\bot$ and such that $x\theta$ is $Q\mathcal{R}\mathcal{S}$-normal. If $x\theta$ contains a Boolean green subterm different from $\mathbf{T}$ and $\bot$, we can replace it by $\mathbf{T}$ or $\bot$ while preserving its denotation and thus the property that $[[t\theta]]_{J'} = [[t]]_{J'}^\xi$ for all subterms $t$ of $C$. If $x\theta$ is not $Q\mathcal{R}\mathcal{S}$-normal, we $Q\mathcal{R}\mathcal{S}$-normalize it, which preserves the denotation of terms by Lemma 55.

By Lemma 9, it follows that $C\theta$ is $Q\mathcal{R}\mathcal{S}$-normal. Thus, $C\theta \in G(C)$. Since $J' \models G(C)$ and thus $C\theta$ is true in $J'$, also $C$ is true in $J'$ under $\xi$ because $[[t\theta]]_{J'} = [[t]]_{J'}^\xi$ for all subterms $t$ of $C$. $\square$

Using this lemma, we can derive the following theorem, which is essentially dynamic refutational completeness with the caveat that the initial clause set must be $Q\mathcal{R}\mathcal{S}$-normal, which in practice can be fulfilled by $Q\mathcal{R}\mathcal{S}$-normalizing the input problem in preprocessing.

**Theorem 74 (Dynamic refutational completeness w.r.t. $\models$)** Let $(N_i)_i$ be a derivation w.r.t. $HRed_C$, as per Definition 50, such that $N_0$ is $Q\mathcal{R}\mathcal{S}$-normal and $N_0 \models \bot$. Moreover, assume that $(N_i)_i$ is fair w.r.t. $HInf$ and $HRed_1$. Then we have $\bot \in N_i$ for some $i$.

*Proof* This is a consequence of Lemmas 72 and 73. $\square$

<figure><img src="image_10.png" /></figure>

We can derive dynamic refutational completeness for $\models \approx$ with additional assumptions on $Q\mathcal{R}\mathcal{S}$-normality and the absence of sk-symbols. These assumptions can be fulfilled by $Q\mathcal{R}\mathcal{S}$-preprocessing and by making the sk symbols internal such that they can not be expressed by the input language of the prover.

**Theorem 75 (Dynamic refutational completeness w.r.t. $\models$)** Let $(N_i)_i$ be a derivation w.r.t. $HRed_C$, as defined in Definition 50, such that $N_0$ is $Q\mathcal{R}\mathcal{S}$-normal, $N_0$ does not contain any sk symbols, and $N_0 \models \bot$. Moreover, assume that $(N_i)_i$ is fair w.r.t. $HInf$ and $HRed_1$. Then we have $\bot \in N_i$ for some $i$.

*Proof* By Lemma 32, $N_0 \models \bot$. Hence, Theorem 74 applies. $\square$

<figure><img src="image_11.png" /></figure>

# 5 Implementation

We implemented our calculus in the Zipperposition prover<fnref n="1" />, whose OCaml source code makes it convenient to prototype calculus extensions. It has also assimilated some of E's [33] heuristics, which helps it achieve strong performance at the CASC competition.

Like the calculus, its implementation extends the implementations of $\lambda$Sup and oSup. From the former, we inherit the given clause loop which supports enumerating infinitely many inference conclusions [37, Sect. 5], calculus extensions, and higher-order heuristics [37]. From the latter, we inherit the encoding of negative predicate literals as $s \approx \bot$ and a basis

<footnote n="1">¹ https://github.com/sneeuwballen/zipperposition</footnote>