Completeness of First-Order Bi-Intuitionistic Logic

Kirst, Dominik; Shillito, Ian

doi:10.4230/LIPIcs.CSL.2025.40

Completeness of First-Order Bi-Intuitionistic Logic

Dominik Kirst

Université Paris Cité, IRIF, Inria, Paris, France
Ben-Gurion University, Beer-Sheva, Israel Ian Shillito

The Australian National University, Canberra, Ngunnawal & Ngambri Country, Australia

Abstract

We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.

Keywords and phrases:

bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant

Funding:

Dominik Kirst: Received funding from the European Union’s Horizon research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101152583 and a Minerva Fellowship of the Minerva Stiftung Gesellschaft für die Forschung mbH.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof theory ; Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Modal and temporal logics

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In the 1970s, Cecylia Rauszer provided foundations for bi-intuitionistic logic (first studied by Moisil [34]), an extension of intuitionistic logic with a binary operator $\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure0% .pdf}}}\hskip 0.43057pt}$ called exclusion, dual to the intuitionistic implication $\rightarrow$ . Her work spanned over most approaches to non-classical logics, ranging from algebras [43, 45], Kripke semantics [44, 46, 47], sequent calculus [42], to Hilbert systems [43, 42]. The impressiveness and exhaustiveness of Rauszer’s study of bi-intuitionistic logic is not only measured by the variety of fields she introduced bi-intuitionistic in, but by the analysis in each case of both the propositional and first-order logic.

Unfortunately, through time several mistakes were detected in Rauszer’s work. First, her sequent calculus for propositional bi-intuitionistic logic was shown by Pinto and Uustalu [38] not to admit cut, contradicting her claim [42, Result 2.3]. To correct this, they provided a calculus based on sequents with richer structure, which they proved to admit cut. Secondly, a confusion around the status of the deduction theorem led Goré and Shillito [18] to notice the conflation in Rauszer’s work of two different propositional bi-intuitionistic logics. This conflation resulted in an incorrect completeness proof for the propositional case, ultimately resolved by Goré and Shillito. Finally, the errors contained in the propositional case continue being present in Rauszer’s work on the first-order case as noted by Shillito [50], who failed to fix the proof in this setting. So, to date, no completeness proof for first-order bi-intuitionistic logic ( $\mathsf{FOBIL}$ ) along the lines of Rauszer’s argument is known.

To our knowledge, the only other candidate proof was given by Klemke in 1971 [30], thereby in fact predating Rauszer’s work. He attributes the semantics of the logic to Grzegorczyk [19] and uses a Henkin-style argument to construct a universal model. However, its correctness is questioned by Olkhovikov and Badia [35], who write:

“Incidentally, there is an alternative completeness argument by Klemke, where bi-intuitionistic predicate logic is studied possibly for the first time in print (and, as far as we know, independently from Rauszer’s work) and that contains other errors.”

As his proof strategy is technically involved and, being written in fairly old style (and German language), the presentation is rather inaccessible to a broader audience, it is hard to assess whether these errors are locally fixable or as substantially unfixable as Rauszer’s.

We therefore opt for an alternative route to settle the completeness of $\mathsf{FOBIL}$ once and for all: we present a succinct proof based on standard techniques, coming in a modern (and English) presentation for easy assessment, and use the Coq proof assistant to verify our argument, therefore leaving no room for ambiguity and error.

In that vein, our formal investigation finally establishes solid foundations for $\mathsf{FOBIL}$ , and simultaneously tightly connects the provability of the constant domain axiom in this logic with constant domain models. That is, contrarily to the propositional case, first-order bi-intuitionistic logic is known not to be a conservative extension of first-order intuitionistic logic [48, p.56][32, 50]: it derives the constant domain axiom (CD), displayed below, which is not provable in the purely intuitionistic counterpart [16].

\forall x(\varphi(x)\lor\psi)\rightarrow(\forall x\varphi(x)\lor\psi)

(CD)

Here, the variable $x$ is required not to occur freely in $\psi$ . As the name suggests, this axiom characterises the constant domain property on models in the Kripke semantics for the intuitionistic language [19, 16, 36]. Rauszer suggested that this connection between the axiom and the property on models should also hold in the bi-intuitionistic setting [44, 48]. The first-order Kripke semantics she developed uses frames for intuitionistic logic satisfying the constant domain property, thus capturing the semantics for $\mathsf{FOCDIL}$ , i.e. first-order intuitionistic logic extended with the (CD) axiom. Our results provide a confirmation of Rauszer’s suggestion by showing $\mathsf{FOBIL}$ complete relative to the constant domain semantics, notably settling the logic as a conservative extension of $\mathsf{FOCDIL}$ [48, p.57][5].

In fact, our presented completeness proof for bi-intuitionistic logic mostly follows the textbook proof of Gabbay, Shehtman, and Skvortsov [17] for $\mathsf{FOCDIL}$ . As our only actually novel idea, we observe that their use of a custom Lindenbaum lemma exploiting the (CD) axiom to obtain successor worlds in a universal model can be dualised, namely, to obtain also predecessor worlds, exploiting a dualisation of the (CD) axiom presented below.

(\exists x\varphi(x)\land\psi)\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure1.pdf}}}\hskip 0.43057pt}\exists x(% \varphi(x)\land\psi)

(DCD)

While (CD) is used as a theorem, i.e. ${\top}\vdash{\ref{ax:CD}}$ , we exploit the contradictory nature of (DCD) in our custom lemma, as it satisfies ${\ref{ax:DCD}}\vdash{\bot}$ . The remaining argument is also streamlined to dispose of the usual Henkin-style syntax extensions to obtain a particularly succinct presentation that is feasible to verify in Coq with little technical overhead.

In summary, the contributions of the present paper are as follows:

$\blacksquare$

We give a succinct completeness proof for $\mathsf{FOBIL}$ based on standard techniques, closing a gap in the literature not featuring a single unquestionably correct proof.
$\blacksquare$

We illustrate the tight connection of $\mathsf{FOBIL}$ and $\mathsf{FOCDIL}$ , in that our completeness proof of the former extends and dualises the one of the latter.
$\blacksquare$

We provide a Coq mechanisation verifying all definitions and results in the paper for absolute clarity and correctness, hyperlinked within this paper via clickable icons.
$\blacksquare$

As a by-product, we contribute, to the best of our knowledge, the first mechanisation of the completeness of $\mathsf{FOCDIL}$ and the conservativity of $\mathsf{FOBIL}$ over $\mathsf{FOCDIL}$ .

After some preliminary remarks on our meta-theory based on constructive type theory in Section 2, we recall the syntax, deduction system, and semantics of $\mathsf{FOBIL}$ in Section 3, including a dedicated discussion of the different constant domain axioms. In Section 4, we then prove the three versions of Lindenbaum lemmas needed to establish completeness and conservativity in Section 5. We end with remarks on the Coq development as well as related and future work in Section 6.

2 Preliminaries

The forthcoming mathematical development can be performed in any standard meta-theoretical foundation. To be formally precise and close to the mechanisation, we work in the calculus of inductive constructions (CIC) [4, 37] underlying the Coq proof assistant [53] and briefly sketch the key features we need. The core of the system is a predicative hierarchy of computational types closed under the usual type formers like (dependent) function types and (dependent) pair types. CIC further comes with an impredicative universe $\mathbb{P}$ of propositions in which the above type formers take common logical notation. Inductive types and predicates can be formed via a general scheme, for instance to accommodate the types $\mathbb{N}$ of natural numbers, $\mathbb{B}$ of boolean values, and of finite lists $X^{*}$ over a given type $X$ .

The logic represented in $\mathbb{P}$ is constructive but also agnostic, so in particular the excluded middle ( $\forall P:\mathbb{P}.P\lor\neg P$ ) is not provable but it can be assumed consistently. As in this paper we are aiming at a minimalistic proof directed to an audience not necessarily interested in questions of constructivism, we in fact assume the excluded middle globally and highlight its uses in the most crucial cases. Moreover, we assume the axiom of unique choice to freely identify total functional relations $X\to Y\to\mathbb{P}$ with functions $X\to Y$ where convenient. That is, we effectively simulate a traditional foundation based on classical set-theory to make the text as accessible as possible to readers unfamiliar with constructive type theory.

3 Basics of Bi-intuitionistic Logic

We present the basics of first-order bi-intuitionistic logic: its syntax, axiomatic proof system, constant domain Kripke semantics, and known facts of relevance, mostly following the presentations in [50] and [51].

3.1 Syntax

As mentioned above, first-order bi-intuitionistic logic is expressed in the language of first-order intuitionistic logic extended with the exclusion operator $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure2.pdf}}}\hskip 0.43057pt}}\,$ . More formally:

Definition 1 ().

Fix a countable signature $\mathcal{S}$ of function symbols $f$ and predicate symbols $P$ , denoting their arities by $\mid\!\!{f}\!\!\mid$ and $\mid\!\!{P}\!\!\mid$ , respectively. Let $V$ be the countable type of variables $x, y, z : V$ .

The term and formula language for bi-intuitionistic logic is defined as follows:

\mathbb{T}\leavevmode\nobreak\ ::=\leavevmode\nobreak\ x\mid f(t_{1},\dots,t_{% |f|})

\mathbb{F}\leavevmode\nobreak\ ::=\leavevmode\nobreak\ P(t_{1},\dots,t_{|P|})% \mid\dot{\bot}\mid\varphi\,\dot{\land}\,\varphi\mid\varphi\,\dot{\lor}\,% \varphi\mid\varphi\,\dot{\rightarrow}\,\varphi\mid\varphi\,\dot{\mathrel{% \hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure3.pdf}}}% \hskip 0.43057pt}}\,\varphi\mid\dot{\forall}x\varphi\mid\dot{\exists}x\varphi

We call a formula of the shape $P(t_{1},\dots,t_{|P|})$ an atomic formula. Here we use dots to distinguish the object-level connectives and quantifiers of bi-intuitionistic logic from the meta-level connectives and quantifiers of the ambient meta-logic. We define $\dot{\top}:=(\dot{\bot}\,\dot{\rightarrow}\,\dot{\bot})$ , as well as the abbreviations $\dot{\neg}\varphi:=(\varphi\,\dot{\rightarrow}\,\dot{\bot})$ and $\dot{\sim}\varphi:=(\dot{\top}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure4.pdf}}}\hskip 0.43057pt}}\,\varphi)$ , respectively called negation and weak negation.

The added binary operator $\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure5.pdf}}}\hskip 0.43057pt}}\,\psi$ is intended to be the dual of $\varphi\,\dot{\rightarrow}\,\psi$ and is usually read as “ $\varphi$ excludes $\psi$ ”. Consequently, $\dot{\sim}$ is also defined dually to $\dot{\neg}$ .

In the following, we use $t,t_{0},t_{1},\dots$ for terms the greek letters $\varphi,\psi,\chi,\delta,\dots$ for formulas and $\Gamma,\Delta,\Phi,\Psi\dots$ for sets or lists of formulas, depending on the context. When $\Gamma$ refers to a set of formulas, we write $\Gamma,\varphi$ or $\varphi,\Gamma$ to mean $\Gamma\cup\{\varphi\}$ . For a set of formulas $\Gamma$ , we define $\overline{\Gamma}$ as $\{\varphi:\varphi\not\in\Gamma\}$ , where $\varphi\not\in\Gamma$ means $\neg(\varphi\in\Gamma)$ .

For a formula $\varphi$ we denote its set of free variables, i.e. under the scope of a corresponding quantifier by $FV({\varphi})$ , and say that it is closed if $FV({\varphi})=\emptyset$ . A set of formulas is closed if all formulas in $\Gamma$ are closed. We denote by $\varphi[t/x]$ the substitution of the free occurrences of the variable $x$ in $\varphi$ by the term $t$ . We sometimes stress that $x$ is free in $\varphi$ by using the notation $\varphi(x)$ and in such a context just writing $\psi$ is meant to suggest that $x$ is not free in $\psi$ . In that regard, our convention for quantifier scopes is that $\dot{\forall}x\varphi\,\dot{\rightarrow}\,\psi$ refers to $(\dot{\forall}x\varphi)\,\dot{\rightarrow}\,\psi$ and not to $\dot{\forall}x(\varphi\,\dot{\rightarrow}\,\psi)$ .

Finally, note that our language is built on countable sets of variables, function symbols and predicate symbols. In consequence, the set of formulas is recursively enumerable.

3.2 Axiomatic Calculus

The generalised Hilbert calculus $\mathsf{FOBIH}$ [50] () for $\mathsf{FOBIL}$ extends the one for intuitionistic logic, containing the axioms $A_{1}$ to $A_{9}$ (for the propositional basis, implicit here) and $A_{14}$ to $A_{16}$ (for the first-order basis), with the axioms $A_{10}$ to $A_{13}$ and the rule (wDN), shown in Figure 1. There, $\mathcal{A}$ in the rule (Ax) refers to the set of all instances of axioms. In the following we write ${\Gamma}\vdash{\varphi}$ to mean that the syntactic expression $\Gamma\vdash\varphi$ , called a consecution, is provable in $\mathsf{FOBIH}$ , i.e. there is a tree of consecutions built using the rules in Figure 1 with instances of (Ax) and (El) as leaves. We also abbreviate $\neg(\Gamma\vdash\varphi)$ by $\Gamma\not\vdash\varphi$ . We formally define the logic $\mathsf{FOBIL}$ as the set $\{(\Gamma,\varphi):\;{\Gamma}\vdash{\varphi}\}$ .

