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 [Reference Gödel36] as an answer to a question raised by Hilbert and Ackermann in 1928 [Reference Hilbert and Ackermann47], 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 setFootnote ¹ ${\mathcal {F}\!un}$ of function symbols, each of them coming with an arity, as well as of a set $\mathcal {P}\!red$ 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:

$$ \begin{align*}\begin{array}{lll} t & ::= & x ~\mid~ f(t_1,...,t_{a_f}).\\ \end{array} \end{align*} $$

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

$$ \begin{align*}\begin{array}{lll} A & ::= & P(t_1,...,t_{P_f}) ~\mid~ \dot{\bot} ~\mid~ A \,\dot{\Rightarrow}\, A ~\mid~ \dot{\forall} x\,A.\\ \end{array} \end{align*} $$

Note that in classical first-order logic, the language of negativeFootnote ² connectives and quantifiers made of $\,\dot{\Rightarrow }\,$ , $\dot{\forall }$ and $\dot{\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 $\dot{\bot }$ as a primitive connective and this allows to express consistency of the object logic as the non-provability of $\dot{\bot }$ . Negation can then be defined as $\dot{\neg } A \triangleq A \,\dot{\Rightarrow }\, \dot{\bot }$ . Also, in $\dot{\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 $\dot{\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:

$$ \begin{align*}\begin{array}{lll} \Gamma & ::= & \epsilon ~\mid~ \Gamma, A.\\ \end{array} \end{align*} $$

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 [Reference Frege31] or in Hilbert and Ackermann [Reference Hilbert and Ackermann47], or one of the systems, such as Gentzen–Jaśkowski’s natural deduction [Reference Gentzen35, Reference Jaškowski56] or Gentzen’s sequent calculus [Reference Gentzen35], 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}} \vDash _{\sigma } A$ for the statement expressing that A is true in the model $\mathcal {M}$ (to be defined in Section 1.4). Validity of A under assumptions $\Gamma $ , written $\Gamma \vDash A$ is defined to be $\forall \mathcal {M}\;\forall \sigma \;({\mathcal {M}} \vDash _{\sigma } \Gamma \Rightarrow {\mathcal {M}} \vDash _{\sigma } A),$ where ${\mathcal {M}} \vDash _{\sigma } \Gamma $ is the conjunction of all ${\mathcal {M}} \vDash _{\sigma } B$ for every B in $\Gamma $ , i.e., $\bigwedge _{B\in \Gamma } {\mathcal {M}} \vDash _{\sigma } B$ . Note that $\Rightarrow $ , $\forall $ , $\wedge $ and, later on, below, $\lor $ , $\exists $ , $\bot $ , as well as derived $\neg $ , represent the connectives and quantifiers of the metalanguage.

We say that $\Gamma $ is inconsistent if $\Gamma \vdash \dot{\bot }$ and consistent if $\Gamma \not \vdash \dot{\bot }$ , i.e., if $(\Gamma \vdash \dot{\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 $\mathcal {M}$ and $\sigma $ such that ${\mathcal {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:

$$ \begin{align*}\begin{array}{ll} C1. & \vDash A ~\Rightarrow~ \vdash A.\\ C2. & \Gamma\text{ is consistent} ~\Rightarrow~ \Gamma\text{ has a model}.\\ C3. & \Gamma,\neg A\text{ has a model} ~\lor~ \Gamma \vdash A.\\ \end{array} \end{align*} $$

1.2 Weak and strong completeness

In a strong form, referred to as strong completeness,Footnote ³ 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 [Reference Gödel37], 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 $\mathcal {M} \vDash _\sigma \mathcal {T}$ be $\forall B\in \mathcal {T}\,{\mathcal {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:

$$ \begin{align*}\begin{array}{ll} S1. & \mathcal{T} \vDash A ~\Rightarrow~\mathcal{T} \vdash A.\\ S2. & \mathcal{T}\text{ is consistent} ~\Rightarrow~ \mathcal{T}\text{ has a model}.\\ S3. & \mathcal{T} \cup \{\neg A\}\text{ has a model} ~\lor~ \mathcal{T} \vdash A.\\ \end{array} \end{align*} $$

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

1.3 Standard existing proofs of completeness

Let us list a few traditional proofs from the classic literature.Footnote ⁴

• • Gödel’s original proof [Reference Gödel36] 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. The base case of the induction uses classical logic and Kőnig’s lemma.

• • Henkin’s proof [Reference Henkin41] 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 1950s, a new kind of proof independently credited to Beth [Reference Beth11], Hintikka [Reference Hintikka49, Reference Hintikka50], Kanger [Reference Kanger59] and Schütte [Reference Schwichtenberg and Wainer77] 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 1950s also, Rasiowa and Sikorski [Reference Rasiowa and Sikorski75] 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 article 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 {F}\!un}$ such that $\mathcal {F}(f) \in \mathcal {D}^{a_f} \rightarrow \mathcal {D}$ , where $\mathcal {D}^{a_f} \rightarrow \mathcal {D}$ denotes the set of functions of arity $a_f$ over $\mathcal {D}$ . Then, given an assignment $\sigma \in \mathcal {X} \rightarrow \mathcal {D}$ of the variables to arbitrary values of the domain, the interpretation of terms in $\mathcal {D}$ is given by

$$ \begin{align*} &[\![x]\!]^{\sigma}_{\mathcal{M}} \qquad\qquad\qquad \triangleq \quad \sigma(x),\\ &[\![f(t_1,\ldots,t_{a_f})]\!]^{\sigma}_{\mathcal{M}} \quad \ \triangleq \quad \mathcal{F}(f) ([\![t_1]\!]^{\sigma}_{\mathcal{M}}, \ldots, [\![t_{a_f}]\!]^{\sigma}_{\mathcal{M}}). \end{align*} $$

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 [Reference Barwise and Barwise6], the Handbook of Proof Theory [Reference Buss and Buss15] or in the original proof of Gödel [Reference Gödel36]. 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

  $$ \begin{align*}\mathcal{C}\mathit{lassic} ~\triangleq~ \{\dot{\neg} \dot{\neg} A \,\dot{\Rightarrow}\, A~|~A\in {\mathcal{F}\!orm}\}\end{align*} $$
  would be true in all models. On the other hand, in an intuitionistic metalanguage, a formula such as, say, $\dot{\neg }\dot{\neg } X \,\dot{\Rightarrow }\, X$ could not be proved true in all models.Footnote ⁵ In a strongly anti-classical intuitionistic metalanguage refuting double-negation elimination, it could even be proved that there are modelsFootnote ⁶ which refute $\dot{\neg }\dot{\neg } X \,\dot{\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 $\dot{\neg }\dot{\neg } X \,\dot{\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:

  $$ \begin{align*}\mathcal{T} \vDash A ~\triangleq ~ \forall \mathcal{M}\;\forall \sigma\;({\mathcal{M}} \vDash_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash_{\sigma} \mathcal{T}\Rightarrow {\mathcal{M}} \vDash_{\sigma} A).\end{align*} $$

• • 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 ${\mathcal {M}} \vDash _{\sigma } A$ as $\mathit {truth}_{\mathcal {M}}(A,\sigma ) = 1$ for the corresponding $\mathit {truth}$ function. This is the approach followed, e.g., in Rasiowa–Sikorski’s proof, or also, e.g., in [Reference Church16, Reference Simpson80], among others.Footnote ⁷ In particular, relying on a two-valued truth makes the theory $\mathcal {C}\mathit {lassic}$ automatically true.

  Depending on the metalanguage, a function from $\mathcal {F}\!orm$ to $\{0,1\}$ can itself be represented either as a functional relation, i.e., as a relation $\mathit {istrue}$ on $\mathcal {F}\!orm \times \{0,1\}$ such that for all A, there is a unique b such that $\mathit {istrue}(A,b)$ holds (this is the representation used, e.g., for the completeness proof in [Reference Simpson80]), 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 [Reference Troelstra84], or Martin-Löf’s type theory [Reference Coquand, Paulin-Mohring, Martin-Löf and Mints22, Reference Martin-Löf71]).

  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 ^0_1$ -separability, or equivalently, of Weak Kőnig’s Lemma [Reference Simpson80]. This implies that the corresponding $\mathit {truth}$ function is in general not recursive [Reference Kleene, Graves, Hille, Smith and Zariski61]. Expecting $\mathit {truth}$ to be definable primitively as a computable function to $\{0,1\}$ in an intuitionistic logic is thus hopeless, deciding whether it returns $0$ or $1$ would require classical logic. As for representing truth by a functional relation $\mathit {istrue}$ , the expected property $\mathit {istrue}(A,0) \lor \mathit {istrue}(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 [Reference Griffin39, Reference Krivine67, Reference Parigot74] 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.

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 definitionsFootnote ⁸ of validity and existence of a model:

$$ \begin{align*}\begin{array}{lll} \mathcal{T} \vDash A & \triangleq & \forall \mathcal{M}\, \forall \sigma\, ({\mathcal{M}} \vDash_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash_{\sigma} \mathcal{T} \Rightarrow {\mathcal{M}} \vDash_{\sigma} A)\\ \mathcal{T}\text{ has a model} & \triangleq & \exists \mathcal{M}\, \exists \sigma\, ({\mathcal{M}} \vDash_{\sigma} \mathcal{C}\mathit{lassic} \wedge {\mathcal{M}} \vDash_{\sigma} \mathcal{T}).\\ \end{array} \end{align*} $$

Two auxiliary choices of presentation of Tarski semantics can be made.Footnote ⁹

• • Recursively-defined truth. The approach followed, e.g., in the Handbook of Mathematical Logic [Reference Barwise and Barwise6] or the Handbook of Proof Theory [Reference Buss and Buss15] 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 {P}\!red$ 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:

  $$ \begin{align*}\begin{array}{lll} {\mathcal{M}} \vDash_{\sigma} P(t_1,\ldots,t_{a_f}) & \triangleq & ([\![t_1]\!]^{\sigma}_{\mathcal{M}}, \ldots, [\![t_{a_P}]\!]^{\sigma}_{\mathcal{M}}) \in \mathcal{P}(P)\\ {\mathcal{M}} \vDash_{\sigma} \dot{\bot} & \triangleq & \bot\\ {\mathcal{M}} \vDash_{\sigma} A \,\dot{\Rightarrow}\, B & \triangleq & {\mathcal{M}} \vDash_{\sigma} A \Rightarrow {\mathcal{M}} \vDash_{\sigma} B\\ {\mathcal{M}} \vDash_{\sigma} \dot{\forall} x\, A & \triangleq & \forall v\in\mathcal{D}\,{\mathcal{M}} \vDash_{\sigma\cup[x\leftarrow v]} A.\\ \end{array} \end{align*} $$

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

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 {F}\!un}$ to a function $\mathcal {F}(f) \in \mathcal {D}^{a_f} \rightarrow \mathcal {D}$ and $\mathcal {P}$ maps any symbol $P\in \mathcal {P}\!red$ to a set $\mathcal {P}(P) \subset \mathcal {D}^{a_P}$ .

1.5 Regarding the metalanguage as a formal system

Let M be the metalanguage in which completeness is stated and O be the object language used to represent provability in first-order logic. In 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 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 M into a proof of A expressed in the proof object language O (and conversely, 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 $\mathcal {T}$ is a proof in M of the universal closure of $(\forall B \in \mathcal {T} [\![B]\!]^{}_{}) \Rightarrow [\![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 $\mathcal {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 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.Footnote ¹⁰ Now, if the proofs of soundness and completeness are formalised in a metalanguage equipped with a normalisation procedure, e.g., in a $\lambda $ -calculus-based proofs-as-programs presentation of second-order arithmetic [Reference Krivine64; Reference Krivine66, Chapter 9], one gets an effective cut-elimination theorem, namely, an effective procedure which turns any non-necessarily-normal proof of $\Gamma \vdash A$ into a normal proof of $\Gamma \vdash 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 [Reference Berger and Schwichtenberg10] in the context of simply-typed $\lambda $ -calculus, it was studied for the realisability semantics of second-order implicative propositional logicFootnote ¹¹ by Altenkirch, Hofmann, and Streicher [Reference Altenkirch, Hofmann and Streicher3], for the realisability semantics of implicative propositional logic in Hilbert styleFootnote ¹² by T. Coquand and Dybjer [Reference Coquand and Dybjer21], for the Kripke semantics of implicative propositional logic in natural deduction styleFootnote ¹³ by C. Coquand [Reference Coquand20], for Heyting algebras by Hermant and Lipton [Reference Hermant and Urzyczyn45, Reference Hermant and Lipton46], etc. It has also been applied to phase semantics of linear logic by Okada [Reference Okada73]. It also connects to a normalisation technique in computer science called typed-directed partial evaluation (TDPE) [Reference Danvy24].

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 [Reference Coquand20]. 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 \,\dot{\Rightarrow }\, B \triangleq \forall w' (w' \geq 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)$ .

Figure 1

Inference rules characterising minimal implicational logic.

The metalanguage being here a $\lambda $ -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 universal quantification, possibly also writing $(x:A) \mapsto 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 $t\,u$ . 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 $\forall x_1,...,x_n\,(A \Rightarrow B)$ we shall use the notation $f^{x_1,...,x_n}(a:A) : B$ followed by clauses of the form $f^{x_1,...,x_n}(a) \triangleq t$ (for readability, we may also write some of the $x_i$ as subscripts rather than superscripts of f).

For instance, the proof that Kripke forcing is monotone, i.e., that $\forall w w'\,(w' \geq w \land w \Vdash A \Rightarrow w' \Vdash A)$ , can be written as the following function $\Uparrow _A$ , recursive in the structure of A, taking as arguments two worlds w and $w'$ :

$$ \begin{align*}\begin{array}{lcrlcllcl} \Uparrow_A^{w,w'} & : & \!\!\!\! & w' \geq w & \land & w \Vdash A & \!\!\!\! & \Rightarrow & w' \Vdash A\\ \Uparrow_X^{w,w'} & & (\!\!\!\!& h & , & m &\!\!\!\!) &\triangleq& p_X(h,m)\\ \Uparrow_{A\,\dot{\Rightarrow}\, B}^{w,w'} & & (\!\!\!\!& h & , & m &\!\!\!\!)& \triangleq& w" \mapsto (h':w"\geq w')\\ &&&&&&&&\qquad \mapsto m\,w"\,(\mathit{trans}(h,h')),\\\end{array} \end{align*} $$

where $p_X$ is the proof of monotonicity of $\Vdash X$ (for X a predicate) and $\mathit {trans}$ is the proof of transitivity of $\geq $ , both coming with the definition of Kripke models, while, in the definition, h is a proof of $w' \geq w$ and m is 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 w w'\,(w' \geq w \land w \Vdash \Gamma \Rightarrow w' \Vdash \Gamma )$ :

$$ \begin{align*}\begin{array}{lcrlcllcl} \Uparrow_\Gamma^{w,w'} & : & \!\!\!\!& w' \geq w & \land & w \Vdash \Gamma &\!\!\!\!& \Rightarrow & w' \Vdash \Gamma\\ \Uparrow_\epsilon^{w,w'} & & (\!\!\!\!& h & , & () &\!\!\!\!)&\triangleq& ()\\ \Uparrow_{\Gamma,A}^{w,w'} & & (\!\!\!\!& h & , & (\sigma,m) &\!\!\!\!)&\triangleq& (\Uparrow_{\Gamma}^{w,w'}(h,\sigma),\Uparrow_A^{w,w'}(h,m)).\\ \end{array}\end{align*} $$

Let us write $\Gamma \vdash _I A$ for intuitionistic provability. Let us consider the canonical proof $\mathit {soundness}^{\Gamma }_A$ of $(\Gamma \vdash _I A) \Rightarrow (\Gamma \Vdash _I A) $ proved by induction on the derivation of $\Gamma \vdash _I A$ . We write the proof as a recursive function, recursively on the structure of formulae:

$$ \begin{align*}\!\!\begin{array}{llcl} \mathit{soundness}^\Gamma_A ~~:\!\!\! & \Gamma \vdash_I A & \!\!\Rightarrow\!\! & \Gamma \vDash_I A\\ \mathit{soundness}^\Gamma_A & \dot{\mathit{ax}}_i & \triangleq & \mathcal{K} \mapsto w \mapsto \sigma \mapsto \sigma(i)\\ \mathit{soundness}^\Gamma_{A\Rightarrow B} \!\!& \dot{\mathit{abs}}(p) & \triangleq & \!\!\!\begin{array}[t]{l}\mathcal{K} \mapsto w \mapsto \sigma \mapsto w' \mapsto (h:w\leq w') \mapsto m \mapsto \\ \mathit{soundness}^{\Gamma,A}_B \,p\,\mathcal{K}\, w'\, (\Uparrow_{\Gamma}^{w,w'} (h,\sigma),m)\end{array}\\ \mathit{soundness}^\Gamma_B & \dot{\mathit{app}}(p,q) & \triangleq & \!\!\!\begin{array}[t]{l}\mathcal{K} \mapsto w \mapsto \sigma \mapsto \\ (\mathit{soundness}^{\Gamma}_{A\Rightarrow B}\,p\, \mathcal{K}\, w\, \sigma)~w~\mathit{refl}~(\mathit{soundness}^{\Gamma}_{A}\,q\, \mathcal{K}\, w\, \sigma),\end{array}\\ \end{array} \end{align*} $$

where u is a proof of $\Gamma \vdash _I A$ in the last line, $\dot{\mathit {app}}$ , $\dot{\mathit {abs}}$ , and $\dot{\mathit {ax}}_i$ are the name of inference rules defining object-level implicational propositional logic in a natural deduction style (see Figure 1); $\sigma (i)$ is the $(i+1)^{ {\scriptsize {th}}}$ component of $\sigma $ starting from the right, and $\mathit {refl}$ is the proof of reflexivity of $\geq $ coming with the definition of Kripke models.

Let us also consider the following somehow canonical proof of cut-free completeness, $\mathit {completeness} : (\Gamma \vDash _I A) \Rightarrow (\Gamma \vdash _I^{\mathit {cf}} A)$ . It is based on the universal model of context $\mathcal {K}_0$ defined by taking for $\mathcal {W}$ the set of contexts $\Gamma $ ordered by inclusion and $\Gamma \vdash _I^{\mathit {cf}} X$ for the forcing $\Vdash X$ of atom/predicate X at world $\Gamma $ . Now, the proof proceeds by showing the two directions of $\Gamma \Vdash _{\mathcal {K}_0} A ~{\Leftrightarrow }~ \Gamma \vdash _I^{\mathit {cf}} A$ by mutual induction on A. It is common to write $\downarrow $ for the left-to-right direction (called reify, or quote) and $\uparrow $ for the right-to-left direction (called reflect, or eval):

$$ \begin{align*}\begin{array}{llcl} {\downarrow^\Gamma_A~:} & \Gamma \Vdash_{\mathcal{K}_0} A & {\Rightarrow} & \Gamma \vdash_I^{\mathit{cf}} A\\ \downarrow^\Gamma_{P} & m & \triangleq & m\\ \downarrow^\Gamma_{A \,\dot{\Rightarrow}\, B} & m & \triangleq & \dot{\mathit{abs}}\,(\downarrow^{\Gamma,A}_B (m \;(\Gamma,A) \;\mathit{inj}^A_\Gamma \; (\uparrow^{\Gamma,A}_A\, \dot{\mathit{ax}}_0)))\\ \\ {\uparrow^\Gamma_A~:} & \Gamma \vdash_I^{\mathit{cf}} A & {\Rightarrow} & \Gamma \Vdash_{\mathcal{K}_0} A\\ \uparrow^\Gamma_{P} & p & \triangleq & p \\ \uparrow^\Gamma_{A \,\dot{\Rightarrow}\, B} & p & \triangleq & \Gamma' \mapsto f \mapsto m \mapsto \uparrow^{\Gamma'}_B(\dot{\mathit{app}}(\dot{\mathit{weak}}(f,p),\downarrow^{\Gamma'}_A m))\\ \\ \mathit{init}^\Gamma_{\Gamma'} & & : & \Gamma \Vdash_{\mathcal{K}_0} \Gamma'\\ \mathit{init}^\Gamma_\epsilon & & \triangleq & ()\\ \mathit{init}^\Gamma_{\Gamma',A} & & \triangleq & (\mathit{init}^{\Gamma}_{\Gamma'},\uparrow^\Gamma_A(\dot{\mathit{ax}}_{|\Gamma|-|\Gamma',A|}))\\ \\ \mathit{completeness}^\Gamma_A~ : & \Gamma \vDash_I A & \Rightarrow & \Gamma \vdash_I^{\mathit{cf}} A\\ \mathit{completeness}^\Gamma_A & m & \triangleq & \downarrow^\Gamma_A~ (m~\mathcal{K}_0~\Gamma~\mathit{init}^\Gamma_\Gamma), \end{array} \end{align*} $$

where $|\Gamma |$ is the length of $\Gamma $ , $\dot{\mathit {weak}}$ is the admissible rule of weakening in object-level implicational propositional logic, and $\mathit {inj}^A_\Gamma $ 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,Footnote ¹⁴ 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^{\mathit {cf}} A$ obtained by completeness is, by normalisation in the metalanguage, the same $\lambda $ -term with the abstractions and applications over $\mathcal {K}$ , w and proofs of $w \leq w'$ removed.

On the other hand, 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 [Reference Martin-Löf71]), 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:

$$ \begin{align*}\begin{array}{l} \forall p : (\Gamma \vdash_I A)\;p \sim \mathit{soundness}^\Gamma_A\,p\,\mathcal{K}_0\,\Gamma\, init^{\Gamma}_{\Gamma} \\ \forall p :(\Gamma \vdash_I A)\,\forall m :(\Gamma \vDash_I A)\; (p \sim m\,\mathcal{K}_0\,\Gamma\, init^{\Gamma}_{\Gamma} ~\Rightarrow~ p =_{\beta\eta} \mathit{completeness}^{\Gamma}_A\,m),\\ \end{array} \end{align*} $$

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

Then, since $\mathit {completeness}$ returns normal forms, we get that the composite function $\mathit {completeness}\,(\mathit {soundness}\,p)$ evaluates to a normal form q such that $q =_{\beta \eta } 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 [Reference Herbelin, Lee, Ono, Kanazama and de Queiroz44]. The extension to first-order classical logic has been studied, e.g., in [Reference Ilik, Lee and Herbelin55]. The case of disjunction and existential quantification is typically addressedFootnote ¹⁵ using variants of Kripke semantics [Reference Ilik53], Beth models, topological models [Reference Coquand and Smith23], or various alternative semantics (e.g., [Reference Abel and Sattler1, Reference Altenkirch, Dybjer, Hofmann and Scott2, Reference Okada73, Reference Sambin76]).

One of the purposes of this article 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, similarly to the semantic normalisation for intuitionistic calculi described above. 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 Intuitionistic provability of the different statements of completeness

Statements C1, C2, and C3, as well as statements S1, S2, and 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 ${\mathcal {M}} \vDash _{\sigma } \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 [Reference Kleene, Graves, Hille, Smith and Zariski61] and Simpson [Reference Simpson80]).

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 [Reference Kreisel62] showed, using a result by Gödel [Reference Gödel38], that C1 is equivalent to Markov’s principle—namely, the variant $\neg \neg \exists n\,A(n) \Rightarrow \exists n\,A(n)$ for primitive recursive predicate A, called $\text {MP}_{\text {PR}}$ in Cohen et al. [Reference Cohen, Forster, Kirst, Paiva and Rahli17]—over intuitionistic second-order arithmetic. This has been studied in depth by McCarty [Reference McCarty72] and it turns out that S1 is actually equivalent to Markov’s principle if the theory is recursively enumerable.

However, for arbitrary theories, not only Markov’s principle, but 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{\bot }) \land \mathcal {A} \lor (B = X) \land \neg \mathcal {A}$ for X a distinct propositional atom of the object language. We intuitionistically have that $\mathcal {T} \vDash X$ because this is a negative formulation of a classically provable statement.Footnote ¹⁶ 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 $\dot{\bot }$ is interpreted in the model. Krivine [Reference Krivine68] showed that for a language without $\dot{\bot }$ ,Footnote ¹⁷ C1 is provable intuitionistically. As analysed by Berardi [Reference Berardi7] and Berardi and Valentini [Reference Berardi and Valentini8], Markov’s principle is not needed anymore if we additionally accept the degenerate model where all formulae including $\dot{\bot }$ are interpreted as true.Footnote ¹⁸ Let us formalise this precisely.

We define a possibly-exploding model $\mathcal {M}$ to be a modelFootnote ¹⁹ $(\mathcal {D},\mathcal {F},\mathcal {P},\mathcal {A}_{\dot{\bot }})$ such that $(\mathcal {D},\mathcal {F},\mathcal {P})$ is a model in the previous sense and $\mathcal {A}_{\dot{\bot }}$ is a fixed formula intended to interpret $\dot{\bot }$ . The definition of truth is then modified as follows:

$$ \begin{align*}\begin{array}{lll} {\mathcal{M}} \vDash^e_{\sigma} \dot{\bot} & \triangleq & \mathcal{A}_{\dot{\bot}}\\ \end{array} \end{align*} $$

with the rest of clauses unchanged.Footnote ²⁰

Note that because $\dot{\bot } \,\dot{\Rightarrow }\, A$ is a consequence of $\dot{\neg }\dot{\neg } A \,\dot{\Rightarrow }\, A$ , the following holds for all A and all $\sigma $ in any classical possibly-exploding model:

$$ \begin{align*}\mathcal{A}_{\dot{\bot}} ~\Rightarrow~ {\mathcal{M}} \vDash^e_{\sigma} A, \end{align*} $$

so we do not need to further enforce it.Footnote ²¹ Let us rephrase C1 and S1 using classical possibly-exploding models:

$$ \begin{align*}\begin{array}{ll} C1'. & \vDash^e A ~\Rightarrow~ \vdash A\\ S1'. & \mathcal{T} \vDash^e A ~\Rightarrow~\mathcal{T} \vdash A,\\ \end{array} \end{align*} $$

where

$$ \begin{align*}\mathcal{T} \vDash^e A ~ \triangleq ~ \forall \mathcal{M}\, \forall \sigma\, ({\mathcal{M}} \vDash^e_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash^e_{\sigma} \mathcal{T} \Rightarrow {\mathcal{M}} \vDash^e_{\sigma} A). \end{align*} $$

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.Footnote ²²

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., [Reference Parigot74]), 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 [Reference Blanchette, Popescu, Traytel, Demri, Kapur and Weidenbach12] 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 [Reference Ilik51] in the Coq proof assistant [18] of Henkin’s proof. It was first presented at the TYPES conference in Warsaw, 2010. The article 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 [Reference Forster, Kirst and Wehr29, Reference Forster, Kirst and Wehr30]. This encouraged us in 2022 to polish the article one step further with the objective of a submission.

A new version was made public on the web page of the first author in November 2022 together with an implementation,Footnote ²³ given in Appendix A, of the underlying computational content 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 unadressed 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 ( $\mathsf {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 $\mathsf {DNS}$ that Kirst recently identified [Reference Kirst60].

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 [Reference Forster, Kirst and Wehr29, Reference Forster, Kirst and Wehr30, Reference Kirst60], this includes papers by Krivtsov [Reference Krivtsov70] in intuitionistic arithmetic and Espíndola [Reference Espíndola25, Reference Espíndola26] in intuitionistic set theory (IZF). Their results are discussed in Section 2.6.

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 [Reference Henkin41], 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.Footnote ²⁴

Let $\mathcal {T}$ be a consistent set of formulae mentioning an at most countableFootnote ²⁵ number of function symbols and predicate symbols. Let $\mathcal {X}_1$ and $\mathcal {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 $\mathcal {X}_1$ leaving $\mathcal {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 $\mathcal {S}_{\omega }$ of formulae which is maximal in the sense that if $A \not \in \mathcal {S}_{\omega }$ then $\dot{\neg } A \in \mathcal {S}_{\omega }$ . We shall also ensure that for every universally quantified formula $\dot{\forall } x\,A(x)$ , there is a corresponding so-called Henkin axiom $A(y) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x)$ in $\mathcal {S}_{\omega }$ with y fresh in $\dot{\forall } x\, A(x)$ . For the purpose of this construction, we fix an injective enumeration $\phi $ of formulae of the form $\dot{\forall } x\,A(x)$ or $A\,\dot{\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 $\dot{\forall } x\,A(x)$ and formulae of odd index are of the form $A\,\dot{\Rightarrow }\, B$ .

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

$$ \begin{align*}\begin{array}{lll} \mathcal{D} & \triangleq & \mathcal{T}\!erm\\ \mathcal{F}(f)(t_1,...,t_n) & \triangleq & f(t_1,...,t_n)\\ \mathcal{P}(P)(t_1,...,t_n) & \triangleq & P(t_1,...,t_n) \in \mathcal{S}_{\omega.}\\ \end{array} \end{align*} $$

By induction, each $\mathcal {S}_n$ is consistent. Indeed, if $\phi (n)$ is implicative and $\mathcal {S}_{n+1} \equiv \mathcal {S}_n \cup \phi (n)$ , it is precisely because $\mathcal {S}_{n+1}$ is consistent. Otherwise, the consistency of $\mathcal {S}_{n+1}$ comes from the consistency of $\mathcal {S}_n$ . If $\phi (n)$ is some $\dot{\forall } x\,A(x)$ , then $\mathcal {S}_{n+1} \equiv \mathcal {S}_n \cup (A(x_{n/2}) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x))$ . This is consistent by freshness of $x_{n/2}$ in both $\mathcal {T}$ and in the $\phi (i)$ for $i\leq n$ . Indeed, because $x_{n/2}$ is fresh, any proof of $\mathcal {S}_n \cup (A(x_{n/2}) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x)) \vdash \dot{\bot } $ can be turned into a proof of $\mathcal {S}_n \cup \dot{\neg } \dot{\forall } y\, \dot{\neg } (A(y) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x)) \vdash \dot{\bot } $ , which itself can be turned into a proof of $\mathcal {S}_n \vdash \dot{\bot } $ since $\dot{\neg } \dot{\forall } y\, \dot{\neg } \,(A(y) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x))$ is a classical tautology.Footnote ²⁶

Let A be a formula and $\sigma $ a substitution of its free variables. We now show by induction on the logical depthFootnote ²⁷ of A that ${\mathcal {M}_0} \vDash _{\sigma } A \Leftrightarrow A[\sigma ] \in \mathcal {S}_{\omega }$ , where $A[\sigma ]$ denotes the 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 is $B\,\dot{\Rightarrow }\, C$ . One way to show $B[\sigma ] \,\dot{\Rightarrow }\, C[\sigma ] \in \mathcal {S}_{\omega }$ from ${\mathcal {M}_0} \vDash _{\sigma } B\,\dot{\Rightarrow }\, C$ is to show that for n being $\lceil B[\sigma ]\,\dot{\Rightarrow }\, C[\sigma ] \rceil $ , the set $\mathcal {S}_n \cup B[\sigma ] \,\dot{\Rightarrow }\, C[\sigma ]$ is consistent, i.e., that a contradiction arises from $\mathcal {S}_n \cup B[\sigma ] \,\dot{\Rightarrow }\, C[\sigma ] \vdash \dot{\bot }$ . Indeed, from the latter, we get both $\mathcal {S}_n \vdash B[\sigma ]$ and $\mathcal {S}_n \vdash \dot{\neg } C[\sigma ]$ . From $\mathcal {S}_n \vdash B[\sigma ]$ we get ${\mathcal {M}_0} \vDash _{\sigma } B$ by induction hypothesis, hence ${\mathcal {M}_0} \vDash _{\sigma } C$ by assumption on the truth of $B\,\dot{\Rightarrow }\, C$ . Then $C[\sigma ] \in \mathcal {S}_{\omega }$ again by induction hypothesis, hence $\mathcal {S}_{n'} \vdash C[\sigma ]$ for some $n'$ . But also $\mathcal {S}_n \vdash \dot{\neg } C[\sigma ]$ , hence $\mathcal {S}_{\mathit {max}(n,n')} \vdash \dot{\bot ,}$ which contradicts the consistency of $\mathcal {S}_{\mathit {max}(n,n')}$ .

• • Conversely, if $B[\sigma ] \,\dot{\Rightarrow }\, C[\sigma ] \in \mathcal {S}_{\omega }$ , this means $\mathcal {S}_n \vdash B[\sigma ] \,\dot{\Rightarrow }\, C[\sigma ]$ for some n. To prove ${\mathcal {M}_0} \vDash _{\sigma } B\,\dot{\Rightarrow }\, C$ , let us assume ${\mathcal {M}_0} \vDash _{\sigma } B$ . By induction hypothesis we get $\mathcal {S}_{n'} \vdash B[\sigma ]$ for some $n'$ and hence $\mathcal {S}_{\mathit {max}(n,n')} \vdash C[\sigma ]$ , i.e., $C[\sigma ] \in \mathcal {S}_{\omega }$ . We conclude by induction hypothesis to get ${\mathcal {M}_0} \vDash _{\sigma } C$ .

• • Let us then focus on the case when A is $\dot{\forall } x\,B$ . For n even being $\lceil (\dot{\forall } x\,B)[\sigma ] \rceil $ , we have $(B[\sigma ,x\leftarrow x_{n/2}] \,\dot{\Rightarrow }\, (\dot{\forall } x\,B)[\sigma ]) \in \mathcal {S}_{n+1}$ . From ${\mathcal {M}_0} \vDash _{\sigma } \dot{\forall } x\,B(x)$ we get ${\mathcal {M}_0} \vDash _{\sigma , x\leftarrow x_{n/2}} B(x)$ and by the induction hypothesis we then get the existence of some $n'$ such that $\mathcal {S}_{n'} \vdash B[\sigma ,x \leftarrow x_{n/2}]$ . Hence, $\mathcal {S}_{\mathit {max}(n+1,n')} \vdash (\dot{\forall } x\,B)[\sigma ]$ , which means $(\dot{\forall } x\,B)[\sigma ] \in \mathcal {S}_{\omega }$ .

• • Conversely, assume $\mathcal {S}_n \vdash (\dot{\forall } x\,B)[\sigma ]$ for some n and prove ${\mathcal {M}_0} \vDash _{\sigma } \forall x\,B$ . Let t be a term. From $\mathcal {S}_n \vdash (\dot{\forall } x\,B)[\sigma ]$ we get $\mathcal {S}_n \vdash B[\sigma ,x\leftarrow t]$ , hence, by induction hypothesis, ${\mathcal {M}_0} \vDash _{\sigma ,x\leftarrow t} B(x)$ .

• • Let us then consider the case A is $\dot{\bot }$ . By ex falso quodlibet in the metalanguage, it is direct that $\bot \Rightarrow (\dot{\bot } \in \mathcal {S}_{\omega })$ .

• • Conversely, let us prove $(\dot{\bot } \in \mathcal {S}_{\omega }) \Rightarrow \bot $ . From $\dot{\bot } \in \mathcal {S}_{\omega }$ we know $\mathcal {S}_n \vdash \dot{\bot }$ for some n which, again, contradicts the consistency of $\mathcal {S}_n$ .

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

Before completing the proof, it remains to prove that the model is classical. Using the equivalence between ${\mathcal {M}_0} \vDash _{\mathit {id}} A$ and $A \in \mathcal {S}_{\omega }$ for A closed and $\mathit {id}$ the empty substitution, it is enough to prove that $\dot{\neg }\dot{\neg } A\in \mathcal {S}_{\omega }$ implies $A\in \mathcal {S}_{\omega }$ . But the former means $\mathcal {S}_{n} \vdash \dot{\neg }\dot{\neg } A$ for some n, hence $\mathcal {S}_{n} \vdash A$ by classical reasoning in the object language, hence $A \in \mathcal {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 \mathcal {S}_\omega $ and hence ${\mathcal {M}_0} \vDash _{\mathit {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 ^0_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 \vDash A_0$ , let us assume the contrary, namely, that $\mathcal {T}_0 \cup \dot{\neg } A_0$ is consistent. Then, we can complete $\mathcal {S}_0 \triangleq \mathcal {T}_0 \cup \dot{\neg } A_0$ into $\mathcal {S}_{\omega }$ and build out of it a classical model $\mathcal {M}_0$ such that $\forall B\in \mathcal {T}_0\, {\mathcal {M}_0} \vDash _{\mathit {id}} B$ as well as ${\mathcal {M}_0} \vDash _{\mathit {id}} \dot{\neg } A_0$ , i.e., $\neg ({\mathcal {M}_0} \vDash _{\mathit {id}} A_0)$ . But this contradicts $\mathcal {T}_0 \vDash A_0$ and, because $\mathcal {T}_0$ is $\Sigma ^0_1$ , 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 $\mathcal {S}_{\omega }$ from $\mathcal {T}_0 \cup \dot{\neg } A_0$ so that it is not consistent in an absolute sense, but instead consistent relative to $\mathcal {T}_0 \cup \dot{\neg } A_0 $ . In particular, we change the condition for extending $\mathcal {S}_{2n+1}$ with $\phi (2n+1)$ to be that $\mathcal {S}_{2n+1} \cup \phi (2n+1)$ is consistent relative to $\mathcal {T}_0 \cup \dot{\neg } A_0$ .

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

For the construction of the now possibly-exploding model, we take as interpretation of $\dot{\bot }$ the formula $\mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot }$ . Proving $\dot{\bot } \in \mathcal {S}_{\omega } \Rightarrow {\mathcal {M}_0} \vDash ^e_{\sigma } \dot{\bot }$ now reduces to proving $\mathcal {S}_{n} \vdash \dot{\bot } \Rightarrow \mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot ,}$ which is the statement of relative consistency.Footnote ²⁸ Conversely, ${\mathcal {M}_0} \vDash ^e_{\sigma } \dot{\bot } \Rightarrow \dot{\bot } \in \mathcal {S}_{\omega }$ now comes by definition of $\mathcal {S}_{0}$ .

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

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

As a final remark, one could wonder whether the construction of $\mathcal {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 \dot{\neg } A_0$ in order to get $\mathcal {S}_n$ seems to require a use of excluded-middle. However, in the proof of completeness, only the property $A\in \mathcal {S}_n$ matters, and this property is directly definable by recursion as

$$ \begin{align*}\begin{array}{lll} A\in \mathcal{S}_{0} & \triangleq & A \in \mathcal{T}_0 \cup \dot{\neg} A_0\\ A \in \mathcal{S}_{n+1} & \triangleq & A \in \mathcal{S}_n\\ & & \lor~ (\exists p\,(n = 2p+1) ~\land~ \phi(n) = \dot{\forall} x\,B(x) \\ && \land~ A = (B(x_{p+1}) \,\,\dot{\Rightarrow}\,\, \dot{\forall} x\,B(x))\\ & & \lor~ (\exists p\,(n = 2p) ~\land~ (\mathcal{S}_n, A \vdash \dot{\bot} \Rightarrow \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot}) ~\land~ A = \phi(n)). \end{array} \end{align*} $$

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

2.3 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,Footnote ²⁹ 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 $\mathit {dest}\,p\,\mathit {as}\,(x_1,...,x_n)\,\mathit {in}~q$ for a proof obtained by decomposition of the proof p of an n-ary combination of existential quantifiers and conjunctions. We shall write $\mathit {efq}\,p$ for a proof of A obtained by ex falso quodlibet from a proof p of $\bot $ .

We shall use the following letter convention to refer to different kinds of entities:

1. n: natural numbers,

2. A: formulae,

3. Γ: contexts of formulae,

4. m: proofs of truth,

5. p: proofs of derivability in the object language,

6. q: proofs of belonging to $\mathcal {S}_\omega $ ,

7. r: proofs of inconsistency from adding an implicative formula to $\mathcal {S}_{2n+1}$ ,

8. h: proofs of belonging to $\mathcal {T}_0$ ,

9. g: proofs of inclusion in $\mathcal {T}_0$ ,

10. f: proofs of inclusion in extensions of $\mathcal {T}_0$ , and

11. k: proofs of relative consistency.

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

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

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

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

We now write as a program the proof that $\mathcal {S}_\omega $ is consistent relative to $\mathcal {T}_0 \cup \dot{\neg } A_0$ , i.e., that $\dot{\bot } \in \mathcal {S}_{\omega }$ implies $\mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot }$ . The latter expands to $\exists \Gamma \,(\Gamma \subset \mathcal {T}_0\;\land \; \Gamma , \dot{\neg } A_0 \vdash \dot{\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{\neg } A_0 \vdash \dot{\bot }$ .

This proof, which we call $\mathit {flush}_n^\Gamma $ , takes as arguments a quadruple $(n,\Gamma ,f,p),$ where f is a proof of $\Gamma \subset \mathcal {S}_n$ and p is a proof of $\Gamma \vdash \dot{\bot }$ . It proceeds by cases on the proof of $\Gamma \subset \mathcal {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 ( $\dot{\mathit {drinker}}_y$ is the proof which builds a proof of $\Gamma \vdash \dot{\bot }$ from a proof of $\Gamma , A(y) \,\dot{\Rightarrow }\, \dot{\forall } x\,A(x) \vdash \dot{\bot }$ , knowing that y does not occur in $\Gamma , \dot{\forall } x\, A(x)$ , see Figure 2).

$$ \begin{align*}\begin{array}{lllll} \mathit{flush} & {:} & \dot{\bot} \in \mathcal{S}_{\omega} & {\Rightarrow} & \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot}\\ \mathit{flush} & & (0,(\Gamma,\dot{\neg} A_0),\mathit{I_0}\,g,p) & \triangleq & (\Gamma,g,p)\\ \mathit{flush} & & (n+1,\Gamma,\mathit{I_S}\,f,p) & \triangleq & \mathit{flush}\, (n,\Gamma,f,p)\\ \mathit{flush} & & (2n+1,(\Gamma,A),\mathtt{I_\forall}\,f,p) & \triangleq & \mathit{flush}\, (2n,\Gamma,f,\dot{\mathit{drinker}}_{x_n}\,p)\\ \mathit{flush} & & (2n+2,(\Gamma,A),\mathit{I_{\Rightarrow}}\,(f,k),p) & \triangleq & k\;(\Gamma,f,p).\\ \end{array} \end{align*} $$

Figure 2

Inference rules characterising classical first-order predicate calculus.

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

$$ \begin{align*}\begin{array}{lclllcll} \mathit{inj}_n & {:} & {\dot{\neg} A_0 \subset \mathcal{S}_n} \quad~~ \\ \mathit{inj}_0 & \triangleq & \mathit{I_0}(J_{\mathit{base}}) \\ \mathit{inj}_{n+1} & \triangleq & \mathit{I_S} (\mathit{inj}_n).\\ \end{array} \end{align*} $$

A boring lemma which is implicit in the proof of completeness in natural language is that $\Gamma \subset \mathcal {S}_n$ and $\Gamma '\subset \mathcal {S}_{n'}$ imply $\Gamma \cup \Gamma ' \subset \mathcal {S}_{\mathit {max}(n,n')}$ . It looks obvious because one tends to think of $\Gamma \subset \mathcal {S}_n$ as denoting the inclusion of $\Gamma $ within a uniquely defined relatively consistent set $\mathcal {S}_n$ . However, the computational approach to the proof shows that $\mathcal {S}_n$ has no computational content per se: only proofs of $\Gamma \subset \mathcal {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 \mathcal {S}_{\omega } \Leftrightarrow {\mathcal {M}_0} \vDash ^e_{\sigma } 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 $\mathcal {S}_n$ for some n has either the form $\Gamma ', \dot{\neg } 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 $\mathcal {S}_n$ for some n by cases:Footnote ³⁰

$$ \begin{align*}\begin{array}{llllll} \Gamma_1, \dot{\neg} A_0 &\cup& \Gamma_2, \dot{\neg} A_0 & \triangleq & \Gamma_1, \Gamma_2, \dot{\neg} A_0\\ \Gamma_1, \dot{\neg} A_0 &\cup& \Gamma_2, A & \triangleq & (\Gamma_1, \dot{\neg} A_0 ~\cup~ \Gamma_2),A\\ \Gamma_1,A &\cup& \Gamma_2, \dot{\neg} A_0 & \triangleq & (\Gamma_1 ~\cup~ \Gamma_2, \dot{\neg} A_0),A\\ \Gamma_1,A &\cup& \Gamma_2,A & \triangleq & (\Gamma_1 ~\cup~ \Gamma_2),A \quad & \\ \Gamma_1,A &\cup& \Gamma_2,B & \triangleq & (\Gamma_1,A ~\cup ~\Gamma_2),B \quad & \text{if }\lceil B \rceil> \lceil A \rceil \\ \Gamma_1,A &\cup& \Gamma_2,B & \triangleq & (\Gamma_1 ~\cup~ \Gamma_2,B),A & \text{if }\lceil A \rceil > \lceil B \rceil. \\ \end{array} \end{align*} $$

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

$$ \begin{align*}\begin{array}{lrlcllcll} {\mathit{join}_\subset^{\Gamma_1\Gamma_2}} : & \!\!\!\! & {\Gamma_1 \subset \mathcal{T}_0} &\!\!\!{\land}\!\!\!& {\Gamma_2 \subset \mathcal{T}_0} &&{\!\!\Rightarrow\!\!}& {\Gamma_1, \Gamma_2 \subset \mathcal{T}_0}\\ \mathit{join}_\subset^{\Gamma_1\epsilon} & (\!\!\!\! &g_1&\!\!\!,\!\!\!&\mathit{J_{\mathit{base}}} &\!\!\!\!)&\!\!\triangleq\!\!& g_1 &\\ \mathit{join}_\subset^{\Gamma_1(\Gamma_2,A_2)} & (\!\!\!\! &g_1&\!\!\!,\!\!\!&\mathit{J_{\mathit{cons}}}(g_2,h_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{J_{\mathit{cons}}}(\mathit{join}_\subset^{\Gamma_1\Gamma_2}(g_1,g_2),h_2) & \\ \\ {\mathit{join}^{\Gamma_1\Gamma_2}_{n}} : & \!\!\!\! & {\Gamma_1 \subset \mathcal{S}_{n}} &\!\!\!{\land}\!\!\!& {\Gamma_2 \subset \mathcal{S}_{n}} &&{\!\!\Rightarrow\!\!}& {\Gamma_1 \cup \Gamma_2 \subset \mathcal{S}_n}\\ \mathit{join}^{(\Gamma_1,\dot{\neg} A_0)(\Gamma_2,\dot{\neg} A_0)}_{0}\!\!\!\! & (\!\!\!\! &\mathit{I_0}(g_1)&\!\!\!,\!\!\!&\mathit{I_0}(g_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_0}(\mathit{join}_\subset^{\Gamma_1\Gamma_2}(g_1,g_2) & \\ \mathit{join}^{(\Gamma_1A)(\Gamma_2A)}_{2n+1} & (\!\!\!\! &\mathtt{I_\forall}(f_1)&\!\!\!,\!\!\!&\mathtt{I_\forall}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\forall}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n} (f_1, f_2)) & \\ \mathit{join}^{(\Gamma_1A)(\Gamma_2A)}_{2n+2} & (\!\!\!\! &\mathtt{I_\Rightarrow}(f_1,k_1)&\!\!\!,\!\!\!&\mathtt{I_\Rightarrow}(f_2,k_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\Rightarrow}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n+1} (f_1, f_2),k_1) & \\ \mathit{join}^{(\Gamma_1A)\Gamma_2}_{2n+1} & (\!\!\!\! &\mathtt{I_\forall}(f_1)&\!\!\!,\!\!\!&\mathit{I_S}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\forall}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n} (f_1, f_2)) \\ \mathit{join}^{(\Gamma_1A)\Gamma_2}_{2n+2} & (\!\!\!\! &\mathtt{I_\Rightarrow}(f_1,k_1)&\!\!\!,\!\!\!&\mathit{I_S}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\Rightarrow}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n+1} (f_1, f_2),k_1) \\ \mathit{join}^{\Gamma_1(\Gamma_2A)}_{2n+1} & (\!\!\!\! &\mathit{I_S}(f_1)&\!\!\!,\!\!\!&\mathtt{I_\forall}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\forall}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n} (f_1, f_2)) &\\ \mathit{join}^{\Gamma_1(\Gamma_2A)}_{2n+2} & (\!\!\!\! &\mathit{I_S}(f_1)&\!\!\!,\!\!\!&\mathtt{I_\Rightarrow}(f_2,k_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\Rightarrow}(\mathit{join}^{\Gamma_1\Gamma_2}_{2n+1} (f_1, f_2),k_2) &\\ \mathit{join}^{\Gamma_1\Gamma_2}_{n+1} & (\!\!\!\! &\mathit{I_S}(f_1)&\!\!\!,\!\!\!&\mathit{I_S}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_S}(\mathit{join}^{\Gamma_1\Gamma_2}_{n} (f_1, f_2)) &\\ \end{array} \end{align*} $$

$$ \begin{align*}\begin{array}{lrlcllcll} {\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1n_2}} : & \!\!\!\! & {\Gamma_1 \subset \mathcal{S}_{n_1}} &\!\!\!{\land}\!\!\!& {\Gamma_2 \subset \mathcal{S}_{n_2}} &&{\!\!\Rightarrow\!\!}& {\Gamma_1 \cup \Gamma_2 \subset \mathcal{S}_{\mathit{max}(n_1,n_2)}}\\ \mathit{hjoin}^{\Gamma_1\Gamma_2}_{nn} & (\!\!\!\! &f_1&\!\!\!,\!\!\!& f_2 &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{join}^{\Gamma_1\Gamma_2}_{n} (f_1, f_2) &\\ \mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1'+1>n_2} & (\!\!\!\! &\mathit{I_S}(f_1)&\!\!\!,\!\!\!& f_2 &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_S} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1'n_2} (f_1, f_2)) & \\ \mathit{hjoin}^{(\Gamma_1A_1)\Gamma_2}_{n_1'+1>n_2} & (\!\!\!\! &\mathit{I_{\forall}}(f_1)&\!\!\!,\!\!\!& f_2 &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_{\forall}} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1'n_2} (f_1, f_2)) & \\ \mathit{hjoin}^{(\Gamma_1A_1)\Gamma_2}_{n_1'+1>n_2} & (\!\!\!\! &\mathit{I_{\Rightarrow}}(f_1,k_1)&\!\!\!,\!\!\!& f_2 &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_{\Rightarrow}} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1'n_2} (f_1, f_2), k_1) & \\ \mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1<n_2'+1} & (\!\!\!\! &f_1&\!\!\!,\!\!\!& \mathit{I_S}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathit{I_S} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1n_2'} (f_1, f_2)) & \\ \mathit{hjoin}^{\Gamma_1(\Gamma_2A_2)}_{n_1<n_2'+1} & (\!\!\!\! &f_1&\!\!\!,\!\!\!&\mathtt{I_\forall}(f_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\forall} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1n_2'} (f_1, f_2)) & \\ \mathit{hjoin}^{\Gamma_1(\Gamma_2A_2)}_{n_1<n_2'+1} & (\!\!\!\! &f_1&\!\!\!,\!\!\!&\mathtt{I_\Rightarrow}(f_2,k_2) &\!\!\!\!)&\!\!\triangleq\!\!& \mathtt{I_\Rightarrow} (\mathit{hjoin}^{\Gamma_1\Gamma_2}_{n_1n_2'} (f_1, f_2), k_2). & \\ \end{array} \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 \dot{\bot }$ to $\mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot }$ (third clause of $\mathit {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:

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:

$$ \begin{align*}\begin{array}{lcll} \mathit{incl}_i^{\Gamma_1,\Gamma_2} & : & {\Gamma_i \subset \Gamma_1, \Gamma_2}\\ \mathit{incl}_i^{\epsilon,\epsilon} & \triangleq & L_0\\ \mathit{incl}_1^{(\Gamma_1,A),\epsilon} & \triangleq & L_S(\mathit{incl}_1^{\Gamma_1\epsilon})\\ \mathit{incl}_2^{(\Gamma_1,A),\epsilon} & \triangleq & L_N(\mathit{incl}_2^{\Gamma_1\epsilon})\\ \mathit{incl}_1^{\Gamma_1,(\Gamma_2,A)} & \triangleq & L_N(\mathit{incl}_1^{\Gamma_1\Gamma_2})\\ \mathit{incl}_2^{\Gamma_1,(\Gamma_2,A)} & \triangleq & L_S(\mathit{incl}_2^{\Gamma_1\Gamma_2}).\\ \end{array} \end{align*} $$

This allows to prove the following lemma where i is either $1$ or $2$ :

$$ \begin{align*}\begin{array}{lcll} \mathit{incl'}_i^{\Gamma_1,\Gamma_2} & : & {\Gamma_i \subset \Gamma_1 \cup \Gamma_2}\\ \mathit{incl'}_i^{(\Gamma_1,\dot{\neg} A_0),(\Gamma_2,\dot{\neg} A_0)} & \triangleq & L_S(\mathit{incl}_i^{\Gamma_1,\Gamma_2})\\ \mathit{incl'}_1^{(\Gamma_1,\dot{\neg} A_0),(\Gamma_2,A)} & \triangleq & L_N(\mathit{incl'}_1^{(\Gamma_1,\dot{\neg} A_0),\Gamma_2})\\ \mathit{incl'}_2^{(\Gamma_1,\dot{\neg} A_0),(\Gamma_2,A)} & \triangleq & L_S(\mathit{incl'}_2^{(\Gamma_1,\dot{\neg} A_0),\Gamma_2})\\ \mathit{incl'}_1^{(\Gamma_1,A),(\Gamma_2,\dot{\neg} A_0)} & \triangleq & L_S(\mathit{incl'}_1^{\Gamma_1,(\Gamma_2,\dot{\neg} A_0)})\\ \mathit{incl'}_2^{(\Gamma_1,A),(\Gamma_2,\dot{\neg} A_0)} & \triangleq & L_N(\mathit{incl'}_2^{\Gamma_1,(\Gamma_2,\dot{\neg} A_0)})\\ \mathit{incl'}_i^{(\Gamma_1,A),(\Gamma_2,A)} & \triangleq & L_S(\mathit{incl'}_i^{\Gamma_1,\Gamma_2})\\ \mathit{incl'}_1^{(\Gamma_1,A),(\Gamma_2,B)} & \triangleq & L_N(\mathit{incl'}_1^{(\Gamma_1,A),\Gamma_2}) & \text{if }\lceil A \rceil < \lceil B \rceil \\ \mathit{incl'}_2^{(\Gamma_1,A),(\Gamma_2,B)} & \triangleq & L_S(\mathit{incl'}_2^{(\Gamma_1,A),\Gamma_2}) & \text{if }\lceil A \rceil < \lceil B \rceil \\ \mathit{incl'}_1^{(\Gamma_1,A),(\Gamma_2,B)} & \triangleq & L_S(\mathit{incl'}_1^{\Gamma_1,(\Gamma_2,B)}) & \text{if }\lceil A \rceil> \lceil B \rceil \\ \mathit{incl'}_2^{(\Gamma_1,A),(\Gamma_2,B)} & \triangleq & L_N(\mathit{incl'}_2^{\Gamma_1,(\Gamma_2,B)}) & \text{if }\lceil A \rceil > \lceil B \rceil. \\ \end{array} \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 $\dot{\mathit {abs}}^\Rightarrow $ and $\dot{\mathit {abs}}^\forall $ but instead the derived rules $\pi ^{\,\dot{\Rightarrow }\,}_1$ , $\pi ^{\,\dot{\Rightarrow }\,}_2$ and $\dot{\mathit {drinker}}_y$ .

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

