Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Lyon, Tim S.; Shillito, Ian; Tiu, Alwen

doi:10.4230/LIPIcs.CSL.2025.41

Taking Bi-Intuitionistic Logic First-Order:
A Proof-Theoretic Investigation via Polytree Sequents

Tim S. Lyon

Technische Universität Dresden, Germany Ian Shillito

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

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

Abstract

It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.

Keywords and phrases:

Bi-intuitionistic, Cut-elimination, Conservativity, Domain, First-order, Polytree, Proof theory, Reachability, Sequent

Funding:

Tim S. Lyon: European Research Council, Consolidator Grant DeciGUT (771779)

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof theory ; Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Constructive mathematics ; Theory of computation

\rightarrow

Automated reasoning

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

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

1 Introduction

Propositional bi-intuitionistic logic ( $\mathsf{BIP}$ ), also referred to as Heyting-Brouwer logic [33], is a conservative extension of propositional intuitionistic logic ( $\mathsf{IP}$ ), obtained by adding the binary connective $\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure0.% pdf}}}\hskip 0.43057pt}$ (referred to as exclusion)¹¹1 Also referred to as pseudo-difference [33], subtraction, and co-implication [13]. among the traditional intuitionistic connectives. This logic has proven relevant in computer science, having a formulae-as-types interpretation in terms of first-class coroutines [7] and where modal extensions have found import in image processing [38]. While in intuitionistic logic the connectives $\land$ and $\rightarrow$ form a residuated pair, i.e. $(\varphi\land\psi)\rightarrow\chi$ is valid iff $\varphi\rightarrow(\psi\rightarrow\chi)$ is valid iff $\psi\rightarrow(\varphi\rightarrow\chi)$ is valid, in bi-intuitionistic logic the connectives $\lor$ and $\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure1.% pdf}}}\hskip 0.43057pt}$ also form a residuated pair, i.e. $\varphi\rightarrow(\psi\lor\chi)$ is valid iff $(\varphi\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure2.pdf}}}\hskip 0.43057pt}\psi)\rightarrow\chi$ is valid iff $(\varphi\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure3.pdf}}}\hskip 0.43057pt}\chi)\rightarrow\psi$ is valid.²²2However, they are not logically equivalent, e.g., $[\varphi\rightarrow(\psi\lor\chi)]\rightarrow[(\varphi\mathrel{\hskip 0.43057% pt\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure4.pdf}}}% \hskip 0.43057pt}\psi)\rightarrow\chi]$ is not valid. To put it succinctly, $\mathsf{BIP}$ is a bi-intuitionistic extension of $\mathsf{IP}$ that is (1) conservative and (2) has the residuation property, i.e. $(\land,\rightarrow)$ and $(\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure5.% pdf}}}\hskip 0.43057pt},\lor)$ form residuated pairs.

When extending first-order intuitionistic logic ( $\mathsf{IQ}$ ) to its bi-intuitionistic counterpart, a “natural” axiomatization seems to be one obtained by adding the universal axioms (Ax1) $\forall x\varphi\rightarrow\varphi(t/x)$ , (Ax2) $\forall x(\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\forall x\varphi)$ (where $x$ is not free in $\psi$ ), and the rule (Gen) $\varphi/\forall x\varphi$ to the axioms of $\mathsf{BIP}$ . This extension, which we refer to as the logic $\mathsf{BIQ}(\mathcal{CD})$ , turns out not to be conservative over first-order intuitionistic logic $\mathsf{IQ}$ , as it allows one to prove the quantifier shift axiom $\forall x(\varphi\lor\psi)\rightarrow\forall x\varphi\lor\psi$ (where $x$ is not free in $\psi$ ), which is not valid intuitionistically. A proof of the quantifier shift axiom is given below, where MP stands for modus ponens, Res stands for the residuation property described above, and $\delta:=\forall x((\forall x(\varphi\lor\psi)\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure6.pdf}}}% \hskip 0.43057pt}\psi)\rightarrow\varphi)\rightarrow((\forall x(\varphi\lor% \psi)\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure7.pdf}}}\hskip 0.43057pt}\psi)\rightarrow\forall x\varphi)$ .

It is well-known that the quantifier shift axiom characterizes the class of first-order intuitionistic Kripke models with constant domains [10, 16], thus forcing the models for $\mathsf{BIQ}(\mathcal{CD})$ to satisfy this constraint. Indeed, various works in the literature (e.g., [32, 34]) have shown that completeness for $\mathsf{BIQ}(\mathcal{CD})$ requires the domain to be constant. These works and the above example strongly suggest that it might not be possible to have a proof system for a bi-intuitionistic logic with non-constant domains, at least not as a traditional Hilbert system. As far as we know, there is no prior successful attempt at solving this problem.

In this paper, we provide the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains, which we refer to here as $\mathsf{BIQ}(\mathcal{ID})$ . With some minor modifications, the proof system for $\mathsf{BIQ}(\mathcal{ID})$ can be converted into a proof system for $\mathsf{BIQ}(\mathcal{CD}).$ A key insight in avoiding the collapse of domains in $\mathsf{BIQ}(\mathcal{ID})$ is to consider the universal quantifier as implicitly carrying an assumption about the existence of the quantified variable. Proof theoretically, this could be done by introducing a notion of an existence predicate, first studied by Scott [35]. An existence predicate such as $E(x)$ postulates that $x$ exists in the domain under consideration. By insisting that all universally quantified variables be guarded by an existence predicate, i.e. universally quantified formulae would have the form $\forall x(E(x)\rightarrow\varphi(x))$ , the quantifier shift axiom can be rewritten as: $\forall x(E(x)\rightarrow(\varphi\lor\psi))\rightarrow(\forall x(E(x)% \rightarrow\varphi)\lor\psi)$ . Attempting a bottom-up construction of a derivation similar to our earlier example for this rewritten axiom, we get stuck at the the top-most residuation rule, which is in fact not a valid instance of Res:

For the proof construction to proceed, we would have to somehow discharge the assumption $E(x)$ in the premise of Gen before applying the residuation rule. In the logic of constant domains $\mathsf{BIQ}(\mathcal{CD})$ , $E(x)$ is equivalent to $\top$ (i.e. the interpretation of any term in the logic is an object that exists in all worlds in the underlying Kripke model). So the version of the quantifier shift axiom with the existence predicate is provably equivalent to the original one in $\mathsf{BIQ}(\mathcal{CD}).$ This is not the case, however, in the logic of increasing domains $\mathsf{BIQ}(\mathcal{ID})$ , since the assumption $E(x)$ cannot always be discharged. What this example highlights is that a typical proof-theoretical argument used to show the provability of the quantifier shift axiom (and hence the collapse of domains) implicitly depends on an existence assumption on objects in the domains in the underlying Kripke model. What we show here is that by making this dependency explicit and by carefully managing the use of the existence assumptions in proofs, we are able to obtain a sound and complete proof system for $\mathsf{BIQ}(\mathcal{ID}).$

One issue with the existence predicate is that it is not clear how it should interact with the exclusion operator. Semantically, a formula like $\forall x[E(x)\rightarrow((p(x)\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p041-Lyon.latexml-figure8.pdf}}}\hskip 0.43057pt}\exists y(E(y)% \land p(y)))\rightarrow\bot)]$ asserts that, if an object $x$ exists in the current domain, then postulating that $p(x)$ holds in a predecessor world should imply that $x$ exists as well in that predecessor world. This is valid in our semantics, but it was not at all obvious how a proof system that admits this tautology, and does not also degenerate into a logic with constant domains, should be designed. We shall come back to this example later in Section 3. Additionally, the existence predicate poses a problem when proving conservativity over first-order intuitionistic logic that does not feature this predicate. We overcome this remaining hurdle by enriching sequents with an explicit variable context, which can be seen as essentially encoding the existence predicate, while avoiding introducing it explicitly in the language of formulae.

The proof systems for $\mathsf{BIQ}(\mathcal{ID})$ and $\mathsf{BIQ}(\mathcal{CD})$ are both formalized using polytree sequents [5], which are connected binary graphs whose vertices are traditional Gentzen sequents and which are free of (un)directed cycles. Polytree sequents are a restriction of traditional labeled sequents [37, 41] and are notational variants of nested sequents [3, 18, 2]. (NB. For details on the relationship between polytree and nested sequents, see [5].) Nested sequents were introduced independently by Bull [3] and Kashima [18] and employ trees of Gentzen sequents in proofs. Both polytree sequents and nested sequents allow for simple formulations of proof systems for various non-classical logics that enjoy important proof theoretical properties such as cut-elimination and subformula properties. Such systems have also found a range of applications, being used in knowledge integration algorithms [24], serving as a basis for constructive interpolation and decidability techniques [21, 25, 40], and even being used to solve open questions about axiomatizability [17]. We make use of polytree sequents in our work as they admit a formula interpretation (at least in the intuitionistic case), which can be leveraged for direct translations of proofs into sequent calculus or Hilbert calculus proofs.

The calculi for $\mathsf{BIQ}(\mathcal{ID})$ and $\mathsf{BIQ}(\mathcal{CD})$ are based on these richly structured sequents, which internalize the existence predicate into syntactic components, called domain atoms, present in each node of the sequent. The rich structure of these sequents is exploited by special rules within our calculi called reachability rules, which traverse paths in a polytree sequent, propagating and/or consuming data. We demonstrate that our calculi enjoy the height-preserving invertibility of every rule, and show that a wide range of novel and useful structural rules are height-preserving admissible, culminating in a non-trivial proof of cut-elimination.

Outline of Paper.

In Section 2, we define a semantics for first-order bi-intuitionistic logic with increasing domains $\mathsf{BIQ}(\mathcal{ID})$ and constant domains $\mathsf{BIQ}(\mathcal{CD})$ . In Section 3, we define our polytree sequent calculi showing them sound and complete relative to the provided semantics. In Section 4, we establish admissibility and invertibility results as well as prove a non-trivial cut-elimination theorem. We conclude and discuss future work in Section 5. Due to space constraints, most proofs have been deferred to the online appended version [26].

2 Logical Preliminaries

In this section, we introduce the language, models, and semantics for first-order bi-intuitionistic logic with increasing domains, dubbed $\mathsf{BIQ}(\mathcal{ID})$ , and with constant domains, dubbed $\mathsf{BIQ}(\mathcal{CD})$ . Let $\mathrm{Var}:=\{x,y,z,\ldots\}$ be a countably infinite set of variables and $\mathrm{Fun}=\{f,g,h,\ldots\}$ be a countably infinite set of function symbols containing countably many function symbols of each arity $n\in\mathbb{N}$ . We let $ar(f)=n$ denote that the arity of the function symbol $f$ is $n$ and let $a,b,c,\ldots$ denote constants, which are function symbols of arity $0$ . For a set $X\subseteq\mathrm{Var}$ , we define the set $\mathrm{Ter}(X)$ of $X$ -terms to be the smallest set satisfying the following two constraints: (1) $X\subseteq\mathrm{Ter}(X)$ , and (2) if $f\in\mathrm{Fun}$ , $f$ is of arity $n$ , and $t_{1},\ldots,t_{n}\in\mathrm{Ter}(X)$ , then $f(t_{1},\ldots,t_{n})\in\mathrm{Ter}(X)$ . The complete set of terms $\mathrm{Ter}$ is defined to be $\mathrm{Ter}(\mathrm{Var})$ . We use $t$ , $s$ , $\ldots$ (potentially annotated) to denote ( $X$ -)terms and let $VT(t)$ denote the set of variables occurring in the term $t$ . We will often write a list $t_{1},\ldots,t_{n}$ of terms as $\vec{t}$ , and define $VT(\vec{t})=VT(t_{1})\cup\cdots\cup VT(t_{n})$ .

We let $\mathrm{Pred}:=\{p,q,\ldots\}$ be a countably infinite set of predicates containing countably many predicates of each arity $n\in\mathbb{N}$ . We denote the arity of a predicate $p$ as $ar(p)$ and refer to predicates of arity $0$ as propositional atoms. An atomic formula is a formula of the form $p(t_{1},\ldots,t_{n})$ , obtained by prefixing a predicate $p$ of arity $ar(p)=n$ to a tuple of terms of length $n$ . We will often write atomic formulae $p(t_{1},\ldots,t_{n})$ as $p(\vec{t})$ .

Definition 1 (The Language $\mathcal{L}$ ).

The language $\mathcal{L}$ is defined to be the set of formulae generated via the following grammar in Backus-Naur form:

\varphi::=p(\vec{t})\ |\ \bot\ |\ \top\ |\ \varphi\land\varphi\ |\ \varphi\lor% \varphi\ |\ \varphi\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p041-Lyon.latexml-figure9.pdf}}}\hskip 0.43057pt}\varphi\ |\ \varphi% \rightarrow\varphi\ |\ \exists x\varphi\ |\ \forall x\varphi

where $p$ ranges over $\mathrm{Pred}$ , the terms $\vec{t}=t_{1},\ldots,t_{n}$ range over $\mathrm{Ter}$ , and $x$ ranges over the set $\mathrm{Var}$ . We use $\varphi$ , $\psi$ , $\chi$ , $\ldots$ to denote formulae.