Note that our calculus $\mathsf{FOBIH}$ is the calculus $\mathsf{FOwBIH}$ of [50].¹¹1More precisely, $\mathsf{FOBIH}$ is the calculus $\mathsf{FOwBIH}$ minus the axiom $\varphi\,\dot{\rightarrow}\,\top$ . This deletion is caused by the fact that $\top$ is not a primitive connective of our language. In his work, he also considers a stronger system called $\mathsf{FOsBIH}$ , obtained by modifying the premise of the rule (wDN) to $\Gamma\vdash\varphi$ . As the letters $\mathsf{w}$ and $\mathsf{s}$ are only used to distinguish the two calculi, we drop $\mathsf{w}$ in this paper for simplicity.

Figure 1: Generalised Hilbert calculus

\mathsf{FOBIH}

, where

x

is free in

\psi

and

\Gamma

in

A_{14}

,

(\text{Gen})

and

(\text{EC})

.

The name of the rule (Gen) stands for Generalisation, while the name of the rule (EC) stands for for Existential Conditionalisation.

3.3 Basic Proof-Theoretic Results

Next, we present basic proof-theoretic results from the mechanisation of Shillito [50]. They express properties of the proof system $\mathsf{FOBIH}$ , some of which we use to prove completeness.

Unsurprisingly, we can prove that $\mathsf{FOBIL}$ is a finitary logic: it satisfies identity (), monotonicity (), compositionality (), structurality (), and finiteness () [12, 31]. These properties are expressed below, where $\sigma$ is a function substituting atomic formulas by composite formulas satisfying some properties²²2This function needs to commute with substitution of variables (), but we omit these details as they are not in the scope of this paper. and $\subseteq_{f}$ is the finite subset relation.

To present the next results in an elegant way, we introduce helpful derived notions.

Definition 2.

Let $\Delta$ be a list of formulas. We define $\dot{\bigvee}:\mathbb{F}^{*}\to\mathbb{F}$ recursively on the structure of $\Delta$ by $\dot{\bigvee}[]:=\dot{\bot}$ and $\dot{\bigvee}(\varphi::\Delta^{\prime}):=\varphi\,\dot{\lor}\,(\dot{\bigvee}% \Delta^{\prime})$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_GHC.html#list_disj)$ . Analogously, we define $\dot{\bigwedge}:\mathbb{F}^{*}\to\mathbb{F}$ by $\dot{\bigwedge}[]:=\dot{\top}$ and $\dot{\bigwedge}(\varphi::\Delta^{\prime}):=\varphi\,\dot{\land}\,(\dot{% \bigwedge}\Delta^{\prime})$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_GHC.html#list_conj)$ .

The function $\dot{\bigvee}$ essentially creates the disjunction of all members of a list of formulas, with an additional disjunct $\dot{\bot}$ , the neutral element of $\,\dot{\lor}\,$ . Using $\dot{\bigvee}$ , we can bring consecutions $\Gamma\vdash\varphi$ to a fully symmetric setting via pairs of the shape $[{\Gamma}\mid{\Delta}]$ , constituted of a left and right context.

Definition 3.

We define the following:

1.

$\vdash[{\Gamma}\mid{\Delta}]$ if ${\Gamma}\vdash{\dot{\bigvee}\Delta^{\prime}}$ for some $\Delta^{\prime}\subseteq_{f}\Delta$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_GHC.html#pair_der)$ ;
2.

$\not\vdash[{\Gamma}\mid{\Delta}]$ if $\neg(\vdash[{\Gamma}\mid{\Delta}])$ , in which case we say that $[{\Gamma}\mid{\Delta}]$ is relative consistent.

Note that the symmetry in our pairs is only simulated, as it ultimately relies on the asymmetry of consecutions ${\Gamma}\vdash{\varphi}$ which we hide via a derived notion. A similar illusion could be obtained by defining an axiomatic system on symmetric consecutions ${\varphi}\vdash{\Delta}$ as first-class citizens, and define $\vdash[{\Gamma}\mid{\Delta}]$ as the existence of $\Gamma^{\prime}\subseteq_{f}\Gamma$ with ${\dot{\bigwedge}\Gamma}\vdash{\Delta}$ . It would be interesting to see what a truly symmetric axiomatic calculus based on pairs would look like.

While our pairs are crucially used in the completeness proof, as we shall see, they are already convenient to express interesting properties of $\mathsf{FOBIH}$ .

Theorem 4.

We have the following:

(1) above shows that a bi-intuitionistic version of the law of excluded-middle holds in $\mathsf{FOBIL}$ (). (2) is a syntactic analogue of the algebraic dual residuation property below ().

a\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure6.pdf}}}\hskip 0.43057pt}}\,b\leq ca\leq b\lor c

(3) is the deduction-detachment theorem for $\mathsf{FOBIL}$ (,), while (4) is its dual deduction-detachment theorem (,). (5) is the Dual Modus Ponens rule (), which acts as (MP) but on the left-hand side of pairs and using $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure7.pdf}}}\hskip 0.43057pt}}\,$ instead of $\,\dot{\rightarrow}\,$ .

3.4 Constant Domain Axioms

Early on, Rauszer noticed the provability in $\mathsf{FOBIL}$ of the constant domain axiom (CD), as shows the proof below on the left (), where we rely on the commutativity of $\,\dot{\lor}\,$ ().

Moreoever, the bi-intuitionistic language enhances expressivity as it contains both connectives or quantifiers and their duals. This allows us to dualise formulas: recursively replace any connective or quantifier by its dual, and swap the formula on the left of an implication or exclusion by the one on the right. Therefore, we can dualise the axiom (CD) to obtain the dual constant domain dual-axiom (DCD). While the former is a theorem as it is provable from an empty left-context, equivalent to $\dot{\top}$ , the latter is a contradiction as it proves the empty right-context, i.e. $\dot{\bot}$ , as shown above on the right (). We suspect that (DCD) plays a role to enforce constant domains in first-order dual intuitionistic logic, which is expressed in the language of $\mathsf{FOBIL}$ without $\,\dot{\rightarrow}\,$ .

Both (CD) and (DCD) will be of crucial use in our completeness proof.

3.5 Constant Domain Kripke Semantics

We proceed to define a Kripke semantics for $\mathsf{FOBIL}$ which extends the one for $\mathsf{FOCDIL}$ with an interpretation of $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure8.pdf}}}\hskip 0.43057pt}}\,$ . Note that the interpretation we use here is not the traditional one [48] formalised in [50], but an alternative put forward in [51].

Both the traditional semantics and ours are defined using (Kripke) models which are identical to the ones of $\mathsf{FOCDIL}$ , as shown below.

Definition 5 ().

A model $\mathcal{M}$ is a tuple $(W,\leq,D,\mathcal{F},\mathcal{P})$ , where $(W,\leq)$ is a peordered set, $D$ is a non-empty set called the domain, $\mathcal{F}$ is a function interpreting each function symbol $f$ of arity $n$ by a function $\mathcal{F}(f):D^{n}\rightarrow D$ , and $\mathcal{P}$ is a function interpreting, in each $w\in W$ , each predicate symbol $P$ of arity $n$ by a set $\mathcal{P}(w,P)\subseteq D^{n}$ such that:

\forall w\leq v.\,\forall P.\,\forall d_{0},\dots,d_{n}\in D.\;((d_{0},\dots,d% _{n})\in\mathcal{P}(w,P)\,\rightarrow\,(d_{0},\dots,d_{n})\in\mathcal{P}(v,P))

An assignment $\alpha$ on $D$ is a function $\alpha:V\rightarrow D$ , and $\alpha[d/x]$ is the assignment $\alpha$ modified in $x$ to output $d$ . An assignment $\alpha$ is extended to the interpretation $\overline{\alpha}(t)$ of a term $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Kripke_sem.html#eval)$ recursively: $\overline{\alpha}(t)=\alpha(x)$ if $t=x$ , and $\overline{\alpha}(t)=\mathcal{F}(f)(\overline{\alpha}(t_{0}),\dots,\overline{% \alpha}(t_{n}))$ if $t=f(t_{0},\dots,t_{n})$ .

Our Kripke semantics extends the usual forcing relation of first-order intuitionistic logic to incorporate $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure9.pdf}}}\hskip 0.43057pt}}\,$ as follows.

Definition 6 ().

Given a model $\mathcal{M}=(W,\leq,D,\mathcal{F},\mathcal{P})$ and an assignment $\alpha$ for $\mathcal{M}$ , we define the forcing relation $\mathcal{M},w,\alpha\Vdash\varphi$ between a world $w\in W$ and a formula recursively by:

$\mathcal{M},w,\alpha\Vdash P(t_{0},\dots,t_{n})$	$:=$	$(\overline{\alpha}(t_{0}),\dots,\overline{\alpha}(t_{n}))\in\mathcal{P}(w,P)$
$\mathcal{M},w,\alpha\Vdash\dot{\bot}$	$:=$	$\bot$
$\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\land}\,\psi$	$:=$	$\mathcal{M},w,\alpha\Vdash\varphi\;\land\;\mathcal{M},w,\alpha\Vdash\psi$
$\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\lor}\,\psi$	$:=$	$\mathcal{M},w\,\alpha\Vdash\varphi\;\lor\;\mathcal{M},w,\alpha\Vdash\psi$
$\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\rightarrow}\,\psi$	$:=$	$\forall v\geq w.(\mathcal{M},v,\alpha\Vdash\varphi\;\rightarrow\;\mathcal{M},v% ,\alpha\Vdash\psi)$
$\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure10.pdf}}}\hskip 0.43057pt}}\,\psi$	$:=$	$\neg(\forall v\leq w.(\mathcal{M},v,\alpha\Vdash\varphi\;\rightarrow\;\mathcal% {M},v,\alpha\Vdash\psi))$
$\mathcal{M},w,\alpha\Vdash\dot{\forall}x\varphi$	$:=$	$\forall d\in D.\,\mathcal{M},w,\alpha[d/x]\Vdash\varphi$
$\mathcal{M},w,\alpha\Vdash\dot{\exists}x\varphi$	$:=$	$\exists d\in D.\,\mathcal{M},w,\alpha[d/x]\Vdash\varphi$

We abbreviate $\neg(\mathcal{M},w,\alpha\Vdash\varphi)$ by $\mathcal{M},w,\alpha\not\Vdash\varphi$ .

Crucially, while the semantic clause for $\,\dot{\rightarrow}\,$ looks forward on the relation $\leq$ , the clause for $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure11.pdf}}}\hskip 0.43057pt}}\,$ looks backwards. This circumstance shows that $\mathsf{FOBIL}$ shares similarities with tense logic [39, 40, 41]. Additionally, observe that the use of constant domain models allows us to localise the interpretation of $\dot{\forall}$ in a single point, in contrast with the case of first-order intuitionistic logic where it is interpreted on all successors.

Note that our semantic clause for $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure12.pdf}}}\hskip 0.43057pt}}\,$ is intuitionistically weaker but classically equivalent to the traditional clause for instance used by Rauszer [48]:

\exists v\leq w.(\mathcal{M},v,\alpha\Vdash\varphi\;\land\;\mathcal{M},v,% \alpha\not\Vdash\psi)

Two points motivate this clause. First, to our eyes the duality between $\,\dot{\rightarrow}\,$ and $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure13.pdf}}}\hskip 0.43057pt}}\,$ is more visibly expressed in our clause. Indeed, it is obtained in two steps by negating the clause for $\,\dot{\rightarrow}\,$ , and by reversing the order between $v$ and $w$ , witnessing the tense logic flavour of $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure14.pdf}}}\hskip 0.43057pt}}\,$ . Secondly, our analysis led us to believe that the strength of the traditional clause more readily forces one to use non-constructive principles, notably in the proof of the Truth lemma (Lemma 17).

The main feature of the Kripke semantics for intuitionistic logic, i.e. persistence, is preserved in our semantics for $\mathsf{FOBIL}$ .

Lemma 7 (Persistence ).

Let $\mathcal{M}=(W,\leq,D,\mathcal{F},\mathcal{P})$ be a model. The following holds.

\forall\alpha.\,\forall v,w\in W.\,\forall\varphi.\,(w\leq v\,\rightarrow\,% \mathcal{M},w,\alpha\Vdash\varphi\,\rightarrow\,\mathcal{M},v,\alpha\Vdash\varphi)

Finally, we define the (local) consequence relation $\Gamma\vDash\varphi$ on our semantics ():

