AN ANALYSIS OF THE CONSTRUCTIVE CONTENT OF HENKIN'S PROOF
OF GÖDEL'S COMPLETENESS THEOREM

HUGO HERBELIN AND DANKO ILIK

**Abstract.** Gödel's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.

We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin's proof within intuitionistic second-order arithmetic.

It is standard in the context of the completeness of intuitionistic logic with respect to various semantics such as Kripke or Beth semantics to follow the Curry-Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability.

We apply this approach to Henkin's proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.

By doing so, we hope to shed an "effective" light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects that we can manipulate and compute with, like ordinary syntax.

CONTENTS

<table><tbody><tr><td>1. Preliminaries</td><td>2</td></tr><tr><td>1.1. The completeness theorem</td><td>2</td></tr><tr><td>1.2. Weak and strong completeness</td><td>3</td></tr><tr><td>1.3. The standard existing proofs of completeness</td><td>3</td></tr><tr><td>1.4. Models and truth</td><td>4</td></tr><tr><td>1.5. Regarding the metalanguage as a formal system</td><td>6</td></tr><tr><td>1.6. The computational content of completeness proofs for intuitionistic logic</td><td>7</td></tr><tr><td>1.7. The intuitionistic provability of the different statements of completeness</td><td>10</td></tr><tr><td>1.8. Chronology and recent related works</td><td>12</td></tr><tr><td>2. The computational content of Henkin's proof of Gödel's completeness</td><td>12</td></tr><tr><td>2.1. Henkin's proof, slightly simplified</td><td>13</td></tr><tr><td>2.2. From Henkin's proof to a proof with respect to possibly-exploding models</td><td>14</td></tr><tr><td>2.3. The computational content of the proof of completeness</td><td>15</td></tr><tr><td>2.4. The computational content on examples</td><td>21</td></tr><tr><td>2.5. Extension to conjunction</td><td>24</td></tr><tr><td>2.6. Extension to disjunction</td><td>24</td></tr><tr><td>2.7. About the logical strength of completeness in the presence of disjunction</td><td>27</td></tr><tr><td>2.8. Extension to existential quantification</td><td>28</td></tr></tbody></table>
§1. Preliminaries.

**1.1. The completeness theorem.** The completeness theorem for classical first-order logic is one of the most basic and traditional theorems of logic. Proved by Gödel in 1929 [35] as an answer to a question raised by Hilbert and Ackermann in 1928 [46], it states that any of the standard equivalent formal systems for defining provability in first-order logic is complete enough to include a derivation of every valid formula. A formula *A* is valid when it is true under all interpretations of its primitive symbols over any domain of quantification.

Let $\mathcal{L}$ be a signature for first-order logic, i.e. the data of a set<fnref n="1" /> *Fun* of function symbols, each of them coming with an arity, as well as of a set *Pred* of predicate symbols, each of them also coming with an arity. We call constants the function symbols of arity 0 and propositional atoms the predicate symbols of arity 0. When studying the computational content of Gödel’s completeness in Section 2, we shall restrict the language to a countable one but the rest of this section does not require restrictions on the cardinal of the language.

We let $f$ range over $\mathcal{F}un$ and $P$ range over $\mathcal{P}red$. For $f \in \mathcal{F}un$ and $P \in \mathcal{P}red$, we respectively write their arity $a_f$ and $a_P$. Let $x$ range over a countable set $\mathcal{X}$ of variables and let $t$ range over the set $\mathcal{T}erm$ of terms over $\mathcal{L}$ as described by the following grammar:

$$t ::= x \mid f(t_1, \dots, t_{a_f})$$

Let $A$ range over the set $\mathcal{F}orm$ of formulae over $\mathcal{L}$ as described by the following grammar:

$$A ::= P(t_1, \dots, t_{p_f}) \mid \bot \mid A \Rightarrow A \mid \forall x A$$

Note that in classical first-order logic, the language of *negative* connectives and quantifiers made of $\Rightarrow$, $\forall$ and $\bot$ is enough to express all other connectives and quantifiers. The dot over the notations is to distinguish the connectives and quantifier of the logic we are talking about (object logic) from the connectives and quantifiers of the ambient logic in which the completeness theorem is formulated (meta-logic, see below). We take $\bot$ as a primitive connective and this allows to express consistency of the object logic as the non-provability of $\bot$. Negation can then be defined as $\neg A \equiv A \Rightarrow \bot$. Also, in $\forall x A$, we say that $x$ is a binding variable which binds all occurrences of $x$ in $A$ (if any). If the occurrence of a variable is not in the scope of a $\forall$ with same name, it is called free. If a formula has no free variables, we say it is *closed*.

Let us write $\Gamma$ for finite contexts of hypotheses, as defined by the following grammar:

$$\Gamma ::= \epsilon \mid \Gamma, A$$

In particular, $\epsilon$ denotes the empty context, which we might also not write at all, as e.g. in $\vdash A$ standing for $\epsilon \vdash A$.

We assume having chosen a formal system for provability in classical first-order logic, e.g. one of the axiomatic systems given in Frege [30] or in Hilbert and Ackermann [46], or one of the systems such as Gentzen-Jaśkowski's natural deduction [54, 34] or Gentzen's sequent calculus [34], etc., and we write $\Gamma \vdash A$ for the statement that $A$ is provable under the finite context of hypotheses $\Gamma$. If $\mathcal{M}$ is a model for classical logic and $\sigma$ an interpretation of the variables from $\mathcal{X}$ in the model, we write $\mathcal{M} \models_{\sigma} A$ for the statement expressing that $A$ is true in the model $\mathcal{M}$ (to be defined

<footnote n="1">¹We use here “set” in an informal way, not necessarily assuming the metalanguage to be specifically set theory.</footnote>
in Section 1.4). Validity of A under assumptions $\Gamma$, written $\Gamma \vdash A$ is defined to be $\forall M \forall \sigma (M \Vdash_{\sigma} \Gamma \Rightarrow M \Vdash_{\sigma} A)$ where $M \Vdash_{\sigma} \Gamma$ is the conjunction of all $M \Vdash_{\sigma} B$ for every $B$ in $\Gamma$, i.e. $\bigwedge_{B \in \Gamma} M \Vdash_{\sigma} B$. Note that $\Rightarrow$, $\forall$, $\wedge$ and, later on, below, $\vee$, $\exists$, $\perp$, as well as derived $\neg$, represent the connectives and quantifiers of the metalanguage.

We say that $\Gamma$ is inconsistent if $\Gamma \vdash \bot$ and consistent if $\Gamma \Vdash \bot$, i.e. if $(\Gamma \vdash \bot) \Rightarrow \bot$, i.e., if a contradiction in the object language is reflected as a contradiction in the meta-logic. We say that $\Gamma$ has a model if there exist $M$ and $\sigma$ such that $M \Vdash_{\sigma} \Gamma$. The completeness theorem, actually a weak form of the completeness theorem as discussed in the next section, is commonly stated under one of the following classically but not intuitionistically equivalent forms:

$$C1. \quad \vdash A \Rightarrow \Gamma$$

$$C2. \quad \Gamma \text{ is consistent} \Rightarrow \Gamma \text{ has a model}$$

$$C3. \quad \Gamma, \neg A \text{ has a model} \lor \Gamma \vdash A$$

**1.2. Weak and strong completeness.** In a strong form, referred to as strong completeness<fnref n="2" />, completeness states that any formula valid under some possibly infinite theory is provable under a finite subset of this theory. This is the most standard formulation of completeness in textbooks, and, as such, it is a key component of the compactness theorem. Also proved by Gödel [36], the compactness theorem states that it is enough for a theory to have a model that any finite subset of the theory has a model. In contrast, completeness with respect to finite theories as stated above is referred to as weak completeness. Let $\mathcal{T}$ be a set of formulae and let $\mathcal{T} \vdash A$ mean the existence of a finite sequence $\Gamma$ of formulae in $\mathcal{T}$ such that $\Gamma \vdash A$. Let $M \Vdash_{\sigma} \mathcal{T}$ be $\forall B \in \mathcal{T} M \Vdash_{\sigma} B$ and let the definitions of $\mathcal{T}$ is consistent and of $\mathcal{T}$ has model be extended accordingly. The strong formulations of the three views at weak completeness above are now the following:

$$S1. \quad \mathcal{T} \vdash A \Rightarrow \mathcal{T} \vdash A$$

$$S2. \quad \mathcal{T} \text{ is consistent} \Rightarrow \mathcal{T} \text{ has a model}$$

$$S3. \quad \mathcal{T} \cup \{\neg A\} \text{ has a model} \lor \mathcal{T} \vdash A$$

We shall consider the formalisation and computational content of strong completeness. Weak completeness will then come as a special case.

**1.3. The standard existing proofs of completeness.** Let us list a few traditional proofs from the classic literature<fnref n="3" />.

<footnote n="2">²We follow here a terminology dubbed by Henkin in his 1947 dissertation, according to [41]. However, in the context of intuitionistic logic, some authors use the weak and strong adjectives with different meanings. For instance, in Kreisel [60, 61], the statement $(\vdash A) \Rightarrow (\vdash A)$ is called strong completeness while weak completeness is the statement $(\vdash A) \Rightarrow \neg(\vdash A)$. In the context of semantic cut-elimination, e.g. in Okada [71], $(\vdash A) \Rightarrow (\vdash A)$ is only a weak form of completeness whose strong form is the statement $(\vdash A) \Rightarrow (\vdash_{\text{cut-free}} A)$, for a notion of cut-free proof similar to the notion of cut-free proof in Gentzen's sequent calculus or to normal proofs in Prawitz' analysis of normalisation for natural deduction.</footnote>

<footnote n="3">³We cite the most common proofs in the classic pre-1960 literature. Recent developments include e.g. Joyal's categorical presentation of a completeness theorem. We can also cite Berger's [75, Sec. 1.4.3] or Krivtsov [67] construction in intuitionistic logic of a classical model from a Beth model for classical provability. These two latter proofs are variants of the Beth-Hintikka-Kanger-Schütte style of proofs, the first one relying on the axiom of dependent choice and the second on the (weaker) Fan theorem.</footnote>
* Gödel's original proof [35] considers formulae in prenex form and works by induction on the number of quantifiers for reducing the completeness of first-order predicate logic completeness to the completeness of propositional logic.

* Henkin's proof [40] is related to statement S2: from the assumption that $\mathcal{T}$ is consistent, a syntactic model over the terms is built as a maximal consistent extension of $\mathcal{T}$ obtained by ordering the set of formulae and extending $\mathcal{T}$ with those formulae that preserve consistency, following the ordering.

* In the 1950's, a new kind of proof independently credited to Beth [11], Hinkikka [48, 49], Kanger [57] and Schütte [76] was given. The underlying idea is to build an infinite normal derivation, typically in sequent calculus. Rules are applied in a fair way, such that all possible combinations of rules are considered. If the derivation happens to be finite, a proof is obtained. Otherwise, by weak König's lemma, there is an infinite branch and this infinite branch gives rise to a countermodel. The intuition underlying this proof is then best represented by statement S3.

* In the 1950's also, Rasiowa and Sikorski [73] gave a variant of Henkin's proof relying on the existence of an ultrafilter for the Lindenbaum algebra of classes of logically equivalent formulae, identifying validity with having value 1 in all interpretations of a formula within the two-value Boolean algebra $\{0, 1\}$. This is close to Henkin's proof in the sense that Henkin's proof implicitly builds an ultrafilter of the Lindenbaum algebra of formulae.

Our main contribution in this paper is the analysis in Section 2 of the computational content of Henkin's proof.

**1.4. Models and truth.** The interpretation of terms in a model $\mathcal{M}$ is given by a domain $\mathcal{D}$ and by an interpretation $\mathcal{F}$ of the symbols in $\mathcal{Fun}$ such that $\mathcal{F}(f) \in \mathcal{D}^{a_f} \to \mathcal{D}$, where $\mathcal{D}^{a_f} \to \mathcal{D}$ denotes the set of functions of arity $a_f$ over $\mathcal{D}$. Then, given an assignment $\sigma \in \mathcal{X} \to \mathcal{D}$ of the variables to arbitrary values of the domain, the interpretation of terms in $\mathcal{D}$ is given by:

$$ \llbracket x \rrbracket_{\mathcal{M}}^{\sigma} \triangleq \sigma(x) \\ \llbracket f(t_1, \dots, t_{a_f}) \rrbracket_{\mathcal{M}}^{\sigma} \triangleq \mathcal{F}(f)(\llbracket t_1 \rrbracket_{\mathcal{M}}^{\sigma}, \dots, \llbracket t_{a_f} \rrbracket_{\mathcal{M}}^{\sigma}) $$

To interpret formulae, two common approaches are used in the literature.

* Tarski semantics (predicates as predicates). This is the approach followed e.g. in the Handbook of Mathematical Logic [6], the Handbook of Proof Theory [14] or in the original proof of Gödel [35]. This approach interprets formulae of the object language propositionally, i.e. as formulae of the metalanguage. In this case, the interpretation depends on whether the metalanguage is classical or not. For instance, in a classical metalanguage, the theory

$$ \mathit{Classic} \triangleq \{\dot{\vdash}\vdash A \Rightarrow A \mid A \in \mathcal{Form}\} $$

would be true in all models. On the other hand, in an intuitionistic metalanguage, a formula such as, say, $\dot{\vdash}\vdash X \Rightarrow X$ could not be proved true in all models$^4$. In a

<footnote>$^4$For instance, if $\mathrm{coh}_{\mathcal{M}\mathcal{L}}$ is the formula expressing the consistency of the metalanguage represented as an object language in the metalanguage itself, then a model $\mathcal{M}$ binding atom $X$ to the metalanguage formula $\mathrm{coh}_{\mathcal{M}\mathcal{L}} \lor \neg\mathrm{coh}_{\mathcal{M}\mathcal{L}}$ would intuitionistically satisfy $\mathcal{M} \models \neg\neg X$ but not $\mathcal{M} \models X$.</footnote>
strongly anti-classical intuitionistic metalanguage refuting double-negation elimination, it could even be proved that there are models<fnref n="5" /> which refute $\vdash\vdash X \Rightarrow X$.

The possible presence of models provably anti-classical is not a problem per se for proving completeness as completeness is only about exhibiting one particular model and it is possible to ensure that $\vdash\vdash X \Rightarrow X$ holds in this particular model. However, whether the metalanguage is classical or not has an impact on the soundness property, i.e. on the statement that the provability of A implies the validity of A. Indeed, there is little hope to prove the soundness of double-negation elimination if the quantification over models include non-classical models. Therefore, for the definition of validity to be both sound and complete for classical provability with respect to Tarski semantics, independently of whether the metalanguage is intuitionistic or classical, we would need to define classical validity using an explicit restriction to classical models:

$$ \mathcal{T} \Vdash A \triangleq \forall M \forall \sigma (M \Vdash_{\sigma} \mathit{Classic} \Rightarrow M \Vdash_{\sigma} \mathcal{T} \Rightarrow M \Vdash_{\sigma} A) $$

* Bivalent semantics (predicates as binary functions). Another approach is to assign to formulae a truth value in the two-valued set {0, 1} and to define $M \Vdash_{\sigma} A$ as $\mathit{truth}_M(A, \sigma) = 1$ for the corresponding truth function. This is the approach followed e.g. in Rasiowa-Sikorski's proof, or also e.g. in [15, 78], among others<fnref n="6" />. In particular, relying on a two-valued truth makes the theory *Classic* automatically true.