$$ \begin{align*}\begin{array}{llclccllll} \mathit{share} : & \!\!\!\!A_1 \in \mathcal{S}_{\omega} &\!\!\!{\land}\!\!\!& {A_2 \in \mathcal{S}_{\omega}} &{\!\!\!\Rightarrow\!\!\!}& \exists n\exists \Gamma (\Gamma \subset \mathcal{S}_n \land \Gamma \vdash A_1 \land \Gamma \vdash A_2)\\ \mathit{share}\!\!\!\! &\!\!\!\! (n_1,\Gamma_1,f_1,p_1)&\!\!\!\!\!\!\!&(n_2,\Gamma_2,f_2,p_2) &\!\!\!\triangleq\!\!\!& \left(\begin{array}{l}\mathit{max}(n_1,n_2),(\Gamma_1 \cup \Gamma_2),\mathit{hjoin}^{}_{}(f_1,f_2),\\\dot{\mathit{weak}}(\mathit{incl'}_1^{\Gamma_1,\Gamma_2},p_1),\\\dot{\mathit{weak}}(\mathit{incl'}_2^{\Gamma_1,\Gamma_2},p_2)\end{array}\right),\\ \end{array} \end{align*} $$

where $\dot{\mathit {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 $\mathcal {S}_\omega $ , as well as provide proofs of specific formulae:

Similarly, we can formulate rules on provability in $\mathcal {T}_0$ :

$$ \begin{align*}\begin{array}{llclcl} \dot{\mathit{DNABS}}: & \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot} \qquad &{\Rightarrow}& \mathcal{T}_0 \vdash A_0\\ \dot{\mathit{DNABS}} & (\Gamma,g,p) &\!\!\triangleq\!\!& (\Gamma,g,{\dot{\mathit{dn}}}(\dot{\mathit{abs^{\,\dot{\Rightarrow}\,}}}(p)))\\ \\ \dot{\mathit{BOT}}: & \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot} &{\Rightarrow}& \dot{\bot} \in \mathcal{S}_\omega\hspace{5.7cm}\\ \dot{\mathit{BOT}} & (\Gamma,g,p) &\!\!\triangleq\!\!& (0,(\Gamma,\dot{\neg} A_0),\mathit{I_0}(g),p).\\ \end{array} \end{align*} $$