The occurrence of a variable $x$ in $\varphi$ is defined to be free given that $x$ does not occur within the scope of a quantifier binding $x$ . We let $FV(\varphi)$ denote the set of all free variables occurring in the formula $\varphi$ and use $\varphi(x_{1},\ldots,x_{n})$ to denote that $FV(\varphi)=\{x_{1},\ldots,x_{n}\}$ . We let $\varphi(t/x)$ denote the formula obtained by replacing each free occurrence of the variable $x$ in $\varphi$ by $t$ , potentially renaming bound variables to avoid unwanted variable capture; e.g. $(\forall yp(x,y))(y/x)=\forall zp(y,z)$ . The complexity of a formula $\varphi$ , written $|\varphi|$ , is recursively defined as follows: (1) $|p(t_{1},\ldots,t_{n})|=|\bot|=|\top|:=0$ , (2) $|Qx\varphi|:=|\varphi|+1$ for $Q\in\{\forall,\exists\}$ , and (3) $|\varphi\circ\psi|:=|\varphi|+|\psi|+1$ for $\circ\in\{\lor,\land,\rightarrow,\mathrel{\hskip 0.43057pt\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}% {dagpub-tikzpictures/p041-Lyon.latexml-figure10.pdf}}}\hskip 0.43057pt}\}$ .

Following [32], we give a Kripke-style semantics for $\mathsf{BIQ}(\mathcal{ID})$ , defining the models used first, and explaining how formulae are evaluated over them second.

Definition 2 ( $\mathrm{ID}$ -Frame).

An $\mathrm{ID}$ -frame (or, frame) is a tuple $F=(W,\leq,U,D)$ such that:

$\blacksquare$

$W$ is a non-empty set $\{w,u,v,\ldots\}$ of worlds;
$\blacksquare$

$\leq\ \subseteq W\times W$ is a reflexive and transitive binary relation;
$\blacksquare$

$U$ is a non-empty set referred to as the universe;
$\blacksquare$

$D:W\to\mathcal{P}(U)$ is a domain function mapping each $w\in W$ to a non-empty set $D(w)\subseteq U$ with $U=\bigcup_{w\in W}D(w)$ , which satisfies the increasing domain condition: $\mathrm{(ID)}$ If $w\leq u$ , then $D(w)\subseteq D(u)$ .

Definition 3 ( $\mathrm{ID}$ -Model).

We define an $\mathrm{ID}$ -Model (or, model) $M$ to be an ordered triple $(F,I_{1},I_{2})$ such that:

$\blacksquare$

$F=(W,\leq,U,D)$ is a frame;
$\blacksquare$

$I_{1}$ is a function interpreting each function symbol $f\in\mathrm{Fun}$ such that $ar(f)=n$ by a function $I_{1}(f):U^{n}\to U$ , satisfying two conditions: $\mathrm{(C_{1})}$ For each $w\in W$ and constant $a$ , $I_{1}(a)\in D(w)$ , and $\mathrm{(C_{2})}$ For each $w\in W$ , $\vec{a}\in D(w)^{n}$ iff $I_{1}(f)(\vec{a})\in D(w)$ .
$\blacksquare$

$I_{2}$ is a function interpreting, in each $w\in W$ , each predicate $p\in\mathrm{Pred}$ such that $ar(p)=n$ by a set $I_{2}(w,p)\subseteq D(w)^{n}$ , satisfying the following monotonicity condition: $\mathrm{(M)}$ If $w\leq u$ , then $I_{2}(w,p)\subseteq I_{2}(u,p)$ .

Definition 4 ( $M$ -assignment).

Let $M=(F,I_{1},I_{2})$ be a model. We define an $M$ -assignment to be a function $\alpha:\mathrm{Var}\rightarrow U$ . We note $\alpha[a/x]$ is the function $\alpha$ modified in $x$ such that $\alpha[a/x](x)=a$ and $\alpha[a/x](y)=\alpha(y)$ if $y\not=x$ . Given an $M$ -assignment $\alpha$ , we define the interpretation of $t$ in $M$ given $\alpha$ , denoted $\overline{\alpha}(t)$ , inductively as follows: $\overline{\alpha}(x):=\alpha(x)$ and $\overline{\alpha}(f(t_{1},...,t_{n})):=I_{1}(f)(\overline{\alpha}(t_{1}),...,% \overline{\alpha}(t_{n}))$ .

Definition 5 (Semantics).

Let $M=(W,\leq,U,D,I_{1},I_{2})$ be a model with $w\in W$ and $\alpha$ an $M$ -assignment. The satisfaction relation $\Vdash$ is defined as follows:

$\blacksquare$

$M,w,\alpha\Vdash p(t_{1},\ldots,t_{n})$ iff $(\overline{\alpha}(t_{1}),\ldots,\overline{\alpha}(t_{n}))\in I_{2}(w,p)$ ;
$\blacksquare$

$M,w,\alpha\not\Vdash\bot$ ;
$\blacksquare$

$M,w,\alpha\Vdash\top$ ;
$\blacksquare$

$M,w,\alpha\Vdash\varphi\lor\psi$ iff $M,w,\alpha\Vdash\varphi$ or $M,w,\alpha\Vdash\psi$ ;
$\blacksquare$

$M,w,\alpha\Vdash\varphi\land\psi$ iff $M,w,\alpha\Vdash\varphi$ and $M,w,\alpha\Vdash\psi$ ;
$\blacksquare$

$M,w,\alpha\Vdash\varphi\mathrel{\hskip 0.43057pt\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p041-Lyon.latexml-figure11.pdf}}}\hskip 0.43057pt}\psi$ iff there exists a $u\in W$ such that $u\leq w$ , $M,u,\alpha\Vdash\varphi$ , and $M,u,\alpha\not\Vdash\psi$ ;
$\blacksquare$

$M,w,\alpha\Vdash\varphi\rightarrow\psi$ iff for all $u\in W$ , if $w\leq u$ and $M,u,\alpha\Vdash\varphi$ , then $M,u,\alpha\Vdash\psi$ ;
$\blacksquare$

$M,w,\alpha\Vdash\exists x\varphi$ iff there exists an $a\in D(w)$ such that $M,w,\alpha[a/x]\Vdash\varphi$ ;
$\blacksquare$

$M,w,\alpha\Vdash\forall x\varphi$ iff for all $u\in W$ and all $a\in D(u)$ , if $w\leq u$ , then $M,u,\alpha[a/x]\Vdash\varphi$ .

For a set $\Gamma\subseteq\mathcal{L}$ of formulae, we write $\Gamma\Vdash\varphi$ iff for all models $M$ , $M$ -assignments $\alpha$ , and worlds $w$ in $M$ , if $M,w,\alpha\Vdash\psi$ for each $\psi\in\Gamma$ , then $M,w,\alpha\Vdash\varphi$ . A formula $\varphi$ is valid iff $\emptyset\Vdash\varphi$ . Finally, we define the logic $\mathsf{BIQ}(\mathcal{ID})$ to be the set $\{\varphi\ |\ \emptyset\Vdash\varphi\}$ of all valid formulae.

Note that here we define logics as sets of formulae, and not consequence relations. While this is fit for our purpose, the reader should be warned that historical confusions emerged around this distinction in the case of propositional bi-intuitionistic logic [15, 36], notably pertaining to the deduction theorem.

Proposition 6.

Let $M=(W,\leq,U,D,I_{1},I_{2})$ be a model with $\alpha$ an $M$ -assignment. For any $\varphi\in\mathcal{L}$ , if $M,w,\alpha\Vdash\varphi$ and $w\leq u$ , then $M,u,\alpha\Vdash\varphi$ .

$\blacktriangleright$ Remark 7.

We define a $\mathrm{CD}$ -model to be a model satisfying the constant domain condition: $\mathrm{(CD)}$ If $w,u\in W$ , then $D(w)=D(u)$ . If we impose the $\mathrm{(CD)}$ condition on models, then first-order bi-intuitionistic logic with constant domains, dubbed $\mathsf{BIQ}(\mathcal{CD})$ , can be defined as the set of all valid formulae over the class of $\mathrm{CD}$ -models. In what follows, we let $\mathcal{ID}$ denote the class of $\mathrm{ID}$ -models and $\mathcal{CD}$ denote the class of $\mathrm{CD}$ -models.

Example 8.

Consider the formula $\forall x((p(x)\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p041-Lyon.latexml-figure12.pdf}}}\hskip 0.43057pt}\exists yp(y))\rightarrow\bot)$ , discussed in the introduction, but with the existence predicate removed. In the semantics with increasing domains, this formula is valid. To see this, suppose otherwise, i.e. that there exists a world $w$ where the formula is false. Thus, there is a successor $w\leq u$ such that $\bar{\alpha}(x)\in D(u)$ and $p(x)\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure13.pdf}}}\hskip 0.43057pt}\exists yp(y)$ is true, for some assignment $\alpha$ . The latter implies that for some $u^{\prime}$ such that $u^{\prime}\leq u$ , $p(x)$ is true (i.e. $\alpha(x)\in I_{P}(u^{\prime},p)$ ), but $\exists yp(y)$ is false. The former implies that $\alpha(x)\in D(u^{\prime})$ , so by the semantic clause for the $\exists$ quantifier, $\exists yp(y)$ must be true – contradiction.

3 Polytree Sequent Systems

Let $\mathrm{Lab}=\{w,u,v,\ldots\}$ be a countably infinite set of labels. For a formula $\varphi\in\mathcal{L}$ and label $w\in\mathrm{Lab}$ , we define $w\!:\!\varphi$ to be a labeled formula. We use $\Gamma$ , $\Delta$ , $\Sigma$ , $\ldots$ to denote finite multisets of labeled formulae, and let $w\!:\!\Gamma$ denote a multiset of labeled formulae all labeled with $w$ . A relational atom is an expression of the form ${w}R{u}$ and a domain atom is an expression of the form $w : x$ , where $w,u\in\mathrm{Lab}$ and $x\in\mathrm{Var}$ . Intuitively, the domain atom formalizes an existence predicate: $w : x$ can be interpreted as saying that the interpretation of $x$ exists at world $w$ . We use $\mathcal{R}$ and $\mathcal{T}$ (and annotated versions thereof) to denote finite multisets of, respectively, relational atoms and domain atoms. Also, we define $w\!:\!VT(t)=w:x_{1},\ldots,w:x_{n}$ with $VT(t)=\{x_{1},\ldots,x_{n}\}$ , define $w\!:\!VT(\vec{t})=w:VT(t_{1}),\ldots,w:VT(t_{n})$ with $\vec{t}=t_{1},\ldots,t_{n}$ , and let $w:\vec{x}=w:x_{1},\ldots,w:x_{n}$ for $\vec{x}=x_{1},\ldots,x_{n}$ . For multisets $X$ and $Y$ of labeled formulae, relational atoms, and/or domain atoms, we let $X, Y$ denote the multiset union of $X$ and $Y$ , and $\mathrm{Lab}(X)$ denote the set of labels occurring in $X$ .

Definition 9 (Polytree Sequent).

We define a polytree sequent to be an expression of the form $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ such that (1) if $\mathcal{R}\neq\emptyset$ , then $\mathrm{Lab}(\mathcal{T},\Gamma,\Delta)\subseteq\mathrm{Lab}(\mathcal{R})$ and if $\mathcal{R}=\emptyset$ , then $|\mathrm{Lab}(\mathcal{T},\Gamma,\Delta)|=1$ , and (2) $\mathcal{R}$ forms a polytree, i.e. the graph $G=(V,E)$ such that $V=\mathrm{Lab}(\mathcal{R})$ and $E=\{(w,u)\ |\ {w}R{u}\in\mathcal{R}\}$ is connected and free of both directed and undirected cycles. We refer to $\mathcal{R},\mathcal{T},\Gamma$ as the antecedent and $\Delta$ as the consequent of a polytree sequent. We will often refer to polytree sequents more simply as sequents.

We sometimes use $S$ , $S_{0}$ , $S_{1}$ , $\ldots$ to denote sequents, and for $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ , we define $\mathrm{Lab}(S)=\mathrm{Lab}(\mathcal{R},\mathcal{T},\Gamma,\Delta)$ . A flat sequent is an expression of the form $\mathcal{T},\Gamma\vdash\Delta$ such that $|\mathrm{Lab}(\mathcal{T},\Gamma,\Delta)|=1$ , i.e. all labeled formulae and domain atoms share the same label. Polytree sequents encode certain binary graphs whose nodes are flat sequents and such that if you ignore the orientation of the edges, the graph is a tree (cf. [5]). For example, the sequent

S=\underbrace{{u^{\prime}}R{w},{u}R{w},{w}R{v}}_{\mathcal{R}},\underbrace{u^{% \prime}:x,u:x,u:y,w:z,v:y,}_{\mathcal{T}}\underbrace{w:\varphi,w:\psi,v:\theta% }_{\Gamma}\vdash\underbrace{u^{\prime}:\tau,u:\chi,v:\xi}_{\Delta}

can be graphically depicted as the polytree $pt(S)$ , shown below:

$\blacktriangleright$ Remark 10.

To simplify the proofs of our results in Section 4, we assume w.l.o.g. that sequents with isomorphic polytree representations are mutually derivable from one another.

3.1 Semantics and Proof Systems

The following definition specifies how to interpret sequents. In essence, we lift the semantics of $\mathcal{L}$ to sequents by means of “ $M$ -interpretations”, mapping sequents into models.

Definition 11 (Sequent Semantics).

Let $M=(W,\leq,U,D,I_{1},I_{2})$ be a model and $\alpha$ an $M$ -assignment. We define an $M$ -interpretation to be a function $\iota$ mapping every label $w\in\mathrm{Lab}$ to a world $\iota(w)\in W$ . The satisfaction of multisets $\mathcal{R}$ , $\mathcal{T}$ , and $\Gamma$ are defined accordingly:

$\blacksquare$

$M,\iota,\alpha\models\mathcal{R}$ iff for all ${w}R{u}\in\mathcal{R}$ , $\iota(w)\leq\iota(u)$ ;
$\blacksquare$