Depending on the metalanguage, a function from *Form* to {0, 1} can itself be represented either as a functional relation, i.e. as a relation *istru*e on *Form* × {0, 1} such that for all A, there is a unique b such that *istru*e(A, b) holds (this is the representation used e.g. for the completeness proof in [78]), or, primitively as a function if ever the metalanguage provides such primitive notion of function (as is typically the case in intuitionistic logics, e.g. Heyting Arithmetic in finite types [82], or Martin-Löf's type theory [69, 21]).

Reverse mathematics of the subsystems of classical second-order arithmetic have shown that building a model from a proof of consistency requires the full strength of $\Sigma_1^0$-separability, or equivalently, of Weak Kőnig's Lemma [78]. This implies that the corresponding *truth* function is in general not recursive [59]. Expecting *truth* to be definable primitively as a computable function in an intuitionistic logic is thus hopeless. As for representing truth by a functional relation *istru*e, the expected property *istru*e(A, 0) ∨ *istru*e(A, 1) could only be proven by requiring some amount of classical reasoning.

It is known how to compute with classical logic in second-order arithmetic [38, 72, 65] and we could study the computational content of a formalisation of the completeness proof which uses this definition of truth. The extra need for classical reasoning in this approach looks however like a useless complication, so we shall concentrate on the predicates-as-predicates approach.

<footnote n="5">⁵For instance, in second-order intuitionistic arithmetic extended with Church Thesis (CT), excluded-middle on undecidable formulae is provably contradictory and the same model interpreting X as $\coth_{ML} \lor \neg \coth_{ML}$ invalidates $\vdash\vdash X \Rightarrow X$.</footnote>

<footnote n="6">⁶For instance, the definition of validity used in Henkin [40], though not fully formal, also intends a two-valued semantics.</footnote>
So, to summarise, we will not expect truth to be two-valued and will require explicitly as a counterpart that models are classical, leading to the following refined definitions<fnref n="7" /> of validity and existence of a model:

$$ \mathcal{T} \Vdash A \qquad \triangleq \quad \forall \mathcal{M} \forall \sigma (\mathcal{M} \Vdash_{\sigma} \mathcal{Classic} \Rightarrow \mathcal{M} \Vdash_{\sigma} \mathcal{T} \Rightarrow \mathcal{M} \Vdash_{\sigma} A) $$

$$ \mathcal{T} \text{ has a model} \quad \triangleq \quad \exists \mathcal{M} \exists \sigma (\mathcal{M} \Vdash_{\sigma} \mathcal{Classic} \wedge \mathcal{M} \Vdash_{\sigma} \mathcal{T}) $$

Two auxiliary choices of presentation of Tarski semantics can be made<fnref n="8" />.

* **Recursively-defined truth.** The approach followed e.g. in the Handbook of Mathematical Logic [6] or the Handbook of Proof Theory [14] is to have the model interpret only the predicate symbols and to have the truth of formulae defined recursively. This is obtained by giving an interpretation $\mathcal{P}$ where any symbol $P \in \mathcal{Pred}$ is mapped to a set $\mathcal{P}(P) \subset \mathcal{D}^{a_P}$. Then, the truth of a formula with respect to some assignment $\sigma$ of the free variables is given recursively by:

$$ \mathcal{M} \Vdash_{\sigma} P(t_1, \dots, t_{a_P}) \quad \triangleq \quad (\llbracket t_1 \rrbracket_{\mathcal{M}}^{\sigma}, \dots, \llbracket t_{a_P} \rrbracket_{\mathcal{M}}^{\sigma}) \in \mathcal{P}(P) $$

$$ \mathcal{M} \Vdash_{\sigma} \bot \qquad \triangleq \quad \bot $$

$$ \mathcal{M} \Vdash_{\sigma} A \Rightarrow B \qquad \triangleq \quad \mathcal{M} \Vdash_{\sigma} A \Rightarrow \mathcal{M} \Vdash_{\sigma} B $$

$$ \mathcal{M} \Vdash_{\sigma} \forall x A \qquad \triangleq \quad \forall v \in \mathcal{D} \mathcal{M} \Vdash_{\sigma \cup \{x \leftarrow v\}} A $$

* **Axiomatically-defined truth.** A common alternative approach is to define truth as a subset $S$ of closed formulae in the language of terms extended with the constants of $\mathcal{D}$, such that: $\bot$ is not in $S$; $A \Rightarrow B$ is in $S$ iff $B$ is whenever $A$ is; $\forall x A$ is in $S$ iff $A[x \leftarrow v]$ is for all values $v \in \mathcal{D}$; $A[x \leftarrow f(v_1, \dots, v_n)]$ is in $S$ iff $A[x \leftarrow v]$ is in $S$ whenever $\mathcal{F}(f)(v_1, \dots, v_n) = v$ for some value $v \in S$. This approach is adopted e.g. in Krivine [66].

We will retain the first approach which conveniently exempts us from defining the set of formulae enriched with constants from $\mathcal{D}$. So, shortly, a model $\mathcal{M}$ will be a triple $(\mathcal{D}, \mathcal{F}, \mathcal{P})$ where $\mathcal{F}$ maps any symbol $f \in \mathcal{Fun}$ to a function $\mathcal{F}(f) \in \mathcal{D}^{a_f} \to \mathcal{D}$ and $\mathcal{P}$ maps any symbol $P \in \mathcal{Pred}$ to a set $\mathcal{P}(P) \subset \mathcal{D}^{a_P}$.

**1.5. Regarding the metalanguage as a formal system.** Let $\mathcal{M}$ be the metalanguage in which completeness is stated and $\mathcal{O}$ be the object language used to represent provability in first-order logic. In $\mathcal{M}$, a proof of the validity of a formula $A$ is essentially a proof of the universal closure of $A$, seen as a formula of $\mathcal{M}$, with the closure made over the domain of quantification of quantifiers, over the free predicate symbols, over the free function symbols and over the free variables of $A$. Otherwise said, adopting a constructive view at proofs of the metalanguage, we can think of the weak completeness theorem in form C1 as a process to transform a proof of the universal closure of $A$ expressed in $\mathcal{M}$ into a proof of $A$ expressed in the proof object language $\mathcal{O}$ (and conversely,

$$ \mathcal{M} \Vdash_{\sigma} P(t_1, \dots, t_{a_P}) \triangleq \neg(\llbracket t_1 \rrbracket_{\mathcal{M}}^{\sigma}, \dots, \llbracket t_{a_P} \rrbracket_{\mathcal{M}}^{\sigma}) \in \mathcal{M}(P) $$

or even, saving a negation as in Krivine [63], by

$$ \mathcal{M} \Vdash_{\sigma} P(t_1, \dots, t_{a_P}) \triangleq -(\llbracket t_1 \rrbracket_{\mathcal{M}}^{\sigma}, \dots, \llbracket t_{a_P} \rrbracket_{\mathcal{M}}^{\sigma}) \in \mathcal{M}(P) $$

Indeed, in these cases, the definition of truth becomes a purely negative formula for which intuitionistic and classical provability coincide.

<footnote n="7">⁷For the record, note that, in the presence of only negative connectives, an equivalent way to define $\Vdash A$ so that it means the same in an intuitionistic and classical setting is to replace the definition of $\mathcal{M} \Vdash_{\sigma} P(t_1, \dots, t_{a_P})$ by</footnote>

<footnote n="8">⁸These auxiliary choices would have been relevant as well if we had chosen to represent truth as a map to $\{0, 1\}$.</footnote>
the soundness theorem can be seen as stating an embedding of *O* into *M*. Similarly, a proof of the validity of a formula *A* with respect to an infinite theory *T* is a proof in *M* of the universal closure of (∀*B* ∈ *T*[[*B*]]) ⇒ [[*A*]] where [[*C*]] is the replication of *C* as a formula of *M* and, computationally speaking, statement S1 is a process to turn such a proof in *M* (which has to use only a finite subset of *T* in *M*, since *M*, seen itself as a formal system, supports only finite proofs) into a proof in *O*.

The key point is however that this transformation of a proof in *M* into a proof in *O* is done in *M* itself, and, within *M* itself, the only way to extract information out of a proof of validity is by instantiating the free symbols of the interpretation of *A* in *M* by actual function and predicate symbols of *M*, i.e. by producing what at the end is a model, i.e. a domain, functions and predicates actually definable in *M*.

**1.6. The computational content of completeness proofs for intuitionistic logic.** It is known that composing the soundness and completeness theorems for propositional or predicate logic gives a cut-elimination theorem, as soon as completeness is formulated in such a way that it produces a normal proof<fnref n="9" />. Now, if the proofs of soundness and completeness are formalised in a metalanguage equipped with a normalisation procedure, e.g. in a λ-calculus-based proofs-as-programs presentation of second-order arithmetic [62, 64, Ch. 9], one gets an effective cut-elimination theorem, namely an effective procedure which turns any non-necessarily-normal proof of Γ ⊢ A into a normal proof of Γ ⊢ A.

In the context of intuitionistic provability, this has been explored abundantly under the name of semantic normalisation, or normalisation by evaluation. Initially based on ideas from Berger and Schwichtenberg [10] in the context of simply-typed λ-calculus, it was studied for the realisability semantics of second-order implicative propositional logic<fnref n="10" /> by Altenkirch, Hofmann and Streicher [3], for the realisability semantics of implicative propositional logic in Hilbert style<fnref n="11" /> by Coquand and Dybjer [20], for the Kripke semantics of implicative propositional logic in natural deduction style<fnref n="12" /> by C. Coquand [19], for Heyting algebras by Hermant and Lipton [44, 45], etc. It has also been applied to phase semantics of linear logic by Okada [71]. It also connects to a normalisation technique in computer science called Typed-Directed Partial Evaluation (TDPE) [23].

Let us recall how this approach works in the case of minimal implicative propositional logic (Figure 1) using soundness and completeness with respect to Kripke models [19]. Let $\mathcal{K}$ range over Kripke models $(\mathcal{W}, \leq, \vdash_X)$ where $\leq$ is a preorder on $\mathcal{W}$ and $\vdash_X$ a monotonic predicate over $\mathcal{W}$ for each propositional atom $X$. Let $w$ range over $\mathcal{W}$, i.e. worlds in the corresponding Kripke models. Let us write $w \Vdash_{\mathcal{K}} A$ (resp. $w \Vdash_{\mathcal{K}} \Gamma$) for truth of $A$ (resp. for the conjunction of the truth of all formulae in $\Gamma$) at world $w$ in the Kripke model $\mathcal{K}$. In particular, $w \Vdash_{\mathcal{K}} A$ is extended from atoms to all formulae by defining $w \Vdash_{\mathcal{K}} A \Rightarrow B \triangleq \forall w' (w' \ge w \Rightarrow w' \Vdash_{\mathcal{K}} A \Rightarrow w' \Vdash_{\mathcal{K}} B)$. Let us write $\Gamma \vdash_I A$ for the validity of $A$ relative to $\Gamma$ at all worlds of all Kripke models, i.e. for the formula $\forall \mathcal{K} \forall w (w \Vdash_{\mathcal{K}} \Gamma \Rightarrow w \Vdash_{\mathcal{K}} A)$.

The metalanguage being here a λ-calculus, we shall write its proofs as mathematical functions. We write $x \mapsto t$ for the proof of an implication as well as for the proof of a

<footnote n="9">⁹Using e.g. Beth-Hintikka-Kanger-Schütte's proof.</footnote>

<footnote n="10">¹⁰I.e., Girard-Reynolds System *F*.</footnote>

<footnote n="11">¹¹I.e., equivalently, simply-typed combinatory logic.</footnote>

<footnote n="12">¹²I.e., equivalently, simply-typed λ-calculus.</footnote>
universal quantification, possibly also writing (x : A) ↦→ t to make explicit that x is the name of a proof of A. We shall represent modus ponens and instantiation of universal quantification by function application, written *tu*. We shall use the notation () for the canonical proof of a nullary conjunction and the notation (t, u) for the proof of a binary conjunction, seen as a product type and obtained by taking the pair of the proofs of the components of the conjunction. To give a name *f* to the proof of a statement of the form ∀x₁, ..., xₙ (A ⇒ B) we shall use the notation f<sup>x₁,...,xₙ</sup>(a : A) : B followed by clauses of the form f<sup>x₁,...,xₙ</sup>(a) ≜ t (for readability, we may also write some of the xᵢ as subscripts rather than superscripts of *f*).

For instance, the proof that Kripke forcing is monotone, i.e. that ∀ww' (w' ≥ w ∧ w ⊩ A ⇒ w' ⊩ A), can be written as the following function ⪑<sub>A</sub>, recursive in the structure of A, taking as arguments two worlds w and w':

$$
\begin{align*}
\hat{\Gamma}_{A}^{w,w'} & : \quad w' \ge w \quad \wedge \quad w \vdash A & \Rightarrow & w' \vdash A \\
\hat{\Gamma}_{X}^{w,w'} & (h \quad , \quad m \quad ) & \triangleq & p_X(h, m) \\
\hat{\Gamma}_{A \Rightarrow B}^{w,w'} & (h \quad , \quad m \quad ) & \triangleq & w'' \mapsto (h' : w'' \ge w') \mapsto m w'' (\mathit{trans}(h, h'))
\end{align*}
$$

where $p_X$ is the proof of monotonicity of $\vdash_X$ and $\mathit{trans}$ is the proof of transitivity of $\ge$,
both coming with the definition of Kripke models, while, in the definition, $h$ is a proof
of $w' \ge w$ and $m$ a proof of $w \vdash A$.

Similarly, the extension of $\Uparrow$ to a proof that forcing of contexts is monotone can be
written as follows, where we reuse the notation $\Uparrow$, now with a context as index, to denote
a proof of $\forall ww'(w' \ge w \wedge w \vdash \Gamma \Rightarrow w' \vdash \Gamma)$:

$$
\begin{align*}
\hat{\Gamma}^{w,w'} & : \quad w' \ge w \quad \wedge \quad w \Vdash \Gamma & \Rightarrow & w' \Vdash \Gamma \\
\hat{\Gamma}^{\epsilon,w'} & (h \quad , \quad , \quad ) & \triangleq & (\epsilon) \\
\hat{\Gamma}^{w,w'}_{A} & (h \quad , \quad , \quad ) & \triangleq & (\hat{\Gamma}^{w,w'}_{A} (h, \sigma), \hat{\Gamma}^{w,w'}_{A} (h, m))
\end{align*}
$$

Let us write Γ ⊢<sub>I</sub> A for intuitionistic provability. Let us consider the canonical proof soundness<sub>A</sub><sup>Γ</sup> of (Γ ⊢<sub>I</sub> A) ⇒ (Γ ⊢<sub>I</sub> A) proved by induction on the derivation of Γ ⊢<sub>I</sub> A. We write the proof as a recursive function, recursively on the structure of formulae:

$$
\begin{align*}
soundness_A^\Gamma : \quad & \Gamma \vdash_I A && \Rightarrow \quad \Gamma \vdash_I A \\
soundness_A^\Gamma : \quad & \dot{ax}_i && \triangleq \quad \mathcal{K} \mapsto w \mapsto \sigma \mapsto \sigma(i) \\
soundness_{A \Rightarrow B}^\Gamma : \quad & \text{abs}(p) && \triangleq \quad \mathcal{K} \mapsto w \mapsto \sigma \mapsto w' \mapsto (h : w \le w') \mapsto m \mapsto \\
& & && \text{soundness}_B^{\Gamma,A} : \quad p \mathcal{K} w' (\hat{\Gamma}^{w,w'} (h, \sigma), m) \\
soundness_B^\Gamma : \quad & a \ddot{p}(p, q) && \triangleq \quad \mathcal{K} \mapsto w \mapsto \sigma \mapsto \\
& & && (\text{soundness}_{A \Rightarrow B}^\Gamma : p \mathcal{K} w \sigma) \text{ w refl } (\text{soundness}_A^\Gamma : q \mathcal{K} w \sigma)
\end{align*}
$$

where *u* is a proof of Γ ⊢<sub>*I*</sub> A in the last line, *a*pp, *a*bs, *ā*xᵢ are the name of inference rules defining object-level implicational propositional logic in a natural deduction style (see Figure 1); σ(i) is the (i + 1)th component of σ starting from the right, and *refl* is the proof of reflexivity of ≥ coming with the definition of Kripke models.

Let us also consider the following somehow canonical proof of cut-free completeness,
completeness : (Γ ⊢<sub>I</sub> A) ⇒ (Γ ⊢<sub>I</sub><sup>cf</sup> A). It is based on the universal model of context K<sub>0</sub>
defined by taking for W the set of contexts Γ ordered by inclusion and Γ ⊢<sub>I</sub><sup>cf</sup> X for
the forcing ⊩<sub>X</sub> of atom X at world Γ. Now, the proof proceeds by showing the two
directions of Γ ⊩<sub>K<sub>0</sub></sub> A ⇔ Γ ⊢<sub>I</sub><sup>cf</sup> A by mutual induction on A. It is common to write ↓
for the left-to-right direction (called reify, or quote) and ↑ for the right-to-left direction
Primitive rules

$$ \frac{|\Gamma'| = i}{\Gamma, A, \Gamma' \vdash_I A} \quad \frac{\Gamma \vdash_I A \Rightarrow B \qquad \Gamma \vdash_I A}{\Gamma \vdash_I B} \quad \frac{a \dot{p} p}{a \dot{p} p} \quad \frac{\Gamma, A \vdash_I B}{\Gamma \vdash_I A \Rightarrow B} \quad \frac{}{a \dot{s} s} $$

Admissible rule

$$ \frac{\Gamma \subset \Gamma' \qquad \Gamma \vdash_I A}{\Gamma' \vdash_I A} \qquad \textit{weak} $$

<caption>FIGURE 1. Inference rules characterising minimal implicational logic</caption>

(called *reflect*, or *eval*):

$$
\begin{array}{lclcl}
\downarrow_A^\Gamma : & \Gamma \Vdash_K_0 A & \Rightarrow & \Gamma \Vdash_I^{cf} A \\
\downarrow_P^\Gamma : & m & \triangleq & m \\
\downarrow_{A \Rightarrow B}^\Gamma : & m & \triangleq & a \dot{s} s (\downarrow_B^{\Gamma,A} (m (\Gamma, A) \textit{inj}_\Gamma^A (\uparrow_A^{\Gamma,A} \dot{x}_0))) \\
\uparrow_A^\Gamma : & \Gamma \Vdash_I^{cf} A & \Rightarrow & \Gamma \Vdash_K_0 A \\
\uparrow_P^\Gamma : & p & \triangleq & p \\
\uparrow_{A \Rightarrow B}^\Gamma : & p & \triangleq & \Gamma' \mapsto f \mapsto m \mapsto \uparrow_B^\Gamma (a \dot{p} p (\textit{weak}(f, p), \downarrow_A^{\Gamma'} m)) \\
\textit{init}_{\Gamma'}^\Gamma : & & \Rightarrow & \Gamma \Vdash_K_0 \Gamma' \\
\textit{init}_\epsilon^\Gamma : & & \triangleq & () \\
\textit{init}_{\Gamma', A}^\Gamma : & & \triangleq & (\textit{init}_{\Gamma'}^\Gamma, \uparrow_A^\Gamma (\dot{x}_{|\Gamma|-|\Gamma', A|})) \\
\textit{completeness}_A^\Gamma : & \Gamma \Vdash_I A & \Rightarrow & \Gamma \Vdash_I^{cf} A \\
\textit{completeness}_A^\Gamma : & m & \triangleq & \downarrow_A^\Gamma (m K_0 \Gamma \textit{init}_\Gamma^\Gamma)
\end{array}
$$

where $|\Gamma|$ is the length of $\Gamma$, weak is the admissible rule of weakening in object-level implicational propositional logic and $inj_\Gamma^A$ is a proof of $\Gamma \subset \Gamma, A$.

In particular, by placing ourselves in a metametalanguage, such that the metalanguage is seen as a proofs-as-programs-style natural deduction object language, i.e. as a typed $\lambda$-calculus, one would be able to show that

* for every given proof of $\Gamma \vdash_I A$, soundness produces, by normalisation of the metalanguage<fnref n="13" />, a proof of $\Gamma \Vdash_I A$ whose structure follows the one of the proof of $\Gamma \vdash_I A$;

* for every proof of validity taken in canonical form (i.e. as a closed $\beta$-normal $\eta$-long $\lambda$-term of type $\Gamma \Vdash A$ in the metalanguage), the resulting proof of $\Gamma \vdash_I^{cf} A$ obtained by completeness is, by normalisation in the metalanguage, the same $\lambda$-term with the abstractions and applications over $K$, $w$ and proofs of $w \le w'$ removed.

On the other side, if our proofs-as-programs-based metalanguage is able to state properties of its proofs (as is the case for instance of Martin-Löf's style type theories [69]),

<footnote n="13">¹³Typically proved by embedding in another language assumed to be consistent.</footnote>
it can be shown within the metalanguage itself that the composition of completeness and soundness produces normal forms. This is what C. Coquand did by showing that the above proofs of soundness and completeness, seen as typed programs, satisfy the following properties:

$$ \forall p : (\Gamma \vdash_I A) p \sim \text{soundness}_A^\Gamma p \mathcal{K}_0 \Gamma \text{init}_\Gamma^\Gamma \forall p : (\Gamma \vdash_I A) \forall m : (\Gamma \vdash_I A) (p \sim m \mathcal{K}_0 \Gamma \text{init}_\Gamma^\Gamma) \Rightarrow p =_{\beta\eta} \text{completeness}_A^\Gamma m $$

where $\sim$ is an appropriate “Tait computability” relation between object proofs and semantic proofs expressing that soundness $p$ reflects $p$.

Then, since completeness returns normal forms, we get that the composite function completeness (soundness $p$) evaluates to a normal form $q$ such that $q =_{\beta} p$.

Let us conclude this section by saying that the extension of this proof to universal quantification and falsity, using so-called exploding nodes, has been studied e.g. in [43]. The extension to first-order classical logic has been studied e.g. in [53]. The case of disjunction and existential quantification is typically addressed using variants of Kripke semantics [52], Beth models, topological models [22], or various alternative semantics (e.g. [1, 2, 71, 74]).

One of the purposes of this paper is precisely to start a comparative exploration of the computational contents of proofs of Gödel’s completeness theorem and of the question of whether they provide a normalisation procedure. In the case of Henkin’s proof, the answer is negative: even if the resulting object-level proof that will be constructively obtained in Section 2 is related to the proof of validity in the meta-logic, it is neither cut-free nor isomorphic to it. In particular, it drops information from the validity proof by sharing subparts that prove the same subformula as will be emphasised in Section 2.2.

**1.7. The intuitionistic provability of the different statements of completeness.**
Statements C1, C2 and C3, as well as statements S1, S2, S3 are classically equivalent but not intuitionistically equivalent. In particular, only C2 and S2 are intuitionistically provable.

More precisely, since our object language has only negative connectives, the formula $M \vdash_T \mathcal{T}$ is in turn composed of only negative connectives in the metalanguage. Hence, the only positive connective in the statements C2 and S2 is the existential quantifier asserting the existence of a model.

This existential quantifier is intuitionistically provable as our formulation of Henkin’s proof of S2 given in the next section shows: given a proof of consistency of a theory, we can produce a syntactic model in the form of a specific predicate. It shall however be noted that this predicate is not itself recursive in general, since constructing this model is in general equivalent to producing an infinite path in any arbitrary infinite binary tree (such an infinite path is a priori not recursive, see Kleene [59], Simpson [78]).

Otherwise, from an intuitionistic point of view, statements C1 and S1 are particularly interesting, as they promise to produce (object) proofs in the object language out of proofs of validity in the metalanguage. However, Kreisel [60] showed, using a result by Gödel [37], that C1 is equivalent to Markov’s principle over intuitionistic second-order arithmetic. This has been studied in depth by McCarty [70] and it turns out that S1 is actually equivalent to Markov’s principle if the theory is recursively enumerable.

However, for arbitrary theories, reasoning by contradiction on formulae of arbitrarily large logical complexity is in general needed as the following adaptation of McCarty’s proof shows: Let $\mathcal{A}$ be an arbitrary formula of the metalanguage and consider e.g. the theory defined by $B \in \mathcal{T} \triangleq (B = \dot{=} ) \wedge \mathcal{A} \vee (B = X) \wedge \neg \mathcal{A}$ for $X$ a distinct propositional
atom of the object language. We intuitionistically have that $\mathcal{T} \models X$ because this is a negative formulation of a classically provable statement<fnref n="14" />. By completeness, we get $\mathcal{T} \vdash X$, and, by case analysis on the normal form of the so-obtained proof, we infer that either $\mathcal{A}$ or $\neg \mathcal{A}$.

The need for Markov's principle is connected to how $\perp$ is interpreted in the model. Krivine [66] showed that for a language without $\perp$<fnref n="15" />, C1 is provable intuitionistically. As analysed by Berardi [7] and Berardi and Valentini [8], Markov's principle is not needed anymore if we additionally accept the degenerate model where all formulae including $\perp$ are interpreted as true<fnref n="16" />. Let us formalise this precisely.

We define a possibly-exploding model $\mathcal{M}$ to be a model<fnref n="17" /> $(\mathcal{D}, \mathcal{F}, \mathcal{P}, \mathcal{A}_{\perp})$ such that $(\mathcal{D}, \mathcal{F}, \mathcal{P})$ is a model in the previous sense and $\mathcal{A}_{\perp}$ a fixed formula intended to interpret $\perp$. The definition of truth is then modified as follows:

$$ \mathcal{M} \Vdash_{\sigma} \perp \quad \triangleq \quad \mathcal{A}_{\perp} $$

with the rest of clauses unchanged<fnref n="18" />

Note that because $\perp \Rightarrow A$ is a consequence of $\vdash\vdash A \Rightarrow A$, the following holds for all $A$ and all $\sigma$ in any classical possibly-exploding model:

$$ \mathcal{A}_{\perp} \Rightarrow \mathcal{M} \Vdash_{\sigma} A, $$

so we do not need to further enforce it<fnref n="19" />. Let us rephrase C1 and S1 using classical possibly-exploding models:

$$ C1'. \quad \Vdash^e A \Rightarrow \vdash A $$

$$ S1'. \quad \mathcal{T} \Vdash^e A \Rightarrow \mathcal{T} \vdash A $$

<footnote n="14">¹⁴Let $\mathcal{M}$ and $\sigma$ such that $\mathcal{M} \Vdash_{\sigma} \mathcal{T}$. We first show $\neg \mathcal{A}$. Indeed, if $\mathcal{A}$ holds, then $\perp \in \mathcal{T}$ and we get by $\mathcal{M} \Vdash_{\sigma} \mathcal{T}$ that the model is contradictory. But if $\neg \mathcal{A}$, then $X \in \mathcal{T}$, hence $\mathcal{M} \Vdash_{\sigma} X$.</footnote>

<footnote n="15">¹⁵So-called minimal classical logic in [4], which is however not functionally complete since no formula can represent the always-false function.</footnote>

<footnote n="16">¹⁶This is similar to the approach followed by Friedman [32] and Veldman [84] to intuitionistically prove the completeness of intuitionistic logic with respect to a relaxing of Beth models with so-called fallible models, and to a relaxing of Kripke models with so-called exploding nodes, respectively.</footnote>

<footnote n="17">¹⁷Such model is also called intuitionistic structure in Krivsov [67].</footnote>

<footnote n="18">¹⁸In [8], a classical possibly-exploding model is called a minimal model, in reference to minimal logic [56]. The difference between non-exploding models and possibly-exploding models can actually be interpreted from the point of view of linear logic not as a difference of definition of models but as a difference of interpretations of the false connective. An non-exploding model is a model where the false connective is interpreted as the connective $\perp$ of linear logic (a positive connective, neutral for the standard disjunction and with no introduction rule). A possibly-exploding model is a model where the false connective is interpreted as the connective $\perp$ of linear logic (a negative connective informally standing for an empty sequent). See e.g. Okada [71] or Sambin [74] for examples of differences of interpretation of $\perp$ and $\perp$ in completeness proofs for linear logic.</footnote>

<footnote n="19">¹⁹As a matter of purity, since it is standard that the classical scheme $\vdash\vdash A \Rightarrow A$ is equivalent to the conjunction of a purely classical part, namely Peirce's law representing the scheme $((A \Rightarrow B) \Rightarrow A) \Rightarrow B$ and of a purely intuitionistic part, namely ex falso quodlibet representing the scheme $\perp \Rightarrow A$, we could have decomposed *Classic* into the union of *Peirce* $\triangleq \{(A \Rightarrow B) \Rightarrow A\} \Rightarrow A \mid A \in \mathcal{Form}$ and of *Exfalso* $\triangleq \{\perp \Rightarrow A \mid A \in \mathcal{Form}\}$.</footnote>

<footnote>As already said in Section 1.4, the condition $\mathcal{M} \Vdash_{\sigma} \mathcal{Classic}$, and in particular the conditions $\mathcal{M} \Vdash_{\sigma} \mathcal{Peirce}$ and $\mathcal{M} \Vdash_{\sigma} \mathcal{Exfalso}$ are needed to show soundness with respect to classical models in a minimal setting. In an intuitionistic setting, $\mathcal{M} \Vdash_{\sigma} \mathcal{Exfalso}$ holds by default and does not have to be explicitly enforced. In a classical setting, $\mathcal{M} \Vdash_{\sigma} \mathcal{Peirce}$ does not have to be explicitly enforced. So, requiring these conditions is to ensure that the definition of validity is the one we want independently of the specific properties of the metalanguage.</footnote>

<footnote>In contrast, for the purpose of completeness, possibly-exploding models are needed for an intuitionistic proof of C1 to be possible, but none of $\mathcal{Peirce}(\mathcal{M})$ and $\mathcal{Exfalso}(\mathcal{M})$ are required.</footnote>
where

$$ \mathcal{T} \Vdash^e A \triangleq \forall M \forall \sigma (M \Vdash_{\sigma}^{e} \mathit{Classic} \Rightarrow M \Vdash_{\sigma}^{e} \mathcal{T} \Rightarrow M \Vdash_{\sigma}^{e} A) $$

In particular, it is worthwhile to notice that $\mathcal{T} \Vdash^e A$ and $\mathcal{T} \Vdash A$ are classically equivalent since, up to logical equivalence, $\Vdash^e$ only differs from $\Vdash$ by an extra quantification over the degenerate always-true model. Hence C1 and C1', as well as S1 and S1', are classically equivalent too. But C1' as well as S1' are intuitionistically provable for recursively enumerable theories, while C1 and S1, even for recursively enumerable theories, would require Markov's principle<fnref n="20" />.

Let us conclude this section by considering C3 and S3. These statements are not intuitionistically provable: if they were, provability could be decided. This does not mean however that we cannot compute with C3 and S3. Classical logic is computational (see e.g. [72]), but for an evaluation to be possible, an interaction with a proof of a statement which uses C3 or S3 is needed. The formalisation by Blanchette, Popescu and Traytel [12] might be a good starting point to analyse the proof but we will not explore this further here.

**1.8. Chronology and recent related works.** The extraction of a computational content from Henkin's proof was obtained by the authors from an analysis of the formalisation [50] in the Coq proof assistant [17] of Henkin's proof. It was first presented at the TYPES conference in Warsaw, 2010. The paper was essentially written in 2013 but it remained in draft and unstable form until 2016. A non-peer-reviewed version was made publicly available on the web page of the first author late 2016 and slightly updated in 2019. Our constructive presentation of Henkin's proof inspired Forster, Kirst and Wehr to formalise the completeness theorem in the intuitionistic setting of Coq [28, 29]. This encouraged us in 2022 to polish the paper one step further with the objective of a sub-mission.

A new version was made public on the web page of the first author in November 2022 together with an implementation<fnref n="21" /> of the proof in the OCaml programming language. The new version presented the proof in a more structured way and made explicit the need for a weakening rule left unaddressed in the 2016 version. It also provided an extension of the proof to the disjunction conjunctive, relying on (a slight generalisation of) the weakly classical principle of Double Negation Shift (DNS). Finally, the current and last version includes the extra result that completeness in the presence of disjunction requires at least a variant of a weak form of Double Negation Shift that Kirst recently identified [58].

Various investigations of Gödel's completeness in an intuitionistic setting have been published since our proof was first presented. To our knowledge, in addition to [28, 29, 58], this includes papers by Krivtsov [68] in intuitionistic arithmetic and Espíndola [24, 25] in intuitionistic set theory (IZF). Their results are discussed in the section 2.6.

**§2. The computational content of Henkin's proof of Gödel's completeness.** We now recall Henkin's proof of completeness and analyse its computational content.

<footnote n="20">²⁰Markov's principle can actually be "intuitionistically" implemented e.g. by using an exception mechanism [42], so a computational content to weak completeness and strong completeness for recursively enumerable theories could as well be obtained without any change to the interpretation of $\perp$.</footnote>

<footnote n="21">²¹http://herbelin.xyz/articles/henkin.ml</footnote>
**2.1. Henkin's proof, slightly simplified.** We give a simplified form of Henkin's proof of the strong form of Gödel's completeness theorem [40], formulated as a model existence theorem, that is as statement S2. The simplification is on the use of free variables instead of constants in Henkin axioms and in the use of only implicative formulae in the process of completion of a consistent set of formulae into a maximally consistent one<fnref n="22" />.

Let $\mathcal{T}$ be a consistent set of formulae mentioning an at most countable<fnref n="23" /> number of function symbols and predicate symbols. Let $X_1$ and $X_2$ be countable sets of variables forming a partition of $\mathcal{X}$. We can assume without loss of generality that the free variables of the formulae in $\mathcal{T}$ are in $X_1$ leaving $X_2$ as a pool of fresh variables.

We want to show that $\mathcal{T}$ has a model, and for that purpose, we shall complete it into a consistent set $S_\omega$ of formulae which is maximal in the sense that if $A \notin S_\omega$ then $\Vdash A \in S_\omega$. We shall also ensure that for every universally quantified formula $\forall x A(x)$, there is a corresponding so-called Henkin axiom $A(y) \Rightarrow \forall x A(x)$ in $S_\omega$ with y fresh in $\forall x A(x)$. For the purpose of this construction, we fix an injective enumeration $\phi$ of formulae of the form $\forall x A(x)$ or $A \Rightarrow B$ and write $\lceil A \rceil$ for the index of a formula A of such form in the enumeration. We also take $\phi$ so that formulae of even index are of the form $\forall x A(x)$ and formulae of odd index are of the form $A \Rightarrow B$.

Let $S_0$ be $\mathcal{T}$ and assume that we have already built $S_n$. If $n$ is even, $\phi(n)$ has the form $\forall x A(x)$. We then consider a variable $x_{n/2} \in X_2$ which is fresh in all $\phi(i)$ for $i \le n$ and we set $S_{n+1} \triangleq S_n \cup (A(x_{n/2}) \Rightarrow \forall x A(x))$. Otherwise, $\phi(n)$ is an implicative formula and we consider two cases. If $S_n \cup \phi(n)$ is consistent, i.e., if $(S_n \cup \phi(n) \vdash \bot) \Rightarrow \bot$, we set $S_{n+1} \triangleq S_n \cup \phi(n)$. Otherwise, we set $S_{n+1} \triangleq S_n$. We finally define the predicate $A \in S_\omega \triangleq \exists n (S_n \vdash A)$, i.e. $\exists n \exists \Gamma \subset S_n (\Gamma \vdash A)$, and this is the basis of a syntactic model $M_0$ defined by taking

$$ \begin{array}{lclcl} \mathcal{D} & \triangleq & \mathcal{Term} & & \\ \mathcal{F}(f)(t_1, \dots, t_n) & \triangleq & f(t_1, \dots, t_n) & & \\ \mathcal{P}(P)(t_1, \dots, t_n) & \triangleq & P(t_1, \dots, t_n) \in S_\omega & & \\ \end{array} $$

By induction, each $S_n$ is consistent. Indeed, if $\phi(n)$ is implicative and $S_{n+1} \equiv S_n \cup \phi(n)$, it is precisely because $S_{n+1}$ is consistent. Otherwise, the consistency of $S_{n+1}$ comes from the consistency of $S_n$. If $\phi(n)$ is some $\forall x A(x)$, then $S_{n+1} \equiv S_n \cup (A(x_{n/2}) \Rightarrow \forall x A(x))$. This is consistent by freshness of $x_{n/2}$ in both $\mathcal{T}$ and in the $\phi(i)$ for $i \le n$. Indeed, because $x_{n/2}$ is fresh, any proof of $S_n \cup (A(x_{n/2}) \Rightarrow \forall x A(x)) \vdash \bot$ can be turned into a proof of $S_n \cup \Vdash \forall y \Vdash (A(y) \Rightarrow \forall x A(x)) \vdash \bot$, which itself can be turned into a proof of $S_n \vdash \bot$ since $\Vdash \forall y \Vdash (A(y) \Rightarrow \forall x A(x))$ is a classical tautology<fnref n="24" />

Let $A$ be a formula and $\sigma$ a substitution of its free variables. We now show by induction on the logical depth<fnref n="25" /> of $A$ that $M_0 \Vdash_{\sigma} A \Leftrightarrow A[\sigma] \in S_\omega$, where $A[\sigma]$ denotes the

<footnote n="22">²²Smullyan [79] credits Hasenjaeger [39] and Henkin independently for proof variants using free variables (see also Henkin [41]). In particular, this allows to build a maximal consistent theory in one step instead of a countable number of steps as in Henkin's original proof. See also [78, Th. IV.3.3] for a proof building a maximal consistent theory in one step.</footnote>

<footnote n="23">²³In the presence of uncountably many symbols, one would need the ultrafilter theorem to build the model and this would require extra computational tools to make the proof constructive. See [55] for the equivalence in set theory between the ultrafilter theorem and the completeness theorem on non-necessarily countable signatures.</footnote>

<footnote n="24">²⁴The famous “Drinker Paradox”.</footnote>

<footnote n="25">²⁵In particular, we consider $B(t)$ to be smaller to $\forall x B(x)$ for any $t$.</footnote>
result of substituting the free variables of A by the terms in $\sigma$. This is sometimes considered an easy combinatoric argument but we shall detail the proof because it is here that the computational content of the proof is non-trivial. Moreover, we do not closely follow Henkin's proof who is making strong use of classical reasoning. We shall instead reason intuitionistically, which does not raise any practical difficulty here.

* Let us focus first on the case when $A \models B \rightarrow C$. One way to show $B[\sigma] \models C[\sigma] \in S_{\omega}$ from $M_0 \models_{\sigma} B \rightarrow C$ is to show that for $n$ being $[B[\sigma] \rightarrow C[\sigma]]$, the set $S_n \cup B[\sigma] \rightarrow C[\sigma]$ is consistent, i.e. that a contradiction arises from $S_n \cup B[\sigma] \rightarrow C[\sigma] \vdash \perp$. Indeed, from the latter, we get both $S_n \vdash B[\sigma]$ and $S_n \vdash \neg C[\sigma]$. From $S_n \vdash B[\sigma]$ we get $M_0 \models_{\sigma} B$ by induction hypothesis, hence $M_0 \models_{\sigma} C$ by assumption on the truth of $B \rightarrow C$. Then $C[\sigma] \in S_{\omega}$ again by induction hypothesis, hence $S_{n'} \vdash C[\sigma]$ for some $n'$. But also $S_n \vdash \neg C[\sigma]$, hence $S_{max(n,n')} \vdash \perp$ which contradicts the consistency of $S_{max(n,n')}$.

* Conversely, if $B[\sigma] \models C[\sigma] \in S_{\omega}$, this means $S_n \vdash B[\sigma] \models C[\sigma]$ for some $n$. To prove $M_0 \models_{\sigma} B \rightarrow C$, let us assume $M_0 \models_{\sigma} B$. By induction hypothesis we get $S_{n'} \vdash B[\sigma]$ for some $n'$ and hence $S_{max(n,n')} \vdash C[\sigma]$, i.e. $C[\sigma] \in S_{\omega}$. We conclude by induction hypothesis to get $M_0 \models_{\sigma} C$.

* Let us then focus on the case when $A$ is $\forall x B$. For $n$ even being $[\forall x B)[\sigma]$, we have $(B[\sigma, x \leftarrow x_{n/2}] \rightarrow (\forall x B)[\sigma]) \in S_{n+1}$. From $M_0 \models_{\sigma} \forall x B(x)$ we get $M_0 \models_{\sigma, x \leftarrow x_{n/2}} B(x)$ and by the induction hypothesis we then get the existence of some $n'$ such that $S_{n'} \vdash B[\sigma, x \leftarrow x_{n/2}]$. Hence, $S_{max(n+1, n')} \vdash (\forall x B)[\sigma]$, which means $(\forall x B)[\sigma] \in S_{\omega}$.

* Conversely, assume $S_n \vdash (\forall x B)[\sigma]$ for some $n$ and prove $M_0 \models_{\sigma} \forall x B$. Let $t$ be a term. From $S_n \vdash (\forall x B)[\sigma]$ we get $S_n \vdash B[\sigma, x \leftarrow t]$, hence, by induction hypothesis, $M_0 \models_{\sigma, x \leftarrow t} B(x)$.

* Let us then consider the case $A \perp$. By ex falso quodlibet in the metalanguage, it is direct that $\perp \Rightarrow (\perp \in S_{\omega})$.

* Conversely, let us prove $(\perp \in S_{\omega}) \Rightarrow \perp$. From $\perp \in S_{\omega}$ we know $S_n \vdash \perp$ for some $n$ which, again, contradicts the consistency of $S_n$.

* The case when $A$ is $P(t_1, \dots, t_n)$ is by definition.

Before completing the proof, it remains to prove that the model is classical. Using the equivalence between $M_0 \models_{id} A$ and $A \in S_{\omega}$ for $A$ closed and $id$ the empty substitution, it is enough to prove that $\vdash A \in S_{\omega}$ implies $A \in S_{\omega}$. But the former means $S_n \vdash \vdash A$ for some $n$, hence $S_n \vdash A$ by classical reasoning in the object language, hence $A \in S_{\omega}$.

We are now ready to complete the proof: for every $B \in \mathcal{T}$, since $\mathcal{T} \vdash B$, we get $B \in S_{\omega}$ and hence $M_0 \models_{id} B$.

## 2.2. From Henkin's proof to a proof with respect to possibly-exploding models.

Let us fix a formula $A_0$ and a recursively enumerable theory $\mathcal{T}_0$, i.e. a theory defined by a $\Sigma_1$-statement. To get a proof of statement S1 for $\mathcal{T}_0$ and $A_0$ is easy by using Markov's principle: to prove $\mathcal{T}_0 \vdash A_0$ from $\mathcal{T}_0 \models A_0$, let us assume the contrary, namely that $\mathcal{T}_0 \cup \vdash A_0$ is consistent. Then, we can complete $S_0 \triangleq \mathcal{T}_0 \cup \vdash A_0$ into $S_{\omega}$ and build out of it a classical model $M_0$ such that $\forall B \in \mathcal{T}_0 M_0 \models_{id} B$ as well as $M_0 \models_{id} \vdash A_0$, i.e. $\neg(M_0 \models_{id} A_0)$. But this contradicts $\mathcal{T}_0 \models A_0$ and, because $\mathcal{T}_0$ is $\Sigma_1^0$, hence $\mathcal{T}_0 \vdash A$ as well, Markov's principle applies.

As discussed in Section 1.7, S1 cannot be proved without Markov's principle, so we shall instead prove S1'. To turn the proof of S2 into a proof of S1' which does not
require reasoning by contradiction, we shall slightly change the construction of $S_\omega$ from $\mathcal{T}_0 \cup \dashv A_0$ so that it is not consistent in an absolute sense, but instead consistent relative to $\mathcal{T}_0 \cup \dashv A_0$. In particular, we change the condition for extending $S_{2n+1}$ with $\phi(2n+1)$ to be that $S_{2n+1} \cup \phi(2n+1)$ is consistent relative to $\mathcal{T}_0 \cup \dashv A_0$.

Then, we show by induction not that $S_n$ is consistent but that its inconsistency reduces to the inconsistency of $\mathcal{T}_0 \cup \dashv A_0$.

For the construction of the now possibly-exploding model, we take as interpretation of $\perp$ the formula $\mathcal{T}_0, \dashv A_0 \vdash \perp$. Proving $\perp \in S_\omega \Rightarrow M_0 \models_\sigma^e \perp$ now reduces to proving $S_n \vdash \perp \Rightarrow \mathcal{T}_0, \dashv A_0 \vdash \perp$ which is the statement of relative consistency$^{26}$. Conversely, $M_0 \models_\sigma^e \perp \Rightarrow \perp \in S_\omega$ now comes by definition of $S_0$.

The change in the definition of $S_\omega$ as well as the use of possibly-exploding models is connected to Friedman's A-translation [33] being able to turn Markov's principle into an admissible rule. Here, A is the $\Sigma_1^0$-formula $\mathcal{T}_0 \vdash A_0$ and by replacing $\perp$ with A in the definition of model, hence of validity, as well as in the definition of $S_\omega$, we are able to prove ($A \Rightarrow A \Rightarrow A$ whereas only ($A \Rightarrow \perp$) $\Rightarrow \perp$ was otherwise provable. Then, A comes trivially from ($A \Rightarrow A \Rightarrow A$).

This was the idea followed by Krivine [66] in his constructive proof of Gödel's theorem for a language restricted to $\Rightarrow$ and $\dot{\forall}$, as analysed and clarified in Berardi and Valentini [8].

As a final remark, one could wonder whether the construction of $S_{2n+2}$ by case on an undecidable statement is compatible with intuitionistic reasoning. Indeed, constructing the sequence of formulae added to $\mathcal{T}_0 \cup \dashv A_0$ in order to get $S_n$ seems to require a use of excluded-middle. However, in the proof of completeness, only the property $A \in S_n$ matters, and this property is directly definable by induction as

$$A \in S_0 \quad \triangleq \quad A \in \mathcal{T}_0 \cup \dashv A_0$$

$$A \in S_{n+1} \quad \triangleq \quad A \in S_n$$

$$\vee (\exists p (n = 2p + 1) \wedge \phi(n) = \dot{\forall} x B(x) \wedge A = (B(x_{p+1}) \Rightarrow \dot{\forall} x B(x))$$

$$\vee (\exists p (n = 2p) \wedge (S_n, A \vdash \perp \Rightarrow \mathcal{T}_0, \dashv A_0 \vdash \perp) \wedge A = \phi(n))$$

Note however that $S_n$ is used in negative position of an implication in the definition of $S_{n+1}$. Hence, the complexity of the formula $A \in S_n$ seen as a type of functions is a type of higher-order functions of depth $n$.

**2.3. The computational content of the proof of completeness.** We are now ready to formulate the proof as a program. We shall place ourselves in an axiom-free second-order intuitionistic arithmetic equipped with a proof-as-program interpretation$^{27}$, as already considered in Section 1.6. Additionally, we shall identify the construction of existentially quantified formulae and the construction of proofs of conjunctive formulae. For instance, we shall use the notation $(p_1, ..., p_n)$ for the proof of an $n$-ary combination of existential quantifiers and conjunctions. We shall also write dest $p$ as $(x_1, ..., x_n)$ in $q$

<footnote>$^{26}$Interestingly enough, since $\mathcal{T}_0 \vdash A$ effectively holds as soon as an effective proof of validity of A is given, the model we build is then the degenerate one in which all formulae are true.</footnote>

<footnote>$^{27}$A typical effective framework for that purpose would be a fragment of the Calculus of Inductive Constructions such as it is implemented in the Coq proof assistant [16], or Matita [5]. The Calculus of Inductive Constructions is an impredicative extension of Martin-Löf's type theory [69].</footnote>
for a proof obtained by decomposition of the proof *p* of an *n*-ary combination of existential quantifiers and conjunctions. We shall write *efq p* for a proof of *A* obtained by ex falso quodlibet from a proof *p* of *⊥*.

We shall use the letters $n, A, \Gamma, m, p, q, r, h, g, f, k$ and their variants to refer to natural numbers, formulae, contexts of formulae, proofs of truth, proofs of derivability in the object language, proofs of belonging to $S_\omega$, proofs of inconsistency from adding an implicative formula to $S_{2n+1}$, proofs of belonging to $\mathcal{T}_0$, proofs of inclusion in $\mathcal{T}_0$, proofs of inclusion in extensions of $\mathcal{T}_0$, proofs of relative consistency, respectively.

The key property is $A \in S_\omega$ which unfolds as $\exists n \exists \Gamma (\Gamma \subset S_n \wedge \Gamma \vdash A)$. Rather than defining $\Gamma \subset S_n$ from $A \in S_n$ and the latter by cases, we now directly take $\Gamma \subset S_n$ as our primitive concept, so that defining $A \in S_n$ is actually not needed anymore. Rephrasing the property that $S_n$ is inconsistent in terms of $\Gamma \subset S_n$ is easy: it is enough to tell that $\Gamma \vdash \bot$ for some $\Gamma \subset S_n$. In particular, we can write $S_n, A \vdash \bot$ to mean $\exists \Gamma (\Gamma \subset S_n \wedge \Gamma, A \vdash \bot)$.

We first define by cases the predicate $\Gamma \subset \mathcal{T}_0$:

$$ \frac{\Gamma \subset \mathcal{T}_0 \qquad A \in \mathcal{T}_0}{\epsilon \in \mathcal{T}_0} J_{base} \qquad \frac{\Gamma, A \subset \mathcal{T}_0}{\Gamma \subset \mathcal{T}_0} J_{cons} $$

Then, we can define $\Gamma \subset S_n$ by cases: a formula $B$ is allowed to occur in such $\Gamma$ either because it is in $\mathcal{T}_0$ (clause $J_{cons}$), or because it is an Henkin axiom added at step $2n$ (clause $I_\varphi$), or because it is an implication added at step $2n + 1$ together with a proof of relative consistency of $S_{n+1} \cup B$ with respect to $\mathcal{T}_0 \cup \dot{\vdash} A_0$ (clause $I_\Rightarrow$). Note that we enforce in all cases that at least $\dot{\vdash} A_0$ is in such $\Gamma$ (clause $I_0$) and that we can always skip adding a formula at some step of the construction (clause $I_S$). Formally, the definition is:

$$ \frac{\Gamma \subset \mathcal{T}_0}{\Gamma, \dot{\vdash} A_0 \subset S_0} I_0 \qquad \frac{\Gamma \subset S_n}{\Gamma \subset S_{n+1}} I_S \qquad \frac{\Gamma \subset S_{2n}}{\Gamma, A(x_n) \Rightarrow \dot{\forall} x A(x) \subset S_{2n+1}} I_\varphi $$

$$ \frac{\Gamma \subset S_{2n+1} \qquad S_{2n+1}, A \Rightarrow B \vdash \bot \Rightarrow \mathcal{T}_0, \dot{\vdash} A_0 \vdash \bot}{\Gamma, A \Rightarrow B \subset S_{2n+2}} I_\Rightarrow $$

where $\phi(2n)$ is $\dot{\forall} x A(x)$ in $I_\varphi$ and $\phi(2n + 1)$ is $A \Rightarrow B$ in $I_\Rightarrow$.

We now write as a program the proof that $S_\omega$ is consistent relative to $\mathcal{T}_0 \cup \dot{\vdash} A_0$, i.e. that $\bot \in S_\omega$ implies $\mathcal{T}_0, \dot{\vdash} A_0 \vdash \bot$. The latter expands to $\exists \Gamma (\Gamma \subset \mathcal{T}_0 \wedge \Gamma, \dot{\vdash} A_0 \vdash \bot)$ which we see as made of triples of the form $(\Gamma, g, p)$, with $\Gamma$ a context, $g$ a proof of $\Gamma \subset \mathcal{T}_0$ and $p$ a proof of $\Gamma'$, $\dot{\vdash} A_0 \vdash \bot$.

This proof, which we call *flush*<sub>*n*</sub>, takes as arguments a quadruple $(n, \Gamma, f, p)$ where $f$ is a proof of $\Gamma \subset S_n$ and $p$ proof of $\Gamma \vdash \bot$. It proceeds by cases on the proof of $\Gamma \subset S_n$. When extended at odd $n$, it works by calling the *continuation* justifying that adding the formula $\phi(2p + 1)$ preserves consistency, and, when extended at even $n$, by composing the resulting proof of inconsistency with a proof of the Drinker's paradox (*drinker*<sub>*y*</sub> is the proof which builds a proof of $\Gamma \vdash \bot$ from a proof of $\Gamma, A(y) \Rightarrow \dot{\forall} x A(x) \vdash \bot$, knowing
that $y$ does not occur in $\Gamma, \forall x A(x)$, see Figure 2).

$$
\begin{array}{lclcl}
\mathit{flush} : & \perp \in \mathcal{S}_{\omega} & \Rightarrow & \mathcal{T}_0, \dot{\to} A_0 \vdash \perp \\
\mathit{flush} & (0, (\Gamma, \dot{\to} A_0), I_0 g, p) & \triangleq & (\Gamma, g, p) \\
\mathit{flush} & (n + 1, \Gamma, I_S f, p) & \triangleq & \mathit{flush}(n, \Gamma, f, p) \\
\mathit{flush} & (2n + 1, (\Gamma, A), \mathbb{I}_{\forall} f, p) & \triangleq & \mathit{flush}(2n, \Gamma, f, \mathit{drinker}_{x_n} p) \\
\mathit{flush} & (2n + 2, (\Gamma, A), I \Rightarrow (f, k), p) & \triangleq & k(\Gamma, f, p)
\end{array}
$$

A trivial lemma implicit in the natural language formulation of the proof of completeness is the lemma asserting $\dot{\to} A_0 \subset S_n$. The proof is by induction on $n$:

$$
\begin{array}{lclcl}
\mathrm{inj}_n & : & \dot{\to} A_0 \subset S_n & & \\
\mathrm{inj}_0 & \triangleq & I_0(J_{\mathrm{base}}) & & \\
\mathrm{inj}_{n+1} & \triangleq & I_S(\mathrm{inj}_n) & &
\end{array}
$$

A boring lemma which is implicit in the proof of completeness in natural language is
that $\Gamma \subset S_n$ and $\Gamma' \subset S_{n'}$ imply $\Gamma \cup \Gamma' \subset S_{\max(n,n')}$.
It looks obvious because one tends
to think of $\Gamma \subset S_n$ as denoting the inclusion of $\Gamma$ within a uniquely defined relatively
consistent set $S_n$. However, the computational approach to the proof shows that $S_n$
has no computational content per se: only proofs of $\Gamma \subset S_n$ have, and such proofs are
collections of proofs of relative consistency for only those implicative formulae which
are in $\Gamma$. These formulae are those inspected by the lemma $A \in S_\omega \Leftrightarrow M_0 \vDash_A A$, which
in practice are subformulae of the formulae in $\mathcal{T}_0$.

For $\Gamma_1$ and $\Gamma_2$ included in $\mathcal{T}_0$, we write $\Gamma_1, \Gamma_2$ for their concatenation (possibly with redundancies). Otherwise, by construction, any $\Gamma$ included in $S_n$ for some $n$ has either the form $\Gamma', \dot{\to} A_0$ where $\Gamma'$ is included in $\mathcal{T}_0$, or the form $\Gamma', A$ where $A$ has been added in the process of enumeration. We can then define $\Gamma_1 \cup \Gamma_2$ for $\Gamma_1$ and $\Gamma_2$ included in $S_n$ for some $n$ by cases$^{28}$:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\Gamma_1, \dot{\to} A_0 & \cup & \Gamma_2, \dot{\to} A_0 & ::= & \Gamma_1, \Gamma_2, \dot{\to} A_0 \\
\Gamma_1, \dot{\to} A_0 & \cup & \Gamma_2, A & ::= & (\Gamma_1, \dot{\to} A_0 \cup \Gamma_2), A \\
\Gamma_1, A & \cup & \Gamma_2, \dot{\to} A_0 & ::= & (\Gamma_1 \cup \Gamma_2, \dot{\to} A_0), A \\
\Gamma_1, A & \cup & \Gamma_2, A & ::= & (\Gamma_1 \cup \Gamma_2), A \\
\Gamma_1, A & \cup & \Gamma_2, B & ::= & (\Gamma_1, A \cup \Gamma_2), B & \text{if } [B] > [A] \\
\Gamma_1, A & \cup & \Gamma_2, B & ::= & (\Gamma_1 \cup \Gamma_2, B), A & \text{if } [A] > [B]
\end{array}
$$

We can then define the merge of two proofs of $\Gamma \subset S_n$ by distinguishing when the
contexts are considered as subsets of $\mathcal{T}_0$ or as subsets of some $S_n$:

<footnote n="28"><sup>28</sup>Strictly speaking, this decomposition of any Γ included in S<sub>n</sub> for some n should be part of the structure of Γ so as to be able to compute with it.</footnote>
$$
\begin{align*}
\operatorname{join}_{\subset}^{\Gamma_1 \Gamma_2} &: \quad \Gamma_1 \subset \mathcal{T}_0 \quad \wedge \quad \Gamma_2 \subset \mathcal{T}_0 & \Rightarrow & \Gamma_1, \Gamma_2 \subset \mathcal{T}_0 \\
\operatorname{join}_{\subset}^{\Gamma_1 \epsilon} &: \quad (g_1, J_{\text{base}}) & \triangleq & g_1 \\
\operatorname{join}_{\subset}^{\Gamma_1 (\Gamma_2, A_2)} &: \quad (g_1, J_{\text{cons}}(g_2, h_2)) & \triangleq & J_{\text{cons}}(\operatorname{join}_{\subset}^{\Gamma_1 \Gamma_2} (g_1, g_2), h_2)
\end{align*}
$$

$$
\begin{align*}
\operatorname{join}_n^{\Gamma_1 \Gamma_2} &: \quad \Gamma_1 \subset S_n \quad \wedge \quad \Gamma_2 \subset S_n & \Rightarrow & \Gamma_1 \cup \Gamma_2 \subset S_n \\
\operatorname{join}_0^{(\Gamma_1, \dot{\wedge} A_0)(\Gamma_2, \dot{\wedge} A_0)} &: \quad (I_0(g_1), I_0(g_2)) & \triangleq & I_0(\operatorname{join}_{\subset}^{\Gamma_1 \Gamma_2} (g_1, g_2)) \\
\operatorname{join}_2^{(\Gamma_1 A)(\Gamma_2 A)} &: \quad (I_{\vee}(f_1), I_{\vee}(f_2)) & \triangleq & I_{\vee}(\operatorname{join}_{2\mu}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{join}_{\frac{2n+1}{2}}^{(\Gamma_1 A)(\Gamma_2 A)} &: \quad (I \Rightarrow (f_1, k_1), I \Rightarrow (f_2, k_2)) & \triangleq & I \Rightarrow (\operatorname{join}_{\frac{2n+1}{2}}^{\Gamma_1 \Gamma_2} (f_1, f_2), k_1) \\
\operatorname{join}_{\frac{2n+1}{2}}^{(\Gamma_1 A)\Gamma_2} &: \quad (I_{\vee}(f_1), I_S(f_2)) & \triangleq & I_{\vee}(\operatorname{join}_{2\mu}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{join}_{\frac{2n+1}{2}}^{(\Gamma_1 A)\Gamma_2} &: \quad (I \Rightarrow (f_1, k_1), I_S(f_2)) & \triangleq & I \Rightarrow (\operatorname{join}_{\frac{2n+1}{2}}^{\Gamma_1 \Gamma_2} (f_1, f_2), k_1) \\
\operatorname{join}_{\frac{2n+1}{2}}^{(\Gamma_1 \Gamma_2 A)} &: \quad (I_S(f_1), I_{\vee}(f_2)) & \triangleq & I_{\vee}(\operatorname{join}_{2\mu}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{join}_{\frac{2n+1}{2}}^{(\Gamma_1 \Gamma_2 A)} &: \quad (I_S(f_1), I \Rightarrow (f_2, k_2)) & \triangleq & I \Rightarrow (\operatorname{join}_{\frac{2n+1}{2}}^{\Gamma_1 \Gamma_2} (f_1, f_2), k_2) \\
\operatorname{join}_{n+1}^{\Gamma_1 \Gamma_2} &: \quad (I_S(f_1), I_S(f_2)) & \triangleq & I_S(\operatorname{join}_n^{\Gamma_1 \Gamma_2} (f_1, f_2))
\end{align*}
$$

$$
\begin{align*}
\operatorname{hjoin}_{n_1 n_2}^{\Gamma_1 \Gamma_2} &: \quad \Gamma_1 \subset S_{n_1} \quad \wedge \quad \Gamma_2 \subset S_{n_2} & \Rightarrow & \Gamma_1 \cup \Gamma_2 \subset S_{\max(n_1, n_2)} \\
\operatorname{hjoin}_{nn}^{\Gamma_1 \Gamma_2} &: \quad (f_1, f_2) & \triangleq & \operatorname{join}_n^{\Gamma_1 \Gamma_2} (f_1, f_2) \\
\operatorname{hjoin}_{n'_1+1>n_2}^{\Gamma_1 \Gamma_2} &: \quad (I_S(f_1), f_2) & \triangleq & I_S(\operatorname{hjoin}_{n'_1 n_2}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{hjoin}_{n'_1+1>n_2}^{(\Gamma_1 A_1) \Gamma_2} &: \quad (I_{\vee}(f_1), f_2) & \triangleq & I_{\vee}(\operatorname{hjoin}_{n'_1 n_2}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{hjoin}_{n'_1+1>n_2}^{(\Gamma_1 A_1) \Gamma_2} &: \quad (I \Rightarrow (f_1, k_1), f_2) & \triangleq & I \Rightarrow (\operatorname{hjoin}_{n'_1 n_2}^{\Gamma_1 \Gamma_2} (f_1, f_2), k_1) \\
\operatorname{hjoin}_{n_1<n'_2+1}^{\Gamma_1 \Gamma_2} &: \quad (f_1, I_S(f_2)) & \triangleq & I_S(\operatorname{hjoin}_{n_1 n'_2}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{hjoin}_{n_1<n'_2+1}^{\Gamma_1 (\Gamma_2 A_2)} &: \quad (f_1, I_{\vee}(f_2)) & \triangleq & I_{\vee}(\operatorname{hjoin}_{n_1 n'_2}^{\Gamma_1 \Gamma_2} (f_1, f_2)) \\
\operatorname{hjoin}_{n_1<n'_2+1}^{\Gamma_1 (\Gamma_2 A_2)} &: \quad (f_1, I \Rightarrow (f_2, k_2)) & \triangleq & I \Rightarrow (\operatorname{hjoin}_{n_1 n'_2}^{\Gamma_1 \Gamma_2} (f_1, f_2), k_2)
\end{align*}
$$

In particular, it has to be noticed that the merge possibly does arbitrary choices: when the same implicative formula A occurs in both contexts, only one of the two proofs telling how to reduce $\Gamma, A \vdash \bot$ to $\mathcal{T}_0, \dot{\wedge} A_0 \vdash \bot$ (third clause of $\operatorname{join}_n$) is (arbitrarily) kept.

Another combinatoric lemma is that the merge of contexts indeed produces a bigger context. To state the lemma, we already need to define the inclusion of contexts $\Gamma \subset \Gamma'$. This can be done inductively by the following clauses:

$$
\frac{\epsilon \subset \epsilon}{\Gamma \subset \Gamma'} L_0^c \quad \frac{\Gamma \subset \Gamma', A}{\Gamma \subset \Gamma'} L_N^c \quad \frac{\Gamma \subset \Gamma'}{\Gamma, A \subset \Gamma', A} L_S^c
$$

Two straightforward lemmas are that $\Gamma_1 \subset \Gamma_1, \Gamma_2$ and $\Gamma_2 \subset \Gamma_1, \Gamma_2$ for $\Gamma_1$ and $\Gamma_2$ included in $\mathcal{T}_0$. The proofs are by induction on $\Gamma_1$ and $\Gamma_2$ where $i$ is either 1 or 2:

$$
\mathrm{incl}_i^{\Gamma_1, \Gamma_2} : \quad \Gamma_i \subset \Gamma_1, \Gamma_2
$$

$$
\mathrm{incl}_i^{\epsilon, \epsilon} \triangleq L_0
$$

$$
\mathrm{incl}_1^{(\Gamma_1, A), \epsilon} \triangleq L_S (\mathrm{incl}_1^{\Gamma_1 \epsilon})
$$

$$
\mathrm{incl}_2^{\Gamma_1, A), \epsilon} \triangleq L_N (\mathrm{incl}_2^{\Gamma_1 \epsilon})
$$

$$
\mathrm{incl}_1^{\Gamma_1, (\Gamma_2, A)} \triangleq L_N (\mathrm{incl}_1^{\Gamma_1 \Gamma_2})
$$

$$
\mathrm{incl}_2^{\Gamma_1, (\Gamma_2, A)} \triangleq L_S (\mathrm{incl}_2^{\Gamma_1 \Gamma_2})
$$
This allows to prove the following lemma where $i$ is either 1 or 2:

$$
\begin{align*}
\text{incl}'_{i}^{\Gamma_1, \Gamma_2} &::= \Gamma_i \subset \Gamma_1 \cup \Gamma_2 \\
\text{incl}'_{i}^{(\Gamma_1, \dot{\wedge} A_0), (\Gamma_2, \dot{\wedge} A_0)} &::= L_S(\text{incl}'_{i}^{\Gamma_1, \Gamma_2}) \\
\text{incl}'_{i}^{(\Gamma_1, \dot{\wedge} A_0), (\Gamma_2, A)} &::= L_N(\text{incl}'_{i}^{(\Gamma_1, \dot{\wedge} A_0), \Gamma_2}) \\
\text{incl}'_{i}^{(\Gamma_1, \dot{\wedge} A_0), (\Gamma_2, \Gamma_2, A)} &::= L_S(\text{incl}'_{i}^{(\Gamma_1, \dot{\wedge} A_0), \Gamma_2}) \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, \dot{\wedge} A_0)} &::= L_S(\text{incl}'_{i}^{\Gamma_1, (\Gamma_2, \dot{\wedge} A_0)}) \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, \dot{\wedge} A_0)} &::= L_N(\text{incl}'_{i}^{\Gamma_1, (\Gamma_2, \dot{\wedge} A_0)}) \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, A)} &::= L_S(\text{incl}'_{i}^{\Gamma_1, \Gamma_2}) \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, B)} &::= L_N(\text{incl}'_{i}^{(\Gamma_1, A), \Gamma_2}) \quad \text{if } [A] < [B] \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, B)} &::= L_S(\text{incl}'_{i}^{(\Gamma_1, A), \Gamma_2}) \quad \text{if } [A] < [B] \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, B)} &::= L_S(\text{incl}'_{i}^{\Gamma_1, (\Gamma_2, B)}) \quad \text{if } [A] > [B] \\
\text{incl}'_{i}^{(\Gamma_1, A), (\Gamma_2, B)} &::= L_N(\text{incl}'_{i}^{\Gamma_1, (\Gamma_2, B)}) \quad \text{if } [A] > [B]
\end{align*}
$$