When $\lceil A \,\dot{\Rightarrow }\, B \rceil = 2n+1$ , we can also derive the following properties:

$$ \begin{align*}\begin{array}{ll@{\;}c@{\;}l@{\;}c@{\;}l} \dot{\mathit{AX}}_{A\,\dot{\Rightarrow}\, B}: & \!\!((\mathcal{S}_{2n+1}, A\,\dot{\Rightarrow}\, B \vdash \dot{\bot}) \Rightarrow (\mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot})) &{\!\!\Rightarrow\!\!}& A \,\dot{\Rightarrow}\, B \in \mathcal{S}_\omega\\ \dot{\mathit{AX}}_{A \,\dot{\Rightarrow}\, B} & \!\!k & \triangleq & \left(\begin{array}{l}2n+2,(\dot{\neg} A_0, A\,\dot{\Rightarrow}\, B),\\\mathit{I_{\Rightarrow}}(\mathit{inj}_{2n+1},k),\dot{\mathit{ax}}_0\end{array}\right)\\ \\ \dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1: & \!\!\mathcal{S}_{2n+1}, A \,\dot{\Rightarrow}\, B \vdash \dot{\bot} &{\!\!\Rightarrow\!\!}& A \in \mathcal{S}_\omega\\ \dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1 & \!\!(\Gamma,f,p) &\!\!\triangleq\!\!& (2n+1,\Gamma,f,\pi^{\,\dot{\Rightarrow}\,}_1\,p)\\ \\ \dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2: & \!\!\mathcal{S}_{2n+1}, A \,\dot{\Rightarrow}\, B \vdash \dot{\bot} &{\!\!\Rightarrow\!\!}& \dot{\neg} B \in \mathcal{S}_\omega\\ \dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2 & \!\!(\Gamma,f,p) &\!\!\triangleq\!\!& (2n+1,\Gamma,f,\pi^{\,\dot{\Rightarrow}\,}_2\,p).\\ \end{array} \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 [Reference Coquand20], or TDPE [Reference Danvy24], as considered when proving completeness of intuitionistic logic with respect to models, such as Kripke or Beth models.