\Gamma\vDash\varphi\text{ if }\forall\mathcal{M}.\forall\alpha.\forall w.\,(% \mathcal{M},w,\alpha\Vdash\Gamma\hskip 2.84544pt\rightarrow\hskip 2.84544pt% \mathcal{M},w,\alpha\Vdash\varphi)

Here $\mathcal{M},w,\alpha\Vdash\Gamma$ means $\forall\gamma\in\Gamma.\,\mathcal{M},w,\alpha\Vdash\gamma$ . We then also abbreviate $\neg(\Gamma\vDash\varphi)$ by $\Gamma\not\vDash\varphi$ .

Crucially using classical reasoning, soundness of $\mathsf{FOBIH}$ is straightforwardly obtained.

Lemma 8 (Soundness ).

If ${\Gamma}\vdash{\varphi}$ then $\Gamma\vDash\varphi$ .

Proof.

We show $\Gamma\vDash\varphi$ by induction on a given derivation of $\Gamma\vdash\varphi$ . The validity of the inference rules holds constructively using routine arguments and so does the validity of all axioms but $A_{10}$ , $A_{12}$ , and $A_{13}$ , which rely on the excluded middle. We here only present the case of $A_{10}$ for illustrative purposes.

In this case, we need to show that assuming $\mathcal{M},w,\alpha\Vdash\varphi$ we have either $\mathcal{M},w,\alpha\Vdash\psi$ or $\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure15.pdf}}}\hskip 0.43057pt}}\,\psi$ . To proceed, we classical reasoning to distinguish whether $\mathcal{M},w,\alpha\Vdash\psi$ or $\mathcal{M},w,\alpha\not\Vdash\psi$ . In the former case we are done, in the latter case we show $\mathcal{M},w,\alpha\Vdash\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure16.pdf}}}\hskip 0.43057pt}}\,\psi$ , so for a contradiction we assume that $\mathcal{M},v,\alpha\Vdash\varphi$ implies $\mathcal{M},v,\alpha\Vdash\psi$ for all predecessors $v\leq w$ . For the choice $v:=w$ we thus obtain $\mathcal{M},w,\alpha\Vdash\psi$ , in contradiction to the assumption $\mathcal{M},w,\alpha\not\Vdash\psi$ . $\hfill\blacktriangleleft$

4 A Forest of Lindenbaum Lemmas

In this section we are interested in the generation of Henkin prime theories, defined below.

Definition 9.

We say that a set of formulas $\Gamma$ is:

$\blacksquare$

consistent if ${\Gamma}\not\vdash{\bot}$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Stand_Lindenbaum_lem% .html#consist)$ ;
$\blacksquare$

deductively closed if ${\Gamma}\vdash{\varphi}$ implies $\varphi\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Stand_Lindenbaum_lem% .html#ded_clos)$ ;
$\blacksquare$

a theory if it is consistent and deductively closed;
$\blacksquare$

prime if $\varphi\,\dot{\lor}\,\psi\in\Gamma$ implies $\varphi\in\Gamma\lor\psi\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Stand_Lindenbaum_lem% .html#prime)$ ;
$\blacksquare$

$\dot{\exists}$ -Henkin if $\dot{\exists}x\varphi\in\Gamma$ then one can compute some $k\in V$ such that $\varphi[k/x]\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Stand_Lindenbaum_lem% .html#ex_henk)$ ;
$\blacksquare$

$\dot{\forall}$ -Henkin if $\dot{\forall}x\varphi\not\in\Gamma$ then one can compute some $k\in V$ such that $\varphi[k/x]\not\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Stand_Lindenbaum_lem% .html#all_henk)$ ;
$\blacksquare$

Henkin if it is $\dot{\exists}$ -Henkin and $\dot{\forall}$ -Henkin.

Note that we deviate from the standard presentation of the Henkin properties by observing that they actually carry computational content. Later on we use Henkin prime theories as worlds of the canonical model we define to prove completeness.

Traditionally, this proof technique via canonical model construction requires us to connect any set $\Gamma$ such that ${\Gamma}\not\vdash{\varphi}$ to a point in the canonical model, i.e. a Henkin prime theory, extending $\Gamma$ and not containing $\varphi$ . We call this result the standard Lindenbaum lemma.

Additionally, on the way to completeness we are required to show that if a point in the canonical model does not contain $\varphi\,\dot{\rightarrow}\,\psi$ then we can find an extension of this point containing $\varphi$ but not $\psi$ . We call this result the constant domain Lindenbaum lemma.

Similarly, we also need to prove that the presence of $\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure17.pdf}}}\hskip 0.43057pt}}\,\psi$ in such a point entails the existence of a restriction of this point containing $\varphi$ but not $\psi$ . We call this result the dual constant domain Lindenbaum lemma.

In the remainder of this section, we prove these three flavours of Lindenbaum lemma, employing classical logic to describe the underlying extension processes via case distinctions.

4.1 Standard Lindenbaum Lemma

The standard lemma acts on pairs $\not\vdash[{\Gamma}\mid{\Delta}]$ of closed sets of formulas, which allows us to treat ${\Gamma}\not\vdash{\varphi}$ as special case. The sets $\Gamma$ and $\Delta$ are required to be closed as we need enough “safe” variables to witness quantifiers throughout the enumeration.

Lemma 10 (Standard Lindenbaum Lemma ).

For closed $\Gamma$ and $\Delta$ such that $\not\vdash[{\Gamma}\mid{\Delta}]$ , there is a Henkin prime theory $\Gamma^{\prime}\supseteq\Gamma$ such that $\not\vdash[{\Gamma^{\prime}}\mid{\Delta}]$ .

Proof.

We construct $\Gamma^{\prime}$ by iteratively extending the pair $[{\Gamma}\mid{\Delta}]$ , starting from $\Gamma_{0}:=\Gamma$ and $\Delta_{0}:=\Delta$ () and using an enumeration $\varphi_{n}$ of formulas with the additional property that the $n$ -th variable is not free in $\varphi_{k}$ for all $k\leq n$ .