Our object logic is defined by the rules on Figure 2. Note that we shall use non standard derived rules. For instance, we shall not use the rule $abs \Rightarrow$ and $abs^\nabla$ but instead the derived rules $\pi_1 \Rightarrow$, $\pi_2 \Rightarrow$ and $ drinker_y$.

Thanks to the previous lemma, we are able to translate proofs of $A_1 \in S_\omega$ and $A_2 \in S_\omega$ living in possibly two different contexts to eventually live in the union of the two contexts:

$$
\begin{align*}
\text{share} : A_1 \in S_\omega \wedge A_2 \in S_\omega &\Rightarrow \exists n \exists \Gamma (\Gamma \subset S_n \wedge \Gamma \vdash A_1 \wedge \Gamma \vdash A_2) \\
\text{share} \quad (n_1, \Gamma_1, f_1, p_1) \quad (n_2, \Gamma_2, f_2, p_2) &\triangleq \left. \begin{array}{@{}l@{}}
\max(n_1, n_2), (\Gamma_1 \cup \Gamma_2), \text{hjoin}(f_1, f_2), \\
\text{weak}(\text{incl}'^{\Gamma_1, \Gamma_2}_{1, \Gamma_2}, p_1), \\
\text{weak}(\text{incl}'^{\Gamma_1, \Gamma_2}_{2, \Gamma_2}, p_2)
\end{array} \right\}
\end{align*}
$$

where *weak* is an admissible rule of the object logic.

Thanks to the ability to ensure distinct proofs to live in the same context, we can
reformulate the relevant rules of the object logic as rules over $S_\omega$, as well as provide
proofs of specific formulae:

$$
\begin{align*}
AP\dot{P} \Rightarrow & : A \Rightarrow B \in S_{\omega} \wedge A \in S_{\omega} \Rightarrow B \in S_{\omega} \\
AP\dot{P} \Rightarrow & q \qquad q' \qquad \begin{array}[t]{c} \triangleq \\ \text{dest share} (q, q') \text{ as } (n', \Gamma', f', p'p'') \text{ in} \\ (n', \Gamma', f', \text{app} \Rightarrow (p', p'')) \end{array}
\end{align*}
$$