We have to prove ${\mathcal {M}_0} \vDash ^e_{\sigma } A \Leftrightarrow A[\sigma ] \in \mathcal {S}_{\omega }$ , which means proving ${\mathcal {M}_0} \vDash ^e_{\sigma } A \Rightarrow A[\sigma ] \in \mathcal {S}_{\omega }$ and $A[\sigma ] \in \mathcal {S}_{\omega } \Rightarrow {\mathcal {M}_0} \vDash ^e_{\sigma } A$ . As in semantic normalisation (see Section 1.6), we shall call reification and write $\downarrow _\sigma ^A$ the proof mapping a semantic formula (i.e., ${\mathcal {M}_0} \vDash ^e_{\sigma } A$ ) to a syntactic formula, i.e., $A[\sigma ] \in \mathcal {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{align*}\begin{array}{llcl} {\downarrow_\sigma^A~:} & {\mathcal{M}_0} \vDash^e_{\sigma} A & {\Rightarrow} & {A[\sigma]\in \mathcal{S}_\omega}\\ \downarrow_\sigma^{P(\vec{t})} & m & \!\triangleq\! & m\\ \downarrow_\sigma^{\dot{\bot}} & m & \!\triangleq\! & \dot{\mathit{BOT}}(m)\\ \downarrow_\sigma^{A \,\dot{\Rightarrow}\, B} & m & \!\triangleq\! & \dot{\mathit{AX}}_{A[\sigma] \,\dot{\Rightarrow}\, B[\sigma]}(\mathit{kont}^{A\,\dot{\Rightarrow}\, B}_{\sigma}(m))\\ \downarrow_\sigma^{\dot{\forall} x\, A} & m & \!\triangleq\! & \dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{AX}}_{(\forall x\,A)[\sigma]},\downarrow_{\sigma,x\leftarrow x_n}^{A}\! (m\, x_n))\\ &&&\quad \mathit{where}\ 2n = \lceil (\dot{\forall} x\, A)[\sigma] \rceil\\ \\ {\uparrow_\sigma^A~:} & {A[\sigma] \in \mathcal{S}_\omega} & {\Rightarrow} & {\mathcal{M}_0} \vDash^e_{\sigma} A\\ \uparrow_\sigma^{P(\vec{t})} & q & \!\triangleq\! & q \\ \uparrow_\sigma^{\dot{\bot}} & q & \!\triangleq\! & \mathit{flush}\,q\\ \uparrow_\sigma^{A \,\dot{\Rightarrow}\, B} & q & \!\triangleq\! & m \mapsto \uparrow_\sigma^B\!(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(q,\downarrow_\sigma^A\! m))\\ \uparrow_\sigma^{\dot{\forall} x\, A} & q & \!\triangleq\! & t \mapsto \uparrow_{\sigma,x\leftarrow t}^{A}\!(\dot{\mathit{APP^{\dot{\forall}}}}(q,t)),\\ \end{array} \end{align*} $$