$M,\iota,\alpha\models\mathcal{T}$ iff for all $w:x\in\mathcal{T}$ , $\overline{\alpha}(x)\in D(\iota(w))$ ;
$\blacksquare$

$M,\iota,\alpha\models\Gamma$ iff for all $w:\varphi\in\Gamma$ , $M,\iota(w),\alpha\Vdash\varphi$ .

We define a sequent $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ to be satisfied on $M$ with $\iota$ and $\alpha$ , written $M,\iota,\alpha\models S$ , iff if $M,\iota,\alpha\models\mathcal{R}$ , and $M,\iota,\alpha\models\mathcal{T}$ , as well as $M,\iota,\alpha\models\Gamma$ , then there exists a $w:\psi\in\Delta$ such that $M,\iota,\alpha\models w:\psi$ . We write $M,\iota,\alpha\not\models S$ when a sequent $S$ is not satisfied on $M$ with $\iota$ and $\alpha$ . A sequent $S$ is defined to be valid iff for every model $M$ , every $M$ -interpretation $\iota$ , and every $M$ -assignment $\alpha$ , we have $M,\iota,\alpha\models S$ ; otherwise, we say that $S$ is invalid and write $M,\iota,\alpha\not\models S$ .

Figure 1: The System

\mathsf{LBIQ}(\mathcal{ID})

.

Given a sequent $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ , we define the term substitution $S(t/x)$ to be the sequent obtained by replacing (1) every labeled formula $w:\varphi$ in $\Gamma,\Delta$ by $w:\varphi(t/x)$ and (2) $\mathcal{T}$ by $\mathcal{T}(t/x):=(\mathcal{T}\setminus\{w\!:\!x\mid w\!:\!x\in\mathcal{T}\})% \cup\{w\!:\!y\mid w\!:\!x\in\mathcal{T}\text{ and }y\in VT(t)\}.$ For example, if $S={w}R{u},w\!:\!x,u\!:\!x,u\!:\!y,w\!:\!p(x)\vdash u\!:\!\forall yq(x,y)$ , then

S(f(y,z)/x)={w}R{u},w\!:\!y,w\!:\!z,u\!:\!y,u\!:\!z,u\!:\!y,w\!:\!p(f(y,z))% \vdash u\!:\!\forall x^{\prime}q(f(y,z),x^{\prime})

where the bound variable $y$ in $\forall yq(x,y)$ was renamed to $x^{\prime}$ to avoid capture. We now define two reachability relations $\twoheadrightarrow^{+}_{\mathcal{R}}$ and $\twoheadrightarrow^{*}_{\mathcal{R}}$ as well as the notion of availability [9, 22] – all of which are required to properly formulate certain inference rules in our calculi.

Definition 12 ( $\twoheadrightarrow^{+}_{\mathcal{R}}$ , $\twoheadrightarrow^{*}_{\mathcal{R}}$ ).

Let $\mathcal{R}$ be a finite multiset of relational atoms such that $w,u\in\mathrm{Lab}(\mathcal{R})$ . We say that $u$ is strictly reachable from $w$ , written $w\twoheadrightarrow^{+}_{\mathcal{R}}u$ , iff there exist $v_{1},\ldots,v_{n}\in\mathrm{Lab}(\mathcal{R})$ such that ${w}R{v_{1}},\ldots,{v_{n}}R{u}\in\mathcal{R}$ with $n\in\mathbb{N}$ . We say that $u$ is reachable from $w$ , written $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ , iff $w\twoheadrightarrow^{+}_{\mathcal{R}}u$ or $w=u$ . We write $w\normalsize\not\twoheadrightarrow^{*}_{\mathcal{R}}u$ if $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ does not hold.

Definition 13 (Available).

Let $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ be a sequent with $w\in\mathrm{Lab}(S)$ . We define a term $t$ to be available for $w$ in $\mathcal{R},\mathcal{T}$ , written $\mathsf{A}(t,X_{w},\mathcal{R},\mathcal{T})$ , iff $t\in\mathrm{Ter}(X_{w})$ such that

X_{w}=\{x\ |\ u\!:\!x\in\mathcal{\mathcal{T}}\text{ and }u\twoheadrightarrow^{% *}_{\mathcal{R}}w\text{ for some $u\in\mathrm{Lab}(S)$}\}.

Our polytree calculus $\mathsf{LBIQ}(\mathcal{ID})$ for $\mathsf{BIQ}(\mathcal{ID})$ is shown in Figure 1. The $(ax)$ , $(\bot{\mathrm{L}})$ , and $(\top{\mathrm{R}})$ rules serve as initial rules, the domain shift rule $(ds)$ encodes the fact that $I_{2}(p,w)\subseteq D(w)^{n}$ in any model. We define the principal formula in an inference rule to be the one explicitly mentioned in the conclusion, the auxiliary formulae to be the non-principal formulae explicitly mentioned in the premises, and an active formula to be either a principal or auxiliary formula. For example, $w:\exists x\varphi$ is principal, $w:\varphi(t/x)$ is auxiliary, and both are active in $(\exists{\mathrm{R}})$ . Note that all rules of our calculus preserve the property of being a polytree-structured sequent. We define a proof and its height as usual [39]. Two unique features of our calculi are the inclusion of reachability rules and the domain shift rule ( $d s$ ), which we elaborate on next.

3.2 Reachability Rules

A unique feature of our calculi is the inclusion of reachability rules (introduced in [20]), a generalization of propagation rules (cf. [4, 8, 14]), which are not only permitted to propagate formulae throughout a polytree sequent when applied bottom-up, but may also check to see if data exists along certain paths. The rules $(ax)$ , $({\rightarrow}{\mathrm{L}})$ , $({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure14% .pdf}}}\hskip 0.43057pt}}{\mathrm{R}})$ , $(\exists{\mathrm{R}})$ , and $(\forall{\mathrm{L}})$ serve as our reachability rules. The side conditions of our reachability rules are listed at the bottom of Figure 1. Moreover, we define a label $u$ or a variable $y$ to be fresh in a rule application (as in the $(\exists{\mathrm{L}})$ and $(\forall{\mathrm{R}})$ rules) iff it does not occur in the conclusion of the rule.

$\blacktriangleright$ Remark 14.

If we set ${\dagger}_{4}$ := “ $t\in\mathrm{Ter}$ ”, ${\dagger}_{5}$ := “ $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ and $t\in\mathrm{Ter}$ ”, and remove the $(ds)$ rule, then we obtain a polytree calculus, dubbed $\mathsf{LBIQ}(\mathcal{CD})$ , for the constant domain version of the logic $\mathsf{BIQ}(\mathcal{CD})$ . We also note that in the constant domain setting, domain atoms are unnecessary and can be omitted from sequents.

Figure 2: An example proof in

\mathsf{LBIQ}(\mathcal{CD})

for bi-intuitionistic logic with constant domains.

To provide intuition, we give an example showing the operation of a reachability rule.

Example 15.

Let $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ such that $\mathcal{R}={u}R{w},{w}R{v}$ , $\mathcal{T}=w:x,u:y,v:z$ , $\Gamma=w:\forall xp(x),w:p(f(y)),w:p(z)$ , and $\Delta=u:q(x)\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures% /p041-Lyon.latexml-figure15.pdf}}}\hskip 0.43057pt}q(x),v:r(y)$ . A representation of $S$ as a polytree is shown below. We explain (in)valid applications of the $(\forall{\mathrm{L}})$ reachability rule.

The term $f(y)$ is available for $w$ in $S$ since $u\twoheadrightarrow^{*}_{\mathcal{R}}w$ , namely there is an edge from $u$ to $w$ , and $f(y)\in\mathrm{Ter}(X_{w})$ since $X_{w}=\{x,y\}$ . Therefore, we may (top-down) apply the $(\forall{\mathrm{L}})$ rule to delete $w:p(f(y))$ and derive the sequent $S^{\prime}=\mathcal{R},\mathcal{T},\Gamma^{\prime}\vdash\Delta$ with $\Gamma^{\prime}=w:\forall xp(x),w:p(z)$ . By contrast, $w:p(z)$ cannot be deleted via an application of $(\forall{\mathrm{L}})$ because the term $z$ is not available for $w$ in $S$ (observe that $w$ is not reachable from $v$ ) meaning $z\not\in\mathrm{Ter}(X_{w})$ .

$\blacktriangleright$ Remark 16.

We note that for any set $X\subseteq\mathrm{Var}$ , $\mathrm{Ter}(X)\neq\emptyset$ since all constants are contained in $\mathrm{Ter}(X)$ by definition. This means that bottom-up applications of $(\exists{\mathrm{R}})$ and $(\forall{\mathrm{L}})$ may instantiate existential and universal formulae with any constant.

The reachability rules $(ax)$ , $({\rightarrow}{\mathrm{L}})$ and $({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure16% .pdf}}}\hskip 0.43057pt}}{\mathrm{R}})$ are important to ensure completeness for both $\mathsf{LBIQ}(\mathcal{CD})$ and $\mathsf{LBIQ}(\mathcal{ID}).$ The reachability rules for $(\exists{\mathrm{R}})$ and $(\forall{\mathrm{L}})$ are relevant only for $\mathsf{LBIQ}(\mathcal{ID})$ to ensure that the domains in the model do not collapse into a constant domain. We illustrate the importance of these reachability rules with a couple of examples.

Example 17 (An Intuitionistic Formula Valid in Constant Domain Models).

Consider the intuitionistic formula $\forall x(p\lor r(x))\rightarrow(p\lor(q\rightarrow\forall xr(x)))$ . This formula was adapted from an example in [27], which was used to illustrate the difficulty of obtaining a sound and complete sequent system for intuitionistic logic with constant domains. A proof of this formula in $\mathsf{LBIQ}(\mathcal{CD})$ is shown in Figure 2 and crucially relies on reachability rules. In the figure, the relational atoms $\mathcal{R}=wRu,uRv,vRw^{\prime}$ in the instances of $(ax)$ allow us to conclude that $u\twoheadrightarrow^{*}_{\mathcal{R}}u$ and $u\twoheadrightarrow^{*}_{\mathcal{R}}w^{\prime}$ , justifying the left and right instances of $(ax)$ , respectively.

Example 18 (Non-Provability of the Quantifier Shift Axiom in the Increasing Domain Setting).

Let us consider again the quantifier shift axiom $\forall x(\varphi\lor\psi)\rightarrow(\forall x\varphi\lor\psi)$ and an attempt to construct a proof (bottom-up) of one of its instances in $\mathsf{LBIQ}(\mathcal{ID})$ .

It is obvious that to finish this proof, we would need to instantiate the $\forall x$ quantifier in the labeled formula $u:\forall x(p(x)\lor q)$ with $x$ by applying the $(\forall{\mathrm{L}})$ rule. However, to do so, we would need to demonstrate that the world $u$ is reachable from $v$ where the domain atom $v : x$ resides. Yet, $u$ is not reachable from $v$ , so $x$ is not available at $u$ to be used by $(\forall{\mathrm{L}})$ .

3.3 The Domain Shift Rule $(ds)$

Although the reachability rules for the quantifiers prevent the quantifier shift axiom from being proved, it turns out that they are not sufficient to ensure the completeness of $\mathsf{LBIQ}(\mathcal{ID})$ with respect to the sequent semantics for the logic $\mathsf{BIQ}(\mathcal{ID})$ . Interestingly, this incompleteness only arises when the exclusion connective is involved – if one considers the intuitionistic fragment of $\mathsf{LBIQ}(\mathcal{ID})$ , these reachability rules are sufficient to prove completeness (see Lemma 26 in Section 3.5). To see this incompleteness issue, consider the formula in Example 8, which is semantically valid, and the following attempt at a (bottom-up) construction of a proof:

We have so far applied only invertible rules, so the original sequent is provable iff the top sequent in the above derivation also is. To proceed with the proof construction, one needs to instantiate the existential quantifier $\exists y$ with $x$ . However, the only domain atom containing $x$ is located at the world $u$ , which is not available to $u^{\prime}$ where the existential formula is located.

It is not so obvious how the reachability rules for quantifiers could be amended to allow this example to be proved. Looking at the above derivation, it might be tempting to augment the calculus with a rule that allows a backward reachability condition for domain atoms, e.g., making $u : x$ available to $u^{\prime}$ for when $u^{\prime}\twoheadrightarrow^{*}_{\mathcal{R}}u$ under certain admissibility conditions, but this could easily lead to a collapse of the domains if one is not careful. Instead, our approach here is motivated by the semantic clause for predicates: when $p(x)$ holds in a world, its interpretation requires that $x$ is also defined in that world. Proof theoretically, we could think of this as postulating an axiom such as $\forall x(p(x)\rightarrow E(x))$ where $E(x)$ is an existence predicate (which, as we recall, was behind the semantics of the domain atoms). Translated into our calculus, this gives us the $(ds)$ rule as shown in Figure 1. Using the $(ds)$ rule, the above derivation can now be completed to a proof:

Note that the $(ds)$ rule can only be applied to atomic predicates, but not arbitrary formulae, which rules out unsound instances. It may be possible to relax the restriction to atomic predicates by imposing some positivity conditions on the occurrences of $x$ , but we did not find this necessary – neither for completeness, nor for cut-elimination.

$\blacktriangleright$ Remark 19.

The $(ds)$ rule can be removed without affecting the cut-elimination result for $\mathsf{LBIQ}(\mathcal{ID})$ . This raises the possibility of defining a first-order bi-intuitionistic logic strictly weaker than $\mathsf{BIQ}(\mathcal{ID})$ . It is unclear what the semantics for such a logic would look like.

3.4 Soundness and Completeness