$$
\begin{align*}
\dot{A}P^\nabla : & \quad \forall x A(x) \in S_\omega \wedge \mathcal{T}erm \\
& \Rightarrow A(t) \in S_\omega \\
\dot{A}P^\nabla : & (n, \Gamma, f, p) \qquad t \qquad \triangleq (n, \Gamma, f, \mathit{app}^\nabla(p, t))
\end{align*}
$$

$$
\begin{align*}
\dot{D}N : & \quad \dot{\wedge} \dot{\wedge} A \in S_{\omega} \\
\dot{D}N & (n, \Gamma, f, p) \qquad \begin{array}[t]{@{}c@{}} \Rightarrow \\ \triangleq \end{array} (n, \Gamma, f, \dot{d}n(p))
\end{align*}
$$

$$
\begin{align*}
\dot{A}X_{\forall x A(x)} &::= A(x_n) \Rightarrow \forall x A(x) \in S_{\omega} \\
\dot{A}X_{\forall x A(x)} &::= (2n + 1, (\dot{\wedge} A_0, A(x_n) \Rightarrow \forall x A(x)), \mathbf{I}_{\forall}(\mathrm{inj}_{2n}), \dot{a}x_0) \\
&\qquad \text{where } 2n = \lceil \forall x A(x) \rceil
\end{align*}
$$