where, for m proving ${\mathcal {M}_0} \vDash ^e_{\sigma } A \,\dot{\Rightarrow }\, B$ , the relative consistency proof $\mathit {kont}^{A \,\dot{\Rightarrow }\, B}_{\sigma }(m)$ is defined by

$$ \begin{align*}\!\begin{array}{lcl} \mathit{kont}^{A\,\dot{\Rightarrow}\, B}_{\sigma}(m) &\!\!\!\!:\!\!\!\!& (\mathcal{S}_{\lceil A[\sigma]\,\dot{\Rightarrow}\, B[\sigma] \rceil}, A[\sigma] \,\dot{\Rightarrow}\, B[\sigma] \vdash \dot{\bot}) \Rightarrow (\mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot})\\ \mathit{kont}^{A\,\dot{\Rightarrow}\, B}_{\sigma}(m) &\!\!\!\!\triangleq\!\!\!\!& r \!\mapsto\! \mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r),\downarrow_\sigma^B\! (m\, (\uparrow_\sigma^A\! (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r)))))).\\ \end{array} \end{align*} $$

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

$$ \begin{align*}\begin{array}{lclclcll} {\mathit{classic}_0} & {:} & \forall A\,(({\mathcal{M}_0} \vDash^e_{\mathit{id}} \dot{\neg}\dot{\neg} A) \Rightarrow ({\mathcal{M}_0} \vDash^e_{\mathit{id}} A))\\ \mathit{classic}_0 & \triangleq & A \mapsto m \mapsto \uparrow_{\mathit{id}}^A (\dot{\mathit{DN}}\,(\downarrow_{\mathit{id}}^{\dot{\neg}\dot{\neg} A}m)).\\ \end{array}\qquad\qquad \end{align*} $$

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

$$ \begin{align*}\begin{array}{lllcll} \mathit{init}_0 & {:} & \forall B\in \mathcal{T}_0\, {\mathcal{M}_0} \vDash^e_{\mathit{id}} B\\ \mathit{init}_0 & \triangleq & B \mapsto h \mapsto \uparrow_{\mathit{id}}^B (0,(B,\dot{\neg} A_0),\mathit{I_0}(J_{cons}(J_{\mathit{base}},h)),\dot{\mathit{ax}}_1).\\ \end{array}\qquad\qquad \end{align*} $$

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