[{\Gamma_{n+1}}\mid{\Delta_{n+1}}]:=\begin{cases}[{\Gamma_{n}}\mid{\dot{% \exists}x\psi,\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{\exists}x\psi\text{ and% }\vdash[{\dot{\exists}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]\\ [{\psi[n/x],\dot{\exists}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\exists}x\psi\text{ and }\not\vdash[{\dot{\exists}x\psi,\Gamma_{n}}% \mid{\Delta_{n}}]\\ [{\Gamma_{n}}\mid{\psi[n/x],\dot{\forall}x\psi,\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\forall}x\psi\text{ and }\vdash[{\dot{\forall}x\psi,\Gamma_{n}}\mid{% \Delta_{n}}]\\ [{\dot{\forall}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{% \forall}x\psi\text{ and }\not\vdash[{\dot{\forall}x\psi,\Gamma_{n}}\mid{\Delta% _{n}}]\\ [{\varphi_{n},\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\not\vdash[{\varphi_{n},% \Gamma_{n}}\mid{\Delta_{n}}]\\ [{\Gamma_{n}}\mid{\varphi_{n},\Delta_{n}}]&\text{ if }\vdash[{\varphi_{n},% \Gamma_{n}}\mid{\Delta_{n}}]\\ \end{cases}

We then set $\Gamma^{\prime}:=\bigcup_{n:\mathbb{N}}\Gamma_{n}$ and name $\Delta^{\prime}:=\bigcup_{n:\mathbb{N}}\Delta_{n}$ (). We observe $\Gamma^{\prime}\supseteq\Gamma$ and $\Delta^{\prime}\supseteq\Delta$ by construction (). Before turning to the remaining properties one-by-one, note that $\not\vdash[{\Gamma_{n}}\mid{\Delta_{n}}]$ is preserved inductively (), ensuring that $\not\vdash[{\Gamma^{\prime}}\mid{\Delta}]$ () and hence the consistency of $\Gamma^{\prime}$ ().

$\blacksquare$

For deductive closure (), assume that ${\Gamma^{\prime}}\vdash{\varphi}$ . This entails that when $\varphi$ is considered at $n$ in the enumeration of formulae, then it must be added to $\Gamma_{n+1}$ : indeed, we can prove that $\not\vdash[{\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ , as $\vdash[{\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ implies $\vdash[{\Gamma^{\prime}}\mid{\Delta^{\prime}}]$ , a contradiction, via compositionality as we have that ${\Gamma^{\prime}}\vdash{\psi}$ for all $\psi\in\Gamma_{n},\varphi$ (via the rule (El) or via assumption).
$\blacksquare$

For primeness (), we assume that $\varphi\,\dot{\lor}\,\psi\in\Gamma^{\prime}$ . We make case distinctions on whether $\chi\in\Gamma^{\prime}$ or $\chi\not\in\Gamma^{\prime}$ for $\chi\in\{\varphi,\psi\}$ . Clearly, in the case where we have $\varphi\in\Gamma^{\prime}$ or $\psi\in\Gamma^{\prime}$ we are done. So, we are left to consider the case where $\varphi\not\in\Gamma^{\prime}$ and $\psi\not\in\Gamma^{\prime}$ . From these assumptions, we obtain that $\varphi\in\Delta^{\prime}$ and $\psi\in\Delta^{\prime}$ . Obviously, combined with $\varphi\dot{\lor}\psi\in\Gamma^{\prime}$ the two last statements entail the contradiction $\vdash[{\Gamma^{\prime}}\mid{\Delta^{\prime}}]$ : We have that the list $[\varphi;\psi]$ is such that all its elements are in $\Delta^{\prime}$ , and ${\Gamma^{\prime}}\vdash{\dot{\bigvee}([\varphi;\psi])}$ as $\dot{\bigvee}([\varphi;\psi])=\varphi\,\dot{\lor}\,\psi\,\dot{\lor}\,\dot{\bot}$ is equivalent to $\varphi\,\dot{\lor}\,\psi\in\Gamma^{\prime}$ .
$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\exists}$ -Henkin (), we assume that $\dot{\exists}x\varphi\in\Gamma^{\prime}$ . When $\dot{\exists}x\varphi$ is considered at $n$ in the enumeration of formulae, then it must be added to $\Gamma_{n+1}$ as well as $\varphi[n/x]$ : indeed, we can prove that $\not\vdash[{\dot{\exists}x\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ , as $\vdash[{\dot{\exists}x\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ implies $\dot{\exists}x\varphi\in\Delta_{n+1}\subseteq\Delta^{\prime}$ , hence $\vdash[{\Gamma^{\prime}}\mid{\Delta^{\prime}}]$ , a contradiction.
$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\forall}$ -Henkin (), we assume that $\dot{\forall}x\varphi\not\in\Gamma^{\prime}$ . When $\dot{\forall}x\varphi$ is considered at $n$ in the enumeration of formulae, then it must be added to $\Delta_{n+1}$ as well as $\varphi[n/x]$ : indeed, we can prove that $\vdash[{\dot{\exists}x\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ , as $\not\vdash[{\dot{\forall}x\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ implies $\dot{\forall}x\varphi\in\Gamma_{n+1}\subseteq\Gamma^{\prime}$ , hence $\vdash[{\Gamma^{\prime}}\mid{\Delta^{\prime}}]$ , a contradiction.

$\hfill\blacktriangleleft$

We now have sufficient machinery to generate a Henkin prime theory from a consistent closed theory. Next, we turn to the generation of prime Henkin theories from prime Henkin theories, via extension and restriction.

4.2 Constant Domain Lindenbaum Lemma

For this subsection and for the next, we generate new Henkin prime theories from previous Henkin prime theories. Here, we take a Henkin prime theory $\Gamma$ and two formulas $\psi_{1}$ and $\psi_{2}$ and assume that ${\Gamma,\psi_{1}}\not\vdash{\psi_{2}}$ . We aim at generating a Henkin prime theory $\Gamma^{\prime}$ which extends $\Gamma\cup\{\psi_{1}\}$ and does not contain $\psi_{2}$ . We use this result in the Truth lemma, when assuming that $\psi_{1}\,\dot{\rightarrow}\,\psi_{2}\not\in\Gamma$ or equivalently ${\Gamma}\not\vdash{\psi_{1}\,\dot{\rightarrow}\,\psi_{2}}$ or yet ${\Gamma,\psi_{1}}\not\vdash{\psi_{2}}$ .

We cannot use the standard Lindenbaum lemma 10 to extend $\Gamma\cup\{\psi_{1}\}$ , as it requires closed formulas. Given that $\Gamma$ is Henkin, we are prima facie not ensured to have enough safe variables to extend it. However, we can extend $\Gamma\cup\{\psi_{1}\}$ using a trick relying on the (CD) axiom and the very fact that $\Gamma$ is Henkin. This trick can be found in the book of Gabbay, Shehtman and Skvortsov [17, Section 7.2], where they use it for superintuitionistic logics based on the constant domain axiom.

We first establish a proof-theoretic lemma which isolates the use of the (CD) axiom.

Lemma 11.

Let $\Gamma$ be a $\dot{\forall}$ -Henkin set of formulas and $\varphi(x),\psi_{1},\psi_{2}$ be formulas.

1.

If ${\Gamma}\not\vdash{(\dot{\exists}x\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{% \rightarrow}\,\psi_{2}}$ , then one can compute $k$ such that $(\varphi[k/x]\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2}\not\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Up_Lindenbaum_lem.% html#Lext_ex)$ .
2.

If ${\Gamma}\not\vdash{\psi_{1}\,\dot{\rightarrow}\,(\dot{\forall}x\varphi(x)\,% \dot{\lor}\,\psi_{2})}$ , then one can compute $k$ such that $\psi_{1}\,\dot{\rightarrow}\,(\varphi[k/x]\,\dot{\lor}\,\psi_{2}\not\in\Gamma)$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Up_Lindenbaum_lem.% html#Lext_all)$ .

Proof.

We give both proofs in detail, noting that only (2) relies on the (CD) axiom.

1.

It is sufficient to show that $\dot{\forall}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2% })\not\in\Gamma$ . Indeed, as $\Gamma$ is $\dot{\forall}$ -Henkin, one can then compute $k$ with $((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2})[k/x]\not\in\Gamma$ and therefore $(\varphi[k/x]\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2}\not\in\Gamma$ . So suppose $\dot{\forall}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2% })\in\Gamma$ , so in particular ${\Gamma}\vdash{\dot{\forall}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{% \rightarrow}\,\psi_{2})}$ . From there we can derive ${\Gamma}\vdash{(\dot{\exists}x\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{% \rightarrow}\,\psi_{2}}$ in contradiction to the assumption using standard proof rules as follows: assuming $\varphi(x_{0})$ for some particular $x_{0}$ together with $\psi_{1}$ , we simply instantiate $\dot{\forall}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\rightarrow}\,\psi_{2})$ to $x_{0}$ and obtain $\psi_{2}$ .
2.

It is sufficient to show that $\dot{\forall}x(\psi_{1}\,\dot{\rightarrow}\,(\varphi(x)\,\dot{\lor}\,\psi_{2})% )\not\in\Gamma$ , which again leverages the fact that $\Gamma$ is $\dot{\forall}$ -Henkin. So suppose $\dot{\forall}x(\psi_{1}\,\dot{\rightarrow}\,(\varphi(x)\,\dot{\lor}\,\psi_{2})% )\in\Gamma$ and hence ${\Gamma}\vdash{\dot{\forall}x(\psi_{1}\,\dot{\rightarrow}\,(\varphi(x)\,\dot{% \lor}\,\psi_{2}))}$ , we this time derive ${\Gamma}\vdash{\psi_{1}\,\dot{\rightarrow}\,(\dot{\forall}x\varphi(x)\,\dot{% \lor}\,\psi_{2})}$ for a contradiction. So assuming $\psi_{1}$ and then applying the (CD) axiom, it remains to show $\dot{\forall}x(\varphi(x)\,\dot{\lor}\,\psi_{2})$ , so $\varphi(x_{0})\,\dot{\lor}\,\psi_{2}$ for some arbitrary $x_{0}$ . This follows directly from instantiating $\dot{\forall}(\psi_{1}\,\dot{\rightarrow}\,(\varphi(x)\,\dot{\lor}\,\psi_{2}))$ to $x_{0}$ .

$\hfill\blacktriangleleft$

We can then show how to perform the extension of $\Gamma$ as Henkin theory.

Lemma 12 (CD Lindenbaum Lemma ).

For any Henkin theory $\Gamma$ and formulas $\psi_{1}$ , $\psi_{2}$ such that ${\Gamma,\psi_{1}}\not\vdash{\psi_{2}}$ , there is a Henkin prime theory $\Gamma^{\prime}\supseteq\Gamma$ with $\psi_{1}\in\Gamma^{\prime}$ and $\psi_{2}\not\in\Gamma^{\prime}$ .

Proof.

We construct $\Gamma^{\prime}$ by iteratively constructing pairs $[{\Gamma_{n}}\mid{\Delta_{n}}]$ , using any enumeration $\varphi_{n}$ of formulas and letting $\Gamma_{0}:=\{\psi_{1}\}$ and $\Delta_{0}:=\{\psi_{2}\}$ ():

[{\Gamma_{n+1}}\mid{\Delta_{n+1}}]:=\begin{cases}[{\Gamma_{n}}\mid{\dot{% \exists}x\psi,\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{\exists}x\psi\text{ and% }\vdash[{\dot{\exists}x\psi,\Gamma,\Gamma_{n}}\mid{\Delta_{n}}]\\ [{\psi[k/x],\dot{\exists}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\exists}x\psi\text{ and }\not\vdash[{\dot{\exists}x\psi,\Gamma,% \Gamma_{n}}\mid{\Delta_{n}}]\\ &\text{ and }k\text{ as obtained from (1) of \lx@cref{creftypecap~refnum}{lem:% CD_help}}\\ [{\dot{\forall}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{% \forall}x\psi\text{ and }\vdash[{\Gamma,\Gamma_{n}}\mid{\dot{\forall}x\psi,% \Delta_{n}}]\\ [{\Gamma_{n}}\mid{\psi[k/x],\dot{\forall}x\psi,\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\forall}x\psi\text{ and }\not\vdash[{\Gamma,\Gamma_{n}}\mid{\dot{% \forall}x\psi,\Delta_{n}}]\\ &\text{ and }k\text{ as obtained from (2) of \lx@cref{creftypecap~refnum}{lem:% CD_help}}\\ [{\varphi_{n},\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\not\vdash[{\varphi_{n},% \Gamma,\Gamma_{n}}\mid{\Delta_{n}}]\\ [{\Gamma_{n}}\mid{\varphi_{n},\Delta_{n}}]&\text{ if }\vdash[{\varphi_{n},% \Gamma,\Gamma_{n}}\mid{\Delta_{n}}]\\ \end{cases}

We then set $\Gamma^{\prime}:=\bigcup_{n:\mathbb{N}}\Gamma_{n}$ () and name $\Delta^{\prime}:=\bigcup_{n:\mathbb{N}}\Delta_{n}$ . For this choice, $\Gamma^{\prime}\supseteq\Gamma\cup\{\psi_{1}\}$ is by construction (,) and $\psi_{2}\not\in\Gamma^{\prime}$ (), or equivalently ${\Gamma^{\prime}}\not\vdash{\psi_{2}}$ , follows since $\not\vdash[{\Gamma,\Gamma_{n}}\mid{\Delta_{n}}]$ () and thus $\not\vdash[{\Gamma^{\prime}}\mid{\Delta_{n}}]$ is preserved inductively (). The remaining properties of $\Gamma^{\prime}$ being a Henkin prime theory are established mostly as in Lemma 10.

$\blacksquare$

For deductive closure () and primeness (), one can follow analogous arguments as in the respective claims of Lemma 10.
$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\exists}$ -Henkin (), we assume that $\dot{\exists}x\varphi\in\Gamma^{\prime}$ . When $\dot{\exists}x\varphi$ is considered at $n$ in the enumeration of formulae, then it must be added to $\Gamma_{n+1}$ as $\not\vdash[{\Gamma,\dot{\exists}x\varphi,\Gamma_{n}}\mid{\Delta_{n}}]$ follows from $\not\vdash[{\Gamma^{\prime}}\mid{\Delta_{n}}]$ . But then $\Gamma_{n+1}$ by construction also contains $\varphi[k/x]$ for $k$ obtained from (1) of Lemma 11 for the choice of $\psi_{1}:=\dot{\bigwedge}\Gamma_{n}$ and $\psi_{2}:=\dot{\bigvee}\Delta_{n}$ .
$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\forall}$ -Henkin () one can use an analogous argument, this time relying on (2) of Lemma 11.

$\hfill\blacktriangleleft$

Note that we do not need primeness of the input theory $\Gamma$ as it is obtained as a side-product of the iterative construction.

4.3 Dual Constant Domain Lindenbaum Lemma

Now, we aim at restricting a Henkin prime theory $\Gamma$ containing $\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure18.pdf}}}\hskip 0.43057pt}}\,\psi_{2}$ into another such theory $\Gamma^{\prime}$ with $\psi_{1}$ but not $\psi_{2}$ . This result is now motivated by the case of $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure19.pdf}}}\hskip 0.43057pt}}\,$ in the Truth lemma. Note that once more we cannot use the standard Lindenbaum lemma 10.

While we easily imagine how to extend theories, as in Lemma 12, the restriction of a Henkin prime theory into a smaller one appears as a tricky and rather mysterious operation to perform. However, its familiarity is regained once seen as an extension, not of a theory but of the complement of a theory. Indeed, as $\Gamma^{\prime}\subseteq\Gamma\leftrightarrow\overline{\Gamma}\subseteq% \overline{\Gamma^{\prime}}$ we restrict $\Gamma$ by extending $\overline{\Gamma}$ .

The next lemma, again isolating the use of constant domain axioms, relies on this insight, by involving the complement of a theory and exploiting the symmetry of our pairs $[{\Phi}\mid{\Psi}]$ by operating on their left.

Lemma 13.

Let $\Gamma$ be a $\dot{\exists}$ -Henkin set of formulas and $\varphi(x),\psi_{1},\psi_{2}$ be formulas.

1.

If $\not\vdash[{(\dot{\exists}x\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{% \hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure20.pdf}}}% \hskip 0.43057pt}}\,\psi_{2}}\mid{\overline{\Gamma}}]$ , then one can compute $k$ with $(\varphi[k/x]\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure21.pdf}}}% \hskip 0.43057pt}}\,\psi_{2}\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Down_Lindenbaum_lem.% html#Ldext_ex)$ .
2.

If $\not\vdash[{(\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure22.pdf}}}\hskip 0.43057pt}}\,\dot{% \forall}x\varphi(x))\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure23.pdf}}}\hskip 0.43057pt}}\,\psi_{2}}% \mid{\overline{\Gamma}}]$ , then one can compute $k$ with $(\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure24.pdf}}}\hskip 0.43057pt}}\,\varphi[k/x])\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure2% 5.pdf}}}\hskip 0.43057pt}}\,\psi_{2}\in\Gamma$ $(\href https://ianshil.github.io/FOBiInt/FObiint.FO_BiInt_Down_Lindenbaum_lem.% html#Ldext_all)$ .

Proof.

We give both proofs in detail, noting that (1) relies on the (DCD) dual-axiom and (2) relies on the (CD) axiom.

1.

It is sufficient to show that $\dot{\exists}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.430% 57pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure26.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})\in\Gamma$ . Indeed, as $\Gamma$ is $\dot{\exists}$ -Henkin, we can thus compute $k$ such that $((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure27.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})[k/x]\in\Gamma$ i.e. $((\varphi[k/x]\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure28.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})\in\Gamma$ . So, we assume for reductio ad absurdum that $\dot{\exists}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.430% 57pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure29.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})\not\in\Gamma$ . We show that the latter implies $\vdash[{(\dot{\exists}x\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{% \hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure30.pdf}}}% \hskip 0.43057pt}}\,\psi_{2}}\mid{\overline{\Gamma}}]$ , contradicting our initial assumption. By the dual deduction Theorem 4 it suffices to show $\vdash[{\dot{\exists}x(x)\varphi\,\dot{\land}\,\psi_{1}}\mid{\psi_{2},% \overline{\Gamma}}]$ , proved as follows.

\vdash[{\dot{\exists}x\varphi(x)\,\dot{\land}\,\psi_{1}}\mid{\psi_{2},% \overline{\Gamma}}]\lx@proof@logical@and\vdash[{\dot{\exists}x(\varphi(x)\,% \dot{\land}\,\psi_{1})}\mid{\psi_{2},\overline{\Gamma}}]\vdash[{(\dot{\exists}% x\varphi(x)\,\dot{\land}\,\psi_{1})\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure31.pdf}}}\hskip 0.43057pt}\dot{% \exists}x(\varphi(x)\,\dot{\land}\,\psi_{1})}\mid{\psi_{2},\overline{\Gamma}}]