$$
\begin{align*}
\dot{A}X_{\dot{\wedge} A_0}^0 &::= \dot{\wedge} A_0 \in S_{\omega} \\
\dot{A}X_{\dot{\wedge} A_0}^0 &::= (0, \dot{\wedge} A_0, J_{\text{base}}, \dot{a}x_0)
\end{align*}
$$
Primitive rules

$$
\frac{\Gamma' | = i}{\Gamma, A, \Gamma' \vdash A} \dot{a}x_i \qquad \frac{\Gamma \vdash \dot{\gamma} \dot{\gamma}' A}{\Gamma \vdash A} \dot{d}n
$$
$$
\frac{\Gamma \vdash A \Rightarrow B \qquad \Gamma' \vdash A}{\Gamma \cup \Gamma' \vdash B} \quad \text{app} \Rightarrow \quad \frac{\Gamma \vdash \dot{\gamma} x A(x)}{\Gamma \vdash A(t)} \quad \text{app}^{\dot{\gamma}}_t
$$
$$
\frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B} \quad \text{abs} \Rightarrow \quad \frac{\Gamma \vdash A(y) \qquad \text{y not in } \dot{\gamma} x A(x), \Gamma}{\Gamma \vdash \dot{\gamma} x A(x)} \quad \text{abs}^{\vee}
$$

Admissible rules

$$
\frac{\Gamma, A(y) \Rightarrow \dot{\gamma} x A(x) \vdash \bot \qquad \text{y not in } \dot{\gamma} x A(x), \Gamma}{\Gamma \vdash \bot} \qquad \text{drinker}_y
$$
$$
\frac{\Gamma, A \Rightarrow B \vdash \bot}{\Gamma \vdash A} \quad \pi_1 \Rightarrow \quad \frac{\Gamma, A \Rightarrow B \vdash \bot}{\Gamma \vdash \dot{\gamma} B} \quad \pi_2 \Rightarrow \quad \frac{\Gamma \vdash \bot}{\Gamma \vdash A} \quad \text{efq} \quad \frac{\Gamma \subset \Gamma' \quad \Gamma \vdash A}{\Gamma' \vdash A} \quad \text{weak}
$$

<caption>FIGURE 2. Inference rules characterising classical first-order predicate calculus</caption>

Similarly, we can formulate rules on provability in T₀:

$$
\begin{array}{lcl}
\mathit{DN\acute{A}BS} : & \mathcal{T}_0, \dot{\gamma} A_0 \vdash \bot & \Rightarrow \mathcal{T}_0 \vdash A_0 \\
\mathit{DN\acute{A}BS} & (\Gamma, g, p) & \triangleq (\Gamma, g, \dot{d}n(\mathit{abs} \Rightarrow (p)))
\end{array}
$$