Theorem 20 (Soundness).

Let $S$ be a sequent. If $S$ is provable in $\mathsf{LBIQ}(\mathcal{ID})$ ( $\mathsf{LBIQ}(\mathcal{CD})$ ), then $S$ is ( $\mathrm{CD}$ -)valid.

Proof.

By induction on the height of the given proof; see Appendix A for details. $\hfill\blacktriangleleft$

The completeness of our polytree calculi (see Theorem 22 below) is shown by taking a sequent of the form $w:\vec{x}\vdash w:\varphi(\vec{x})$ as input and showing that if the sequent is not provable, then the calculus can be used to construct an infinite derivation from which a counter-model of the end sequent can be extracted. We note that completeness only holds relative to sequents of the form $w:\vec{x}\vdash w:\varphi(\vec{x})$ , which includes a domain atom for each free variable in $\varphi(\vec{x})$ . This restriction is needed because quantifier rules can only (bottom-up) instantiate quantified formulae with the free variables $\vec{x}$ of $\varphi(\vec{x})$ if such free variables occur as domain atoms, and such free variables must be accessible to quantifier rules to properly extract a counter-model of the end sequent (see [23] for a relevant discussion).

Below, we outline the cut-free completeness proof for $\mathsf{LBIQ}(\mathcal{ID})$ as the proof for $\mathsf{LBIQ}(\mathcal{CD})$ is similar; the complete proof can be found in the online, appended version [26]. Our proof outline makes use of various new notions, which we now define. A pseudo-derivation is defined to be a (potentially infinite) tree whose nodes are sequents and where every parent node corresponds to the conclusion of a rule in $\mathsf{LBIQ}(\mathcal{ID})$ with the children nodes corresponding to the premises. We remark that a proof in $\mathsf{LBIQ}(\mathcal{ID})$ is a finite pseudo-derivation where all top sequents are instances of $(ax)$ , $(\bot{\mathrm{L}})$ , or $(\top{\mathrm{R}})$ . A branch $\mathcal{B}$ is defined to be a maximal path of sequents through a pseudo-derivation, starting from the conclusion. The following lemma is useful in proving completeness.

Lemma 21.

Let $\mathcal{C}\in\{\mathcal{ID},\mathcal{CD}\}$ . For each $i\in\{0,1,2\}$ , let $S_{i}=\mathcal{R}_{i},\mathcal{T}_{i},\Gamma_{i}\vdash\Delta_{i}$ be a sequent.

1.

If $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ holds for the conclusion of a rule $(r)$ in $\mathsf{LBIQ}(\mathcal{C})$ , then $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ holds for the premises of $(r)$ ;
2.

If $w:p(\vec{t})\in\Gamma_{0},\Delta_{0}$ and $S_{0}$ is the conclusion of a rule $(r)$ in $\mathsf{LBIQ}(\mathcal{C})$ with $S_{1}$ (and $S_{2}$ ) the premise(s) of $(r)$ , then $w:p(\vec{t})\in\Gamma_{1},\Delta_{1}$ (and $w:p(\vec{t})\in\Gamma_{2},\Delta_{2}$ , resp.);
3.

If $w:x\in\mathcal{T}_{0}$ and $S_{0}$ is the conclusion of a rule $(r)$ in $\mathsf{LBIQ}(\mathcal{C})$ with $S_{1}$ (and $S_{2}$ ) the premise(s) of $(r)$ , then $w:x\in\mathcal{T}_{1}$ (and $w:x\in\mathcal{T}_{2}$ , resp.).

The lemma tells us that propagation paths, the position of atomic formulae, and the position of terms are bottom-up preserved in rule applications.

Theorem 22 (Completeness).

If $w:\vec{x}\vdash w:\varphi(\vec{x})$ is ( $\mathrm{CD}$ -)valid, then $w:\vec{x}\vdash w:\varphi(\vec{x})$ is provable in $\mathsf{LBIQ}(\mathcal{ID})$ ( $\mathsf{LBIQ}(\mathcal{CD})$ ).

Proof (Outline).

We assume that $S=w:\vec{x}\vdash w:\varphi(\vec{x})$ is not provable in $\mathsf{LBIQ}(\mathcal{ID})$ and show that a model $M$ can be defined which witnesses that $S$ is invalid. To prove this, we first define a proof-search procedure $\mathtt{Prove}$ that bottom-up applies rules from $\mathsf{LBIQ}(\mathcal{ID})$ to $w:\vec{x}\vdash w:\varphi(\vec{x})$ . Second, we show how a model $M$ can be extracted from failed proof-search. We now describe the proof-search procedure $\mathtt{Prove}$ and let $\prec$ be a well-founded, strict linear order over the set $\mathrm{Ter}$ of terms.

$\mathtt{Prove}$ .

Let us take $w:\vec{x}\vdash w:\varphi(\vec{x})$ as input and continue to the next step. We show some key steps; the complete $\mathtt{Prove}$ procedure can be found in the online appended version [26].

$(ax)$ , $(\bot{\mathrm{L}})$ , and $(\top{\mathrm{R}})$ .

Suppose $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ are all branches occurring in the current pseudo-derivation and let $S_{1},\ldots,S_{n}$ be the top sequents of each respective branch. For each $1\leq i\leq n$ , we halt the computation of $\mathtt{Prove}$ on each branch $\mathcal{B}_{i}$ where $S_{i}$ is of the form $(ax)$ , $(\bot{\mathrm{L}})$ , or $(\top{\mathrm{R}})$ . If $\mathtt{Prove}$ is halted on each branch $\mathcal{B}_{i}$ , then $\mathtt{Prove}$ returns $\mathtt{True}$ because a proof of the input has been constructed. However, if $\mathtt{Prove}$ did not halt on each branch $\mathcal{B}_{i}$ with $1\leq i\leq n$ , then let $\mathcal{B}_{j_{1}},\ldots,\mathcal{B}_{j_{k}}$ be the remaining branches for which $\mathtt{Prove}$ did not halt. For each such branch, copy the top sequent above itself, and continue to the next step.

$(ds)$ .

Suppose $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ are all branches occurring in the current pseudo-derivation and let $S_{1},\ldots,S_{n}$ be the top sequents of each respective branch. For each $1\leq i\leq n$ , we consider $\mathcal{B}_{i}$ and extend the branch with bottom-up applications of $(ds)$ rules. Let $\mathcal{B}_{k+1}$ be the current branch under consideration, and assume that $\mathcal{B}_{1},\ldots,\mathcal{B}_{k}$ have already been considered. We assume that the top sequent in $\mathcal{B}_{k+1}$ is of the form

S_{k+1}=\mathcal{R},\mathcal{T},\Gamma,w:p_{1}(\vec{t}_{1}),\ldots,w_{\ell}:p_% {\ell}(\vec{t}_{\ell})\vdash\Delta

where all atomic input formulae are displayed in $S_{k+1}$ above. We successively consider each atomic input formula and bottom-up apply $(ds)$ , yielding a branch extending $\mathcal{B}_{k+1}$ with a top sequent saturated under $(ds)$ applications. After these operations have been performed for each branch $\mathcal{B}_{i}$ with $1\leq i\leq n$ , we continue to the next step.

$(\exists{\mathrm{L}})$ .

Suppose $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ are all branches occurring in the current pseudo-derivation and let $S_{1},\ldots,S_{n}$ be the top sequents of each respective branch. For each $1\leq i\leq n$ , we consider $\mathcal{B}_{i}$ and extend the branch with bottom-up applications of $(\exists{\mathrm{L}})$ rules. Let $\mathcal{B}_{k+1}$ be the current branch under consideration, and assume that $\mathcal{B}_{1},\ldots,\mathcal{B}_{k}$ have already been considered. We assume that the top sequent in $\mathcal{B}_{k+1}$ is of the form

S_{k+1}=\mathcal{R},\mathcal{T},\Gamma,w_{1}:\exists x_{1}\varphi_{1},\ldots,w% _{m}:\exists x_{m}\varphi_{m}\vdash\Delta

where all existential input formulae $w_{i}:\exists x_{i}\varphi_{i}$ are displayed in $S_{k+1}$ above. We consider each formula $w_{i}:\exists x_{i}\varphi_{i}$ in turn, and bottom-up apply the $(\exists{\mathrm{L}})$ rule. These rule applications extend $\mathcal{B}_{k+1}$ such that

\mathcal{R},\mathcal{T}^{\prime},\Gamma,w_{1}:\varphi_{1}(y_{1}/x_{1}),\ldots,% w_{n}:\varphi_{m}(y_{m}/x_{m})\vdash\Delta

is now the top sequent of the branch with $y_{1},\ldots,y_{m}$ fresh variables and $\mathcal{T}^{\prime}=\mathcal{T},w_{1}:y_{1},\ldots,w_{m}:y_{m}$ . After these operations have been performed for each branch $\mathcal{B}_{i}$ with $1\leq i\leq n$ , we continue to the next step.

$(\exists{\mathrm{R}})$ .

Suppose $\mathcal{B}_{1},\ldots,\mathcal{B}_{n}$ are all branches occurring in the current pseudo-derivation and let $S_{1},\ldots,S_{n}$ be the top sequents of each respective branch. For each $1\leq i\leq n$ , we consider $\mathcal{B}_{i}$ and extend the branch with bottom-up applications of $(\exists{\mathrm{R}})$ rules. Let $\mathcal{B}_{k+1}$ be the current branch under consideration, and assume that $\mathcal{B}_{1},\ldots,\mathcal{B}_{k}$ have already been considered. We assume that the top sequent in $\mathcal{B}_{k+1}$ is of the form

S_{k+1}=\mathcal{R},\mathcal{T},\Gamma\vdash w_{1}:\exists x_{1}\varphi_{1},% \ldots,w_{m}:\exists x_{m}\varphi_{m},\Delta

where all existential formulae $w_{i}:\exists x_{i}\varphi_{i}$ are displayed in $S_{k+1}$ above. We consider each labeled formula $w_{m}:\exists x_{m}\varphi_{i}$ in turn, and bottom-up apply the $(\exists{\mathrm{R}})$ rule. Let $w_{\ell+1}:\exists x_{\ell+1}\varphi_{\ell+1}$ be the current formula under consideration, and assume that $w_{1}:\exists x_{1}\varphi_{1},\ldots,w_{\ell}:\exists x_{\ell}\varphi_{\ell}$ have already been considered. Recall that $\prec$ is a well-founded, strict linear order over the set $\mathrm{Ter}$ of terms. Choose the $\prec$ -minimal term $t\in\mathrm{Ter}(X_{w_{\ell+1}})$ that has yet to be picked to instantiate $w_{\ell+1}:\exists x_{\ell+1}\varphi_{\ell+1}$ and bottom-up apply the $(\exists{\mathrm{R}})$ rule, thus adding $w_{\ell+1}:\varphi_{\ell+1}(t/x_{\ell+1})$ . We perform these operations for each branch $\mathcal{B}_{i}$ with $1\leq i\leq n$ .

The remaining rules of $\mathsf{LBIQ}(\mathcal{ID})$ are processed in a similar fashion. The $\mathtt{Prove}$ procedure will saturate open branches of the pseudo-derivation that is under construction by repeatedly (bottom-up) applying rules from $\mathsf{LBIQ}(\mathcal{ID})$ in a roundabout fashion.

Next, we aim to show that if $\mathtt{Prove}$ does not return $\mathtt{True}$ , then a model $M$ , $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ can be defined such that $M,\iota,\alpha\not\models S$ . If $\mathtt{Prove}$ halts, i.e. $\mathtt{Prove}$ returns $\mathtt{True}$ , then a proof of $S$ may be obtained by “contracting” all redundant inferences from the “ $(ax)$ , $(\bot{\mathrm{L}})$ , and $(\top{\mathrm{R}})$ ” step of $\mathtt{Prove}$ . Therefore, in this case, since a proof exists, we have obtained a contradiction to our assumption. As a consequence, we have that $\mathtt{Prove}$ does not halt, that is, $\mathtt{Prove}$ generates an infinite tree with finite branching. By König’s lemma, an infinite branch must exist in this infinite tree, which we denote by $\mathcal{B}$ . We define a model $M=(W,\leq,U,D,I_{1},I_{2})$ by means of this branch as follows: Let us define the following sets, all of which are obtained by taking the union of each multiset of relational atoms, domain atoms, antecedent labeled formulae, and consequent labeled formulae (resp.) occurring within a sequent in $\mathcal{B}$ :

\mathcal{R}^{\mathcal{B}}=\!\!\!\!\!\!\!\!\bigcup_{(\mathcal{R},\mathcal{T},% \Gamma\vdash\Delta)\in\mathcal{B}}\!\!\!\!\!\!\!\!\mathcal{R}\qquad\mathcal{T}% ^{\mathcal{B}}=\!\!\!\!\!\!\!\!\bigcup_{(\mathcal{R},\mathcal{T},\Gamma\vdash% \Delta)\in\mathcal{B}}\!\!\!\!\!\!\!\!\mathcal{T}\qquad\Gamma^{\mathcal{B}}=\!% \!\!\!\!\!\!\!\bigcup_{(\mathcal{R},\mathcal{T},\Gamma\vdash\Delta)\in\mathcal% {B}}\!\!\!\!\!\!\!\!\Gamma\qquad\Delta^{\mathcal{B}}=\!\!\!\!\!\!\!\!\bigcup_{% (\mathcal{R},\mathcal{T},\Gamma\vdash\Delta)\in\mathcal{B}}\!\!\!\!\!\!\!\!\Delta