$$ \begin{align*} \begin{array}{lcl} {\mathit{completeness}} & {:} & {\forall \mathcal{M}\forall \sigma\, ({\mathcal{M}} \vDash^e_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash^e_{\sigma} \mathcal{T}_0\Rightarrow{\mathcal{M}} \vDash^e_{\sigma} A_0)} \Rightarrow {\mathcal{T}_0 \vdash A_0}\\ \mathit{completeness} & \triangleq & \psi \mapsto \dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}} \\ && (\dot{\mathit{AX}}^0_{\dot{\neg} A_0},\downarrow_{\mathit{id}}^{A_0} (\psi\,\mathcal{M}_0\;\mathit{id}\;{\mathit{classic}_0}\;\mathit{init}_0)))).\\ \end{array} \end{align*} $$

Notice that the final result is a triple $(\Gamma ,g,p)$ such that p is a proof of $\Gamma \vdash A_0$ and g is a proof of $\Gamma \subset \mathcal {T}_0$ .

2.4 Computational content on examples

To illustrate the behaviour of the completeness proofs, we consider two examples. We use notations of $\lambda $ -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 \,\dot{\Rightarrow }\, Y \,\dot{\Rightarrow }\, X$ with X and Y propositional atoms.

The expansion of $\vDash ^e A_0$ is $\forall \mathcal {M}\;\forall \sigma \; ({\sigma } \vDash ^e_{\mathcal {M}} \mathcal {C}\mathit {lassic} \Rightarrow {\mathcal {M}} \vDash ^e_{} X \Rightarrow {\mathcal {M}} \vDash ^e_{} Y \Rightarrow {\mathcal {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

$$ \begin{align*}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.\end{align*} $$

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

$$ \begin{align*}m_0 \triangleq (x:X\in\mathcal{S}_\omega) \mapsto (y:Y\in \mathcal{S}_\omega) \mapsto x.\end{align*} $$

Our object proof is then the result of evaluating

$$ \begin{align*}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{AX}}^0_{\dot{\neg} A_0},\downarrow^{A_0} m_0))), \end{align*} $$

which proceeds as follows:

$$ \begin{align*}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{AX}}^0_{\dot{\neg} A_0},\dot{\mathit{AX}}_{A_0}(\mathit{kont}^{A_0}_{}(m_0))))), \end{align*} $$

where $\mathit {kont}^{A_0}_{}(m_0)(r)$ reduces to $\mathit {flush}\,(\dot{\mathit {APP^{\,\dot{\Rightarrow }\,}}}(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_2(r),\downarrow ^{Y \,\dot{\Rightarrow }\, X} (m_0\, (\uparrow ^X (\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_1(r))))))$ for r proving $\mathcal {S}_{\lceil A_0 \rceil }, A_0 \vdash \dot{\bot }$ , that is to

$$ \begin{align*}\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r),\dot{\mathit{AX}}_{Y \,\dot{\Rightarrow}\, X}(\mathit{kont}^{Y \,\dot{\Rightarrow}\, X}_{}(m_0\,(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r)))))). \end{align*} $$

In there, $\mathit {kont}^{Y \,\dot{\Rightarrow }\, X}_{}(m_0\,(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_1(r)))(r')$ , for $r'$ proving $\mathcal {S}_{\lceil Y \,\dot{\Rightarrow }\, X \rceil }, Y \,\dot{\Rightarrow }\, X \vdash \dot{\bot }$ , reduces in turn to

$$ \begin{align*}\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r'),m_0\, (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r))\, (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r')))). \end{align*} $$

Evaluating $\dot{\mathit {APP^{\,\dot{\Rightarrow }\,}}}(\dot{\mathit {AX}}^0_{\dot{\neg } A_0},\dot{\mathit {AX}}_{A_0}(\mathit {kont}^{A_0}_{}(m_0)))$ gives a tuple

$$ \begin{align*}(\lceil A_0 \rceil,(\dot{\neg} A_0,A_0),I_\Rightarrow(\mathit{inj}_{\lceil A_0 \rceil},\mathit{kont}^{A_0}_{}(m_0)),p_0),\end{align*} $$

where $p_0 \triangleq \dot{\mathit {app^{\,\dot{\Rightarrow }\,}}}(\dot{\mathit {ax}}_1,\dot{\mathit {ax}}_0)$ is a proof of $\dot{\neg } A_0, A_0 \vdash \dot{\bot }$ obtained by application of the two axiom rules proving $\dot{\neg } A_0 \vdash \dot{\neg } A_0$ and $\dot{\neg } A_0, A_0 \vdash A_0$ .

Evaluating the outermost $\mathit {flush}$ triggers the application of the continuation $\mathit {kont}^{A_0}_{}(m_0)$ to $r_0 \triangleq (\dot{\neg } A_0,\mathit {inj}_{\lceil A_0 \rceil },p_0)$ , meaning that the whole object proof becomes

$$ \begin{align*}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2\!(r_0),\dot{\mathit{AX}}_{Y \,\dot{\Rightarrow}\, X}(\mathit{kont}^{Y \,\dot{\Rightarrow}\, X}_{}(m_0\,(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_0))))))). \end{align*} $$

Evaluating $\dot{\mathit {APP^{\,\dot{\Rightarrow }\,}}}(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_2(r_0),\dot{\mathit {AX}}_{Y \,\dot{\Rightarrow }\, X}(\mathit {kont}^{Y \,\dot{\Rightarrow }\, X}_{}(m_0\,(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_1(r_0)))))$ gives a tuple

$$ \begin{align*}(\lceil Y \,\dot{\Rightarrow}\, X \rceil,(\dot{\neg} A_0,Y \,\dot{\Rightarrow}\, X),I_\Rightarrow(\mathit{inj}_{\lceil Y \,\dot{\Rightarrow}\, X \rceil},\mathit{kont}^{Y \,\dot{\Rightarrow}\, X}_{}(m_0\,(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_0)))),p_1),\end{align*} $$

where $p_1 \triangleq \dot{\mathit {app^{\,\dot{\Rightarrow }\,}}}(\pi ^{\,\dot{\Rightarrow }\,}_2\,(p_0),\dot{\mathit {ax}}_0)$ is a proof of $\dot{\neg } A_0, Y \,\dot{\Rightarrow }\, X \vdash \dot{\bot }$ .

Evaluating the new outermost $\mathit {flush}$ triggers in turn the application of the continuation $\mathit {kont}^{Y \,\dot{\Rightarrow }\, X}_{}(m_0\,(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_1(r_0)))$ to $r_1 \triangleq (\dot{\neg } A_0,\mathit {inj}_{\lceil Y \,\dot{\Rightarrow }\, X \rceil },p_1)$ and this results in

(1) $$ \begin{align}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r_1),m_0\, (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_0))\, (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_1))))), \end{align} $$

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

$$ \begin{align*}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r_1),\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_0)))). \end{align*} $$

No continuations are produced by $\dot{\mathit {APP^{\,\dot{\Rightarrow }\,}}}(\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_2(r_1),\dot{\mathit {PROJ}}^{\,\dot{\Rightarrow }\,}_1(r_0))$ so the only role of the last $\mathit {flush}$ is to peel the $\mathit {I_S}$ leading to a proof $r_2 \triangleq (\epsilon ,J_{\mathit {base}},\dot{\mathit {dn}}(p_2)),$ where $p_2 \triangleq \dot{\mathit {app^{\,\dot{\Rightarrow }\,}}}(\pi ^{\,\dot{\Rightarrow }\,}_2\,(p_1),\pi ^{\,\dot{\Rightarrow }\,}_1\,(p_0))$ combines a proof of $\dot{\neg } A_0 \vdash \dot{\neg } X$ with a proof of $\dot{\neg } A_0 \vdash X$ to get a proof of $\dot{\neg } A_0 \vdash \dot{\bot }$ .

To summarise, the object proof produced is

where $p_0$ is

As a matter of comparison, for the canonical proof of the validity of $A_0' \triangleq X \,\dot{\Rightarrow }\, Y \,\dot{\Rightarrow }\, Y$ , everything up to step (1) above is the same modulo the change of $A_0$ into $A_0'$ and of $Y \,\dot{\Rightarrow }\, X$ into $Y \,\dot{\Rightarrow }\, Y$ . After step (1), one obtains

$$ \begin{align*}\dot{\mathit{DNABS}}\,(\mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r_1'),\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r_1')))), \end{align*} $$

where