$$
\begin{array}{lcl}
\mathit{B\acute{O}T} : & \mathcal{T}_0, \dot{\gamma} A_0 \vdash \bot & \Rightarrow \bot \in \mathcal{S}_\omega \\
\mathit{B\acute{O}T} & (\Gamma, g, p) & \triangleq (0, (\Gamma, \dot{\gamma} A_0), I_0(g), p)
\end{array}
$$

When $[A \Rightarrow B] = 2n + 1$, we can also derive the following properties:

$$
\begin{align*}
\dot{A}X_{A \Rightarrow B} : & ((S_{2n+1}, A \Rightarrow B \vdash \bot) \Rightarrow (T_0, \dot{\gamma} A_0 \vdash \bot)) && \Rightarrow \quad A \Rightarrow B \in S_{\omega} \\
\dot{A}X_{A \Rightarrow B} : & k && \triangleq \quad \begin{pmatrix} 2n+2, (\dot{\gamma} A_0, A \Rightarrow B), \\ I \Rightarrow (\text{inj}_{2n+1}, k), \dot{a}x_0 \end{pmatrix}
\end{align*}
$$

$$
\begin{align*}
\dot{P}\acute{R}\dot{O}\dot{J}_{1} &\stackrel{\sim}{\Rightarrow} S_{2n+1}, A \Rightarrow B \vdash \bot \\
\dot{P}\acute{R}\dot{O}\dot{J}_{1} &\stackrel{\sim}{(}\Gamma, f, p)
\end{align*}
\begin{align*}
&\Rightarrow A \in S_{\omega} \\
&\triangleq (2n+1, \Gamma, f, \pi_{1} \stackrel{\sim}{\Rightarrow} p)
\end{align*}
$$

$$
\begin{align*}
\dot{P}\acute{R}\dot{O}\dot{J}_{2} &\stackrel{\sim}{\Rightarrow} S_{2n+1}, A \Rightarrow B \vdash \bot \\
\dot{P}\acute{R}\dot{O}\dot{J}_{2} &\stackrel{\sim}{(}\Gamma, f, p)
\end{align*}
\begin{align*}
&\Rightarrow \dot{\gamma} B \in S_{\omega} \\
&\triangleq (2n+1, \Gamma, f, \pi_{2} \stackrel{\sim}{\Rightarrow} p)
\end{align*}
$$

We are now ready to present the main computational piece of the completeness proof and we shall use for that notations reminiscent from semantic normalisation [19], or type-directed partial evaluation [23], as considered when proving completeness of intuitionistic logic with respect to models such a Kripke or Beth models.
We have to prove $M_0 \Vdash_{\sigma}^e A \Leftrightarrow A[\sigma] \in S_\omega$, which means proving $M_0 \Vdash_{\sigma}^e A \Rightarrow A[\sigma] \in S_\omega$ and $A[\sigma] \in S_\omega \Rightarrow M_0 \Vdash_{\sigma}^e A$. As in semantic normalisation (see Section 1.6), we shall call *reification* and write $\searrow_{\sigma}^A$ the proof mapping a semantic formula (i.e. $M_0 \Vdash_{\sigma}^e A$) to a syntactic formula, i.e. $A[\sigma] \in S_\omega$. We shall call *reflection* and write $\uparrow_{\sigma}^A$ for the way up going from the syntactic view to the semantic view.

$$
\begin{array}{lclcl}
\searrow_{\sigma}^{A}: & M_0 \Vdash_{\sigma}^{e} A & \Rightarrow & A[\sigma] \in S_{\omega} \\
\searrow_{\sigma}^{P(\vec{i})} & m & \triangleq & m \\
\searrow_{\sigma}^{\perp} & m & \triangleq & \text{B\"OT}(m) \\
\searrow_{\sigma}^{A \Rightarrow B} & m & \triangleq & \dot{A}X_{A[\sigma]} \Rightarrow B[\sigma](\text{kont}_{\sigma}^{A \Rightarrow B}(m)) \\
\searrow_{\sigma}^{\forall x A} & m & \triangleq & \dot{A}P\dot{P} \Rightarrow (\dot{A}X_{(\forall x A)[\sigma]}, \searrow_{\sigma,x \leftarrow x_n}^{A} (m x_n)) \text{ where } 2n = (\forall \forall x A)[\sigma]
\end{array}
$$

$$
\begin{array}{lclcl}
\uparrow_{\sigma}^{A}: & A[\sigma] \in S_{\omega} & \Rightarrow & M_{0} \Vdash_{\sigma}^{e} A \\
\uparrow_{\sigma}^{P(\vec{i})} & q & \triangleq & q \\
\uparrow_{\sigma}^{\perp} & q & \triangleq & \text{flush } q \\
\uparrow_{\sigma}^{A \Rightarrow B} & q & \triangleq & m \mapsto \uparrow_{\sigma}^{B} (A P \dot{P} \Rightarrow (q, \searrow_{\sigma}^{A} m)) \\
\uparrow_{\sigma}^{\forall x A} & q & \triangleq & t \mapsto \uparrow_{\sigma,x \leftarrow t}^{A} (A P \dot{P}^{\forall} (q, t))
\end{array}
$$

where, for $m$ proving $M_0 \Vdash_{\sigma}^e A \Rightarrow B$, the relative consistency proof $\text{kont}_{\sigma}^{A \Rightarrow B}(m)$ is defined by:

$$
\text{kont}_{\sigma}^{A \Rightarrow B}(m) : (S_{\lceil A[\sigma] \rceil \Rightarrow B[\sigma]}], A[\sigma] \Rightarrow B[\sigma] \vdash \bot) \Rightarrow (T_0, \dot{\eta}A_0 \vdash \bot)
$$

$$
\text{kont}_{\sigma}^{A \Rightarrow B}(m) \triangleq r \mapsto \text{flush} (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\Rightarrow} (r), \searrow_{\sigma}^{B} (m (\uparrow_{\sigma}^{A} (P\dot{R}OJ_1 \stackrel{\rightarrow}{\Rightarrow} (r))))))
$$

We still have to prove that the model is classical, which we do by lifting the double-
negation elimination rule to the semantics:

$$
\text{classic}_0 : \quad \forall A ((M_0 \Vdash_{id}^e \dot{\eta} \dot{A}) \Rightarrow (M_0 \Vdash_{id}^e A))
$$

$$
\text{classic}_0 \triangleq A \mapsto m \mapsto \uparrow_{id}^{A} (\dot{D}N (\searrow_{id}^{\dot{\eta}A} m))
$$

It remains also to show that every formula of $\mathcal{T}_0$ is true in $M_0$ and this is obtained by
the axiom rule:

$$
\text{init}_0 : \quad \forall B \in \mathcal{T}_0 M_0 \Vdash_{id}^e B
$$

$$
\text{init}_0 \triangleq B \mapsto h \mapsto \uparrow_{id}^{B} (0, (B, \dot{\eta}A_0), I_0(J_{\text{cons}}(J_{\text{base}}, h)), \dot{dx}_1)
$$

Finally, we get the completeness result stated as S1' by:

$$
\textit{completeness} : \quad \forall \mathcal{M} \forall \sigma (\mathcal{M} \Vdash_{\sigma}^{e} \mathit{Classic} \Rightarrow \mathcal{M} \Vdash_{\sigma}^{e} \mathcal{T}_0 \Rightarrow \mathcal{M} \Vdash_{\sigma}^{e} A_0) \Rightarrow \mathcal{T}_0 \vdash A_0
$$

$$
\textit{completeness} \triangleq \psi \mapsto DN\dot{A}BS (\text{flush} (AP\dot{P} \Rightarrow (\dot{A}X_{\dot{\eta}A_0}^0, \searrow_{id}^{A_0} (\psi M_0 \text{ id classic}_0 \text{ init}_0))))
$$

Notice that the final result is a triple (Γ, g, p) such that p is a proof of Γ ⊢ A₀ and g is a proof of Γ ⊂ T₀.

**2.4. The computational content on examples.** To illustrate the behaviour of the completeness proofs, we consider two examples. We use notations of λ-calculus to represent proofs in the meta-logic and constructors from Figure 2 for proofs in the object logic.

We place ourselves in the empty theory and consider the formula $A_0 \triangleq X \Rightarrow Y \Rightarrow X$
with X and Y propositional atoms.

The expansion of $\Vdash^e A_0$ is $\forall M \forall \sigma (\sigma \Vdash_M^e \text{Classic} \Rightarrow M \Vdash^e X \Rightarrow M \Vdash^e Y \Rightarrow M \Vdash^e X)$. It has a canonical proof, which, as a $\lambda$-term, is the closure of the so-called
combinator $K$ over the symbols it depends on:

$$m \triangleq (\mathcal{D}, \mathcal{F}, \mathcal{P}, B) \mapsto \sigma \mapsto c \mapsto (x : \mathcal{P}(X)) \mapsto (y : \mathcal{P}(Y)) \mapsto x$$

Applying completeness means instantiating the model by the syntactic model and the substitution by the empty substitution so as to obtain from $m$ the proof

$$m_0 \triangleq (x : X \in S_\omega) \mapsto (y : Y \in S_\omega) \mapsto x$$

Our object proof is then the result of evaluating

$$DN\acute{A}BS (flush (AP\dot{P} \Rightarrow (A\dot{X}^{0}_{\sim A_0}, \downarrow^{A_0} m_0)))$$

which proceeds as follows:

$$DN\acute{A}BS (flush (AP\dot{P} \Rightarrow (A\dot{X}^{0}_{\sim A_0}, A\dot{X}_{A_0} (kont^{A_0}(m_0)))))$$

where $kont^{A_0}(m_0)(r)$ reduces to flush $(AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r), \downarrow^{Y \Rightarrow X} (m_0 (\uparrow^X (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r))))))$ for $r$ proving $S_{\lfloor A_0 \rfloor}, A_0 \vdash \bot$, that is to

$$flush (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r), A\dot{X}_{Y \Rightarrow X} (kont^{Y \Rightarrow X} (m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r)))))$$

In there, $kont^{Y \Rightarrow X}(m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r))(r')$, for $r'$ proving $S_{\lfloor Y \Rightarrow X \rfloor}, Y \Rightarrow X \vdash \bot$, reduces in turn to

$$flush (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r'), m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r)) (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r'))))$$

Evaluating $AP\dot{P} \Rightarrow (A\dot{X}^{0}_{\sim A_0}, A\dot{X}_{A_0} (kont^{A_0}(m_0)))$ gives a tuple

$$(\lfloor A_0 \rfloor, (\dot{\vdash} A_0, A_0), I \Rightarrow (inj_{\lfloor A_0 \rfloor}, kont^{A_0}(m_0)), p_0)$$

where $p_0 \triangleq app \Rightarrow (\dot{a}x_1, \dot{a}x_0)$ is a proof of $\dot{\vdash} A_0, A_0 \vdash \bot$ obtained by application of the two axiom rules proving $\dot{\vdash} A_0 \vdash \dot{\vdash} A_0$ and $\dot{\vdash} A_0, A_0 \vdash A_0$.

Evaluating the outermost flush triggers the application of the continuation $kont^{A_0}(m_0)$ to $r_0 \triangleq (\dot{\vdash} A_0, inj_{\lfloor A_0 \rfloor}, p_0)$, meaning that the whole object proof becomes

$$DN\acute{A}BS (flush (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r_0), A\dot{X}_{Y \Rightarrow X} (kont^{Y \Rightarrow X} (m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0)))))$$

Evaluating $AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r_0), A\dot{X}_{Y \Rightarrow X} (kont^{Y \Rightarrow X} (m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0)))))$ gives a tuple

$$(\lfloor Y \Rightarrow X \rfloor, (\dot{\vdash} A_0, Y \Rightarrow X), I \Rightarrow (inj_{\lfloor Y \Rightarrow X \rfloor}, kont^{Y \Rightarrow X} (m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0))), p_1)$$

where $p_1 \triangleq app \Rightarrow (\pi_2 \stackrel{\rightarrow}{\rightleftharpoons} (p_0), \dot{a}x_0)$ is a proof of $\dot{\vdash} A_0, Y \Rightarrow X \vdash \bot$.

Evaluating the new outermost flush triggers in turn the application of the continuation $kont^{Y \Rightarrow X}(m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0)))$ to $r_1 \triangleq (\dot{\vdash} A_0, inj_{\lfloor Y \Rightarrow X \rfloor}, p_1)$ and this results in

$$(1) \quad DN\acute{A}BS (flush (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r_1), m_0 (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0)) (P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_1))))$$

that is, taking into account the definition of $m_0$

$$DN\acute{A}BS (flush (AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r_1), P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0))))$$

No continuations are produced by $AP\dot{P} \Rightarrow (P\dot{R}OJ_2 \stackrel{\rightarrow}{\rightleftharpoons} (r_1), P\dot{R}OJ_1 \stackrel{\rightarrow}{\rightleftharpoons} (r_0))$ so the only role of the last flush is to peel the $I_S$ leading to a proof $r_2 \triangleq (\epsilon, J_{base}, \dot{dn}(p_2))$ where $p_2 \triangleq app \Rightarrow (\pi_2 \stackrel{\rightarrow}{\rightleftharpoons} (p_1), \pi_1 \stackrel{\rightarrow}{\rightleftharpoons} (p_0))$ combines a proof of $\dot{\vdash} A_0 \vdash \dot{\vdash} X$ with a proof of $\dot{\vdash} A_0 \vdash X$ to get a proof of $\dot{\vdash} A_0 \vdash \bot$.

To summarise, the object proof produced is:
**2.5. Extension to conjunction.** Henkin's original proof [40] includes only implication, universal quantification and the false connective. Handling conjunction in our presentation of Henkin's proof is straightforward. Let us assume the object language being equipped with the following rules for conjunction:

$$ \frac{\Gamma \vdash A_1 \quad \Gamma \vdash A_2}{\Gamma \vdash A_1 \dot{\wedge} A_2} \qquad \text{p\'air} \qquad \frac{\Gamma \vdash A_1 \dot{\wedge} A_2}{\Gamma \vdash A_1} \qquad \dot{\pi}_1^\wedge \qquad \frac{\Gamma \vdash A_1 \dot{\wedge} A_2}{\Gamma \vdash A_2} \qquad \dot{\pi}_2^\wedge $$

Truth for conjunction being defined by

$$ \mathcal{M} \Vdash_{\sigma} A_1 \dot{\wedge} A_2 \triangleq \mathcal{M} \Vdash_{\sigma} A_1 \wedge \mathcal{M} \Vdash_{\sigma} A_2 $$

a case is added for conjunctive formulae in each direction of the proof of $M_0 \Vdash_{\sigma} A \Leftrightarrow A[\sigma] \in S_{\omega}$ as follows:

$$ \begin{array}{lclcl} \downarrow_{\sigma}^{A_1 \dot{\wedge} A_2} & (m_1, m_2) & \triangleq & \mathrm{PAIR}(\downarrow_{\sigma}^{A_1} m_1, \downarrow_{\sigma}^{A_2} m_2) & \\ \uparrow_{\sigma}^{A_1 \dot{\wedge} A_2} & q & \triangleq & (\uparrow_{\sigma}^{A_1} (\mathrm{PROJ}_1^{\wedge} q), \uparrow_{\sigma}^{A_2} (\mathrm{PROJ}_2^{\wedge} q)) & \end{array} $$

where the following combinators lift inference rules on $S_{\omega}$:

$$ \mathrm{PAIR}(q_1, q_2) \triangleq \mathrm{dest\,share}(q_1, q_2) \text{ as } (n, \Gamma, f, p_1, p_2) \text{ in } (n, \Gamma, f, \mathrm{p\'air}(p_1, p_2)) $$

$$ \mathrm{PROJ}_i^{\wedge} (n, \Gamma, f, p) \triangleq (n, \Gamma, f, \dot{\pi}_i^{\wedge} p) $$

In particular, there is no need to consider conjunctive formulae in the enumeration.

**2.6. Extension to disjunction.** Taking inspiration from works on normalisation-by-evaluation in the presence of disjunction (e.g. [1, 2]), we give a proof for disjunction that relies on the following arithmetical generalised form of Double Negation Shift introduced<sup>29</sup> in [51]:

$$ \mathrm{DNS}_C^{\nabla} \quad \forall n ((\mathcal{A}(n) \Rightarrow C) \Rightarrow C) \Rightarrow (\forall n \mathcal{A}(n) \Rightarrow C) \Rightarrow C $$

for $C$ a $\Sigma_1^0$-formula and $\mathcal{A}$ arbitrary (usual DNS is then $\mathrm{DNS}_{\perp}^{\nabla}$).

The proof however requires a significant change: instead of proving $M_0 \Vdash_{\sigma} A \Leftrightarrow A[\sigma] \in S_{\omega}$, we prove:

$$ \downarrow_{\sigma}^{A} : M_0 \Vdash_{\sigma} A \Rightarrow A[\sigma] \in S_{\omega} $$

$$ \uparrow_{\sigma}^{A'} : A[\sigma] \in S_{\omega} \Rightarrow \mathrm{KONT}(M_0 \Vdash_{\sigma} A) $$

where $\mathrm{KONT}(\mathcal{A})$, a continuation monad<sup>30</sup>, is defined by:

$$ \mathrm{KONT}(\mathcal{A}) \triangleq (\mathcal{A} \Rightarrow \mathcal{T}_0, \dot{\wedge} A_0 \vdash \dot{\wedge}) \Rightarrow \mathcal{T}_0, \dot{\wedge} A_0 \vdash \dot{\wedge} $$

As such, the proof can also be seen as an adaptation to Tarski semantics of the proof of completeness with respect to continuation-passing style models given in [52].

Let us assume the object language equipped with the following rules for disjunction:

$$ \frac{\Gamma \vdash A_1 \qquad \Gamma \vdash A_2 \qquad \Gamma \vdash A_1 \dot{\wedge} A_2 \qquad \Gamma \vdash A_1 \Rightarrow B \qquad \Gamma \vdash A_2 \Rightarrow B}{\Gamma \vdash A_1 \dot{\wedge} A_2} \quad \text{case} $$

<footnote n="29"><sup>29</sup>In the presence of Markov's principle, this generalised form of DNS is equivalent to the usual form. The interest of the generalised form is precisely that it can be used in situations which would have required Markov's principle without requiring Markov's principle explicitly.</footnote>

<footnote n="30"><sup>30</sup>Note that $\mathrm{KONT}(M_0 \Vdash_{\sigma} A)$ is actually the same as $M_0 \Vdash_{\sigma} \dot{\wedge} A$ but we shall use $\mathrm{KONT}$ also on formulae which are not of the form $M_0 \Vdash_{\sigma} A$.</footnote>
Let us also consider the following lifting of the inference rules to provability in $S_\omega$:

$$I\acute{N}J_i : \quad A_i \in S_\omega \quad \Rightarrow \quad A_1 \dot{\vee} A_2 \in S_\omega$$

$$I\acute{N}J_i : \quad (n, \Gamma, f, p) \quad \triangleq \quad (n, \Gamma, f, inj_i p)$$

$$C\acute{A}SE : \quad \left( \begin{array}{l} A \dot{\vee} B \in S_\omega \\ A \Rightarrow C \in S_\omega \\ B \Rightarrow C \in S_\omega \end{array} \right) \quad \Rightarrow \quad C \in S_\omega$$

$$C\acute{A}SE \quad (q, q_1, q_2) \quad \triangleq \quad \begin{array}{l} \text{dest share}_3(q, q_1, q_2) \text{ as } (n, \Gamma, f, p, p_1, p_2) \text{ in} \\ \text{(n, \Gamma, f, case } p_1 p_2) \end{array}$$

where we needed the following three-part variant share₃ of share:

$$\text{share}_3 : A_1 \in S_\omega \wedge A_2 \in S_\omega \wedge A_3 \in S_\omega \Rightarrow \exists n \exists \Gamma (\Gamma \subset S_n \wedge \Gamma \vdash A_1 \wedge \Gamma \vdash A_2 \wedge \Gamma \vdash A_3)$$

$$\text{dest share}(q_1, q_2) \text{ as } (n', \Gamma', f', p_1, p_2) \text{ in}$$

$$\text{dest share}((n', \Gamma', f', p_2), (n, \Gamma, f, p_3))$$

$$\text{share}_3 (q_1, q_2, (n, \Gamma, f, p_3)) \quad \triangleq \quad \begin{array}{l} \text{as } (n'', \Gamma'', f'', p'_2, p_3) \\ \text{in } (n'', \Gamma'', f'', \text{weak}(incl'_1^{\Gamma, \Gamma}, p_1), p'_2, p_3) \end{array}$$

Truth for disjunction being defined by

$$M \Vdash_{\sigma} A_1 A_2 \triangleq M \Vdash_{\sigma} A_1 \lor M \Vdash_{\sigma} A_2$$

we show the extended reification below where case does a case analysis on the form $inj_1(m)$ or $inj_2(m)$ of a proof of disjunction in the typed $\lambda$-calculus which we use to represent our metalanguage.

$$\downarrow_{\sigma}^{A} : \quad M_0 \Vdash_{\sigma} A \quad \Rightarrow \quad A[\sigma] \in S_{\omega}$$

$$\downarrow_{\sigma}^{P(\bar{i})} : \quad m \quad \triangleq \quad m$$

$$\downarrow_{\sigma}^{\dot{\wedge}} : \quad m \quad \triangleq \quad B\dot{O}T(m)$$

$$\downarrow_{\sigma}^{A \Rightarrow B} : \quad m \quad \triangleq \quad A\dot{X}_{A[\sigma]} \Rightarrow B[\sigma] (kont'_{\sigma}^{A \Rightarrow B}(m))$$

$$\downarrow_{\sigma}^{\forall x A} : \quad m \quad \triangleq \quad AP\dot{P} \Rightarrow (A\dot{X}_{(\forall x A)[\sigma]} \downarrow_{\sigma, x \leftarrow x_n}^{A} (m x_n)) \text{ where } 2n = [\dot{\forall} x A][\sigma]$$

$$\downarrow_{\sigma}^{A_1 \wedge A_2} : \quad (m_1, m_2) \quad \triangleq \quad PAIR (\downarrow_{\sigma}^{A_1} m_1, \downarrow_{\sigma}^{A_2} m_2)$$

$$\downarrow_{\sigma}^{A_1 \vee A_2} : \quad m \quad \triangleq \quad \begin{array}{l} \text{case } m \text{ of } [inj_1(m_1) \mapsto I\acute{N}J_1(\downarrow_{\sigma}^{A_1} m_1) \\ \qquad \downarrow \quad \downarrow] \\ \text{in } inj_2(m_2) \mapsto I\acute{N}J_2(\downarrow_{\sigma}^{A_2} m_2)] \end{array}$$

Note that this extended reification is unchanged except for the replacement of $kont'_{\sigma}^{A \Rightarrow B}$ by $kont'_{\sigma}^{A \Rightarrow B}$ so as to take into account the use of KONT in $\uparrow'$:

$$kont'_{\sigma}^{A \Rightarrow B}(m)(r) \triangleq (\uparrow'_{\sigma}^{A}(P\acute{R}OJ_{1} \stackrel{\rightarrow}{\Rightarrow} (r))) (m' \mapsto \text{flush } (AP\dot{P} \Rightarrow (P\acute{R}OJ_{2} \stackrel{\rightarrow}{\Rightarrow} (r), \downarrow_{\sigma}^{B} (mm'))))$$

Before giving the modified reflection proof, we need to prove a form of ex falso quodlibet deriving the truth of any formula A from any inconsistency $T_0, \dot{\Gamma}A_0 \vdash \dot{\Gamma}$. This is a standard proof by induction on A:

$$EFQ_{\sigma}^{A} : \quad T_0, \dot{\Gamma}A_0 \vdash \dot{\Gamma} \quad \Rightarrow \quad M_0 \Vdash_{\sigma} A$$

$$EFQ_{\sigma}^{P(\bar{i})} : \quad (\Gamma, g, p) \quad \triangleq \quad (0, (\Gamma, \dot{\Gamma}A_0), I_0(g), efq p)$$

$$EFQ_{\sigma}^{\perp} : \quad (\Gamma, g, p) \quad \triangleq \quad (\Gamma, g, p)$$

$$EFQ_{\sigma}^{A \Rightarrow B} : \quad (\Gamma, g, p) \quad \triangleq \quad m \mapsto EFQ_{\sigma}^{B}(\Gamma, g, p)$$

$$EFQ_{\sigma}^{\forall x A} : \quad (\Gamma, g, p) \quad \triangleq \quad t \mapsto EFQ_{\sigma, x \leftarrow t}^{A}(\Gamma, g, p)$$

$$EFQ_{\sigma}^{A_1 \wedge A_2} : \quad (\Gamma, g, p) \quad \triangleq \quad (EFQ_{\sigma}^{A_1}(\Gamma, g, p), EFQ_{\sigma}^{A_2}(\Gamma, g, p))$$

$$EFQ_{\sigma}^{\dot{A} \wedge A_2} : \quad (\Gamma, g, p) \quad \triangleq \quad inj_1(EFQ_{\sigma}^{A_1}(\Gamma, g, p))$$
which is in turn required to prove our specific version of DNS$^>$, itself used to prove reflection for the connective $\Rightarrow$, as well as to prove classic$_0$ and init$_0$.

## 2.7. About the logical strength of completeness in the presence of disjunction.

Kirst [58, Fact 7.36] proved in the context of intuitionistic propositional epistemic logic that completeness with respect to (non-exploding) Kripke semantics implies the following classical principle:

$$ \neg\neg\forall n (\neg\mathcal{A}(n) \lor \neg\neg\mathcal{A}(n)) $$

which in turn is equivalent to the following instance of DNS$_\perp^\gamma$ for disjunctions:

$$ \mathbf{DDNS} \quad \forall n \neg\neg (\neg\mathcal{A}(n) \lor \neg\mathcal{B}(n)) \Rightarrow \neg\neg\forall n (\neg\mathcal{A}(n) \lor \neg\mathcal{B}(n)) $$

In private communication, Kirst even showed that DDNS is enough, showing that it is exactly the extra bit of classical reasoning needed to handle disjunction in a constructive metalanguage (in the case of intuitionistic propositional epistemic logic).

Kirst's proof$^{31}$ can be adapted to the case of completeness of classical logic with respect to non-exploding Tarski semantics. We give here a variant of his proof showing that completeness in the presence of $\Rightarrow$, $\vec{\lor}$ and $\perp$ relative to enumerable theories and a $\Sigma_1^0$ exploding interpretation of $\perp$ implies the following generalised$^{32 33}$ form of DDNS for $\mathcal{A}$, $\mathcal{B}$ and $C$ $\Sigma_0^1$-formulas and for $\mathcal{D}$ ranging over $\Sigma_0^1$-formulas too:

$$ \mathbf{DDNS}_C \quad \forall n \neg_C (\forall \mathcal{D} \neg_D (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))) \Rightarrow \neg_C (\forall \mathcal{D} \neg_D \forall n (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))) $$
where $\neg_F \mathcal{E}$ abbreviates $\mathcal{E} \Rightarrow \mathcal{F}$.

Indeed, take a language with families of atoms $X_n$ and $Y_n$, and consider the theory $\mathcal{T}$ made of $\dot{X}_n \ \dot{\vee} \ \dot{Y}_n$ for each $n$, as well as $X_n$ for each $n$ such that $\mathcal{A}(n)$, and $Y_n$ for each $n$ such that $\mathcal{B}(n)$. The idea of the proof is that $\forall \mathcal{D} \neg_D \forall n (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))$ implies$^{34}$ $\mathcal{T} \models \perp$, which implies $\Gamma \vdash \perp$ for a finite subset $\Gamma$ of $\mathcal{T}$ by completeness, which implies in turn $\Gamma \models \perp$ by soundness. Now, by taking the exploding model $M_{\text{std}}$ interpreting $X_n$ by $\mathcal{A}(n)$, $Y_n$ by $\mathcal{B}(n)$ and $\perp$ by $C$, the final goal $C$, that is $M_{\text{std}} \models \perp$, can eventually be obtained by proving $M_{\text{std}} \models \mathcal{T}$, that is, $M_{\text{std}} \models \dot{X}_n \ \dot{\vee} \ \dot{Y}_n$, that is $\neg_C \mathcal{A}(n) \lor \neg_C \mathcal{B}(n)$, for only those finite number of $\dot{X}_n \ \dot{\vee} \ \dot{Y}_n$ in $\Gamma$. The latter can be obtained by first chaining a finite number of instances of $\forall n \neg_C \neg_C (\neg_C \mathcal{A}(n) \lor \neg_C \mathcal{B}(n))$, each of them coming by instantiating $\mathcal{D}$ with $C$ in $\forall n \neg_C \forall \mathcal{D} \neg_D (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))$ for the corresponding $n$'s.

The conjunction of facts that $\mathbf{DDNS}_C$ is provable from completeness with possibly-exploding semantics, that it is equivalent to $\mathbf{DDNS}_\perp$ in the presence of Markov's principle, that Markov's principle is the principle needed to handle falsity in a non-exploding

<footnote>$^{31}$A variant of his original proof directly proving DDNS from the completeness of bi-intuitionistic logic with respect to its Kripke semantics can be found in [77].</footnote>

<footnote>$^{32}$Like in the case of DNS$^\gamma$, $\mathbf{DDNS}_C$ is useful to reason in the absence of Markov's principle but is equivalent to DDNS in the presence of Markov's principle.</footnote>

<footnote>$^{33}$Using conjunction, $\mathbf{DDNS}_C$ can be equivalently stated as $\forall n \neg_C (\mathcal{A}(n) \land \mathcal{B}(n)) \Rightarrow \neg_C (\forall \mathcal{D} \neg_D \forall n (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n)))$.</footnote>

<footnote>$^{34}$Indeed, assuming a model of $\mathcal{T}$ interpreting the atoms $X_n$ and $Y_n$ by some predicates $\mathcal{X}$ and $\mathcal{Y}$ respectively, as well as $\perp$ by some $\Sigma_1^0$ proposition $\mathcal{Z}$, then, the truth of $X_n$ whenever $\mathcal{A}(n)$ implies $\neg_Z X(n) \Rightarrow \neg_Z \mathcal{A}(n)$, and, similarly $\neg_Z Y(n) \Rightarrow \neg_Z \mathcal{B}(n)$. Moreover, the truth of $\dot{X}_n \ \dot{\vee} \ \dot{Y}_n$ for each $n$ implies $\neg_Z X(n) \lor \neg_Z Y(n)$, thus $\neg_Z \mathcal{A}(n) \lor \neg_Z \mathcal{B}(n)$ for each $n$. We then get $\mathcal{Z}$ by the initial hypothesis $\forall \mathcal{D} \neg_D \forall n (\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))$. Remark that restricting the interpretation of $\perp$ to $\Sigma_1^0$ propositions is actually not a restriction since the syntactic model in Henkin's proof for enumerable theory $\mathcal{U}$ and conclusion A precisely interprets $\perp$ by $\mathcal{U}$, $\dot{A} \vdash \perp$ which is $\Sigma_1^0$ and because, by composition with soundness, completeness is equivalent to its restriction to the syntactic model.</footnote>
semantics and that Kirst showed that nothing more is needed to handle both falsity and disjunction suggests that $DDNS_C$ is exactly the amount of classical reasoning needed to handle disjunction in the presence of a possibly-exploding interpretation of falsity.

Even though our proof of completeness with respect to possibly-exploding models in the presence of disjunction uses a priori the full generality of $DNS_C^\nabla$ for $\exists$-free formulae, we conjecture that it could be obtained using $DDNS_C$ instead of $DNS_C^\nabla$, that is, we conjecture that either $DNS_C^\nabla$ for $\exists$-free formulae derives from $DDNS$ or that the completeness proof can be modified to depend only on $DDNS_C$.

Two other recent lines of research about the logical strength of completeness with disjunction are Krivtsov [68] and Espíndola [24, 25]. Krivtsov showed that with respect to exploding models$^{35}$ Gödel's completeness for recursively enumerable theories is equivalent to the Weak Fan Theorem (WFT) over a rather weak intuitionistic arithmetic. This is to be compared to Veldman's proof of completeness with respect to Kripke semantics [84] which already required WFT. Since WFT is classically equivalent to Weak Kőnig's Lemma, this is also to be compared to the equivalence of Gödel's completeness with Weak Kőnig's Lemma over a weak arithmetic with recursive comprehension in the classical reverse mathematics of the subsystems of second-order arithmetic [78]. On his side, reasoning in the language of topos theory, Espíndola proved the same result in IZF, where WFT was formulated as the compactness of the Cantor space.