We now define: (1) $u\in W$ iff $u\in\mathrm{Lab}(\mathcal{R}^{\mathcal{B}},\mathcal{T}^{\mathcal{B}},\Gamma^{% \mathcal{B}},\Delta^{\mathcal{B}})$ , (2) $\leq\ =\{(u,v)\ |\ uRv\in\mathcal{R}\}^{*}$ where $*$ denotes the reflexive-transitive closure, (3) $t\in U$ iff there exists a label $u\in\mathrm{Lab}(\mathcal{R}^{\mathcal{B}},\mathcal{T}^{\mathcal{B}},\Gamma^{% \mathcal{B}},\Delta^{\mathcal{B}})$ such that $t\in\mathrm{Ter}(X_{u})$ , (4) $t\in D(u)$ iff $t\in\mathrm{Ter}(X_{u})$ , and (5) $(t_{1},\ldots,t_{n})\in I_{2}(u,p)$ iff $v,u\in\mathrm{Lab}(\mathcal{R}^{\mathcal{B}},\mathcal{T}^{\mathcal{B}},\Gamma^% {\mathcal{B}},\Delta^{\mathcal{B}})$ , $v\twoheadrightarrow^{*}_{\mathcal{R}^{\mathcal{B}}}u$ , and $v:p(t_{1},\ldots,t_{n})\in\Gamma^{\mathcal{B}}$ .

It can be shown that $M$ is indeed a model. Let us define $\alpha$ to be the $M$ -assignment mapping every variable in $U$ to itself and every variable in $\mathrm{Var}\setminus U$ arbitrarily. To finish the proof of completeness, we now argue the following by mutual induction on the complexity of the formula $\psi$ : (1) if $u:\psi\in\Gamma^{\mathcal{B}}$ , then $M,u,\alpha\Vdash\psi$ , and (2) if $u:\psi\in\Delta^{\mathcal{B}}$ , then $M,u,\alpha\not\Vdash\psi$ . Let $\iota$ to be the $M$ -interpretation such that $\iota(u)=u$ for $u\in W$ and $\iota(v)\in W$ for $v\not\in W$ . By the proof above, $M,\iota,\alpha\not\models w:\vec{x}\vdash w:\varphi(\vec{x})$ , showing that if a sequent of the form $w:\vec{x}\vdash w:\varphi(\vec{x})$ is not provable in $\mathsf{LBIQ}(\mathcal{ID})$ , then it is invalid, that is, every valid sequent of the form $w:\vec{x}\vdash w:\varphi(\vec{x})$ is provable in $\mathsf{LBIQ}(\mathcal{ID})$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 23.

We remark that cut admissibility follows from the soundness of the $(cut)$ rule (see Figure 3) and the completeness theorem above. However, this method of proof has two downsides: first, the restriction in the completeness theorem above implies that cut admissibility only holds for proofs with an end sequent of the form $w:\vec{x}\vdash w:\varphi(\vec{x})$ . Second, this (semantic) method of proof does not define an algorithm showing how instances of $(cut)$ can be permuted upward and eliminated from a given proof. In Section 4, we will prove that cut admissibility holds for all proofs and will provide such an algorithm (see Theorem 30).

3.5 Intuitionistic Subsystems

We end this section by discussing two subsystems of $\mathsf{LBIQ}(\mathcal{ID})$ and $\mathsf{LBIQ}(\mathcal{CD})$ arising from restricting the connectives to the intuitionistic fragment. In the former case, we obtain a proof system for the usual first-order intuitionistic logic (with non-constant domains) $\mathsf{IQ}$ , and in the latter, we obtain a proof system for intuitionistic logic with constant domains $\mathsf{IQC}$ .

Corollary 24 (Conservativity).

Let $\varphi$ be an intuitionistic formula (i.e. a formula with no occurrences of $\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure17% .pdf}}}\hskip 0.43057pt}$ ). Then, $\varphi$ is valid in $\mathsf{IQ}$ ( $\mathsf{IQC}$ ) iff $\vdash w:\varphi$ is provable in $\mathsf{LBIQ}(\mathcal{ID})$ (respectively, $\mathsf{LBIQ}(\mathcal{CD})$ ).

The proof of Corollary 24 is straightforward from Definition 11. We show here a stronger proof-theoretic conservativity result: we can in fact extract a purely intuitionistic fragment out of $\mathsf{LBIQ}(\mathcal{ID})$ , where every sequent in the fragment is interpretable in the semantics without the existence predicate. We prove this via syntactic means, by showing how we can translate intuitionistic proofs in $\mathsf{LBIQ}(\mathcal{ID})$ to proofs in Gentzen’s $\mathsf{LJ}$ [11, 12]. A key idea is to first define a formula interpretation of a polytree sequent, and then show that every inference rule corresponds to a valid implication in $\mathsf{LJ}$ . We start by defining a notion of intuitionistic (polytree) sequent.

Definition 25.

A sequent $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ is an intuitionistic sequent iff $\mathcal{R}$ is a tree rooted at node $u$ such that

$\blacksquare$

every formula in $S$ is an intuitionistic formula (i.e. it contains no occurrences of $\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure18% .pdf}}}\hskip 0.43057pt}$ ),
$\blacksquare$

for every labeled formula $w:\varphi$ in $S$ and variable $x\in VT(\varphi)$ , $x$ is available for $w$ , and
$\blacksquare$

if $w : x$ and $z : x$ are in $\mathcal{T}$ , then $w=z.$

By $\mathsf{NIQ}(\mathcal{ID})$ we denote the restriction to intuitionistic sequents of the proof system $\mathsf{LBIQ}(\mathcal{ID})$ without the $(ds)$ rule. The next lemma states an important property of $\mathsf{LBIQ}(\mathcal{ID})$ , called the separation property, which was first discussed in the context of tense logics [14].

Lemma 26 (Separation).

An intuitionistic sequent $S$ is provable in $\mathsf{NIQ}(\mathcal{ID})$ iff it is provable in $\mathsf{LBIQ}(\mathcal{ID}).$

Proof (Outline).

One direction, from $\mathsf{NIQ}(\mathcal{ID})$ to $\mathsf{LBIQ}(\mathcal{ID})$ is trivial. For the other direction, suppose $\pi$ is a proof of $S$ in $\mathsf{LBIQ}(\mathcal{ID}).$ By induction on the structure of $\pi$ , it can be shown that there is a proof $\pi^{\prime}$ in $\mathsf{LBIQ}(\mathcal{ID})$ in which every sequent in $\pi^{\prime}$ is almost intuitionistic – it satisfies all the requirements in Definition 25 except possibly the last condition (due to the possible use of the $(ds)$ rule). Then, from $\pi^{\prime}$ we can construct another proof $\pi^{\prime\prime}$ of $S$ that does not use $(ds)$ , by showing that one can always permute the rule $(ds)$ up until it disappears. Since all the rules of $\mathsf{LBIQ}(\mathcal{ID})$ , other than $(ds)$ , preserve the property of being an intuitionistic sequent, it then follows that $\pi^{\prime\prime}$ is a proof in $\mathsf{NIQ}(\mathcal{ID}).$ $\hfill\blacktriangleleft$

To translate a proof in $\mathsf{NIQ}(\mathcal{ID})$ to $\mathsf{LJ}$ , we need to interpret a polytree sequent as a formula. This turns out to be somewhat problematic, due to the difficulty in interpreting the scopes of domain atoms, when interpreting them as universally quantified variables. Fortunately, in the case of intuitionistic sequents, the scopes of such variables follow a straightforward lexical scoping (i.e. their scopes are over formulae in the subtrees). To define the translation, we first relax the requirement on the domain atoms in intuitionistic sequents: a quasi-intuitionistic sequent is defined as in Definition 25, except that in the second clause, $x$ is either available for $w$ , or it does not occur in $\mathcal{T}$ . Obviously an intutionistic sequent is also a quasi-intuitionistic sequent. Given a quasi-intuitionistic sequent $S$ and a label $w$ , we write $S_{w}$ to denote the quasi-intuitionistic sub-sequent of $S$ that is rooted in $w$ , i.e. the sequent obtained from $S$ by removing any relational atoms, domain atoms, and labeled formulae that mention a world $v$ not reachable from $w .$ Given a multiset of labeled formulae $\Gamma$ , we denote with $\Gamma_{u}$ the labeled formulae in $\Gamma$ that are labeled with $u$ .

Definition 27.

Let $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ be a quasi-intuitionistic sequent. We define its formula interpretation $F(S)$ recursively on the height of the sequent tree and suppose $S$ is rooted at $u$ .

$\blacksquare$

If $S$ is a flat sequent, then $F(X)=\forall\vec{x}(\bigwedge\Gamma\rightarrow\bigvee\Delta)$ where $\vec{x}$ are all the variables in $\mathcal{T}$ ;
$\blacksquare$

otherwise, if $u$ has $n$ successors $w_{1},\ldots,w_{n}$ , then

$F(S)=\forall\vec{x}(\bigwedge\Gamma_{u}\rightarrow(\bigvee\Delta_{u}\lor F(S_{% w_{1}})\lor\cdots\lor F(S_{w_{n}}))).$

The following proof-theoretic conservativity result can then be proved using a standard translation technique for relating nested sequents and traditional Gentzen sequent calculi [6].

Proposition 28.

Let $S$ be an intuitionistic sequent. $S$ is provable in $\mathsf{NIQ}(\mathcal{ID})$ iff $F(S)$ is provable in $\mathsf{LJ}$ .

Proof (Outline).

The proof is tedious, but not difficult and follows a general strategy to translate nested sequent proofs (which, recall, are notational variants of polytree sequent proofs) to traditional sequent proofs (with cuts) from the literature, see e.g., the translation from nested sequent to traditional sequent proofs for full intuitionistic linear logic [6]. For every inference rule in $\mathsf{NIQ}(\mathcal{ID})$ of the form:

we show that the formula $F(S_{1})\land\cdots\land F(S_{n})\rightarrow F(S)$ is provable in $\mathsf{LJ}$ . Then, given any proof in $\mathsf{NIQ}(\mathcal{ID})$ , we simulate every inference step with its corresponding implication, followed by a cut. $\hfill\blacktriangleleft$

As far as we know, for intuitionistic logic with constant domains $\mathsf{IQC}$ , there is no formalization in the traditional Gentzen sequent calculus that admits cut-elimination. There is, however, a formalization in prefixed tableaux by Fitting [9], which happens to be a syntactic variant of the intuitionistic fragment of $\mathsf{LBIQ}(\mathcal{CD})$ (shown in [19]).

4 Cut-Elimination

Figure 3: Admissible rules.

In this section, we show that $\mathsf{LBIQ}(\mathcal{ID})$ and $\mathsf{LBIQ}(\mathcal{CD})$ satisfy a sizable number of favorable properties culminating in syntactic cut-elimination. We explain here some key steps; the full details are available in the online appended version [26].

$\mathsf{LBIQ}(\mathcal{ID})$ and $\mathsf{LBIQ}(\mathcal{CD})$ can be seen as first-order extensions of Postniece’s deep-nested sequent calculus for bi-intuitionistic logic $\mathrm{DBiInt}$ [31, 13]. Cut-elimination for $\mathrm{DBiInt}$ [13] was proven in two stages. First, cut-elimination was proven for a “shallow” version of the nested sequent calculus $\mathrm{LBiInt}$ , which can be seen as a variant of a display calculus [1]. The cut-elimination proof for this shallow calculus follows from Belnap’s generic cut-elimination for display calculi [1]. Second, cut-free proofs in the shallow calculus are shown to be translatable to proofs in the deep-nested calculus. We do not have the corresponding shallow versions of $\mathsf{LBIQ}(\mathcal{ID})$ and $\mathsf{LBIQ}(\mathcal{CD})$ , so we cannot rely on Belnap’s generic cut-elimination. It may be possible to define shallow versions of our calculi, and then follow the same methodology outlined in [13] to prove cut-elimination, but we find that a direct cut-elimination proof is simpler, e.g., it avoids the need for proving the admissibility of certain structural rules called the display postulates [1], which lets one transition from shallow to deep inference systems.

Since our polytree sequents are a restriction of ordinary labeled sequents, another possible approach to cut-elimination is to apply the methodology for labeled sequent calculi [28]. A main issue in adapting this methodology is ensuring that the proof transformations needed in cut-elimination preserve the polytree structure of sequents. A key proof transformation in a typical cut-elimination proof for labeled calculi is label substitution: given a proof $\pi_{1}$ and labels $u$ and $w$ , one constructs another proof $\pi_{2}$ by replacing $u$ with $w$ everywhere in $\pi_{1}$ and adjusts the inference rules accordingly. This is typically needed in the reduction of a cut where the last rules in both branches of the cut apply to the cut formula, and where one of the rules introduces (reading the rule bottom up) a new label and a new relational atom (e.g., $({\rightarrow}{\mathrm{R}})$ ). Such a substitution operation may not preserve polytree structures. Another notable difference between our calculi and traditional labeled calculi is the absence of structural rules manipulating relational atoms. These differences mean that cut-elimination techniques for labeled sequent calculi cannot be immediately applied in our setting.

Instead, our cut-elimination proof builds on an approach by Pinto and Uustalu [29, 30], which deals with a polytree sequent calculus for propositional bi-intuitionistic logic. We thus provide a series of proof transformations, culminating in the elimination of cuts, which shares similarities with their work in the propositional case and expands in the first-order direction. These transformations are captured in proofs of the admissibility of rules shown in Figure 3. We illustrate some key transformations and why they are needed, through an example of a cut where $({\rightarrow}{\mathrm{L}})$ and $({\rightarrow}{\mathrm{R}})$ are applied to the cut formula. The formal details are available in the proof of Theorem 30.