The right premise is nothing but an instance of the (DCD) dual-axiom, so we are left to prove the left premise. All we need to do is to apply the dual detachment Theorem 4 to reduce our goal to $\vdash[{\dot{\exists}x(\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{% \hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure32.pdf}}}% \hskip 0.43057pt}}\,\psi_{2}}\mid{\overline{\Gamma}}]$ , which obviously holds as we have $\dot{\exists}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.430% 57pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure33.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})\in\overline{\Gamma}$ by our assumption $\dot{\exists}x((\varphi(x)\,\dot{\land}\,\psi_{1})\,\dot{\mathrel{\hskip 0.430% 57pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure34.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})\not\in\Gamma$ .

2.

It is sufficient to show that $\dot{\exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure35.pdf}}}\hskip 0.43057pt}}\,\varphi(x))% \,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure36.pdf}}}\hskip 0.43057pt}}\,\psi_{2})\in\Gamma$ , which again leverages the fact that $\Gamma$ is $\dot{\exists}$ -Henkin, i.e. $((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure37.pdf}}}\hskip 0.43057pt}}\,\varphi[k/x])\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure3% 8.pdf}}}\hskip 0.43057pt}}\,\psi_{2})\in\Gamma$ . So, we assume for reductio that $\dot{\exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure39.pdf}}}\hskip 0.43057pt}}\,\varphi(x))% \,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure40.pdf}}}\hskip 0.43057pt}}\,\psi_{2})\not\in\Gamma$ and show $\vdash[{(\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure41.pdf}}}\hskip 0.43057pt}}\,\dot{% \forall}x\varphi(x))\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure42.pdf}}}\hskip 0.43057pt}}\,\psi_{2}}% \mid{\overline{\Gamma}}]$ , a contradiction. More precisely, we show ${(\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure43.pdf}}}\hskip 0.43057pt}}\,\dot{\forall}x\varphi(x% ))\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure44.pdf}}}\hskip 0.43057pt}}\,\psi_{2}}\vdash{\dot{\exists}x((% \psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure45.pdf}}}\hskip 0.43057pt}}\,\varphi(x))\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure4% 6.pdf}}}\hskip 0.43057pt}}\,\psi_{2})}$ , noting that $\dot{\exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure47.pdf}}}\hskip 0.43057pt}}\,\varphi(x))% \,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure48.pdf}}}\hskip 0.43057pt}}\,\psi_{2})\in\overline{\Gamma}$ . By the dual deduction theorem it is sufficient to show ${\psi_{1}}\vdash{\dot{\forall}x\varphi(x)\,\dot{\lor}\,(\psi_{2}\lor\dot{% \exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure49.pdf}}}\hskip 0.43057pt}}\,\varphi(x))% \,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure50.pdf}}}\hskip 0.43057pt}}\,\psi_{2}))}$ .

We use the (CD) axiom to reduce our goal to ${\psi_{1}}\vdash{\dot{\forall}x(\varphi(x)\,\dot{\lor}\,(\psi_{2}\,\dot{\lor}% \,\dot{\exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p040-Kirst.latexml-figure51.pdf}}}\hskip 0.43057pt}}\,% \varphi(x))\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure52.pdf}}}\hskip 0.43057pt}}\,\psi_{2})))}$ , as $x$ is not free in $\psi_{2}$ and $\dot{\exists}x((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure53.pdf}}}\hskip 0.43057pt}}\,\varphi(x))% \,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure54.pdf}}}\hskip 0.43057pt}}\,\psi_{2})$ . We obtain a proof of the latter applying the rule (Gen), leaving us to prove ${\psi_{1}}\vdash{\varphi(x)\,\dot{\lor}\,(\psi_{2}\,\dot{\lor}\,\dot{\exists}x% ((\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure55.pdf}}}\hskip 0.43057pt}}\,\varphi(x))\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure5% 6.pdf}}}\hskip 0.43057pt}}\,\psi_{2}))}$ . This can easily be proved using the dual detachment theorem as ${(\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure57.pdf}}}\hskip 0.43057pt}}\,\varphi(x))\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure5% 8.pdf}}}\hskip 0.43057pt}}\,\psi_{2}}\vdash{\dot{\exists}x((\psi_{1}\,\dot{% \mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure5% 9.pdf}}}\hskip 0.43057pt}}\,\varphi(x))\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure60.pdf}}}% \hskip 0.43057pt}}\,\psi_{2})}$ holds.

$\hfill\blacktriangleleft$

Turning back to the restriction of $\Gamma$ , we note that $\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure61.pdf}}}\hskip 0.43057pt}}\,\psi_{2}\in\Gamma$ is equivalent to $\not\vdash[{\psi_{1}\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p040-Kirst.latexml-figure62.pdf}}}\hskip 0.43057pt}}\,\psi_{2}}% \mid{\overline{\Gamma}}]$ by consistency of $\Gamma$ , and in turn to $\not\vdash[{\psi_{1}}\mid{\psi_{2},\overline{\Gamma}}]$ . So, to restrict $\Gamma$ in a way that preserves $\psi_{1}$ but excludes $\psi_{2}$ , we extend $\overline{\Gamma}$ using $\not\vdash[{\psi_{1}}\mid{\psi_{2},\overline{\Gamma}}]$ as a stepping stone.

Lemma 14 (DCD Lindenbaum Lemma ).

For any Henkin prime theory $\Gamma$ and formulas $\psi_{1}$ , $\psi_{2}$ with $\not\vdash[{\psi_{1}}\mid{\psi_{2},\overline{\Gamma}}]$ , there is a Henkin prime theory $\Gamma^{\prime}\subseteq\Gamma$ with $\psi_{1}\in\Gamma^{\prime}$ and $\psi_{2}\not\in\Gamma^{\prime}$ .

Proof.

We construct $\Gamma^{\prime}$ by iteratively constructing pairs $[{\Gamma_{n}}\mid{\Delta_{n}}]$ , using any enumeration $\varphi_{n}$ of formulas and letting $\Gamma_{0}:=\{\psi_{1}\}$ and $\Delta_{0}:=\{\psi_{2}\}$ ():

[{\Gamma_{n+1}}\mid{\Delta_{n+1}}]:=\begin{cases}[{\Gamma_{n}}\mid{\dot{% \exists}x\psi,\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{\exists}x\psi\text{ and% }\vdash[{\dot{\exists}x\psi,\Gamma_{n}}\mid{\overline{\Gamma},\Delta_{n}}]\\ [{\psi[k/x],\dot{\exists}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\exists}x\psi\text{ and }\not\vdash[{\dot{\exists}x\psi,\Gamma_{n}}% \mid{\overline{\Gamma},\Delta_{n}}]\\ &\text{ and }k\text{ as obtained from (1) of \lx@cref{creftypecap~refnum}{lem:% DCD_help}}\\ [{\dot{\forall}x\psi,\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\varphi_{n}=\dot{% \forall}x\psi\text{ and }\vdash[{\Gamma_{n}}\mid{\dot{\forall}x\psi,\overline{% \Gamma},\Delta_{n}}]\\ [{\Gamma_{n}}\mid{\psi[k/x],\dot{\forall}x\psi,\Delta_{n}}]&\text{ if }\varphi% _{n}=\dot{\forall}x\psi\text{ and }\not\vdash[{\Gamma_{n}}\mid{\dot{\forall}x% \psi,\overline{\Gamma},\Delta_{n}}]\\ &\text{ and }k\text{ as obtained from (2) of \lx@cref{creftypecap~refnum}{lem:% DCD_help}}\\ [{\varphi_{n},\Gamma_{n}}\mid{\Delta_{n}}]&\text{ if }\not\vdash[{\varphi_{n},% \Gamma_{n}}\mid{\overline{\Gamma},\Delta_{n}}]\\ [{\Gamma_{n}}\mid{\varphi_{n},\Delta_{n}}]&\text{ if }\vdash[{\varphi_{n},% \Gamma_{n}}\mid{\overline{\Gamma},\Delta_{n}}]\\ \end{cases}

We then set $\Gamma^{\prime}:=\bigcup_{n:\mathbb{N}}\Gamma_{n}$ (). For this choice, $\psi_{1}\in\Gamma^{\prime}$ () holds by construction and $\psi_{2}\not\in\Gamma^{\prime}$ () follows since $\not\vdash[{\Gamma_{n}}\mid{\Delta_{n},\overline{\Gamma}}]$ () is preserved inductively and $\psi_{2}\in\Delta_{n}$ . We also have that $\Gamma^{\prime}\subseteq\Gamma$ (), as if there is a $\chi\in\Gamma^{\prime}$ but $\chi\not\in\Gamma$ we get that at the point $n$ in the enumeration where $\chi$ is added to form $\Gamma_{n+1}$ we have $\vdash[{\Gamma_{n+1}}\mid{\Delta_{n+1},\overline{\Gamma}}]$ , a contradiction. As $\Gamma^{\prime}$ can be shown to be a prime theory (,) as in Lemma 12, we focus on its being Henkin.

$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\exists}$ -Henkin (), we assume that $\dot{\exists}x\varphi\in\Gamma^{\prime}$ . When $\dot{\exists}x\varphi$ is considered at $n$ in the enumeration of formulae, then it must be added to $\Gamma_{n+1}$ as $\not\vdash[{\dot{\exists}x\varphi,\Gamma_{n}}\mid{\overline{\Gamma},\Delta_{n}}]$ follows from $\not\vdash[{\Gamma^{\prime}}\mid{\overline{\Gamma},\Delta_{n}}]$ . But then $\Gamma_{n+1}$ by construction also contains $\varphi[k/x]$ for $k$ obtained from (1) of Lemma 13 for the choice of $\psi_{1}:=\dot{\bigwedge}\Gamma_{n}$ and $\psi_{2}:=\dot{\bigvee}\Delta_{n}$ .
$\blacksquare$

To show that $\Gamma^{\prime}$ is $\dot{\forall}$ -Henkin () one can use an analogous argument, this time relying on (2) of Lemma 13.

$\hfill\blacktriangleleft$

5 Completeness and Conservativity

Using the Lindenbaum lemmas of the previous section, we now first turn to the completeness of $\mathsf{FOBIL}$ relative to our constant domain semantics.

Theorem 15 (Completeness ).

If $\Gamma\cup\{\varphi\}$ is closed and $\Gamma\vDash\varphi$ then ${\Gamma}\vdash{\varphi}$ .

We rely on a canonical model construction based on Henkin prime theories, defined below.

Definition 16 ().

The canonical model $\mathcal{M}^{c}=(W^{c},\leq^{c},D^{c},\mathcal{F}^{c},\mathcal{P}^{c})$ is defined as follows:

1.

$W^{c}=\{\Gamma:\Gamma\text{ is a Henkin prime theory}\}$ ;
2.

$\Gamma_{1}\leq^{c}\Gamma_{2}$ if $\Gamma_{1}\subseteq\Gamma_{2}$ ;
3.

$D^{c}=\mathbb{T}$ ;
4.

$\mathcal{F}^{c}(f)(t_{0},\dots,t_{\mid f\mid})=f(t_{0},\dots,t_{|f|})$ ;
5.

$\mathcal{P}^{c}(w,P)(t_{0},\dots,t_{\mid P\mid})=\{(t_{0},\dots,t_{|P|})\mid P% (t_{0},\dots,t_{|P|})\in w\}$ .

The canonical assignment $\alpha^{c}$ is defined as $\alpha^{c}(x)=x$ .

Note that the interpretation of terms in $\mathcal{M}^{c}$ through the canonical assignment $\alpha^{c}$ is the identity function: $\overline{\alpha^{c}}(t)=t$ follows from a simple induction on $t$ ().

As foreshadowed, the two custom Lindenbaum lemmas come in action to show that the canonical model satisfies the crucial Truth lemma, relating elementhood and forcing.

Lemma 17 (Truth lemma ).

For every $\Gamma\in W^{c}$ we have $\psi\in\Gamma$ iff $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\psi$ .

Proof.

By induction on $\psi$ . We consider the most interesting cases, and refer to the appendix for the remaining cases.

$\blacksquare$

$\psi=\varphi\,\dot{\rightarrow}\,\chi$ : $(\Rightarrow)$ Assume $\varphi\,\dot{\rightarrow}\,\chi\in\Gamma$ . To show $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\rightarrow}\,\chi$ , let $\Gamma^{\prime}\in W^{c}$ such that $\Gamma\leq^{c}\Gamma^{\prime}$ , and assume $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\Vdash\varphi$ . Then, we obtain $\varphi\in\Gamma^{\prime}$ by induction hypothesis. Using $\Gamma\leq^{c}\Gamma^{\prime}$ , we get $\varphi\,\dot{\rightarrow}\,\chi\in\Gamma\subseteq\Gamma^{\prime}$ . Via deductive closure of $\Gamma^{\prime}$ we thus obtain $\chi\in\Gamma^{\prime}$ , hence $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\Vdash\chi$ using the induction hypothesis. So, we are done.
$(\Leftarrow)$ Assume $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\rightarrow}\,\chi$ . Assume for reductio that $\varphi\,\dot{\rightarrow}\,\chi\not\in\Gamma$ . Then the constant domain Lindenbaum lemma 12 entails the existence of $\Gamma^{\prime}\in W^{c}$ such that $\Gamma\leq^{c}\Gamma^{\prime}$ and $\varphi\in\Gamma^{\prime}$ and $\chi\not\in\Gamma^{\prime}$ (). By induction hypothesis we get $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\Vdash\varphi$ and $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\not\Vdash\chi$ . This contradicts $\Gamma\leq^{c}\Gamma^{\prime}$ and $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\rightarrow}\,\chi$ . So $\varphi\,\dot{\rightarrow}\,\chi\in\Gamma$ .
$\blacksquare$

$\psi=\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure63.pdf}}}\hskip 0.43057pt}}\,\chi$ : $(\Rightarrow)$ Assume $\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure64.pdf}}}\hskip 0.43057pt}}\,\chi\in\Gamma$ . The dual constant domain Lindenbaum lemma 14 entails the existence of $\Gamma^{\prime}\in W^{c}$ with $\Gamma^{\prime}\leq^{c}\Gamma$ and $\varphi\in\Gamma^{\prime}$ and $\chi\not\in\Gamma^{\prime}$ (). By induction hypothesis we get $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\Vdash\varphi$ and $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\not\Vdash\chi$ . As $\Gamma^{\prime}\leq^{c}\Gamma$ we get $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure65.pdf}}}% \hskip 0.43057pt}}\,\chi$ .
$(\Leftarrow)$ Assume $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure66.pdf}}}% \hskip 0.43057pt}}\,\chi$ . Then, there is $\Gamma^{\prime}\in W^{c}$ such that $\Gamma^{\prime}\leq^{c}\Gamma$ and $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\Vdash\varphi$ and $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\not\Vdash\chi$ . By induction hypothesis we obtain that $\varphi\in\Gamma^{\prime}$ and $\chi\not\in\Gamma^{\prime}$ . Note that ${\Gamma^{\prime}}\vdash{\varphi\,\dot{\rightarrow}\,(\chi\,\dot{\lor}\,(% \varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure67.pdf}}}\hskip 0.43057pt}}\,\chi))}$ using axiom $A_{10}$ . Thus by applying (MP) we obtain ${\Gamma^{\prime}}\vdash{\chi\,\dot{\lor}\,(\varphi\,\dot{\mathrel{\hskip 0.430% 57pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p040-Kirst.latexml-figure68.pdf}}}% \hskip 0.43057pt}}\,\chi)}$ , as we have ${\Gamma^{\prime}}\vdash{\varphi}$ knowing $\varphi\in\Gamma^{\prime}$ . Via deductive closure and primeness we get $\chi\in\Gamma^{\prime}$ or $\varphi\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure69.pdf}}}\hskip 0.43057pt}\chi\in\Gamma^{\prime}$ . But we know $\chi\not\in\Gamma^{\prime}$ , so we have $\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure70.pdf}}}\hskip 0.43057pt}}\,\chi\in\Gamma^{\prime}$ . We finally obtain $\varphi\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p040-Kirst.latexml-figure71.pdf}}}\hskip 0.43057pt}}\,\chi\in\Gamma$ , as $\Gamma^{\prime}\subseteq\Gamma$ given $\Gamma^{\prime}\leq^{c}\Gamma$ .
$\blacksquare$