The situation regarding WFT is rather subtle as there are different formulations depending on how infinite paths are represented in a binary tree (see [13]). Let us call $WFT_{pred}$ the intuitionistically provable$^{36}$ variant of WFT where infinite paths are represented using a predicate and $WFT_{dec}$ the weakly classical variant$^{37}$ where infinite paths are represented using a decidable predicate. Both Krivtsov and Espíndola's results refer to $WFT_{dec}$. On the other side, Krivine's proof and our own proof for the language without disjunction are intuitionistic and thus do not require $WFT_{dec}$. This is consistent with another result of Espíndola with Forssell [25, 27] showing that $WFT_{dec}$ is not needed on top of IZF to prove completeness with respect to exploding Kripke semantics in the absence of disjunction. And indeed, in IZF, like in second-order intuitionistic arithmetic where Krivine and us are reasoning, $WFT_{pred}$ is provable (if we had instead reasoned in a weaker arithmetic, we would certainly have explicitly needed $WFT_{pred}$, the same way as Weak Kőnig's Lemma was needed in [78]). Moreover, this is consistent with yet another result, namely the formal equivalence between $WFT_{pred}$ and completeness with respect to Scott entailment relations in [13]. In turn, we conjecture that $WFT_{dec}$, thus completeness with respect to exploding models and all connectives, disjunction included, is equivalent to $WFT_{pred}$ together with $DDNS_C$.

To conclude, note also that like Markov's principle, $DNS_C^\nabla$ and thus $DDNS_C$ as well preserve the witness and disjunction properties of intuitionistic logic, so they are in this sense intuitionistically valid. Also, to compute with $DNS_C^\nabla$, bar recursion [80] or delimited continuations [51] can be used.

**2.8. Extension to existential quantification.** The situation for existential quantification is simpler than for disjunction and modifying the statement of reflection is not

<footnote>$^{35}$Krivtsov calls such models intuitionistic structures.</footnote>

<footnote>$^{36}$See a proof relying on intuitionistic $ACA_0$ in the Coq standard library [18, WeakFan.v].</footnote>

<footnote>$^{37}$See Berger [9] who identifies the classical part of (a functional form of) WFT as a principle called $L_{fan}$.</footnote>
necessary. The idea is to consider an enumeration of formulae which takes existen-
tial formulae into account, then to add a clause to the definition of Γ ⊂ S<sub>n</sub> similar to
the one for universal quantification, using Henkin's axiom ∃y A(y) ⇄ A(x) for x taken
fresh in the finite set of formulae coming before ∃y A(y) in the enumeration<sup>38</sup>. Reifi-
cation is direct, using the witness coming from the proof of truth as a witness for the
proof of derivability. For reflection, the idea is to combine a proof of (∃y A)[σ] ∈ S<sub>ω</sub>
with the proof of (∃y A)[σ] ⇄ A[σ, y ← x] available at some level S<sub>n</sub> to get a proof of
A[σ, y ← x] ∈ S<sub>ω</sub>, then a proof of M ⊑<sub>σ,y←x</sub> A, thus a proof<sup>39</sup> of M ⊑<sub>σ</sub><sup>e</sup> ∃y A.

REFERENCES

[1] ANDREAS ABEL and CHRISTIAN SATTLER, *Normalization by evaluation for call-by-push-value and polarized lambda calculus*, *Proceedings of the 21st international symposium on principles and practice of declarative programming* (New York, NY, USA), PPDP '19, Association for Computing Machinery, 2019.

[2] THORSTEN ALTENKIRCH, PETER DYBJER, MARTIN HOFMANN, and PHILIP J. SCOTT, *Normalization by evaluation for typed lambda calculus with coproducts*, *Lics '01: Proceedings of the 16th annual ieee symposium on logic in computer science* (Washington, DC, USA), IEEE Computer Society, 2001, pp. 303–310.

[3] THORSTEN ALTENKIRCH, MARTIN HOFMANN, and THOMAS STREICHER, *Reduction-free normalisation for a polymorphic system*, *Proceedings, 11th annual IEEE symposium on logic in computer science, new brunswick, new jersey, usa, July 27-30, 1996*, 1996, pp. 98–106.

[4] ZENA M. ARIOLA and HUGO HERBELIN, *Minimal classical logic and control operators*, *Thirtieth international colloquium on automata, languages and programming, ICALP'03, eindhoven, the netherlands, June 30 - July 4, 2003*, Lecture Notes in Computer Science, vol. 2719, Springer-Verlag, 2003, pp. 871–885.

[5] ANDREA ASPERTI, WILMER RICCIOTTI, CLAUDIO SACERDOTI COEN, and ENRICO TASSI, *Formal metatheory of programming languages in the Matita interactive theorem prover*, *J. Autom. Reasoning*, vol. 49 (2012), no. 3, pp. 427–451.

[6] JON BARWISE, *An introduction to first-order logic*, *Handbook of mathematical logic* (Jon Barwise, editor), Studies in Logic and The Foundations of Mathematics, vol. 90, Elsevier, 1977, pp. 5–46.

[7] STEFANO BERARDI, *Intuitionistic completeness for first order classical logic*, *J. Symb. Log.*, vol. 64 (1999), no. 1, pp. 304–312.

[8] STEFANO BERARDI and SILVIO VALENTINI, *Krivine's intuitionistic proof of classical completeness (for countable languages)*, *Ann. Pure Appl. Logic*, vol. 129 (2004), no. 1-3, pp. 93–106.

[9] JOSEF BERGER, *A decomposition of Brouwer's fan theorem*, *J. Logic & Analysis*, vol. 1 (2009).

[10] ULRICH BERGER and HELMUT SCHWICHTENBERG, *An inverse of the evaluation functional for typed lambda-calculus*, *Proceedings, sixth annual ieee symposium on logic in computer science, 15-18 July, 1991, Amsterdam, the Netherlands*, IEEE Computer Society, 1991, pp. 203–211.

[11] EVERT WILLEM BETH, *Semantic entailment and formal derivability*, *Meded. Kon. Ned. Akad. Weten-schappen, Afd. Letterhunde, N.R.*, vol. 18 (1955), pp. 309–342.

[12] JASMIN CHRISTIAN BLANCHETTE, ANDREI POPESCU, and MITRIY TRAYTEL, *Unified classical logic completeness, Automated reasoning* (Cham) (Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors), Springer International Publishing, 2014, pp. 46–60.

[13] NURIA BREDE and HUGO HERBELIN, *On the logical structure of choice and bar induction principles*, LICS, IEEE, 2021, pp. 1–13.

[14] SAMUEL R. BUSS, *An introduction to proof theory*, *Handbook of proof theory* (Samuel R. Buss, editor), North-Holland, North-Holland, 1998, pp. 1–78.

<footnote n="38"><sup>38</sup>If universal quantification is present among the connectives, we can also reuse Henkin's axiom
$\vdash_A A(x) \dashv \dot{\forall} y \dashv A(y)$ up to some extra classical reasoning in the object language.</footnote>

<footnote n="39">³⁹One may wonder if the ability to extend Henkin’s proof to existential quantification without modifying the statement of reflection is compatible with the ability to encode A ∨ B as an existential formula ∃b ((b = 0 ⇔ A) ∧ (b = 1 ⇔ B)) in any signature containing symbols 0 and 1. The point is, that to justify this encoding, we still need to do a case analysis on the value of b to determine which of the conjunct we may use in (b = 0 ⇔ A) ∧ (b = 1 ⇔ B). This typically requires an axiom of the form b = 0 ∨ b = 1, which moves us back to a situation where ∨ is actually already part of the language.</footnote>
[15] ALONZO CHURCH, *Introduction to mathematical logic*, vol. 1, The Princeton University Press, 1956.

[16] THE COQ DEVELOPMENT TEAM, *The Coq reference manual, version 8.9*, October 2019, Distributed electronically at http://coq.inria.fr/doc.

[17] ——, *The Coq reference manual, version 8.15*, December 2021, Distributed electronically at http://coq.inria.fr/refman.

[18] ——, *The Coq standard library, version 8.15, Technical report*, November 2022, Distributed electronically at http://coq.inria.fr/distrib/current/stdlib.

[19] CATARINA COQUAND, *A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions*, *Higher Order Symbol. Comput.*, vol. 15 (2002), no. 1, pp. 57–90.

[20] THIERRY COQUAND and PETER DYBJER, *Intuitionistic model constructions and normalization proofs, Mathematical Structures in Computer Science*, vol. 7 (1997), no. 1, pp. 75–94.

[21] THIERRY COQUAND and CHRISTINE PAULIN-MOHRING, *Inductively defined types, Proceedings of colog '88* (P. Martin-Löf and G. Mints, editors), Lecture Notes in Computer Science, vol. 417, Springer-Verlag, 1990.

[22] THIERRY COQUAND and JAN M. SMITH, *An application of constructive completeness, TYPES*, Lecture Notes in Computer Science, vol. 1158, Springer, 1995, pp. 76–84.

[23] OLIVIER DANVY, *Type-directed partial evaluation, Popl*, 1996, pp. 242–257.

[24] CHRISTIAN ESPÍNDOLA, *Achieving completeness: from constructive set theory to large cardinals, Ph.D. thesis*, Stockholm University, 2016.

[25] ——, *Semantic completeness of first-order theories in constructive reverse mathematics, Notre Dame J. Formal Logic*, vol. 57 (2016), no. 2, pp. 281–286.

[26] Solomon Feferman, John W. Dawson Jr, Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort (editors), *Kurt gödel: Collected works. vol. 1: Publications 1929-1936*, Oxford University Press, New York, 1986.

[27] HENRIK FORSSELL and CHRISTIAN ESPÍNDOLA, *Constructive completeness and non-discrete languages*, 2017.

[28] YANNICK FORSTER, DOMINIK KIRST, and DOMINIK WEHR, *Completeness theorems for first-order logic analysed in constructive type theory*, LFCS, Lecture Notes in Computer Science, vol. 11972, Springer, 2020, pp. 47–74.

[29] YANNICK FORSTER, DOMINIK KIRST, and DOMINIK WEHR, *Completeness theorems for first-order logic analysed in constructive type theory: Extended version, Journal of Logic and Computation*, vol. 31 (2021), no. 1, pp. 112–151.

[30] GOTTLOB FREGE, *Begriffschrift, eine der arithmetischen nachgebildete formelsprache des reinen denkens*, Halle, 1879, English translation e.g. in [31] or [83].

[31] ——, *Begriffschrift, eine der arithmetischen nachgebildete formelsprache des reinen denkens*, Halle, 1879, English translation e.g. in [83].

[32] HARVEY FRIEDMAN, *Intuitionistic completeness of heying's predicate calculus, Notices of the American Mathematical Society*, vol. 22 (1975), pp. A-64-8.

[33] ——, *Classically and intuitionistically provably recursive functions, Higher set theory* (D. S. Scott and G. H. Muller, editors), Lecture Notes in Mathematics, vol. 669, Springer, Berlin/Heidelberg, 1978, pp. 21–27.

[34] GERHARD GENTZEN, *Untersuchungen über das logische Schließen, Mathematische Zeitschrift*, vol. 39 (1935), pp. 176–210, 405–431, English Translation in [81], “Investigations into logical deduction”, pages 68-131.

[35] KURT GÖDEL, *Über die vollständigkeit des logikkalküls, Doctoral thesis*, University of Vienna, 1929, English translation in [83] or [26].

[36] ——, *Die vollständigkeit des axiome des logischen functionenkalküls, Monatshefte für Mathematik und Physik*, vol. 37 (1930), pp. 349–360, Reprinted in [26].

[37] ——, *Über formal unentscheidbare sätze der principia mathematica und verwandter systeme, Monatshefte für Mathematik und Physik*, vol. 38 (1931), pp. 173–198.

[38] TIMOTHY G. GRIFFIN, *The formulae-as-types notion of control, Conf. record 17th annual ACM symp. on principles of programming languages, POPL '90, san francisco, CA, USA, 17-19 jan 1990*, ACM Press, New York, 1990, pp. 47–57.

[39] GISBERT HASENJAEGER, *Eine bemerkung zu henkin's beweis für die vollständigkeit des prädikatenkalküls der ersten stufe*, this JOURNAL, (1953), p. 18:42–48.

[40] LEON HENKIN, *The completeness of the first-order functional calculus, J. Symb. Log.*, vol. 14 (1949), no. 3, pp. 159–166.
[41] ——, *The discovery of my completeness proofs, The Bulletin of Symbolic Logic*, vol. 2 (1996), no. 2, pp. 127–158.

[42] HUGO HERBELIN, *An intuitionistic logic that proves Markov's principle, Proceedings of the 25th annual ieee symposium on logic in computer science, lics 2010, 11-14 july 2010, edinburgh, united kingdom*, IEEE Computer Society, 2010, pp. 50–56.

[43] HUGO HERBELIN and GYESIK LEE, *Forcing-based cut-elimination for gentzen-style intuitionistic sequent calculus, Logic, language, information and computation, 16th international workshop, wollic 2009, tokyo, japan, june 21-25, 2009, proceedings* (Hiroakira Ono, Makoto Kanazama, and Ruy de Queiroz, editors), Lecture Notes in Computer Science, vol. 5514, Springer, 2009, pp. 209–217.

[44] OLIVIER HERMANT, *Semantic cut elimination in the intuitionistic sequent calculus, Typed lambda calculi and applications, 7th international conference, TLCA 2005, nara, japan, april 21-23, 2005, proceedings* (Paweł Urzyczyn, editor), Lecture Notes in Computer Science, vol. 3461, Springer, 2005, pp. 221–233.

[45] OLIVIER HERMANT and JAMES LIPTON, *Completeness and cut-elimination in the intuitionistic theory of types - part 2, J. Log. Comput.*, vol. 20 (2010), no. 2, pp. 597–602.

[46] DAVID HILBERT and WILHEM ACKERMANN, *Grundzüge der theoretischen logik*, Springer Verlag, Berlin, 1928, English translation of the 1938 edition in [47].

[47] ——, *Principles of mathematical logic*, Oxford University Press, New York, 1928.

[48] JAAKKO HINTIKKA, *Form and content in quantification theory, Acta Philosophica Fennica*, vol. 8 (1955), pp. 11–55.

[49] ——, *Notes on the quantification theory, Societas Scientiarum Fennica, Commentationes physico-mathematicae*, vol. 17 (1955), no. 1.

[50] DANKO ILIK, *Constructive ultrafilter theorem and completeness for classical predicate logic (formalisation)*, https://iaddg.net/danko/boolean_completeness.zip, 2008.

[51] ——, *Delimited control operators prove double-negation shift, Annals of Pure and Applied Logic*, vol. 163 (2011), no. 11, pp. 1549–1559, In press.

[52] ——, *Continuation-passing style models complete for intuitionistic logic, Annals of Pure and Applied Logic*, vol. 164 (2013), no. 6, pp. 651–662.

[53] DANKO ILIK, GYESIK LEE, and HUGO HERBELIN, *Kripke models for classical logic, Annals of Pure and Applied Logic*, vol. 161 (2010), no. 11, pp. 1367–1378, Special Issue on Classical Logic and Computation.

[54] STANASLAW JAŠKOWSKI, *On the rules of suppositions in formal logic, Studia Logica*, vol. 1 (1934), pp. 5–32, Reprinted in S. McCall (1967) Polish Logic 1920-1939, Oxford: Oxford Univ. Press, pp. 232–258.

[55] THOMAS J. JECH, *The axiom of choice*, Dover Books on Mathematics Series, Courier corporation, 1973.

[56] INGEBRIGT JOHANSSON, *Der minimalkalkül, ein reduzierter intuitionistischer formalismus, Compositio Mathematica*, vol. 4 (1937), pp. 119–136.

[57] STIG KANGER, *Provability in logic*, Acta Universitatis Stockholmiensis, Stockholm, Almqvist & Wiksell, 1957.

[58] DOMINIK KIRST, *Mechanised metamathematics: An investigation of first-order logic and set theory in constructive type theory, Ph.D. thesis*, University of Sarrbrücken, 2023, private communication.

[59] STEPHEN C. KLEENE, *Recursive functions and intuitionistic mathematics, Proceedings of the international congress of mathemaiticans* (L.M. Graves, E. Hille, P.A. Smith, and O. Zariski, editors), Cambridge, Mass., August 1950, p. 679–685.

[60] GEORG KREISEL, *Mathematical significance of consistency proofs*, this JOURNAL, vol. 23 (1958), no. 2, pp. 155–182.

[61] ——, *On weak completeness of intuitionistic predicate logic, J. Symb. Log.*, vol. 27 (1962), no. 2, pp. 139–158.

[62] JEAN-LOUIS KRIVINE, *Lambda-calcul, types et modèles*, Masson, Paris, 1990.

[63] JEAN-LOUIS KRIVINE, *Opérateurs de mise en mémoire et traduction de gödel, Archive for Mathematical Logic*, vol. 30 (1990), no. 4, pp. 241–267 (French).

[64] JEAN-LOUIS KRIVINE, *Lambda-calculus, types and models*, Ellis Horwood, 1993.

[65] JEAN-LOUIS KRIVINE, *Classical logic, storage operators and second-order lambda-calculus, Ann. Pure Appl. Logic*, vol. 68 (1994), no. 1, pp. 53–78.

[66] JEAN-LOUIS KRIVINE, *Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, The Bulletin of Symbolic Logic*, vol. 2 (1996), no. 4, pp. 405–421.

[67] VICTOR N. KRIVTSOV, *An intuitionistic completeness theorem for classical predicate logic, Studia Logica: An International Journal for Symbolic Logic*, vol. 96 (2010), no. 1, pp. 109–115.
[68] ——, *Semantical completeness of first-order predicate logic and the weak fan theorem*, *Studia Logica*, vol. 103 (2015), no. 3, pp. 623–638.

[69] PER MARTIN-LÖF, *An intuitionistic theory of types, predicative part*, *Logic colloquium*, North Holland, 1975, pp. 73–118.

[70] CHARLES MCCARTY, *Completeness and incompleteness for intuitionistic logic*, this JOURNAL, vol. 73 (2008), no. 4.

[71] MITSUHIRO OKADA, *A uniform semantic proof for cut-elimination and completeness of various first and higher order logics*, *Theor. Comput. Sci.*, vol. 281 (2002), no. 1-2, pp. 471–498.

[72] MICHEL PARIGOT, *Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction*, *Logic programming and automated reasoning: International conference Ipar '92 proceedings*, st. peters-burg, russia, Springer-Verlag, 1992, pp. 190–201.

[73] HELENA RASIOWA and ROMAN SIKORSKI, *A proof of the completeness theorem of grödel.*, *Fundamenta Mathematicae*, vol. 37 (1950), no. 1, pp. 193–200.

[74] GIOVANNI SAMBIN, *Pretopologies and completeness proofs*, *J. Symb. Log.*, vol. 60 (1995), no. 3, pp. 861–878.

[75] HELMUT SCHWICHTENBERG and STANLEY S. WAINER, *Proofs and computations*, Cambridge University Press, 2011.

[76] KURT SCHÜTTE, *Ein system des verknüpfenden schliessens, Archiv für mathematische Logik und Grundlagenforschung*, vol. 2 (1956), no. 2-4, pp. 55–67 (German).

[77] IAN SHILLITO and DOMINIK KIRST, *A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic*, *Proceedings of the 13th ACM SIGPLAN international conference on certified programs and proofs, CPP 2024, London, UK, January 15-16, 2024* (Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors), ACM, 2024, pp. 218–229.

[78] STEPHEN G. SIMPSON, *Subsystems of second order arithmetic*, Springer seminars in immunopathology, Springer, 1999.

[79] RAYMOND M. SMULLYAN, *First-order logic*, Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 43, Springer-Verlag New York, Inc., New York, 1968.

[80] CLIFFORD SPECTOR, *Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics, Recursive function theory: Proceedings of symposia in pure mathematics* (Providence, Rhode Island) (F. D. E. Dekker, editor), vol. 5, American Mathematical Society, 1962, p. 1–27.

[81] Manfred E. Szabo (editor), *The collected works of gerhard gentzen*, North Holland, Amsterdam, 1969.

[82] ANNE S. TROELSTRA, *Metamathematical investigation of intuitionistic arithmetic and analysis*, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.

[83] Jean van Heijenoort (editor), *From frege to gödel, a source book in mathematical logic, 1879-1931*, Harvard University Press, New York, 1967.

[84] WIM VELDMAN, *An intuitionistic completeness theorem for intuitionistic predicate logic*, *J. Symb. Log.*, vol. 41 (1976), no. 1, pp. 159–166.

IRIF, CNRS, INRIA, UNIVERSITÉ PARIS CITÉ

E-mail: Hugo.Herbelin@inria.fr

CNES, FRANCE

E-mail: dankoilik@gmail.com