$$ \begin{align*}\begin{array}{lll} r_1' &\triangleq& (\dot{\neg} A_0',\mathit{inj}_{\lceil Y \,\dot{\Rightarrow}\, Y \rceil},p_1')\\ p_1' &\triangleq& \dot{\mathit{app^{\,\dot{\Rightarrow}\,}}}(\pi^{\,\dot{\Rightarrow}\,}_2\,(p_0'),\dot{\mathit{ax}}_0)\\ p_0' &\triangleq& \dot{\mathit{app^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{ax}}_1,\dot{\mathit{ax}}_0).\\ \end{array} \end{align*} $$

Finally, this yields $(\epsilon ,J_{\mathit {base}},\dot{\mathit {dn}}(p_2')),$ where $p_2' \triangleq \dot{\mathit {app^{\,\dot{\Rightarrow }\,}}}(\pi ^{\,\dot{\Rightarrow }\,}_2\,(p_1'),\pi ^{\,\dot{\Rightarrow }\,}_1\,(p_1'))$ , that is, graphically:

where, graphically, $p_1'$ is

We can notice in particular that, treating the metalanguage as a $\lambda $ -calculus as we did, the two canonical proofs of validity of $X \,\dot{\Rightarrow }\, X \,\dot{\Rightarrow }\, X$ would not produce the same object language proofs.

2.5 Extension to conjunction

Henkin’s original proof [Reference Henkin41] 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:

Truth for conjunction being defined by

$$ \begin{align*}{\mathcal{M}} \vDash^e_{\sigma} A_1 \,\dot{\wedge}\, A_2 ~~\triangleq~~ {\mathcal{M}} \vDash^e_{\sigma} A_1 \wedge {\mathcal{M}} \vDash^e_{\sigma} A_2 \end{align*} $$

a case is added for conjunctive formulae in each direction of the proof of ${\mathcal {M}_0} \vDash _{\sigma } A \Leftrightarrow A[\sigma ] \in \mathcal {S}_{\omega }$ as follows:

$$ \begin{align*}\begin{array}{llcl} \downarrow_\sigma^{A_1 \,\dot{\wedge}\, A_2} & (m_1,m_2) & \triangleq & \dot{\mathit{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}\!(\dot{\mathit{PROJ}}^{\land}_1\,q),\uparrow_\sigma^{A_2}\!(\dot{\mathit{PROJ}}^{\land}_2\,q)),\\ \end{array} \end{align*} $$

where the following combinators lift inference rules on $\mathcal {S}_\omega $ :

$$ \begin{align*}\begin{array}{lll} \dot{\mathit{PAIR}}(q_1,q_2) &\!\!\triangleq\!\!\!& \mathit{dest}\,\mathit{share}(q_1,q_2)\,\mathit{as}\,(n,\Gamma,f,p_1,p_2)\,\mathit{in}~(n,\Gamma,f,{\dot{\mathit{pair}}}(p_1,p_2))\\\dot{\mathit{PROJ}}^{\land}_{i}(n,\Gamma,f,p) &\!\!\triangleq\!\!\!& (n,\Gamma,f,{\dot{\mathit{\pi^{\wedge}}_{i}}}\,p).\\ \end{array} \end{align*} $$

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., [Reference Abel and Sattler1, Reference Altenkirch, Dybjer, Hofmann and Scott2]), we give a proof for disjunction that relies on the following arithmetical generalised form of $\mathsf {DNS}$ introducedFootnote ³¹ in [Reference Ilik52]:

$$ \begin{align*}\begin{array}{ll} \mathsf{DNS}^{\forall}_{\mathcal{C}} \quad & \forall n\, ((\mathcal{A}(n) \Rightarrow \mathcal{C}) \Rightarrow \mathcal{C}) \Rightarrow (\forall n\, \mathcal{A}(n) \Rightarrow \mathcal{C}) \Rightarrow \mathcal{C} \end{array} \end{align*} $$

for $\mathcal {C}$ a $\Sigma ^0_1$ -formula and $\mathcal {A}$ arbitrary (usual $\mathsf {DNS}$ is then $\mathsf {DNS}^\forall _\bot $ ).

The proof however requires a significant change: instead of proving ${\mathcal {M}_0} \vDash ^e_{\sigma } A \Leftrightarrow {A[\sigma ]\in \mathcal {S}_\omega }$ , we prove:

$$ \begin{align*}\begin{array}{lll} \downarrow^A_\sigma &:& {\mathcal{M}_0} \vDash^e_{\sigma} A \Rightarrow {A[\sigma]\in \mathcal{S}_\omega}\\ {\uparrow'_\sigma}^A &:& {A[\sigma]\in \mathcal{S}_\omega} \Rightarrow \mathsf{KONT}({\mathcal{M}_0} \vDash^e_{\sigma} A),\\ \end{array} \end{align*} $$

where $\mathsf {KONT}(\mathcal {A})$ , a continuation monad,Footnote ³² is defined by

$$ \begin{align*}\mathsf{KONT}(\mathcal{A}) ~~~\triangleq~~~ (\mathcal{A} \,\Rightarrow\, \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot}) \,\Rightarrow\, \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot.} \end{align*} $$

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 [Reference Ilik53].

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

Let us also consider the following lifting of the inference rules to provability in $\mathcal {S}_\omega $ :

$$ \begin{align*}\begin{array}{llclclllll} \dot{\mathit{INJ}}_i: & A_i \in \mathcal{S}_\omega &{\!\!\Rightarrow\!\!}& A_1 \,\dot{\vee}\, A_2 \in \mathcal{S}_\omega\\\dot{\mathit{INJ}}_i & (n,\Gamma,f,p) &\!\!\triangleq\!\!& (n,\Gamma,f,\dot{\mathit{inj}}_i\,p)\\ \\ \dot{\mathit{CASE}}: & \!\!\!\left(\begin{array}{l}A \,\dot{\vee}\, B \in \mathcal{S}_\omega\\ A \,\dot{\Rightarrow}\, C \in \mathcal{S}_\omega\\ B \,\dot{\Rightarrow}\, C \in \mathcal{S}_\omega\end{array}\right)&{\!\!\Rightarrow\!\!}& C \in \mathcal{S}_\omega\\ \dot{\mathit{CASE}} & (q,q_1,q_2) & \!\!\triangleq\!\!& \!\!\!\begin{array}{l}\mathit{dest}\,\mathit{share_3}(q,q_1,q_2)\,\mathit{as}\,(n,\Gamma,f,p,p_1,p_2)\,\mathit{in}\\ (n,\Gamma,f,\dot{\mathit{case}}\,p\,p_1\,p_2),\end{array}\\ \end{array} \end{align*} $$

where we needed the following three-part variant $\mathit {share_3}$ of $\mathit {share}$ :

$$ \begin{align*}\begin{array}{ll}\mathit{share_3} : & A_1 \in \mathcal{S}_{\omega} \land A_2 \in \mathcal{S}_{\omega} \land A_3 \in \mathcal{S}_{\omega} \\& \Rightarrow \exists n\exists \Gamma (\Gamma \subset \mathcal{S}_n \land \Gamma \vdash A_1 \land \Gamma \vdash A_2 \land \Gamma \vdash A_3)\\\mathit{share_3} &(q_1,q_2,(n,\Gamma,f,p_3)) \\ & \triangleq \begin{array}{l}\mathit{dest}\,\mathit{share}(q_1,q_2)\,\mathit{as}\\ (n',\Gamma',f',p_1,p_2)\,\mathit{in}\\\end{array} {\begin{array}{l}\mathit{dest}\,\mathit{share}((n',\Gamma',f',p_2),(n,\Gamma,f,p_3))\,\\\mathit{as}\,(n",\Gamma",f",p_2',p_3)\,\\\mathit{in}~(n",\Gamma",f",\dot{\mathit{weak}}(\mathit{incl'}^{\Gamma',\Gamma}_1,p_1),p_2',p_3).\end{array}}\\\end{array} \end{align*} $$

Truth for disjunction being defined by

$$ \begin{align*}{\mathcal{M}} \vDash^e_{\sigma} A_1 \,\dot{\vee}\, A_2 ~~\triangleq~~ {\mathcal{M}} \vDash^e_{\sigma} A_1 \vee {\mathcal{M}} \vDash^e_{\sigma} A_2,\end{align*} $$

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

$$ \begin{align*}\begin{array}{llcl} {\downarrow_\sigma^A~:} & {\mathcal{M}_0} \vDash^e_{\sigma} A & {\Rightarrow} & {A[\sigma]\in \mathcal{S}_\omega}\\ \downarrow_\sigma^{P(\vec{t})} & m & \!\triangleq\! & m\\ \downarrow_\sigma^{\dot{\bot}} & m & \!\triangleq\! & \dot{\mathit{BOT}}(m)\\ \downarrow_\sigma^{A \,\dot{\Rightarrow}\, B} & m & \!\triangleq\! & \dot{\mathit{AX}}_{A[\sigma] \,\dot{\Rightarrow}\, B[\sigma]}(\mathit{kont'}^{A\,\dot{\Rightarrow}\, B}_{\sigma}(m))\\ \downarrow_\sigma^{\dot{\forall} x\, A} & m & \!\triangleq\! & \dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{AX}}_{(\forall x\,A)[\sigma]},\downarrow_{\sigma,x\leftarrow x_n}^{A}\! (m\, x_n))~ \\ &&&\mathit{where}\ 2n = \lceil (\dot{\forall} x\, A)[\sigma] \rceil\\ \downarrow_\sigma^{A_1 \,\dot{\wedge}\, A_2} & (m_1,m_2) & \triangleq & \dot{\mathit{PAIR}}\,(\downarrow_\sigma^{A_1}\!m_1, \downarrow_\sigma^{A_2}\!m_2)\\ \downarrow^{A_1 \,\dot{\vee}\, A_2}_{\sigma} &\!\! m\!\! & \!\!\!\triangleq\!\!\! & \mathit{case}~{m}~\mathit{of}~\!\!\!\begin{array}[t]{l}[{\mathit{inj}_1(m_1)} \mapsto {\dot{\mathit{INJ}}_1(\downarrow^{A_1}_{\sigma}\!\!m_1)}~\\|\,{\mathit{inj}_2(m_2)} \mapsto {\dot{\mathit{INJ}}_2(\downarrow^{A_2}_{\sigma}\!\!m_2)}].\end{array}\\ \end{array} \end{align*} $$

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

$$ \begin{align*}& \mathit{kont'}^{A\,\dot{\Rightarrow}\, B}_{\sigma}(m)(r)\\ & \triangleq (\uparrow_\sigma^{'A} (\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r)))\, (m' \mapsto \mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_2(r),\downarrow_\sigma^B (m m')))). \end{align*} $$

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 $\mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot }$ . This is a standard proof by induction on A:

$$ \begin{align*}\begin{array}{lllll} \mathit{EFQ}_{\sigma}^A : & \mathcal{T}_0, \dot{\neg} A_0 \vdash \dot{\bot} & \Rightarrow & {\mathcal{M}_0} \vDash^e_{\sigma} A\\ \mathit{EFQ}_{\sigma}^{P(\vec{t})} & (\Gamma,g,p) & \triangleq & (0,(\Gamma,\dot{\neg} A_0),\mathit{I_0}(g),\mathit{efq}\, p)\\ \mathit{EFQ}_{\sigma}^{\dot{\bot}} & (\Gamma,g,p) & \triangleq & (\Gamma,g,p)\\ \mathit{EFQ}_{\sigma}^{A \,\dot{\Rightarrow}\, B} & (\Gamma,g,p) & \triangleq & m \mapsto \mathit{EFQ}_{\sigma}^{B} (\Gamma,g,p)\\ \mathit{EFQ}_{\sigma}^{\dot{\forall} x\,A} & (\Gamma,g,p) & \triangleq & t \mapsto \mathit{EFQ}_{\sigma,x\leftarrow t}^{A} (\Gamma,g,p)\\ \mathit{EFQ}_{\sigma}^{A_1 \,\dot{\wedge}\, A_2} & (\Gamma,g,p) & \triangleq & (\mathit{EFQ}_{\sigma}^{A_1} (\Gamma,g,p), \mathit{EFQ}_{\sigma}^{A_2} (\Gamma,g,p))\\ \mathit{EFQ}_{\sigma}^{A_1 \,\dot{\vee}\, A_2} & (\Gamma,g,p) & \triangleq & \mathit{inj}_1\,(\mathit{EFQ}_{\sigma}^{A_1} (\Gamma,g,p)),\\ \end{array} \end{align*} $$

where we may notice in passing that an arbitrary choice is made in the disjunction case.

We need the shift of double negation with respect to implication to formulae expressing truth. Ex falso quodlibet being obtained on formulae expressing truth with respect to possibly-exploding models, the proof is standard:

$$ \begin{align*}\begin{array}{lcl} \mathsf{DNS}^{\Rightarrow} &\!\!:\!\!& (\mathcal{A} \Rightarrow \mathsf{KONT}({\mathcal{M}_0} \vDash^e_{\sigma} B)) ~\Rightarrow~ \mathsf{KONT}(\mathcal{A} \Rightarrow {\mathcal{M}_0} \vDash^e_{\sigma} B)\\ \mathsf{DNS}^{\Rightarrow} &\!\!\triangleq\!\! & H \mapsto K \mapsto K\, (m_A \mapsto \mathit{EFQ}_{\sigma}^B\, (H~m_A~(m_B \mapsto K~(m_A' \mapsto m_B)))).\\ \end{array} \end{align*} $$

We also need the shift of double negation with respect to conjunction. The intuitionistic proof is easy:

$$ \begin{align*}\begin{array}{lcl} \mathsf{DNS}^{\land} &\!\!:\!\!& \mathsf{KONT}(\mathcal{A}_1) \land \mathsf{KONT}(\mathcal{A}_2) \Rightarrow \mathsf{KONT}(\mathcal{A}_1 \land \mathcal{A}_2)\\ \mathsf{DNS}^{\land} &\!\!\triangleq\!\! & (H_1,H_2) \mapsto K \mapsto H_1\, (m_1 \mapsto H_2\, (m_2 \mapsto K~(m_1,m_2))).\\ \end{array} \end{align*} $$

We are now ready to reformulate reflection, including the case for disjunction:

$$ \begin{align*}\begin{array}{llcl} {\uparrow_\sigma^{'A~}:} & {A[\sigma] \in \mathcal{S}_\omega} & {\rightarrow} & \mathsf{KONT}\,({\mathcal{M}_0} \vDash^e_{\sigma} A)\\ \uparrow_\sigma^{'P(\vec{t})} & q & \!\triangleq\! & K \mapsto K\,q \\ \uparrow_\sigma^{'\dot{\bot}} & q & \!\triangleq\! & K \mapsto \mathit{flush}\,q\\ \uparrow_\sigma^{'A \,\dot{\Rightarrow}\, B} & q & \!\triangleq\! & \mathsf{DNS}^{\Rightarrow} (m \mapsto \uparrow_\sigma^{'B} (\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(q,\downarrow_A m)))\\ \uparrow_\sigma^{'\dot{\forall} x\, A(x)} & q & \!\triangleq\! & \mathsf{DNS}^{\forall}\, (t \mapsto \uparrow_{\sigma,x\leftarrow t}^{'A}(\dot{\mathit{APP^{\dot{\forall}}}}(q,t)))\\ \uparrow_\sigma^{'A_1 \,\dot{\wedge}\, A_2} & q & \triangleq & \mathsf{DNS}^{\land}(\uparrow_\sigma^{'A_1}(\dot{\mathit{PROJ}}^{\land}_1\,q),\uparrow_\sigma^{'A_2}(\dot{\mathit{PROJ}}^{\land}_2\,q))\\ \uparrow_\sigma^{'A_1 \,\dot{\vee}\, A_2} & q & \!\!\triangleq\!\! & K \mapsto \mathit{flush}\,(\dot{\mathit{CASE}}(q,\!\!\!\begin{array}[t]{l}\dot{\mathit{AX}}_{\dot{\neg} A_1}(\mathit{kont}^{A_1\,\dot{\vee}\, A_2}_{\sigma,1}(K)),\\\dot{\mathit{AX}}_{\dot{\neg} A_2}(\mathit{kont}^{A_1\,\dot{\vee}\, A_2}_{\sigma,2}(K)))),\end{array}\\ \end{array} \end{align*} $$

where, for K proving ${\mathcal {M}_0} \vDash ^e_{id} \dot{\neg } (A_1\,\dot{\vee }\, A_2)$ , the continuation $\mathit {kont}^{A_1\,\dot{\vee }\, A_2}_{\sigma ,i}(K)$ is defined by

$$ \begin{align*}\begin{array}{lclclcll} \mathit{kont}^{A_1\,\dot{\vee}\, A_2}_{\sigma,i}(K) &\!\!\!:\!\!\!& (\mathcal{S}_{\lceil \dot{\neg} A_i[\sigma] \rceil}, \dot{\neg} A_i[\sigma] \vdash \dot{\bot}) ~\Rightarrow~ (\mathcal{T}_0,\dot{\neg} A_0 \vdash \dot{\bot})\\ \mathit{kont}^{A_1\,\dot{\vee}\, A_2}_{\sigma,i}(K) & \triangleq & r \mapsto (\uparrow_\sigma^{'A_i}(\dot{\mathit{PROJ}}^{\,\dot{\Rightarrow}\,}_1(r)))\,(m \mapsto K\,(\mathit{inj}_i\,m)).\\ \end{array} \end{align*} $$

The proof of $\mathit {classic}_0$ follows a different pattern than the one without $\mathsf {KONT}$ . For it and for the proof of $\mathit {init}_0$ , we use again $\mathsf {DNS}^{\forall }$ to distribute the quantification over the axioms of the theory:

$$ \begin{align*}\begin{array}{lllcll} {\mathit{classic}_0} & {:} & \mathsf{KONT}(\forall A\, (({\mathcal{M}_0} \vDash^e_{\mathit{id}} \dot{\neg}\dot{\neg} A) \Rightarrow ({\mathcal{M}_0} \vDash^e_{id} A)))\\ \mathit{classic}_0 & \triangleq & \mathsf{DNS}^{\forall}\, (A \mapsto \mathsf{DNS}^{\Rightarrow} (m \mapsto m))\\ \\ \mathit{init}_0 & {:} & \mathsf{KONT}(\forall B\in \mathcal{T}_0\, {\mathcal{M}_0} \vDash^e_{\mathit{id}} B)\\ \mathit{init}_0 & \triangleq & \mathsf{DNS}^{\forall}\, (B \mapsto \mathsf{DNS}^{\Rightarrow} (h \mapsto \uparrow_{\mathit{id}}^{'B}(0,(B,\dot{\neg} A_0),\mathit{I_0}(J_{cons}(J_{\mathit{base}},h)),\dot{\mathit{ax}}_1))).\\ \end{array} \end{align*} $$

Finally, the proof of completeness also needs to chain continuations:

$$ \begin{align*}\begin{array}{lllcl} {\mathit{completeness}} & {:} & {\forall \mathcal{M}\forall \sigma\, ({\mathcal{M}} \vDash^e_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash^e_{\sigma} \mathcal{T}_0\Rightarrow{\mathcal{M}} \vDash^e_{\sigma} A_0)} \Rightarrow {\mathcal{T}_0 \vdash A_0}\\ \mathit{completeness} & \triangleq & \psi \mapsto \dot{\mathit{DNABS}}\,({\mathit{completeness}'}\,\psi),\\ \end{array} \end{align*} $$

where

$$ \begin{align*}\!\begin{array}{lllcl} {\mathit{completeness}'} : {\forall \mathcal{M}\forall \sigma\, ({\mathcal{M}} \vDash^e_{\sigma} \mathcal{C}\mathit{lassic} \Rightarrow {\mathcal{M}} \vDash^e_{\sigma} \mathcal{T}_0\Rightarrow{\mathcal{M}} \vDash^e_{\sigma} A_0)} \Rightarrow \dot{\neg} A_0, {\mathcal{T}_0 \vdash \dot{\bot}}\\ \mathit{completeness}' \triangleq\\ \qquad\psi \!\mapsto\! \mathit{classic}_0\, (c \!\mapsto\! \mathit{init}_0\, (i \!\mapsto\! \mathit{flush}\,(\dot{\mathit{APP^{\,\dot{\Rightarrow}\,}}}(\dot{\mathit{AX}}^0_{\dot{\neg} A_0},\downarrow_{\mathit{id}}^{A_0} (\psi\,\mathcal{M}_0\,\mathit{id}\,c\,i))))).\\ \end{array} \end{align*} $$

An interesting remark is that $\mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot }$ intuitionistically implies $\mathsf {KONT}(\bot )$ , so, by using $\mathsf {KONT}$ , reflection for $\dot{\bot }$ does not need any more to consider possibly-exploding model in order to be intuitionistically valid. The need for possibly-exploding models (or Markov’s principle) shows up instead in proving $\mathit {EFQ}_{\sigma }^{\dot{\bot }} : \mathcal {T}_0, \dot{\neg } A_0 \vdash \dot{\bot } \Rightarrow {\mathcal {M}_0} \vDash ^e_{\sigma } \dot{\bot }$ which is in turn required to prove our specific version of $\mathsf {DNS}^{\Rightarrow }$ , itself used to prove reflection for the connective $\,\dot{\Rightarrow }\,$ , as well as to prove $\mathit {classic}_0$ and $\mathit {init}_0$ .

2.7 Reverse mathematics of completeness in the presence of disjunction

Kirst [Reference Kirst60, 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:

$$ \begin{align*}\neg\neg\forall n\,(\neg \mathcal{A}(n) \lor \neg\neg \mathcal{A}(n)), \end{align*} $$

which in turn is equivalent to the following instance of $\mathsf {DNS}^{\forall }_{\bot }$ for disjunctions:

$$ \begin{align*}\mathsf{DDNS} \qquad \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)). \end{align*} $$

In private communication, Kirst even showed that $\mathsf {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 proofFootnote ³³ 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 $\,\dot{\Rightarrow }\,$ , $\,\dot{\vee }\,$ , and $\dot{\bot }$ relative to enumerable theories and a $\Sigma ^0_1$ exploding interpretation of $\dot{\bot }$ implies the following generalisedFootnote ³⁴ Footnote ³⁵ form of $\mathsf {DDNS}$ for $\mathcal {A}$ , $\mathcal {B}$ , and $\mathcal {C} \Sigma _0^1$ -formulas and for $\mathcal {D}$ ranging over $\Sigma _0^1$ -formulas too:

$$ \begin{align*}\mathsf{DDNS}_{\mathcal C} \qquad &\forall n\,\neg_{\mathcal{C}}(\forall \mathcal{D}\,\neg_{\mathcal{D}}\,(\neg_{\mathcal{D}} \mathcal{A}(n) \\ &\lor \neg_{\mathcal{D}} \mathcal{B}(n))) \Rightarrow \neg_{\mathcal{C}}(\forall \mathcal{D}\,\neg_{\mathcal{D}}\forall n\,(\neg_{\mathcal{D}} \mathcal{A}(n) \lor \neg_{\mathcal{D}} \mathcal{B}(n))), \end{align*} $$

where $\neg _{\mathcal {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{\neg } X_n \,\dot{\vee }\, \dot{\neg } 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 _{\mathcal {D}} \forall n\,(\neg _{\mathcal {D}} \mathcal {A}(n) \lor \neg _{\mathcal {D}} \mathcal {B}(n))$ impliesFootnote ³⁶ $\mathcal {T} \vDash \dot{\bot }$ , which implies $\Gamma \vdash \dot{\bot }$ for a finite subset $\Gamma $ of $\mathcal {T}$ by completeness, which implies in turn $\Gamma \vDash \dot{\bot }$ by soundness. Now, by taking the exploding model $\mathcal {M}_{\mathit {std}}$ interpreting $X_n$ by $\mathcal {A}(n)$ , $Y_n$ by $\mathcal {B}(n)$ and $\dot{\bot }$ by $\mathcal {C}$ , the final goal $\mathcal {C}$ , that is, $\mathcal {M}_{\mathit {std}} \vDash \dot{\bot }$ , can eventually be obtained by proving $\mathcal {M}_{\mathit {std}} \vDash \mathcal {T}$ , that is, $\mathcal {M}_{\mathit {std}} \vDash \dot{\neg } X_n \,\dot{\vee }\, \dot{\neg } Y_n$ , that is, $\neg _{\mathcal {C}} \mathcal {A}(n) \lor \neg _{\mathcal {C}} \mathcal {B}(n)$ , for only those finite number of $\dot{\neg } X_n \,\dot{\vee }\, \dot{\neg } Y_n$ in $\Gamma $ . The latter can be obtained by first chaining a finite number of instances of $\forall n\,\neg _{\mathcal {C}}\neg _{\mathcal {C}}\,(\neg _{\mathcal {C}} \mathcal {A}(n) \lor \neg _{\mathcal {C}} \mathcal {B}(n))$ , each of them coming by instantiating $\mathcal {D}$ with $\mathcal {C}$ in $\forall n\,\neg _{\mathcal {C}}\forall {\mathcal {D}}\,\neg _{\mathcal {D}}\,(\neg _{\mathcal {D}} \mathcal {A}(n) \lor \neg _{\mathcal {D}} \mathcal {B}(n))$ for the corresponding n’s.

The conjunction of facts that $\mathsf {DDNS}_{\mathcal {C}}$ is provable from completeness with possibly-exploding semantics, that it is equivalent to $\mathsf {DDNS}_{\bot }$ in the presence of Markov’s principle, that Markov’s principle is the principle needed to handle falsity in a non-exploding semantics and that Kirst showed that nothing more is needed to handle both falsity and disjunction suggests that $\mathsf {DDNS}_{\mathcal {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 $\mathsf {DNS}^{\forall }_{\mathcal {C}}$ for $\exists $ -free formulae, we conjecture that it could be obtained using $\mathsf {DDNS}_{\mathcal {C}}$ instead of $\mathsf {DNS}^{\forall }_{\mathcal {C}}$ , that is, we conjecture that either $\mathsf {DNS}^{\forall }_{\mathcal {C}}$ for $\exists $ -free formulae derives from $\mathsf {DDNS}$ or that the completeness proof can be modified to depend only on $\mathsf {DDNS}_{\mathcal {C}}$ .

Two other recent lines of research about the reverse mathematics of completeness with disjunction are Krivtsov [Reference Krivtsov70] and Espíndola [Reference Espíndola25, Reference Espíndola26]. Krivtsov showed that with respect to exploding modelsFootnote ³⁷ Gödel’s completeness for recursively enumerable theories is equivalent to the Weak Fan Theorem ( $\mathsf {WFT}$ ) over a rather weak intuitionistic arithmetic. This is to be compared to Veldman’s proof of completeness with respect to Kripke semantics [Reference Veldman87] which already required $\mathsf {WFT}$ . Since $\mathsf {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 [Reference Simpson80]. On his side, reasoning in the language of topos theory, Espíndola proved the same result in IZF, where $\mathsf {WFT}$ was formulated as the compactness of the Cantor space.

The situation regarding $\mathsf {WFT}$ is rather subtile as there are different formulations depending on how infinite paths are represented in a binary tree (see [Reference Brede and Herbelin13]). Let us call $\mathsf {WFT}_{\mathit {pred}}$ the intuitionistically provableFootnote ³⁸ variant of $\mathsf {WFT}$ where infinite paths are represented using a predicate and $\mathsf {WFT}_{\mathit {dec}}$ the weakly classical variantFootnote ³⁹ where infinite paths are represented using a decidable predicate. Both Krivtsov and Espíndola’s results refer to $\mathsf {WFT}_{\mathit {dec}}$ . On the other side, Krivine’s proof and our own proof for the language without disjunction are intuitionistic and thus do not require $\mathsf {WFT}_{\mathit {dec}}$ . This is consistent with another result of Espíndola with Forssell [Reference Espíndola26, Reference Forssell and Espíndola28] showing that $\mathsf {WFT}_{\mathit {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, $\mathsf {WFT}_{\mathit {pred}}$ is provable (if we had instead reasoned in a weaker arithmetic, we would certainly have explicitly needed $\mathsf {WFT}_{\mathit {pred}}$ , the same way as Weak Kőnig’s Lemma was needed in [Reference Simpson80]). Moreover, this is consistent with yet another result, namely, the formal equivalence between $\mathsf {WFT}_{\mathit {pred}}$ and completeness with respect to Scott entailment relations in [Reference Brede and Herbelin13]. In turn, we conjecture that $\mathsf {WFT}_{\mathit {dec}}$ , thus completeness with respect to exploding models and all connectives, disjunction included, is equivalent to $\mathsf {WFT}_{\mathit {pred}}$ together with $\mathsf {DDNS}_{\mathcal {C}}$ .

To conclude, note also that like Markov’s principle, $\mathsf {DNS}^{\forall }_{\mathcal {C}}$ and thus $\mathsf {DDNS}_{\mathcal {C}}$ as well preserve the witness and disjunction properties of intuitionistic logic, so they are in this sense intuitionistically valid. Also, to compute with $\mathsf {DNS}^{\forall }_{\mathcal {C}}$ , bar recursion [Reference Spector and Dekker82] or delimited continuations [Reference Ilik52] 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 necessary. The idea is to consider an enumeration of formulae which takes existential formulae into account, then to add a clause to the definition of $\Gamma \subset \mathcal {S}_n$ similar to the one for universal quantification, using Henkin’s axiom $\dot{\exists } y\, A(y) \,\dot{\Rightarrow }\, A(x)$ for x taken fresh in the finite set of formulae coming before $\dot{\exists } y\,A(y)$ in the enumeration.Footnote ⁴⁰ Reification 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 $(\exists y\, A)[\sigma ] \in \mathcal {S}_\omega $ with the proof of $(\dot{\exists } y\, A)[\sigma ] \,\dot{\Rightarrow }\, A[\sigma ,y\leftarrow x]$ available at some level $\mathcal {S}_n$ to get a proof of $A[\sigma ,y\leftarrow x] \in \mathcal {S}_\omega $ , then a proof of ${\mathcal {M}} \vDash ^e_{\sigma ,y\leftarrow x} A$ , thus a proofFootnote ⁴¹ of ${\mathcal {M}} \vDash ^e_{\sigma } \exists y\,A$ .

2.9 Constructive content of the presented proofs

In this article, when talking about proofs, we have used the words “constructive”, “computational”, and “effective” as synonyms. This is common practice, although one can distinguish between the three words if one wants to, thanks to the varieties of constructive mathematics available [Reference Bridges, Palmgren, Ishihara, Zalta and Nodelman14].Footnote ⁴² In any case, for each of the constructive proofs presented, our (informal) metatheory has the disjunction and the existence property and its proof terms are (or can be extracted to) recursive programs.

One may wonder what is the formal relation between the OCaml program from Appendix A and the completeness theorem from Section 2.3 (page 22). One can think of that OCaml program as a program extracted by a modified realisability interpretation, or, if one prefers, a program extracted from a formalization in the Calculus of Inductive Construction (a first version of the theorem has been formalized in Coq in 2008).

The OCaml program is not a formal extraction from a formal proof of the theorem. Its purpose is to be a self-contained and optimal expression of the constructive content of the completeness theorem. It is an attempt to demystify the mechanisms that underlie Henkin’s proofs, and especially its model theoretic part.