$\psi:=\dot{\forall}x\varphi$ : $(\Rightarrow)$ Assume $\forall x\varphi\in\Gamma$ . To show $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\forall}x\varphi$ let $d\in D^{c}$ . We need to show $\mathcal{M}^{c},\Gamma,\alpha^{c}[d/x]\Vdash\varphi$ . Note that $d\in\mathbb{T}=D^{c}$ . Using $\forall x\varphi\in\Gamma$ and deductive closure we obtain $\varphi[d/x]\in\Gamma$ . Thus, we apply the induction hypothesis to obtain $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi[d/x]$ . We finally push the syntactic substitution to a modification of the assignment () to obtain $\mathcal{M}^{c},\Gamma,\alpha^{c}[d/x]\Vdash\varphi$ .
$(\Leftarrow)$ Assume $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\forall}x\varphi$ . Assume for reductio that $\forall x\varphi\not\in\Gamma$ . The theory $\Gamma$ being $\dot{\forall}$ -Henkin, there is a $n\in\mathbb{N}$ such that $\varphi[n/x]\not\in\Gamma$ . By induction hypothesis we obtain $\mathcal{M}^{c},\Gamma,\alpha^{c}\not\Vdash\varphi[n/x]$ . But this is a contradiction as it implies that $\mathcal{M}^{c},\Gamma,\alpha^{c}[n/x]\not\Vdash\varphi$ as explained above, while we have $\mathcal{M}^{c},\Gamma,\alpha^{c}[n/x]\Vdash\varphi$ from $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\forall}x\varphi$ .
$\blacksquare$

$\psi:=\dot{\exists}x\varphi$ : $(\Rightarrow)$ Assume $\dot{\exists}x\varphi\in\Gamma$ . The theory $\Gamma$ being $\dot{\exists}$ -Henkin, there is $n\in\mathbb{N}$ such that $\varphi[n/x]\in\Gamma$ . By induction hypothesis we get $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi[n/x]$ . This implies $\mathcal{M}^{c},\Gamma,\alpha^{c}[n/x]\Vdash\varphi$ as argued above. Hence $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\exists}x\varphi$ .
$(\Leftarrow)$ Assume $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\exists}x\varphi$ . Thus there is a $d\in D^{c}$ such that $\mathcal{M}^{c},\Gamma,\alpha^{c}[d/x]\Vdash\varphi$ . Note that $d\in\mathbb{T}=D^{c}$ . We reason as above to get that $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi[d/x]$ . By induction hypothesis we obtain $\varphi[d/x]\in\Gamma$ . We thus get $\dot{\exists}x\varphi\in\Gamma$ by deductive closure.

$\hfill\blacktriangleleft$

Employing the Truth lemma we can now deduce completeness, also relying on the standard Lindenbaum lemma to extend the initial context into a point of the canonical model.

Proof of Theorem 15.

Assume that $\Gamma\vDash\varphi$ , and that ${\Gamma}\not\vdash{\varphi}$ for reductio. As $\Gamma\cup\{\varphi\}$ is closed, the standard Lindenbaum lemma 10 conjointly with our last assumption ensure us of the existence of $\Gamma^{\prime}\in W^{c}$ such that $\Gamma^{\prime}\supseteq\Gamma$ and $\varphi\not\in\Gamma^{\prime}$ (). By the Truth lemma 17 we obtain both $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\vdash\Gamma$ and $\mathcal{M}^{c},\Gamma^{\prime},\alpha^{c}\not\vdash\varphi$ , hence $\Gamma\not\vDash\varphi$ , a contradiction. $\hfill\blacktriangleleft$

We conclude with two results concerning $\mathsf{FOCDIL}$ that illustrate the close connection to our completeness proof for $\mathsf{FOBIL}$ . To this end, we write $\mathbb{F}_{\text{CD}}$ for the usual syntax of first-order intuitionistic logic (i.e. $\mathbb{F}$ without $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure72.pdf}}}\hskip 0.43057pt}}\,$ ) (), $\vdash_{\text{CD}}$ for the deduction system of $\mathsf{FOCDIL}$ (i.e. $\vdash$ without the axioms for $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure73.pdf}}}\hskip 0.43057pt}}\,$ but extended with the (CD) axiom) (, and $\vDash_{\text{CD}}$ for the semantic consequence relation of $\mathsf{FOCDIL}$ (i.e. $\vDash$ without the clause for $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure74.pdf}}}\hskip 0.43057pt}}\,$ ) (). To avoid redundancy, we just give proof sketches and refer to the Coq code for full detail.

First, we prove the completeness of $\mathsf{FOCDIL}$ simply by a fragment of the proof of $\mathsf{FOBIL}$ .

Theorem 18 (CD Completeness ).

If $\Gamma\cup\{\varphi\}$ is closed and $\Gamma\vDash_{\text{CD}}\varphi$ then ${\Gamma}\vdash_{\text{CD}}{\varphi}$ , provided that $\Gamma\cup\{\varphi\}$ ranges over $\mathbb{F}_{\text{CD}}$ .

Sketch.

Following exactly the same strategy as Theorem 15, now only relying on the standard Lindenbaum lemma 10 and the constant domain Lindenbaum lemma 12. $\hfill\blacktriangleleft$

Secondly, we deduce the conservativity of $\mathsf{FOBIL}$ over $\mathsf{FOCDIL}$ .

Corollary 19 (Conservativity ).

If $\Gamma\cup\{\varphi\}$ is closed and ${\Gamma}\vdash{\varphi}$ then ${\Gamma}\vdash_{\text{CD}}{\varphi}$ , provided that $\Gamma\cup\{\varphi\}$ ranges over $\mathbb{F}_{\text{CD}}$ .

Sketch.

By composing soundness of $\mathsf{FOBIL}$ (Lemma 8) with completeness of $\mathsf{FOCDIL}$ (Theorem 18), using that obviously $\Gamma\vDash_{\text{CD}}\varphi$ iff $\Gamma\vDash\varphi$ for $\Gamma\cup\{\varphi\}$ ranging over $\mathbb{F}_{\text{CD}}$ . $\hfill\blacktriangleleft$

6 Discussion

In this paper, we provide a succinct and verified completeness proof of $\mathsf{FOBIL}$ relative to its constant domain Kripke semantics. Consequentially, we formally establish the conservativity of $\mathsf{FOBIL}$ over $\mathsf{FOCDIL}$ , notably via the analogous completeness of the latter over the same semantics restricted to the intuitionistic language. We conclude with a brief discussion.

6.1 Coq Development

Our Coq development is based on the design of and is in the process of being integrated³³3https://github.com/uds-psl/coq-library-fol/pull/7 into the Coq library for first-order logic [27], which has been developed to unify several projects concerned with different aspects of first-order logics [13, 14, 28, 26, 24, 23, 29]. It spans roughly 8000 lines of code, with about one half each for the separate $\mathsf{FOBIL}$ and $\mathsf{FOCDIL}$ developments. We globally assume a strong form of the excluded middle, namely $\forall P:\mathbb{P}.P+\neg P$ , to enable the definition of functions by logical case distinction (justified by the consistency of the usual excluded middle and unique choice [56]) and left the particular formula enumeration as a parameter that will be obtained routinely from the library framework once merged.

Most notably, in comparison to the paper presentation, where we use named variables for legibility, the mechanisation is based on a de Bruijn encoding of binding [7] following the design of the Autosubst 2 tool [52], i.e. variables are replaced by indices referring to the amount of quantifiers shadowing their relevant binder. For instance, the formula $\dot{\forall}x\dot{\exists}yP(x,y)$ is represented as $\dot{\forall}\dot{\exists}P(1,0)$ , as $x$ is bound by the $\dot{\forall}$ shadowed by the $\dot{\exists}$ , whereas $y$ is bound by the unshadowed $\dot{\exists}$ . To illustrate just one of the advantages of this approach, in the representation of the deduction calculus, one can use lifting of de Bruijn indices to simulate the usual freshness conditions for variables. For example, the rule (Gen) is encoded as:

\Gamma\vdash\dot{\forall}\varphi\Gamma[\uparrow]\vdash\varphi

By shifting from $\Gamma$ in the conclusion to $\Gamma[\uparrow]$ in the premise, we lift any free index $n$ in $\Gamma$ to its successor $n+1$ . As a consequence, the index 0 made free by the change from $\dot{\forall}\varphi$ to $\varphi$ is not present in $\Gamma[\uparrow]$ , thus creating a canonical “fresh” variable. Using this rule for instance allows a particularly easy monotonicity proof, as no on-the-fly renaming of variables is necessary.

Overall, the use of any proof assistant for our project not only provided the additional guarantee of correctness of our completeness proof but actually was worthwhile already in the mathematical development: for instance the dualised Lindenbaum lemma subject to Section 4.2 was developed incrementally starting from the non-dualised case, with the proof assistant pointing towards the remaining gaps while some proof scripts could be reused. The particular choice of Coq allowed to base our code on the design decisions of the existing library for first-order logic and, implementing a constructive foundation, in principle enables a constructive analysis extending [51], as described in the future work section.

6.2 Related Work

Bi-intuitionistic logic.

As understood in this paper, bi-intuitionistic logic received some attention in computer science, notably through a formulae-as-types interpretation involving the notion of first-class coroutines [6] and in the context of image processing via its connection to mathematical morphology [49]. We mention another line of work [3, 1, 2, 10, 11] initiated by Wansing [54, 55] on a different bi-intuitionistic logic called $\mathsf{2Int}$ , which is both proof-theoretically and philosophically motivated. The alternative interpretation of $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure75.pdf}}}\hskip 0.43057pt}}\,$ in this logic allows for the study of the notions of falsification and verification.

Completeness proofs for $\mathsf{FOBIL}$ .

Rauszer’s proof of completeness for $\mathsf{FOBIL}$ [46] is erroneous for three main reasons. First, as in the propositional case two logics are conflated. This is noticed by the joint use of the deduction theorem, an exclusive property of the weak logic we study here, and of double negation $\neg{\sim}$ of formulas, an exclusive property of the strong. Secondly, her canonical model [46, p.66] is rooted, i.e. there is a point-root $w$ for which any $v$ is such that $w\leq v$ . However, as noticed by Crolard [5] and confirmed by Shillito [50, Lemma 8.11.3], bi-intuitionistic logic is not complete relative to the class of rooted models. Thirdly, in her proof Rauszer relies on a result from Gabbay [15, Lemma 8.11.1] dealing with the language $\mathbb{F}$ without $\,\dot{\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p040-Kirs% t.latexml-figure76.pdf}}}\hskip 0.43057pt}}\,$ , $\,\dot{\lor}\,$ and $\dot{\exists}$ . She dually proves it for $\mathbb{F}$ without $\,\dot{\rightarrow}\,$ , $\,\dot{\land}\,$ and $\dot{\forall}$ , and proceeds to illegitimately combine them on $\mathbb{F}$ , outside of their application range.