Suppose we have the instance of cut shown below left, where $\pi_{1}$ is shown below right and $\pi_{2}$ is shown below bottom with $w\twoheadrightarrow^{*}_{\mathcal{R}}u.$

A typical cut reduction strategy would be to cut $\pi_{1}$ with $\pi_{3}$ and $\pi_{4}$ (both with cut formula $\varphi\rightarrow\psi$ ), producing the proofs $\pi_{5}$ and $\pi_{6}$ of $\mathcal{R},\Gamma\vdash\Delta,u:\varphi$ and $\mathcal{R},\Gamma,u:\psi\vdash\Delta$ , respectively. Next, one would cut $\pi_{5}$ with $\pi_{1}^{\prime}$ (with cut formula $\varphi$ ), producing a proof $\pi_{7}$ , and then cut $\pi_{7}$ with $\pi_{6}$ (with cut formula $\psi$ ). There are a couple of issues with this strategy: (1) the cut formulae in the last two instances of cut have mismatched labels, i.e., $w^{\prime}$ on one side and $u$ on the other ; (2) the label $w^{\prime}$ and the relational atom $wRw^{\prime}$ are not present in the conclusions of $\pi_{5}$ and $\pi_{6}$ , so the contexts of the premises of the cuts do not match.

To fix these issues, we first need to transform the proof $\pi_{1}^{\prime}$ into two proofs $\pi_{5}$ and $\pi_{6}$ , shown below left and right, respectively. As shown in the cut-elimination proof, a transformation that we use in this case is one that is represented by the rule $(iw)$ . This ensures that the contexts match the contexts of the concluding sequents in $\pi_{3}$ and $\pi_{4}$ .

We then cut $\pi_{3}$ and $\pi_{4}$ with $\pi_{5}$ and $\pi_{6}$ , respectively, which yields proofs $\pi_{7}$ and $\pi_{8}$ of $\mathcal{R},\Gamma\vdash u:\varphi,\Delta$ and $\mathcal{R},\Gamma,u:\psi\vdash\Delta$ , respectively. At this stage, we want to cut $\pi_{7}$ with $\pi_{1}^{\prime}$ , and then cut the resulting proof with $\pi_{8}$ . However, this cut cannot be performed until the label $w^{\prime}$ and its associated relational atom are removed from the conclusion of $\pi_{1}^{\prime}$ . Simply substituting $u$ for $w^{\prime}$ may break the polytree shape of the sequent, e.g., if there is a $v$ such that $w R v$ and $v R u$ are in $\mathcal{R}$ , then replacing $u$ for $w^{\prime}$ in $wRw^{\prime}$ would break the polytree shape of the sequent. So the relational atoms in the sequent also need to be modified. A transformation that we use in this case is represented by the rule $(br_{f})$ , which shifts the relational atom $wRw^{\prime}$ “forward” from $w$ to $u$ given that $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ . We also need another transformation to “merge” the label $u$ with the label $w^{\prime}$ , deleting the relational atom in the process, represented as the $(mrg)$ rule.

If we cut the above proof with $\pi_{8}$ , we obtain a proof of $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta.$ Here we gloss over the termination arguments, but the details are available in the proof of Theorem 30.

The above example illustrates one among several proof transformations needed in cut-elimination. These transformations make use of the auxiliary rules in Figure 3. The bulk of the cut-elimination proof consists of showing these rules (height-preserving/hp-) admissible and the rules of $\mathsf{LBIQ}(\mathcal{ID})$ and $\mathsf{LBIQ}(\mathcal{CD})$ height-preserving invertible (i.e., hp-invertible). (NB. We take the notions of (hp-)admissibility and (hp-)invertibility to be defined as usual.) All (hp-)admissible rules preserve the polytree structure of sequents, and with the exception of $(gax)$ , $(cut)$ , and $(cd)$ , all rules in Figure 3 are hp-admissible in both calculi. The $(gax)$ and $(cut)$ rules are strictly admissible in both calculi, while $(cd)$ is hp-admissible in only $\mathsf{LBIQ}(\mathcal{CD})$ as the availability conditions are not imposed on rules, rendering domain atoms unnecessary (see Remark 14). We now discuss some of the most interesting rules of Figure 3.

Let us first explain the rules $(br_{f})$ and $(br_{b})$ . For some labels $w$ , $u$ , and $v$ , assume $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ and $u\normalsize\not\twoheadrightarrow^{*}_{\mathcal{R}}v$ for $\mathcal{R}:=\mathcal{R}^{\prime},{w}R{v}$ . Then, we know that (1) $u$ and $v$ are on two different paths passing through $w$ of the polytree generated from $\mathcal{R}$ , and (2) there is no vertex between $v$ and $w$ since otherwise a cycle would be present in $\mathcal{R}$ . In this scenario, the rule $(br_{f})$ (for branch forward) allows one to move the polytree “rooted” at $v$ forward by connecting it to $u$ instead of $w$ as shown left in the below figure. The rule $(br_{b})$ has a similar functionality; for some labels $w$ , $u$ , and $v$ , assume $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ and $w\normalsize\not\twoheadrightarrow^{*}_{\mathcal{R}}v$ for $\mathcal{R}:=\mathcal{R}^{\prime},{v}R{u}$ . Then, the rule $(br_{b})$ (for branch backward) lets one move the polytree “rooted” at $v$ backward by connecting it to $w$ instead of $u$ as shown right in the below figure.

Figure 4: The left and right diagrams demonstrate the functionality of

(br_{f})

and

(br_{b})

, respectively.

The $(mrg)$ rule merges a label and its direct successor and corresponds to the rules $n o d e m e r g e D$ and $n o d e m e r g e U$ of Pinto and Uustalu [29]. The rule $(id)$ reflects the redundancy of a variable labeled by two labels such that one is reachable by the other. Model-theoretically, this redundancy follows from the fact that if $x$ is interpreted at $w$ , and $u$ is reachable from $w$ (in a model), then $x$ is interpreted at $u$ as well, showing the domain atom $u : x$ superfluous in the premise. Note that when the labels $w$ and $u$ are identical, then the rule represents a contraction on domain atoms; as $w\twoheadrightarrow^{*}_{\mathcal{R}}w$ always holds, we have that identical domain atoms can always be contracted in sequents. The rules $(lwr)$ and $(lft)$ allow us to modify the labels of formulae in a sequent by looking at its underlying polytree. More precisely, reading $(lwr)$ and $(lft)$ bottom-up, if $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ we can both lower the label of $u\!:\!\Pi$ on the right of the sequent to $w$ , and lift the label of $w\!:\!\Sigma$ on the left of the sequent to $u$ .

Lemma 29.

All non-initial rules in $\mathsf{LBIQ}(\mathcal{C})$ are hp-invertible.

Finally, we can prove the admissibility of the $(cut)$ rule. As our proof proceeds via local transformations of proofs, the proof is constructive and yields a cut-elimination algorithm.

Theorem 30 (Cut-elimination).

The $(cut)$ rule is admissible in $\mathsf{LBIQ}(\mathcal{C})$ .

Proof.

We proceed by a primary induction (PIH) on the complexity of the cut formula, and a secondary induction (SIH) on the sum of the heights of the proofs of the premises of $(cut)$ . Assume that we have proofs of the following form, with $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ .

We argue that there is a proof of $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ by a case distinction on $(r_{1})$ and $(r_{2})$ , the last rules applied in the above proofs. We focus on some interesting cases; the remaining cases can be found in the online appended version [26].

$(r_{1})=(ax)$ .

Then $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v_{0}\!:\!p(\vec{t})\vdash\Delta_{0},v_{1}% \!:\!p(\vec{t})$ where $v_{0}\twoheadrightarrow^{*}_{\mathcal{R}}v_{1}$ . If $v_{1}\!:\!p(\vec{t})$ is $w\!:\!\varphi$ , then we have that $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v_{0}\!:\!p(\vec{t}),u\!:\!p(\vec{t})\vdash\Delta$ where $\Gamma=\Gamma_{0},v_{0}\!:\!p(\vec{t})$ . Given that $v_{0}\twoheadrightarrow^{*}_{\mathcal{R}}v_{1}$ and $v_{1}\twoheadrightarrow^{*}_{\mathcal{R}}u$ , we can apply the hp-admissibility of $(lft)$ on the latter to obtain a proof of $\mathcal{R},\mathcal{T},\Gamma_{0},v_{0}\!:\!p(\vec{t}),v_{0}\!:\!p(\vec{t})\vdash\Delta$ . Consequently, we obtain a proof of $\mathcal{R},\mathcal{T},\Gamma_{0},v_{0}\!:\!p(\vec{t})\vdash\Delta$ , i.e. of $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ , using the hp-admissibility of $(ctr_{l})$ . If $v_{1}\!:\!p(\vec{t})$ is not $w\!:\!\varphi$ , then we have that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v_{0}\!:\!p(\vec{t})\vdash\Delta_{0},v_{1}% \!:\!p(\vec{t})$ where $v_{0}\twoheadrightarrow^{*}_{\mathcal{R}}v_{1}$ . The latter is provable by the admissibility of $(gax)$ .

$(r_{1})=(ds)$ .

Then $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!p(\vec{t})\vdash\Delta,w\!:\!\varphi$ and we have a proof of $\mathcal{R},\mathcal{T},v\!:\!VT(\vec{t}),\Gamma_{0},v\!:\!p(\vec{t})\vdash% \Delta,w\!:\!\varphi$ . Consequently, we know that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!p(\vec{t})\vdash\Delta$ . We also have that $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!p(\vec{t}),u\!:\!\varphi\vdash\Delta$ . We can repeatedly apply the hp-admissibility of $(wv)$ on the proof of the latter to obtain a proof of $S:=\mathcal{R},\mathcal{T},v\!:\!VT(\vec{t}),\Gamma_{0},v\!:\!p(\vec{t}),u\!:% \!\varphi\vdash\Delta$ . Then, we proceed as follows:

Note that the instance of SIH is justified because the sum of the heights of the proofs of the premises has decreased.

$(r_{1})=({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure19.pdf}}}\hskip 0.43057pt}}{\mathrm{L}})$ .

Then $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!\psi\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure20.pdf}}}% \hskip 0.43057pt}\chi\vdash\Delta,w\!:\!\varphi$ and we a have proof of $\mathcal{R},{v_{0}}R{v},\mathcal{T},\Gamma_{0},v_{0}\!:\!\psi\vdash\Delta,w\!:% \!\varphi,v_{0}\!:\!\chi$ . Consequently, we know that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!\psi\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure21.pdf}}}% \hskip 0.43057pt}\chi\vdash\Delta$ . We also have that $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma_{0},v\!:\!\psi\mathrel{\hskip 0.43057pt% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure22.pdf}}}% \hskip 0.43057pt}\chi,u\!:\!\varphi\vdash\Delta$ . We apply Lemma 29 on the proof of the latter sequent to obtain a proof of $\mathcal{R},{v_{0}}R{v},\mathcal{T},\Gamma_{0},v_{0}\!:\!\psi,u\!:\!\varphi% \vdash\Delta,v_{0}\!:\!\chi$ , which we call $S$ . Thus, we proceed as shown below. Note that the instance of SIH is justified as the sum of the heights of the proofs of the premises is smaller than that of the original cut.

$(r_{1})=(\exists{\mathrm{R}})$ .

Then there are two cases to consider: in the left premise $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi$ of $(cut)$ , either (1) $w\!:\!\varphi$ is not the principal formula $v\!:\!\exists x\psi$ , or (2) $w\!:\!\varphi$ is the principal formula. In case (1), we have a proof of $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta_{1},v\!:\!\exists x\psi,v\!:\!\psi(% t/x),w\!:\!\varphi$ , which we call $S$ , and $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta_{1},v\!:\!\exists x\psi$ . We proceed as follows.

In case (2), we have proof a of $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,v\!:\!\exists x\psi,v\!:\!\psi(t/x)$ , and $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\varphi\vdash\Delta$ is of the form $\mathcal{R},\mathcal{T},\Gamma,u\!:\!\exists x\psi\vdash\Delta$ . In this case, we need to consider the shape of $(r_{2})$ . If $u\!:\!\exists x\psi$ is not principal in $(r_{2})$ , then we apply the hp-invertibility of $(r_{2})$ (Lemma 29) to the left premise of $(cut)$ and use SIH to cut the result with the premise of $(r_{2})$ , applying $(r_{2})$ afterward to reach our goal. If $u\!:\!\exists x\psi$ is principal in $(r_{2})$ , then the premise of $(r_{2})$ is of the shape $\mathcal{R},\mathcal{T},v\!:\!y,\Gamma,v\!:\!\psi(y/x)\vdash\Delta$ where $y$ is fresh. Then, we proceed as follows where $\pi$ is the first proof given and $x_{0},\dots,x_{n}$ are all the variables appearing in $t$ .

Note that the step involving $(id)$ is justified as $t$ is available for $v$ , meaning for each $x_{i}\in VT(t)$ , there exists a domain atom $u_{i}:x_{i}$ such that $u_{i}\twoheadrightarrow^{*}_{\mathcal{R}}v$ , showing $(id)$ applicable. $\hfill\blacktriangleleft$

5 Concluding Remarks