In Klemke’s proof strategy [30], the main construction is in Satz 6.1, where the extension of consistent pairs $(M,N)$ of sets of formulas over an alphabet $\{x_{1},x_{2},\dots\}$ is described. The extension yields a family of maximal pairs $(M_{s},N_{s})$ in the extended alphabet $\{x_{1},x_{2},\dots\}\cup\{y_{1},y_{2},\dots\}$ where $s$ ranges over the partial order $(U,Q)$ of strings over two copies of natural numbers ( $\mathbb{N}$ and $\mathbb{N}^{*}$ ) such that $s\leq s’$ if $s$ and $s ’$ agree on a prefix and from there continue in the separate copies. This order is called the “universal bush” and a universal model is then defined over the structure $(U,Q,\{x_{1},x_{2},\dots\}\cup\{y_{1},y_{2},\dots\})$ , i.e. on the universal bush with the full alphabet as individuals, interprets variables with the identity and interprets atoms $P(x,y,z\dots)$ at $s$ with $P(x,y,z\dots)$ in $M_{s}$ . From Satz 6.1 the conclusion to completeness is standard. To date, we were neither able to identify an explicit use of the constant domain axioms, nor to confirm or refute the claim by Olkhovikov and Badia [35] concerning errors.

Finally, Shillito [50] tried, but failed, to correct Rauszer’s work in Coq. More precisely, he gave an incomplete proof of completeness relying on two assumptions corresponding to our custom Lindenbaum lemmas 12 and 14. We consequently closed the gap in his proof.

Mechanisation of completeness proofs.

There is a rather long list of works mechanising completeness proofs which for the most prominent case of first-order logic is summarised in [14] and [25]. The only mechanised completeness proofs for (propositional) bi-intuitionistic logic we are aware of are those by Shillito [50] as well as Shillito and Kirst [51].

Regarding other formalisms like bi-intuitionistic logic with a modal aspect, we are aware of the works in Coq of Doczkal and Smolka on CTL [9], Doczkal and Bard on converse PDL [8], and Hagemeier and Kirst on IEL [21], the work in HOL Light of Maggesi and Perini Brogi on the provability logic GL [33]. We finally mention the recent formalisation in Lean of Guo, Chen and Bentzen on propositional intuitionistic logic [20].

6.3 Future Work

While the purpose of this paper is to present the clearest and most minimalistic completeness proof for $\mathsf{FOBIL}$ , which for very natural reasons encompasses classical assumptions, we plan to continue in the spirit of Shillito and Kirst [51] to analyse which logical strength is exactly required. In their case of propositional bi-intuitionistic logic, they observe that the principle WLEMS, identified by Kirst [25] for the case of IEL and applied to first-order logic by Herbelin and Kirst [22], is equivalent to a weak but natural formulation of completeness. However, this observation relies on the property that theories obtained from the standard Lindenbaum lemma are negatively described (i.e. membership of formulas is characterised by non-derivability), while the custom Lindenbaum lemmas yield also positively described theories (membership of universally quantified formulas is characterised by derivability). Therefore it seems unlikely that an exactly analogous analysis is realistic and in fact it might be that the completeness of $\mathsf{FOBIL}$ requires a stronger fragment of classical meta-logic.

References

[1] Sara Ayhan. Uniqueness of logical connectives in a bilateralist setting. In Martin Blicha and Igor Sedlár, editors, The Logica Yearbook 2020, pages 1–16. College Publications, 2021. doi:10.48550/arXiv.2210.00989.
[2] Sara Ayhan. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations. Journal of Logic and Computation, 2024. doi:10.48550/arXiv.2307.01079.
[3] Sara Ayhan and Heinrich Wansing. On synonymy in proof-theoretic semantics. the case of 2int. Bulletin of the Section of Logic, 52(2), 2023.
[4] Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. doi:10.1016/0890-5401(88)90005-3.
[5] Tristan Crolard. Subtractive logic. TCS, 254:1-2:151–185, 2001. doi:10.1016/S0304-3975(99)00124-3.
[6] Tristan Crolard. A formulae-as-types interpretation of subtractive logic. Journal of Logic and Computation, 14:4:529–570, 2004. doi:10.1093/logcom/14.4.529.
[7] Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes mathematicae (proceedings), volume 75(5), pages 381–392. Elsevier, 1972.
[8] Christian Doczkal and Joachim Bard. Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq. In Certified Programs and Proofs, Los Angeles, United States, January 2018. doi:10.1145/3167088.
[9] Christian Doczkal and Gert Smolka. Completeness and decidability results for ctl in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 226–241, Cham, 2014. Springer International Publishing. doi:10.1007/978-3-319-08970-6_15.
[10] Sergey Drobyshevich. A bilateral hilbert-style investigation of 2-intuitionistic logic. J. Log. Comput., 29(5):665–692, 2019. doi:10.1093/logcom/exz010.
[11] Sergey Drobyshevich. Tarskian consequence relations bilaterally: some familiar notions. Synthese, 198(Suppl 22):5213–5240, 2021. doi:10.1007/s11229-019-02267-w.
[12] Josep M. Font. Abstract Algebraic Logic: An Introductory Textbook. Studies in Logic and the Foundations of Mathematics. College Publications, 2016.
[13] Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in coq, with an application to the entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38–51, 2019. doi:10.1145/3293880.3294091.
[14] Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory: Extended version. Journal of Logic and Computation, 31(1):112–151, 2021. arXiv:2006.04399, doi:10.48550/arXiv.2006.04399.
[15] Dov M. Gabbay. Applications of trees to intermediate logics. Journal of Symbolic Logic, 37(1):135–138, 1972. doi:10.2307/2272556.
[16] Dov M. Gabbay. Semantical investigations in Heyting’s intuitionistic logic, volume 148. D. Reidel Pub. Co, Dordrecht, Holland, 1981.
[17] Dov M. Gabbay, Valentin B. Shehtman, and Dmitrij P. Skvortsov. Quantification in Nonclassical Logic, volume 153. Elsevier, London, Amsterdam, 1st edition, 2009.
[18] Rajeev Goré and Ian Shillito. Bi-Intuitionistic Logics: A New Instance of an Old Problem. In Advances in Modal Logic 13, papers from the thirteenth conference on ”Advances in Modal Logic,” held online, 24-28 August 2020, pages 269–288, 2020. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.
[19] Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26:596–601, 1964.
[20] Huayu Guo, Dongheng Chen, and Bruno Bentzen. Verified completeness in Henkin-style for intuitionistic propositional logic. In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong, and Tianwen Xu, editors, Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou, pages 36–48. College Publications, 2023.
[21] Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of iel and similar modal logics. Journal of Logic and Computation, 32(8):1585–1610, 2022. doi:10.1093/logcom/exac068.
[22] Hugo Herbelin and Dominik Kirst. New observations on the constructive content of first-order completeness theorems. In 29th International Conference on Types for Proofs and Programs, 2023.
[23] Marc Hermes and Dominik Kirst. An analysis of Tennenbaum’s theorem in constructive type theory. In International Conference on Formal Structures for Computation and Deduction. LIPIcs, 2022. doi:10.4230/LIPIcs.FSCD.2022.9.
[24] Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of dyadic first-order logic in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2022. doi:10.4230/LIPIcs.ITP.2022.19.
[25] Dominik Kirst. Mechanised Metamathematics: An Investigation of First-Order Logic and Set Theory in Constructive Type Theory. PhD thesis, Saarland University, 2022.
[26] Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2021. doi:10.4230/LIPIcs.ITP.2021.23.
[27] Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, and Dominik Wehr. A Coq library for mechanised first-order logic. In Coq Workshop, 2022.
[28] Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq: Finite model theory through the constructive lens. Logical Methods in Computer Science, 18, 2022. doi:10.46298/lmcs-18(2:17)2022.
[29] Dominik Kirst and Benjamin Peters. Gödel’s theorem without tears: Essential incompleteness in synthetic computability. In Annual conference of the European Association for Computer Science Logic. LIPIcs, 2023. doi:10.4230/LIPIcs.CSL.2023.30.
[30] Dieter Klemke. Ein Henkin-Beweis für die Vollständigkeit eines Kalküls relativ zur Grzegorczyk-Semantik. Archiv für mathematische Logik und Grundlagenforschung, 14:148–161, 1971.
[31] Marcus Kracht. Tools and Techniques in Modal Logic. Elsevier, 1999.
[32] E.G.K. López-Escobar. On intuitionistic sentential connectives I. Revista Colombiana de Matemáticas, 19(1-2):117–130, January 1985.
[33] Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITP.2021.26.
[34] C. Moisil. Logique modale. Disquisitiones malhematicae et physicae, 2:3–98, 1942.
[35] Grigory K Olkhovikov and Guillermo Badia. Craig interpolation theorem fails in bi-intuitionistic predicate logic. The Review of Symbolic Logic, 17(2):611–633, 2024. doi:10.1017/s1755020322000296.
[36] Hiroakira Ono. Craig’s Interpolation Theorem for the Intuitionistic Logic and Its Extensions: A Semantical Approach. Studia Logica: An International Journal for Symbolic Logic, 45(1):19–33, 1986. doi:10.1007/BF01881546.
[37] Christine Paulin-Mohring. Inductive definitions in the system coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328–345. Springer, 1993. doi:10.1007/BFb0037116.
[38] Luís Pinto and Tarmo Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In M. Giese and A. Waaler, editors, Proc. TABLEAUX, pages 295–309, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-02716-1_22.
[39] Arthur N. Prior. Time and Modality. Greenwood Press, Westport, Conn., 1955.
[40] Arthur N. Prior. Past, Present and Future. Clarendon P., Oxford,, 1967.
[41] Arthur N. Prior. Papers on Time and Tense. Oxford University Press UK, Oxford, England, 1968.
[42] Cecylia Rauszer. A Formalization of the Propositional Calculus of H-B Logic. Studia Logica: An International Journal for Symbolic Logic, 33(1):23–34, 1974.
[43] Cecylia Rauszer. Semi-Boolean algebras and their application to intuitionistic logic with dual operations. Fundamenta Mathematicae LXXXIII, pages 219–249, 1974.
[44] Cecylia Rauszer. On the Strong Semantical Completeness of Any Extension of the Intuitionistic Predicate Calculus. Bulletin de l’Académie Polonaise des Sciences, XXIV(2):81–87, 1976.
[45] Cecylia Rauszer. An algebraic approach to the Heyting-Brouwer predicate calculus. Fundamenta Mathematicae, 96(2):127–135, 1977.
[46] Cecylia Rauszer. Applications of Kripke Models to Heyting-Brouwer Logic. Studia Logica: An International Journal for Symbolic Logic, 36(1/2):61–71, 1977.
[47] Cecylia Rauszer. Model Theory for an Extension of Intuitionistic Logic. Studia Logica, 36(1-2):73–87, 1977.
[48] Cecylia Rauszer. An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic. PhD thesis, Instytut Matematyczny Polskiej Akademi Nauk, 1980.
[49] Katsuhiko Sano and John G. Stell. Strong completeness and the finite model property for bi-intuitionistic stable tense logics. In Proc. Methods for Modalities 2017, volume 243 of Electronic Proceedings in Theoretical Computer Science, pages 105–121. Open Publishing Association, 2017. doi:10.4204/EPTCS.243.8.
[50] Ian Shillito. New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq. PhD thesis, Australian National University, Canberra, 2023.
[51] Ian Shillito and Dominik Kirst. A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 218–229. ACM, 2024. doi:10.1145/3636501.3636957.
[52] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 166–180, 2019. doi:10.1145/3293880.3294101.
[53] The Coq Development Team. The coq proof assistant, June 2023. doi:10.5281/zenodo.8161141.
[54] Heinrich Wansing. Falsification, natural deduction and bi-intuitionistic logic. J. Log. Comput., 26(1):425–450, 2016. doi:10.1093/logcom/ext035.
[55] Heinrich Wansing. Connexive Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2023 edition, 2023.
[56] Benjamin Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, pages 530–546. Springer, 1997. doi:10.1007/BFb0014566.

Appendix A Appendix

Proof of Truth lemma 17.

By induction on $\psi$ , only listing the missing cases:

$\blacksquare$

$\psi:=P(t_{0},\dots,t_{|P|})$ : we have $P(t_{0},\dots,t_{|P|})\in\Gamma$ iff $(t_{0},\dots,t_{|P|})\in\mathcal{P}^{c}(\Gamma,P)$ by definition of the canonical model. The latter is equivalent to $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash P(t_{0},\dots,t_{|P|})$ by definition and the fact that terms are interpreted as themselves via $\alpha^{c}$ .
$\blacksquare$

$\psi=\dot{\bot}$ : we have that $\dot{\bot}\not\in\Gamma$ by consistency. We also have $\mathcal{M}^{c},\Gamma,\alpha^{c}\not\Vdash\dot{\bot}$ by definition. So, we trivially have $\dot{\bot}\in\Gamma$ iff $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\dot{\bot}$ .
$\blacksquare$

$\psi=\varphi\,\dot{\land}\,\chi$ : we have that $\varphi\,\dot{\land}\,\chi\in\Gamma$ iff $\varphi\in\Gamma$ and $\chi\in\Gamma$ via deductive closure. By induction hypothesis this holds if and only if $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi$ and $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\chi$ . Then $\varphi\,\dot{\land}\,\chi\in\Gamma$ iff $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\land}\,\chi$ .
$\blacksquare$

$\psi=\varphi\,\dot{\lor}\,\chi$ : we have that $\varphi\,\dot{\lor}\,\chi\in\Gamma$ iff [ $\varphi\in\Gamma$ or $\chi\in\Gamma$ ] by primeness and deductive closure. By induction hypothesis this holds if and only if $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi$ or $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\chi$ . Then $\varphi\,\dot{\lor}\,\chi\in\Gamma$ iff $\mathcal{M}^{c},\Gamma,\alpha^{c}\Vdash\varphi\,\dot{\lor}\,\chi$ .

$\hfill\blacktriangleleft$

[bib.bib1] [1] Sara Ayhan. Uniqueness of logical connectives in a bilateralist setting. In Martin Blicha and Igor Sedlár, editors, The Logica Yearbook 2020, pages 1–16. College Publications, 2021. doi:10.48550/arXiv.2210.00989.

[bib.bib2] [2] Sara Ayhan. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations. Journal of Logic and Computation, 2024. doi:10.48550/arXiv.2307.01079.

[bib.bib3] [3] Sara Ayhan and Heinrich Wansing. On synonymy in proof-theoretic semantics. the case of 2int. Bulletin of the Section of Logic, 52(2), 2023.

[bib.bib4] [4] Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. doi:10.1016/0890-5401(88)90005-3.

[bib.bib5] [5] Tristan Crolard. Subtractive logic. TCS, 254:1-2:151–185, 2001. doi:10.1016/S0304-3975(99)00124-3.

[bib.bib6] [6] Tristan Crolard. A formulae-as-types interpretation of subtractive logic. Journal of Logic and Computation, 14:4:529–570, 2004. doi:10.1093/logcom/14.4.529.

[bib.bib7] [7] Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes mathematicae (proceedings), volume 75(5), pages 381–392. Elsevier, 1972.

[bib.bib8] [8] Christian Doczkal and Joachim Bard. Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq. In Certified Programs and Proofs, Los Angeles, United States, January 2018. doi:10.1145/3167088.

[bib.bib9] [9] Christian Doczkal and Gert Smolka. Completeness and decidability results for ctl in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 226–241, Cham, 2014. Springer International Publishing. doi:10.1007/978-3-319-08970-6_15.

[bib.bib10] [10] Sergey Drobyshevich. A bilateral hilbert-style investigation of 2-intuitionistic logic. J. Log. Comput., 29(5):665–692, 2019. doi:10.1093/logcom/exz010.

[bib.bib11] [11] Sergey Drobyshevich. Tarskian consequence relations bilaterally: some familiar notions. Synthese, 198(Suppl 22):5213–5240, 2021. doi:10.1007/s11229-019-02267-w.

[bib.bib12] [12] Josep M. Font. Abstract Algebraic Logic: An Introductory Textbook. Studies in Logic and the Foundations of Mathematics. College Publications, 2016.

[bib.bib13] [13] Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in coq, with an application to the entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38–51, 2019. doi:10.1145/3293880.3294091.

[bib.bib14] [14] Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory: Extended version. Journal of Logic and Computation, 31(1):112–151, 2021. arXiv:2006.04399, doi:10.48550/arXiv.2006.04399.

[bib.bib15] [15] Dov M. Gabbay. Applications of trees to intermediate logics. Journal of Symbolic Logic, 37(1):135–138, 1972. doi:10.2307/2272556.

[bib.bib16] [16] Dov M. Gabbay. Semantical investigations in Heyting’s intuitionistic logic, volume 148. D. Reidel Pub. Co, Dordrecht, Holland, 1981.

[bib.bib17] [17] Dov M. Gabbay, Valentin B. Shehtman, and Dmitrij P. Skvortsov. Quantification in Nonclassical Logic, volume 153. Elsevier, London, Amsterdam, 1st edition, 2009.

[bib.bib18] [18] Rajeev Goré and Ian Shillito. Bi-Intuitionistic Logics: A New Instance of an Old Problem. In Advances in Modal Logic 13, papers from the thirteenth conference on ”Advances in Modal Logic,” held online, 24-28 August 2020, pages 269–288, 2020. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.

[bib.bib19] [19] Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26:596–601, 1964.

[bib.bib20] [20] Huayu Guo, Dongheng Chen, and Bruno Bentzen. Verified completeness in Henkin-style for intuitionistic propositional logic. In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong, and Tianwen Xu, editors, Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou, pages 36–48. College Publications, 2023.

[bib.bib21] [21] Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of iel and similar modal logics. Journal of Logic and Computation, 32(8):1585–1610, 2022. doi:10.1093/logcom/exac068.

[bib.bib22] [22] Hugo Herbelin and Dominik Kirst. New observations on the constructive content of first-order completeness theorems. In 29th International Conference on Types for Proofs and Programs, 2023.

[bib.bib23] [23] Marc Hermes and Dominik Kirst. An analysis of Tennenbaum’s theorem in constructive type theory. In International Conference on Formal Structures for Computation and Deduction. LIPIcs, 2022. doi:10.4230/LIPIcs.FSCD.2022.9.

[bib.bib24] [24] Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of dyadic first-order logic in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2022. doi:10.4230/LIPIcs.ITP.2022.19.

[bib.bib25] [25] Dominik Kirst. Mechanised Metamathematics: An Investigation of First-Order Logic and Set Theory in Constructive Type Theory. PhD thesis, Saarland University, 2022.

[bib.bib26] [26] Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2021. doi:10.4230/LIPIcs.ITP.2021.23.

[bib.bib27] [27] Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, and Dominik Wehr. A Coq library for mechanised first-order logic. In Coq Workshop, 2022.

[bib.bib28] [28] Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq: Finite model theory through the constructive lens. Logical Methods in Computer Science, 18, 2022. doi:10.46298/lmcs-18(2:17)2022.

[bib.bib29] [29] Dominik Kirst and Benjamin Peters. Gödel’s theorem without tears: Essential incompleteness in synthetic computability. In Annual conference of the European Association for Computer Science Logic. LIPIcs, 2023. doi:10.4230/LIPIcs.CSL.2023.30.

[bib.bib30] [30] Dieter Klemke. Ein Henkin-Beweis für die Vollständigkeit eines Kalküls relativ zur Grzegorczyk-Semantik. Archiv für mathematische Logik und Grundlagenforschung, 14:148–161, 1971.

[bib.bib31] [31] Marcus Kracht. Tools and Techniques in Modal Logic. Elsevier, 1999.

[bib.bib32] [32] E.G.K. López-Escobar. On intuitionistic sentential connectives I. Revista Colombiana de Matemáticas, 19(1-2):117–130, January 1985.

[bib.bib33] [33] Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITP.2021.26.

[bib.bib34] [34] C. Moisil. Logique modale. Disquisitiones malhematicae et physicae, 2:3–98, 1942.

[bib.bib35] [35] Grigory K Olkhovikov and Guillermo Badia. Craig interpolation theorem fails in bi-intuitionistic predicate logic. The Review of Symbolic Logic, 17(2):611–633, 2024. doi:10.1017/s1755020322000296.

[bib.bib36] [36] Hiroakira Ono. Craig’s Interpolation Theorem for the Intuitionistic Logic and Its Extensions: A Semantical Approach. Studia Logica: An International Journal for Symbolic Logic, 45(1):19–33, 1986. doi:10.1007/BF01881546.

[bib.bib37] [37] Christine Paulin-Mohring. Inductive definitions in the system coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328–345. Springer, 1993. doi:10.1007/BFb0037116.

[bib.bib38] [38] Luís Pinto and Tarmo Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In M. Giese and A. Waaler, editors, Proc. TABLEAUX, pages 295–309, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-02716-1_22.

[bib.bib39] [39] Arthur N. Prior. Time and Modality. Greenwood Press, Westport, Conn., 1955.

[bib.bib40] [40] Arthur N. Prior. Past, Present and Future. Clarendon P., Oxford,, 1967.

[bib.bib41] [41] Arthur N. Prior. Papers on Time and Tense. Oxford University Press UK, Oxford, England, 1968.

[bib.bib42] [42] Cecylia Rauszer. A Formalization of the Propositional Calculus of H-B Logic. Studia Logica: An International Journal for Symbolic Logic, 33(1):23–34, 1974.

[bib.bib43] [43] Cecylia Rauszer. Semi-Boolean algebras and their application to intuitionistic logic with dual operations. Fundamenta Mathematicae LXXXIII, pages 219–249, 1974.

[bib.bib44] [44] Cecylia Rauszer. On the Strong Semantical Completeness of Any Extension of the Intuitionistic Predicate Calculus. Bulletin de l’Académie Polonaise des Sciences, XXIV(2):81–87, 1976.

[bib.bib45] [45] Cecylia Rauszer. An algebraic approach to the Heyting-Brouwer predicate calculus. Fundamenta Mathematicae, 96(2):127–135, 1977.

[bib.bib46] [46] Cecylia Rauszer. Applications of Kripke Models to Heyting-Brouwer Logic. Studia Logica: An International Journal for Symbolic Logic, 36(1/2):61–71, 1977.

[bib.bib47] [47] Cecylia Rauszer. Model Theory for an Extension of Intuitionistic Logic. Studia Logica, 36(1-2):73–87, 1977.

[bib.bib48] [48] Cecylia Rauszer. An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic. PhD thesis, Instytut Matematyczny Polskiej Akademi Nauk, 1980.

[bib.bib49] [49] Katsuhiko Sano and John G. Stell. Strong completeness and the finite model property for bi-intuitionistic stable tense logics. In Proc. Methods for Modalities 2017, volume 243 of Electronic Proceedings in Theoretical Computer Science, pages 105–121. Open Publishing Association, 2017. doi:10.4204/EPTCS.243.8.

[bib.bib50] [50] Ian Shillito. New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq. PhD thesis, Australian National University, Canberra, 2023.

[bib.bib51] [51] Ian Shillito and Dominik Kirst. A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 218–229. ACM, 2024. doi:10.1145/3636501.3636957.

[bib.bib52] [52] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 166–180, 2019. doi:10.1145/3293880.3294101.

[bib.bib53] [53] The Coq Development Team. The coq proof assistant, June 2023. doi:10.5281/zenodo.8161141.

[bib.bib54] [54] Heinrich Wansing. Falsification, natural deduction and bi-intuitionistic logic. J. Log. Comput., 26(1):425–450, 2016. doi:10.1093/logcom/ext035.

[bib.bib55] [55] Heinrich Wansing. Connexive Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2023 edition, 2023.

[bib.bib56] [56] Benjamin Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, pages 530–546. Springer, 1997. doi:10.1007/BFb0014566.

Completeness of First-Order Bi-Intuitionistic Logic

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

3 Basics of Bi-intuitionistic Logic

3.1 Syntax

Definition 1 ().

3.2 Axiomatic Calculus

3.3 Basic Proof-Theoretic Results

Definition 2.

Definition 3.

Theorem 4.

3.4 Constant Domain Axioms

3.5 Constant Domain Kripke Semantics

Definition 5 ().

Definition 6 ().

Lemma 7 (Persistence ).

Lemma 8 (Soundness ).

Proof.

4 A Forest of Lindenbaum Lemmas

Definition 9.

4.1 Standard Lindenbaum Lemma

Lemma 10 (Standard Lindenbaum Lemma ).

Proof.

4.2 Constant Domain Lindenbaum Lemma

Lemma 11.

Proof.

Lemma 12 (CD Lindenbaum Lemma ).

Proof.

4.3 Dual Constant Domain Lindenbaum Lemma

Lemma 13.

Proof.

Lemma 14 (DCD Lindenbaum Lemma ).

Proof.

5 Completeness and Conservativity

Theorem 15 (Completeness ).

Definition 16 ().

Lemma 17 (Truth lemma ).

Proof.

Proof of Theorem 15.

Theorem 18 (CD Completeness ).

Sketch.

Corollary 19 (Conservativity ).

Sketch.

6 Discussion

6.1 Coq Development

6.2 Related Work

Bi-intuitionistic logic.

Completeness proofs for 𝗙𝗢𝗕𝗜𝗟.

Mechanisation of completeness proofs.

6.3 Future Work

References

Appendix A Appendix

Proof of Truth lemma 17.

Completeness proofs for $\mathsf{FOBIL}$ .