Our analysis indicates that there may be two interesting and possibly distinct first-order extensions of bi-intuitionistic logic that may be worth exploring. The first is to consider a logic with decreasing domains, i.e., if $w\leq u$ then $D(u)\subseteq D(w)$ in the Kripke model. Semantically, this logic is easy to define, but its proof theory is not at all obvious. We are looking into the possibility of formalizing a notion of “non-existence predicate,” which is dual to the existence predicate, suggested by Restall [34]. This non-existence predicate may play a similar (but dual) role to the existence predicate in $\mathsf{LBIQ}(\mathcal{ID}).$ The other extension is motivated from a proof-theoretic perspective. As mentioned in Remark 19, it seems that one can obtain a subsystem of $\mathsf{LBIQ}(\mathcal{ID})$ without the domain-shift rule $(ds)$ that satisfies cut-elimination. As discussed in Section 3, the $(ds)$ rule is crucial to ensure the completeness of $\mathsf{BIQ}(\mathcal{ID})$ in the presence of the exclusion operator, and so, a natural question to ask is what the semantics of such a logic would look like.

References

[1] Nuel D. Belnap. Display logic. Journal of philosophical logic, 11(4):375–417, 1982. doi:10.1007/BF00284976.
[2] Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, 2009. doi:10.1007/s00153-009-0137-3.
[3] Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85–100, 1992. doi:10.1002/MALQ.19920380107.
[4] Marcos A. Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281–297, 1997. doi:10.3233/FI-1997-323404.
[5] Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1–31, 2021. doi:10.1145/3460492.
[6] Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu. Annotation-free sequent calculi for full intuitionistic linear logic - extended version. CoRR, abs/1307.0289, 2013. arXiv:1307.0289.
[7] 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.
[8] Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237–247, 1972. doi:10.1305/NDJFL/1093894722.
[9] Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41–61, 2014. doi:10.1215/00294527-2377869.
[10] D. Gabbay, V. Shehtman, and D. Skvortsov. Quantification in Non-classical Logics. Studies in Logic and Foundations of Mathematics. Elsevier, Amsterdam, London, 2009.
[11] Gerhard Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39(1):176–210, 1935.
[12] Gerhard Gentzen. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift, 39(1):405–431, 1935.
[13] Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43–66, Nancy, France, 2008. College Publications. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
[14] Rajeev Goré, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science, 7(2):1–38, 2011. doi:10.2168/LMCS-7(2:8)2011.
[15] Rajeev Goré and Ian Shillito. Bi-intuitionistic logics: A new instance of an old problem. In Advances in Modal Logic 13, pages 269–288, Helsinki, Finland, 2020. College Publications. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.
[16] Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26(5):596–601, 1964.
[17] Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149–164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73099-6_13.
[18] Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119–135, 1994. doi:10.1007/BF01053026.
[19] Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213–265, December 2020. doi:10.1093/logcom/exaa078.
[20] Tim Lyon. Refining Labelled Systems for Modal and Constructive Logics with Applications. PhD thesis, Technische Universität Wien, 2021.
[21] Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, volume 152 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CSL.2020.28.
[22] Tim S. Lyon. Nested sequents for intermediate logics: the case of Gödel-Dummett logics. Journal of Applied Non-Classical Logics, 33(2):121–164, 2023. doi:10.1080/11663081.2023.2233346.
[23] Tim S. Lyon. Nested sequents for intermediate logics: The case of Gödel-Dummett logics, 2024. Updated version, on arXiv. URL: https://arxiv.org/abs/2306.07550, doi:10.48550/arXiv.2306.07550.
[24] Tim S. Lyon and Lucía Gómez Álvarez. Automating reasoning with standpoint logic via nested sequents. In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pages 257–266, August 2022. doi:10.24963/kr.2022/26.
[25] Tim S. Lyon and Jonas Karge. Constructive interpolation and concept-based beth definability for description logics via sequents. In Kate Larson, editor, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 3484–3492. International Joint Conferences on Artificial Intelligence Organization, August 2024. Main Track. URL: https://www.ijcai.org/proceedings/2024/386, doi:10.24963/ijcai.2024/386.
[26] Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking bi-intuitionistic logic first-order: A proof-theoretic investigation via polytree sequents, 2024. Appended version on arXiv. URL: https://arxiv.org/abs/2404.15855, doi:10.48550/arXiv.2404.15855.
[27] E. G. K. López-Escobar. On the interpolation theorem for the logic of constant domains. Journal of Symbolic Logic, 46(1):87–88, 1981. doi:10.2307/2273260.
[28] Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5-6):507, 2005.
[29] Luís Pinto and Tarmo Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In Steffen van Bakel, Stefano Berardi, and Ulrich Berger, editors, Proceedings Third International Workshop on Classical Logic and Computation, volume 47 of EPTCS, pages 57–72, 2010. doi:10.4204/EPTCS.47.7.
[30] Luís Pinto and Tarmo Uustalu. A proof-theoretic study of bi-intuitionistic propositional sequent calculus. Journal of Logic and Computation, 28(1):165–202, 2018. doi:10.1093/LOGCOM/EXX044.
[31] Linda Postniece. Deep inference in bi-intuitionistic logic. In Hiroakira Ono, Makoto Kanazawa, and Ruy de Queiroz, editors, Logic, Language, Information and Computation, pages 320–334, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-02261-6_26.
[32] Cecylia Rauszer. Applications of Kripke models to Heyting-Brouwer logic. Studia Logica, 36(1):61–71, 1977. doi:10.1007/BF02121115.
[33] Cecylia Rauszer. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, dissertations mathematicae, 1980.
[34] Greg Restall. Constant domain quantified modal logics without boolean negation. Australasian Journal of Logic, 3:45–62, 2005. doi:10.26686/ajl.v3i0.1772.
[35] Dana Scott. Identity and existence in intuitionistic logic. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, pages 660–696. Springer, 2006.
[36] Ian Shillito. New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq. PhD thesis, Australian National University, Canberra, 2023.
[37] Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.
[38] John G. Stell, Renate A. Schmidt, and David Rydeheard. A bi-intuitionistic modal logic: Foundations and automation. Journal of Logical and Algebraic Methods in Programming, 85(4):500–519, 2016. Relational and algebraic methods in computer science. doi:10.1016/j.jlamp.2015.11.003.
[39] Gaisi Takeuti. Proof theory, volume 81. Courier Corporation, 2013.
[40] Alwen Tiu, Egor Ianovski, and Rajeev Goré. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 516–537. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.
[41] Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000.

Appendix A Soundness

Theorem 20 (Soundness).

Let $S$ be a sequent. If $S$ is provable in $\mathsf{LBIQ}(\mathcal{ID})$ ( $\mathsf{LBIQ}(\mathcal{CD})$ ), then $S$ is ( $\mathrm{CD}$ -)valid.

Proof.

We argue the claim by induction on the height of the given derivation and consider the $\mathsf{LBIQ}(\mathcal{ID})$ case as the $\mathsf{LBIQ}(\mathcal{CD})$ case is similar.

Base case.

It is straightforward to show that any instance of $(\bot{\mathrm{L}})$ or $(\top{\mathrm{R}})$ is valid; hence, we focus on $(ax)$ and show that any instance thereof is valid. Let us consider the following instance of $(ax)$ , where $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ due to the side condition imposed on $(ax)$ , that is, there exist $v_{1},\ldots,v_{n}\in\mathrm{Lab}(\mathcal{R})$ such that $wRv_{1},\ldots,v_{n}Ru\in\mathcal{R}$ .

Let us suppose $\mathcal{R},\mathcal{T},\Gamma,w\!:\!p(\vec{t})\vdash\Delta,u\!:\!p(\vec{t})$ is invalid, i.e., a model $M=(W,\leq,U,D,I_{1},I_{2})$ , $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ exist such that the following hold: $\iota(w)\leq\iota(v_{1}),\ldots,\iota(v_{n})\leq\iota(u)$ , $M,\iota(w),\alpha\Vdash p(\vec{t})$ , and $M,\iota(u),\alpha\not\Vdash p(\vec{t})$ . By the monotonicity condition $\mathrm{(M)}$ (see Definition 3), it must be that $M,\iota(u),\alpha\Vdash p(\vec{t})$ , giving a contradiction. Thus, every instance of $(ax)$ must be valid.

Inductive step.

We prove the inductive step by contraposition, showing that if the conclusion of the last inference in the given proof is invalid, then at least one premise of the final inference must be invalid. We make a case distinction based on the last rule applied in the given derivation.

$(ds)$ .: Suppose $\mathcal{R},\mathcal{T},\Gamma,w\!:\!p(\vec{t})\vdash\Delta$ is invalid with $\vec{t}=t_{1},\ldots,t_{n}$ . Then, there exists a model $M$ , $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\Vdash p(\vec{t})$ . Therefore, $(\overline{\alpha}(t_{1}),\ldots,\overline{\alpha}(t_{n}))\in I_{2}(w,p)$ , and since $I_{2}(w,p)\subseteq D(w)^{n}$ , we have that $\overline{\alpha}(t_{i})\in D(\iota(w))$ for $1\leq i\leq n$ . By the $\mathrm{(C_{1})}$ and $\mathrm{(C_{2})}$ conditions, we know that $M,\iota,\alpha\models w\!:\!VT(\vec{t})$ . Therefore, $\mathcal{R},\mathcal{T},w\!:\!VT(\vec{t}),\Gamma,w\!:\!p(\vec{t})\vdash\Delta$ is invalid as well.
$(\land{\mathrm{L}})$ .: If we assume that $\mathcal{R},\mathcal{T},\Gamma,w\!:\!\varphi\land\psi\vdash\Delta$ is invalid, then there exists a model $M$ , $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\Vdash\varphi\land\psi$ , implying that $M,\iota(w),\alpha\Vdash\varphi$ and $M,\iota(w),\alpha\Vdash\psi$ , showing that the premise $\mathcal{R},\mathcal{T},\Gamma,w\!:\!\varphi,w\!:\!\psi\vdash\Delta$ is invalid as well.
$(\land{\mathrm{R}})$ .: Let us suppose that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi\land\psi$ is invalid. Then, there exists an model $M$ , $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\not\Vdash\varphi\land\psi$ . Hence, either $M,\iota(w),\alpha\not\Vdash\varphi$ or $M,\iota(w),\alpha\not\Vdash\psi$ . In the first case, the left premise of $(\land{\mathrm{R}})$ is invalid, and in the second case, the right premise of $(\land{\mathrm{R}})$ is invalid.
$(\lor{\mathrm{L}})$ .: Similar to the $(\land{\mathrm{R}})$ case.
$(\lor{\mathrm{R}})$ .: Similar to the $(\land{\mathrm{L}})$ case.
$({\rightarrow}{\mathrm{L}})$ .: Assume $\mathcal{R},\mathcal{T},\Gamma,w\!:\!\varphi\rightarrow\psi\vdash\Delta$ is invalid and $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ , i.e. a sequence $wRv_{1},\ldots,v_{n}Ru$ of relational atoms exist in $\mathcal{R}$ . By our assumption, there exists a model $M$ , $M$ -interpretation $\iota$ , and $M$ -assignment such that $\iota(w)\leq\iota(v_{1}),\ldots,\iota(v_{n})\leq\iota(u)$ and $M,\iota(w),\alpha\Vdash\varphi\rightarrow\psi$ . Because $M,\iota(w),\alpha\Vdash\varphi\rightarrow\psi$ and $\leq$ is transitive, we know that either $M,\iota(u),\alpha\not\Vdash\varphi$ or $M,\iota(u),\alpha\Vdash\psi$ . In the first case, the left premise of $({\rightarrow}{\mathrm{L}})$ is invalid, and in the second case, the right premise of $({\rightarrow}{\mathrm{L}})$ is invalid.
$({\rightarrow}{\mathrm{R}})$ .: Assume that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\varphi\rightarrow\psi$ is invalid. Then, there exists a model $M$ , an $M$ -interpretation $\iota$ , and an $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\not\Vdash\varphi\rightarrow\psi$ . Hence, there exists a world $u$ such that $\iota(w)\leq u$ , $M,u,\alpha\Vdash\varphi$ , and $M,u,\alpha\not\Vdash\psi$ . Let $\iota^{\prime}(v)=\iota(v)$ for all labels $v\neq u$ and $\iota^{\prime}(u)=u$ otherwise. Then, $M$ , $\iota^{\prime}$ , and $\alpha$ falsify the premise of $({\rightarrow}{\mathrm{R}})$ , showing it invalid.
$({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure23% .pdf}}}\hskip 0.43057pt}}{\mathrm{L}})$ .: Similar to the $({\rightarrow}{\mathrm{R}})$ case above.
$({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon.latexml-figure25% .pdf}}}\hskip 0.43057pt}}{\mathrm{R}})$ .: Similar to the $({\rightarrow}{\mathrm{L}})$ case above.
$(\exists{\mathrm{L}})$ .: Suppose that $S=\mathcal{R},\mathcal{T},\Gamma,w\!:\!\exists x\varphi\vdash\Delta$ is invalid. Then, there exists a model $M$ , an $M$ -interpretation $\iota$ , and an $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\Vdash\exists x\varphi$ . Therefore, there exists an $a\in D(\iota(w))$ such that $M,\iota(w),\alpha[a/y]\Vdash\varphi(y/x)$ with $y$ not occurring in $S$ . Then, as $y$ is fresh, $M$ , $\iota$ , and $\alpha[a/y]$ falsify the premise of $(\exists{\mathrm{L}})$ , showing it invalid.
$(\exists{\mathrm{R}})$ .: Suppose that $S=\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\exists x\varphi$ is invalid. Then, there exists a model $M$ , and $M$ -interpretation $\iota$ , and $M$ -assignment such that $M,\iota(w),\alpha\not\Vdash\exists x\varphi$ . By the side condition on $(\exists{\mathrm{R}})$ , we know that $\mathsf{A}(t,X_{w},\mathcal{R},\mathcal{T})$ , meaning there exist labels $u_{1},\ldots,u_{n}\in\mathrm{Lab}(S)$ such that $u_{1}:x_{1},\ldots,u_{n}:x_{n}\in\mathcal{T}$ , $VT(t)=\{x_{1},\ldots,x_{n}\}$ , and $u_{1}\twoheadrightarrow^{*}_{\mathcal{R}}w,\ldots,u_{n}\twoheadrightarrow^{*}_% {\mathcal{R}}w$ . It follows that $\iota(u_{1})\leq\iota(w),\ldots,\iota(u_{n})\leq\iota(w)$ and $\overline{\alpha}(x_{1})\in D(\iota(u_{1})),\ldots,\overline{\alpha}(x_{n})\in D% (\iota(u_{n}))$ . By the increasing domain condition $\mathrm{(ID)}$ , we have that $\overline{\alpha}(x_{1})\in D(\iota(w)),\ldots,\overline{\alpha}(x_{n})\in D(% \iota(w))$ . Therefore, by the $\mathrm{(C_{1})}$ and $\mathrm{(C_{2})}$ conditions, we know that $\overline{\alpha}(t)\in D(\iota(w))$ , showing that $M,\iota(w),\alpha\not\Vdash\varphi(t/x)$ , and thus, the premise is invalid.
$(\forall{\mathrm{L}})$ .: Suppose that $S=\mathcal{R},\mathcal{T},\Gamma,w\!:\!\forall x\varphi\vdash\Delta$ is invalid. Then, there exists a model $M$ , and $M$ -interpretation $\iota$ , and $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\Vdash\forall x\varphi$ . By the side condition on $(\forall{\mathrm{L}})$ , we know that $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ and $\mathsf{A}(t,X_{w},\mathcal{R},\mathcal{T})$ . By the latter fact, there exist labels $v_{1},\ldots,v_{n}\in\mathrm{Lab}(S)$ such that $v_{1}:x_{1},\ldots,v_{n}:x_{n}\in\mathcal{T}$ , $VT(t)=\{x_{1},\ldots,x_{n}\}$ , and $v_{1}\twoheadrightarrow^{*}_{\mathcal{R}}w,\ldots,v_{n}\twoheadrightarrow^{*}_% {\mathcal{R}}w$ . It follows that $\iota(v_{1})\leq\iota(w),\ldots,\iota(v_{n})\leq\iota(w)$ and $\overline{\alpha}(x_{1})\in D(\iota(v_{1})),\ldots,\overline{\alpha}(x_{n})\in D% (\iota(v_{n}))$ . By the increasing domain condition $\mathrm{(ID)}$ , we have that $\overline{\alpha}(x_{1})\in D(\iota(w)),\ldots,\overline{\alpha}(x_{n})\in D(% \iota(w))$ . Therefore, by the $\mathrm{(C_{1})}$ and $\mathrm{(C_{2})}$ conditions and our assumption, we know that $\overline{\alpha}(t)\in D(\iota(w))$ , showing that $M,\iota(w),\alpha\Vdash\varphi(t/x)$ . By the fact that $w\twoheadrightarrow^{*}_{\mathcal{R}}u$ , we know $\iota(w)\leq\iota(u)$ and $\overline{\alpha}(t)\in D(\iota(u))$ , showing that $M,\iota(u),\alpha\Vdash\varphi(t/x)$ by Proposition 6. Thus, the premise is invalid.
$(\forall{\mathrm{R}})$ .: Let us assume that $\mathcal{R},\mathcal{T},\Gamma\vdash\Delta,w\!:\!\forall x\varphi$ is invalid. Then, there exists a model $M$ , an $M$ -interpretation $\iota$ , and an $M$ -assignment $\alpha$ such that $M,\iota(w),\alpha\not\Vdash\forall x\varphi$ . Thus, there exists a world $u\in W$ such that $\iota(w)\leq u$ , $a\in D(u)$ , and $M,u,\alpha[a/y]\not\Vdash\varphi(y/x)$ . We define $\iota^{\prime}(v)=\iota(v)$ if $v\neq u$ and $\iota^{\prime}(u)=u$ . Then, $M$ , $\iota^{\prime}$ , and $\alpha[a/y]$ falsify the premise $\mathcal{R},w\leq u,\mathcal{T},u\!:\!y,\Gamma\vdash\Delta,u\!:\!\varphi(y/x)$ , showing it invalid.

$\hfill\blacktriangleleft$

[bib.bib1] [1] Nuel D. Belnap. Display logic. Journal of philosophical logic, 11(4):375–417, 1982. doi:10.1007/BF00284976.

[bib.bib2] [2] Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, 2009. doi:10.1007/s00153-009-0137-3.

[bib.bib3] [3] Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85–100, 1992. doi:10.1002/MALQ.19920380107.

[bib.bib4] [4] Marcos A. Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281–297, 1997. doi:10.3233/FI-1997-323404.

[bib.bib5] [5] Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1–31, 2021. doi:10.1145/3460492.

[bib.bib6] [6] Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu. Annotation-free sequent calculi for full intuitionistic linear logic - extended version. CoRR, abs/1307.0289, 2013. arXiv:1307.0289.

[bib.bib7] [7] 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.bib8] [8] Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237–247, 1972. doi:10.1305/NDJFL/1093894722.

[bib.bib9] [9] Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41–61, 2014. doi:10.1215/00294527-2377869.

[bib.bib10] [10] D. Gabbay, V. Shehtman, and D. Skvortsov. Quantification in Non-classical Logics. Studies in Logic and Foundations of Mathematics. Elsevier, Amsterdam, London, 2009.

[bib.bib11] [11] Gerhard Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39(1):176–210, 1935.

[bib.bib12] [12] Gerhard Gentzen. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift, 39(1):405–431, 1935.

[bib.bib13] [13] Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43–66, Nancy, France, 2008. College Publications. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.

[bib.bib14] [14] Rajeev Goré, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science, 7(2):1–38, 2011. doi:10.2168/LMCS-7(2:8)2011.

[bib.bib15] [15] Rajeev Goré and Ian Shillito. Bi-intuitionistic logics: A new instance of an old problem. In Advances in Modal Logic 13, pages 269–288, Helsinki, Finland, 2020. College Publications. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.

[bib.bib16] [16] Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26(5):596–601, 1964.

[bib.bib17] [17] Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149–164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73099-6_13.

[bib.bib18] [18] Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119–135, 1994. doi:10.1007/BF01053026.

[bib.bib19] [19] Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213–265, December 2020. doi:10.1093/logcom/exaa078.

[bib.bib20] [20] Tim Lyon. Refining Labelled Systems for Modal and Constructive Logics with Applications. PhD thesis, Technische Universität Wien, 2021.

[bib.bib21] [21] Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, volume 152 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CSL.2020.28.

[bib.bib22] [22] Tim S. Lyon. Nested sequents for intermediate logics: the case of Gödel-Dummett logics. Journal of Applied Non-Classical Logics, 33(2):121–164, 2023. doi:10.1080/11663081.2023.2233346.

[bib.bib23] [23] Tim S. Lyon. Nested sequents for intermediate logics: The case of Gödel-Dummett logics, 2024. Updated version, on arXiv. URL: https://arxiv.org/abs/2306.07550, doi:10.48550/arXiv.2306.07550.

[bib.bib24] [24] Tim S. Lyon and Lucía Gómez Álvarez. Automating reasoning with standpoint logic via nested sequents. In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pages 257–266, August 2022. doi:10.24963/kr.2022/26.

[bib.bib25] [25] Tim S. Lyon and Jonas Karge. Constructive interpolation and concept-based beth definability for description logics via sequents. In Kate Larson, editor, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 3484–3492. International Joint Conferences on Artificial Intelligence Organization, August 2024. Main Track. URL: https://www.ijcai.org/proceedings/2024/386, doi:10.24963/ijcai.2024/386.

[bib.bib26] [26] Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking bi-intuitionistic logic first-order: A proof-theoretic investigation via polytree sequents, 2024. Appended version on arXiv. URL: https://arxiv.org/abs/2404.15855, doi:10.48550/arXiv.2404.15855.

[bib.bib27] [27] E. G. K. López-Escobar. On the interpolation theorem for the logic of constant domains. Journal of Symbolic Logic, 46(1):87–88, 1981. doi:10.2307/2273260.

[bib.bib28] [28] Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5-6):507, 2005.

[bib.bib29] [29] Luís Pinto and Tarmo Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In Steffen van Bakel, Stefano Berardi, and Ulrich Berger, editors, Proceedings Third International Workshop on Classical Logic and Computation, volume 47 of EPTCS, pages 57–72, 2010. doi:10.4204/EPTCS.47.7.

[bib.bib30] [30] Luís Pinto and Tarmo Uustalu. A proof-theoretic study of bi-intuitionistic propositional sequent calculus. Journal of Logic and Computation, 28(1):165–202, 2018. doi:10.1093/LOGCOM/EXX044.

[bib.bib31] [31] Linda Postniece. Deep inference in bi-intuitionistic logic. In Hiroakira Ono, Makoto Kanazawa, and Ruy de Queiroz, editors, Logic, Language, Information and Computation, pages 320–334, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-02261-6_26.

[bib.bib32] [32] Cecylia Rauszer. Applications of Kripke models to Heyting-Brouwer logic. Studia Logica, 36(1):61–71, 1977. doi:10.1007/BF02121115.

[bib.bib33] [33] Cecylia Rauszer. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, dissertations mathematicae, 1980.

[bib.bib34] [34] Greg Restall. Constant domain quantified modal logics without boolean negation. Australasian Journal of Logic, 3:45–62, 2005. doi:10.26686/ajl.v3i0.1772.

[bib.bib35] [35] Dana Scott. Identity and existence in intuitionistic logic. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, pages 660–696. Springer, 2006.

[bib.bib36] [36] 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.bib37] [37] Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.

[bib.bib38] [38] John G. Stell, Renate A. Schmidt, and David Rydeheard. A bi-intuitionistic modal logic: Foundations and automation. Journal of Logical and Algebraic Methods in Programming, 85(4):500–519, 2016. Relational and algebraic methods in computer science. doi:10.1016/j.jlamp.2015.11.003.

[bib.bib39] [39] Gaisi Takeuti. Proof theory, volume 81. Courier Corporation, 2013.

[bib.bib40] [40] Alwen Tiu, Egor Ianovski, and Rajeev Goré. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 516–537. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.

[bib.bib41] [41] Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000.

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Outline of Paper.

2 Logical Preliminaries

Definition 1 (The Language ℒ).

Definition 2 (ID-Frame).

Definition 3 (ID-Model).

Definition 4 (M-assignment).

Definition 5 (Semantics).

Proposition 6.

▶ Remark 7.

Example 8.

3 Polytree Sequent Systems

Definition 9 (Polytree Sequent).

▶ Remark 10.

3.1 Semantics and Proof Systems

Definition 11 (Sequent Semantics).

Definition 12 (↠ℛ+, ↠ℛ∗).

Definition 13 (Available).

3.2 Reachability Rules

▶ Remark 14.

Example 15.

▶ Remark 16.

Example 17 (An Intuitionistic Formula Valid in Constant Domain Models).

Example 18 (Non-Provability of the Quantifier Shift Axiom in the Increasing Domain Setting).

3.3 The Domain Shift Rule (𝒅⁢𝒔)

▶ Remark 19.

3.4 Soundness and Completeness

Theorem 20 (Soundness).

Proof.

Lemma 21.

Theorem 22 (Completeness).

Proof (Outline).

𝙿𝚛𝚘𝚟𝚎.

(𝒂⁢𝒙), (⊥𝐋), and (⊤𝐑).

(𝒅⁢𝒔).

(∃𝐋).

(∃𝐑).

▶ Remark 23.

3.5 Intuitionistic Subsystems

Corollary 24 (Conservativity).

Definition 25.

Lemma 26 (Separation).

Proof (Outline).

Definition 27.

Proposition 28.

Proof (Outline).

4 Cut-Elimination

Lemma 29.

Theorem 30 (Cut-elimination).

Proof.

(𝒓𝟏)=(𝒂⁢𝒙).

(𝒓𝟏)=(𝒅⁢𝒔).

(𝒓𝟏)=(𝐋).

(𝒓𝟏)=(∃𝐑).

5 Concluding Remarks

References

Appendix A Soundness

Theorem 20 (Soundness).

Proof.

Base case.

Inductive step.

Taking Bi-Intuitionistic Logic First-Order:
A Proof-Theoretic Investigation via Polytree Sequents

Definition 1 (The Language $\mathcal{L}$ ).

Definition 2 ( $\mathrm{ID}$ -Frame).

Definition 3 ( $\mathrm{ID}$ -Model).

Definition 4 ( $M$ -assignment).

$\blacktriangleright$ Remark 7.

$\blacktriangleright$ Remark 10.

Definition 12 ( $\twoheadrightarrow^{+}_{\mathcal{R}}$ , $\twoheadrightarrow^{*}_{\mathcal{R}}$ ).

$\blacktriangleright$ Remark 14.

$\blacktriangleright$ Remark 16.

3.3 The Domain Shift Rule $(ds)$

$\blacktriangleright$ Remark 19.

$\mathtt{Prove}$ .

$(ax)$ , $(\bot{\mathrm{L}})$ , and $(\top{\mathrm{R}})$ .

$(ds)$ .

$(\exists{\mathrm{L}})$ .

$(\exists{\mathrm{R}})$ .

$\blacktriangleright$ Remark 23.

$(r_{1})=(ax)$ .

$(r_{1})=(ds)$ .

$(r_{1})=({\mathrel{\hskip 0.43057pt\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p041-Lyon% .latexml-figure19.pdf}}}\hskip 0.43057pt}}{\mathrm{L}})$ .

$(r_{1})=(\exists{\mathrm{R}})$ .