Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
Tim S. Lyon Ian Shillito Alwen Tiu





 















  Technische Universität Dresden
  
  Dresden
  Germany
timothy_stephen.lyon@tu-dresden.de
0000-0003-3214-0828




ian.shillito@anu.edu.au
0009-0009-1529-2679


alwen.tiu@anu.edu.au

  Australian National University

  Canberra

  Australia

















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 in the model into a constant domain. This makes it a very challenging 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 in a labeled 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, that may help explain the difficulty in obtaining a complete proof system for first-order bi-intuitionistic logic. 














<ccs2012>
<concept>
<concept_id>10003752.10003790.10003792</concept_id>
<concept_desc>Theory of computation Proof theory</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10003793</concept_id>
<concept_desc>Theory of computation Modal and temporal logics</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10003796</concept_id>
<concept_desc>Theory of computation Constructive mathematics</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10003794</concept_id>
<concept_desc>Theory of computation Automated reasoning</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>


[500]Theory of computation Proof theory
[500]Theory of computation Modal and temporal logics
[500]Theory of computation Constructive mathematics
[500]Theory of computation Automated reasoning










20 February 2007
[revised]12 March 2009
[accepted]5 June 2009




Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
    Alwen Tiu
    December 4, 2023
=================================================================================================






§ INTRODUCTION










Propositional bi-intuitionistic logic (), also referred to as Heyting-Brouwer logic <cit.>, is a conservative extension of propositional intuitionistic logic (), obtained by adding the binary connective  (referred to as exclusion)[

Also referred to as pseudo-difference <cit.>,  subtraction, and co-implication <cit.>.
] 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 <cit.> and where modal extensions have found import in image processing <cit.>. While in intuitionistic logic the connectives  and  form a residuated pair, i.e. (ϕψ) χ is valid ϕ (ψχ) is valid ψ (ϕχ) is valid, in bi-intuitionistic logic the connectives  and  also form a residuated pair, i.e. ϕ (ψχ) is valid (ϕψ) χ is valid (ϕχ) ψ is valid.[However, they are not logically equivalent, e.g., [ϕ (ψχ)]  [(ϕψ) χ] is not valid.

] To put it succinctly,  is a bi-intuitionistic extension of  that is (1) conservative and (2) has the residuation property, i.e. (, ) and (, ) form residuated pairs. 


When extending first-order intuitionistic logic () to its bi-

intuitionistic counterpart, a `natural' axiomatization seems to be one obtained by adding the universal axioms (Ax1) ∀ xφ→φ(t/x), (Ax2) ∀ x(ψ→φ)→(ψ→∀ xφ) (where x is not free in ψ), and the rule (Gen) φ / ∀ xφ to the axioms of . This extension, which we refer to as the logic , turns out not to be conservative over first-order intuitionistic logic , as it allows one to prove the  the quantifier shift axiom ∀ x (ϕψ) ∀ x ϕψ (where x is not free in ψ), 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 δ:=∀ x ((∀ x (ϕψ) ψ) ϕ)  ((∀ x (ϕψ) ψ) ∀ x ϕ).  




Ax1
∀ x (ϕψ)  (ϕψ)
Res
(∀ x (ϕψ) ψ) ϕ
Gen
∀ x((∀ x (ϕψ) ψ) ϕ)

Ax2
δ
MP
(∀ x (ϕψ) ψ) ∀ x ϕ
Res
∀ x (ϕψ) ∀ x ϕψ



It is well-known that the quantifier shift axiom characterizes the class of first-order intuitionistic Kripke models with constant domains <cit.>, thus forcing the models for  to satisfy this constraint. Indeed, various works in the literature (e.g., <cit.>) have shown that completeness for  requires the domain to be constant. These works and the above example strongly suggest that it might not be possible to have a sound and complete 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 have been no prior successful attempts 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 . With some minor modifications, the proof system for  can be converted into a proof system for .

 A key insight in avoiding the collapse of domains in  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 <cit.>. 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  ∀ x ( E(x) ϕ(x)), the quantifier shift axiom can be rewritten as: 
∀ x (E(x)  (φψ))   (∀ x (E(x) φ) ψ).

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:



E(x)  [∀ x( E(x)  (ϕψ)]  (ϕψ)
Res
E(x)  [ (∀ x( E(x)  (ϕψ)) ψ] ϕ
Gen
∀ x(E(x)  [∀ x( E(x)  (ϕψ)) ψ] ϕ)
⋯
MP
[∀ x(E(x)  (ϕψ)) ψ] ∀ x(E(x) ϕ)
Res
∀ x(E(x)  (ϕψ))  (∀ x ( E(x)ϕ) ψ)



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 , E(x) is equivalent to ⊤ (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 .
This is not the case, however, in the logic of increasing domains , 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), like the one we have seen earlier, 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 .

One issue with 
the existence predicate is that it is not clear how it should interact with the exclusion operator. Semantically, a formula such as 
∀ x [E(x)  ((p(x) ∃ y (E(y)  p(y))) )]
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 as it turned out, it was not obvious at all how a proof system that admits this tautology, that does not also degenerate into a logic with constant domains, should be designed. We shall come back to this example later in Section <ref>.  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 formulas.





The proof systems for  and  are both formalized using labeled polytree sequents <cit.>, which are connected binary graphs whose vertices are traditional Gentzen sequents and which are free of (un)directed cycles. Labeled polytree sequents are a restriction of traditional labeled sequents <cit.> and are notational variants of nested sequents <cit.>. (NB. For details on the relationship between labeled polytree and nested sequents, see <cit.>.) Nested sequents were introduced independently by Bull <cit.> and Kashima <cit.> and employ trees of Gentzen sequents in proofs. Both labeled polytree sequents and nested sequents allow for simple formulations of proof systems for various non-classical logics and for important proof theoretical properties, such as cut-elimination, subformula properties, and have found a range of applications, being used in knowledge integration algorithms <cit.>, serving as a basis for constructive interpolation and decidability techniques <cit.>, and even being used to solve open questions about axiomatizability <cit.>. We make use of labeled 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 proofs or proofs in a Hilbert system.



The calculi 
for  and  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 labeled 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. 




A Note on Notation. In this paper, we write our nested sequents in the notation of labeled sequents (cf. <cit.>) to minimize the bureaucracy of our proof systems. This is based on the key insight that nested sequents have a canonical representation as labeled polytree sequents, that is to say, sets of equivalent, but syntactically distinct, nested sequents can be represented as a unique labeled polytree sequent. (NB. A labeled polytree sequent is a connected, directed graph of Gentzen sequents that is free of (un)directed cycles, i.e. if one ignores the orientation of the edges, then the graph is a tree.) To demonstrate what we mean, let us consider the following two nested sequents in the notation of <cit.>.


X = C  D, ∘{A  B, ∙{G  F}}    
Y = A  B, ∙{C  D}, ∙{G  F}




Graphically, each nested sequent can be represented as a tree with two types of edges ∘→ and ∙→. For example, X can be represented as the tree shown below left, while Y can be represented as the tree shown below middle. Alternatively, both nested sequents can be represented as the single polytree shown below right with a single type of edge → and where the orientation of the edge encodes the two types of structures ∘{} and ∙{} (observe that each ∘-edge is portrayed as a forward edge and each ∙-edge has been reversed). This polytree can be written as the labeled polytree sequent uRw, vRw, w : A, u : C, v : G  w : B, u : D, v : F.







[] (w2) [] A  B;
[] (w3) [above left=of w2,yshift=-.5cm,xshift=1.25cm] C  D;
[] (w4) [above right=of w2,yshift=-.5cm,xshift=-1.25cm] G  F;

[->,draw] (w3) – (w2) node [midway,left] ;
[->,draw] (w4) – (w2) node [midway,right] ;


[] (w5) [left=of w2,xshift=-.75cm] A  B;
[] (w6) [above left=of w5,yshift=-.5cm,xshift=1.25cm] C  D;
[] (w7) [above right=of w5,yshift=-.5cm,xshift=-1.25cm] G  F;

[->,draw] (w5) – (w6) node [midway,left] ∙;
[->,draw] (w5) – (w7) node [midway,right] ∙;

[] (w8) [left=of w5,xshift=-.75cm] A  B;
[] (w9) [above left=of w8,yshift=-.5cm,xshift=1.25cm] C  D;
[] (w10) [above right=of w8,yshift=-.5cm,xshift=-1.25cm] G  F;

[->,draw] (w9) – (w8) node [midway,left] ∘;
[->,draw] (w8) – (w10) node [midway,right] ∙;












 
We stress that our labeled notation to represent nested sequents is just a matter of presentation: originally, we had developed our proof systems in the nested notation of <cit.>, but the additional bureaucracy made our nested systems significantly more complicated without yielding any additional benefits. 

Nevertheless, we make use of nested sequents in our work as such objects admit a formula interpretation (at least in the intuitionistic case), which can be leveraged for direct translations of nested sequent proofs into sequent calculus proofs or proofs in a Hilbert system. 



Outline of Paper. 
 In  <ref>, we define a semantics for first-order bi-intuitionistic with increasing domains  and constant domains . In the subsequent section ( <ref>), we define our labeled polytree sequent calculi showing them sound and complete relative to the provided semantics. In  <ref>, we establish height-prserving admissibility and invertibility results as well as prove a non-trivial syntactic cut-elimination theorem. We conclude and discuss future work in  <ref>. Due to space constraints, we defer most proofs to the appendix.






§ LOGICAL PRELIMINARIES



In this section, we introduce the language, models, and semantics for first-order bi-intuitionistic logic with increasing domains, dubbed , and with constant domains, dubbed .

Let := {x, y, z, …} be a countably infinite set of variables and = {f, g, h, …} be a countably infinite set of function symbols containing denumerably many function symbols of each arity n ∈ℕ. We let f = n denote that the arity of the function symbol f is n and let a, b, c, … denote constants, which are function symbols of arity 0. For a set X ⊆, we define the set (X) of X-terms to be the smallest set satisfying the following two constraints: (1) X ⊆(X), and (2) if f ∈, f is of arity n, and t_1, …, t_n∈(X), then f(t_1, …, t_n) ∈(X). The complete set of terms  is defined to be (). We use t, s, … (potentially annotated) to denote (X-)terms and let t denote the set of variables occurring in the term t. We will often write a list t_1, …, t_n of terms as t⃗, and define t⃗ = t_1∪⋯∪t_n.
 
We let := {p, q, …} be a countably infinite set of predicates containing denumerably many predicates of each arity n ∈ℕ. We denote the arity of a predicate p as p and refer to predicates of arity 0 as propositional atoms. An atomic formula is a formula of the form p(t_1, …, t_n), obtained by prefixing a predicate p of arity p = n to a tuple of terms of length n. We will often write atomic formulae p(t_1, …, t_n) as p(t⃗). Our language is defined accordingly:

  The language  is defined to be the set of formulae generated via the following grammar in BNF: 

    ϕ ::= p(t⃗)  |   |  ⊤ |  (ϕ∘ϕ) 
     |  (∃ x ϕ)  |  (∀ x ϕ)

where ∘∈{, , , }, p ranges over , the terms t⃗ = t_1, …, t_n range over , and x ranges over the set . We use ϕ, ψ, χ, … to denote formulae. 


The occurrence of a variable x in ϕ is defined to be free given that x does not occur within the scope of a quantifier. We let ϕ denote the set of all free variables occurring in the formula ϕ and use ϕ(x_1, …, x_n) to denote that ϕ = {x_1, …, x_n}. We let ϕt/x denote the formula obtained by replacing each free occurrence of the variable x in ϕ by t, potentially renaming bound variables to avoid unwanted variable capture; e.g. (∀ y p(x,y))y/x = ∀ z p(y,z). The complexity of a formula ϕ, written |ϕ|, is recursively defined as follows: (1) |p(t_1, …, t_n)| = || = |⊤| := 0, (2) |Q x ϕ| := |ϕ| + 1 for Q ∈{∀, ∃}, and (3) |ϕ∘ψ| := |ϕ| + |ψ| + 1 for ∘∈{, , , }.
 
Following <cit.>, we give a Kripke-style semantics for , defining the models used first, and explaining how formulae are evaluated over them second.


 An 𝕀-frame (or, frame) is a tuple F = (W,≤,U,D) such that:



  * W is a non-empty set {w, u, v, …} of worlds;


  * ≤ ⊆ W × W is a reflexive and transitive binary relation;


  *  is a non-empty set referred to as the universe;


  * D : W→𝒫() is a domain function mapping each w ∈ W to a non-empty set D(w) ⊆ with U = ⋃_w ∈ W D(w), which satisfies the increasing domain condition:  If w ≤ u, then D(w) ⊆ D(u).





We define an 𝕀-Model (or, model) M to be an ordered triple (F,,) such that:


  * F = (W,≤,U,D) is a frame;


  *  is a function interpreting each function symbol f∈ such that f = n by a function (f): ^n→, satisfying the following conditions:





     For each w ∈ W and constant a, (a) ∈ D(w).

     For each w ∈ W, a⃗∈ D(w)^n (f)(a⃗) ∈ D(w).






  *  is a function interpreting, in each w∈ W, each predicate p ∈ such that p = n by a set (w,p)⊆ D(w)^n, satisfying the following monotonicity condition:



     If w ≤ u, then (w,p) 
⊆(u,p).













Let M=(F,,) be a model. We define an M-assignment to be a function α : →. We note α[/x] is the function α modified in x such that α[/x](x)= and α[/x](y)=α(y) if y≠ x. Given an M-assignment α, we define the interpretation of t in M given α, noted α(t), inductively as follows:



α(x)     =     α(x)

α(f(t_1,...,t_n))     =     (f)(α(t_1),...,α(t_n))









 Let M = (W,≤,U,D,,) be a model with w ∈ W and α an M-assignment. The satisfaction relation ⊩ is defined as follows:



  * M,w,α⊩ p(t_1, …, t_n) (α(t_1), …, α(t_n)) ∈(w,p);


  * M,w,α⊮;


  * M,w,α⊩⊤;


  * M,w,α⊩ϕψ M,w,α⊩ϕ or M,w,α⊩ψ;


  * M,w,α⊩ϕψ M,w,α⊩ϕ and M,w,α⊩ψ;


  * M,w,α⊩ϕψ there exists a u ∈ W such that u ≤ w, M,u,α⊩ϕ, and M,u,α⊮ψ;


  * M,w,α⊩ϕψ for all u ∈ W, if w ≤ u and M,u,α⊩ϕ, then M,u,α⊩ψ;


  * M,w,α⊩∃ x ϕ there exists an ∈ D(w) such that M,w,α[/x] ⊩ϕ;


  * M,w, α⊩∀ x ϕ for all u ∈ W and all ∈ D(u), if w ≤ u, then M, u, α[/x] ⊩ϕ;









For a set ⊆ of formulae, we write ϕ for all models M, M-assignments α, and worlds w in M, if M,w,α⊩ψ for each ψ∈, then M,w,α⊩ϕ. A formula ϕ is valid ∅ϕ. Finally, we define the logic  to be the set {ϕ |  ∅ϕ} of all valid formulae.


Note that here we define logics as sets of theorems, 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 <cit.>, notably pertaining to the deduction theorem. 




 Let M = (W,≤,U,D,,) be a model with α an M-assignment. For any ϕ∈, if M,w,α⊩ϕ and w ≤ u, then M,u,α⊩ϕ.



 We define a -model to be an model satisfying the constant domain condition:  If w, u ∈ W, then D(w) = D(u). If we impose the  condition on models, then first-order bi-intuitionistic logic with constant domains, dubbed , can be defined as the set of all valid formulae over the class of -models. In what follows, we let  denote the class of 𝕀-models and  denote the class of -models.




Consider the formula 
∀ x( (p(x) ∃ y p(y)) ), which was 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 such that the formula is false. This means that there is a successor w ≤ u such that α̅(x) ∈ D(u) and p(x) ∃ y p(y) is true, for some assignment α. 
The latter implies that for some u' such that u' ≤ u, p(x) is true (i.e. α(x) ∈ I_P(u', p)), but ∃ y p(y) is false. The former implies that α(x) ∈ D(u'), so by the semantic clause for the ∃ quantifier, ∃ y p(y) must be true – contradiction. 







§ LABELED POLYTREE SEQUENTS




Let = {w, u, v, …} be a countably infinite set of labels. For a formula ϕ∈ and label w∈, we define wϕ to be a labeled formula. We use , , , … to denote finite multisets of labeled formulae, 
and let w denote a multiset of labeled formulae such that every formula is labeled with w. A relational atom is an expression of the form wu such that w,u ∈ and a domain atom is an expression of the form w : x such that w ∈ and x ∈. 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  and annotated versions thereof to denote multisets of relational atoms and  and annotated versions thereof to denote multisets of domain atoms. Also, we 

define wt = w : x_1, …, w : x_n with t = {x_1, …, x_n}, define wt⃗ = w : t_1, …, w : t_n with t⃗ = t_1, …, t_n, and let w : x⃗ = w : x_1, …, w : x_n for x⃗ = x_1, …, 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 (X) denote the set of labels occurring in X.

 We define a labeled polytree sequent to be an expression of the form ,, such that (1) 
 if ≠∅, then (, , ) ⊆() and if = ∅, then |(, , )| = 1, and (2)  forms a polytree, i.e. the graph G = (V,E) such that V = () and E = {(w,u)  |  wu∈} is connected and free of (un)directed cycles. We refer to ,, as the antecedent and  as the consequent of a labeled polytree sequent. We will often times refer to labeled polytree sequents as sequents, more simply.


We sometimes use S, S_0, S_1, … to denote sequents, and for S = ,,, we define (S) = (,,,). A flat sequent is an expression of the form ,⊢ such that |(,,)| = 1, i.e. all labeled formulae and domain atoms share the same label. Labeled 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. <cit.>). For example, the labeled polytree sequent



S = u'w, uw, wv, vv'^, u' : x, u : x, u : y, w : z, v : y,^





u' : τ, w : ϕ, w : ψ, v : θ, v' : ζ_u' : τ, u : χ, v : ξ, v': ψ_



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







@C=.15em

u'u' : x u' : τ@->[drr]             vv : y, v : θv : ξ@->[d] 

uu : x, u : y u : χ@->[rr]          ww : z, w : ϕ, w : ψ@->[ur]       v'v' : ζv' : ψ 








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




 §.§ Semantics and Proof Systems


The following definition specifies how to interpret sequents. In essence, we lift the semantics of  to sequents by means of `M-interpretations', mapping sequents into models.

 Let M = (W,≤,U,D,,) be a model and  an M-assignment. We define an M-interpretation to be a function  mapping every label w ∈ to a world ι(w) ∈ W. The satisfaction of multisets , , and  are defined accordingly:



  * M,ι, for all wu∈, (w) ≤(u);


  * M,ι, for all w : x ∈, (x) ∈ D((w));


  * M,ι, for all w : ϕ∈, M, (w), ⊩ϕ.




We define a sequent S = , , to be satisfied on M with ι and , written M,ι, S, if M, ι,, and M, ι,, as well as M, ι,, then there exists a w : ψ∈ such that M,ι, w : ψ. We write M,ι,S when a sequent S is not satisfied on M with ι and . A sequent S is defined to be valid for every model M, every M-interpretation ι, and every M-assignment , we have M,ι, S; otherwise, we say that S is invalid and write M,ι,S.





Given a sequent S = , ,, we define the term substitution S(t/x) to be the sequent obtained by replacing (1) every labeled formula w : ϕ in , by w : ϕ(t/x) and (2)  by 𝒯(t/x):=

    (𝒯∖{wx|wx∈𝒯})∪{wy|wx∈𝒯 and  y ∈t}.

For example, if S = wu, wx,ux,uy, wp(x)u∀ y q(x,y), then S(f(y,z)/x)  = wu, ,wp(f(y,z))u∀ x' q(f(y,z),x'), where = wy,wz,uy,uz,uy and the bound variable y in ∀ y q(x,y) was renamed to x' to avoid capture. We now define two reachability relations  and  as well as the notion of availability <cit.>–all of which are required to properly formulate certain inference rules in/for our calculi.
 
 Let  be a finite multiset of relational atoms such that w,u ∈(). We say that u is strictly reachable from w, written wu, there exist v_1, …, v_n∈() such that wv_1, …, v_nu∈. We say that u is reachable from w, written wu, wu or w=u. We write wu if wu does not hold.


 Let = , , be a sequent with w ∈(). We define a term t to be available for w in ,, written tX_w,, t ∈(X_w) such that

    X_w = {x  |  ux∈ and uw for some u ∈()}.




Our labeled polytree calculus  for  is shown in  <ref>. The , , and  rules serve as the initial rules, the domain shift rule  encodes the fact that (p,w) ⊆ 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 we define an active formula to be either a principal or auxiliary formula. For example, w : ∃ x ϕ is principal, w : ϕ(t/x) is auxiliary, and both are active in . Note that all rules of our calculus preserve the representability of sequents as polytrees.

 We inductively define a proof in the usual way: (1) any application of an initial rule is a proof, (2) applying any rule to the conclusion of a proof, or between conclusions of proofs, gives a proof. The height of a proof is also defined as usual as the number of sequents occurring along a maximal path in a proof starting from the conclusion and ending at an initial rule; cf. <cit.>. Two unique features of our calculi are the inclusion of reachability rules and the domain shift rule (ds). We elaborate on each next.  



 §.§ Reachability Rules
 

A unique feature of our calculi is the inclusion of reachability rules (introduced in <cit.>), a generalization of propagation rules (cf. <cit.>), which are not only permitted to propagate formulae throughout a labeled polytree sequent when applied bottom-up, but may also check to see if data exists along certain paths. The rules , , , , and  serve as our reachability rules. The side conditions of our reachability rules are listed in the latter section of  <ref>. Moreover, we define a label u or a variable y to be fresh in a rule application (as in the  and  rules) it does not occur in the conclusion of the rule. 

 If we set †_4 := `t ∈', †_5 := `wu and t ∈', and remove the  rule, then we obtain a labeled polytree calculus, dubbed , for the constant domain version of the logic . We also note that in the constant domain setting, domain atoms are unnecessary and can be omitted from sequents.




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

 Let S = , , ΓΔ such that = uw, wv, = w : x, u : y, v : z, Γ = w : ∀ x p(x), w : p(f(y)), w : p(z), and Δ = u : q(x)  q(x), v : r(y). A pictorial representation of the polytree it encodes is shown below. We explain (in)valid applications of the  reachability rule.






!


 ww : x, w : ∀x p(x), w : p(f(y)), w : p(z) [dr]      

  uu : y u : q(x) q(x) [u]     vv : z v : r(y)





 The term f(y) is available for w in  since uw, namely there is an edge from u to w, and f(y) ∈(X_w) since X_w = {x,y}. Therefore, we may (top-down) apply the  rule to delete w : p(f(y)) and derive the sequent ' = , , Γ' Δ with Γ' = w : ∀ x p(x), w : p(z).



 By contrast, w : p(z) cannot be deleted via an application of  because the term z is not available for w in  (observe that w is not reachable from v) meaning z ∉(X_w).


 We note that for any set X ⊆, (X) ≠∅ since all constants are contained in (X) by definition. This means that bottom-up applications of  and  may instantiate existential and universal formulae with any constant.


The reachability rules ,  and  are important to ensure completeness for both  and . The reachability rules for  and  are relevant only for , 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. 

[An intuitionistic formula valid in constant domain models]
Let us consider the intuitionistic formula: ∀ x(p  B(x))  (p  (q ∀ xB(x))). This formula was adapted from an example in <cit.>, 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 , shown in Figure <ref>, crucially relies on reachability rules. In the figure, the relational atoms = {w_1 R w_2, w_2 R w_3, w_3 R w_4} in the instances of  allows us to conclude that w_2w_2, justifying the left instance of , and w_2w_4, justifying the right instance of . 


[Non-provability of the quantifier shift axiom in the increasing domain setting] Consider again the quantifier shift axiom ∀ x(φψ)  (∀ x φψ) and an attempt to construct for one of its instances a proof (bottom-up) in  shown below:



w_1 R w_2, w_2 R w_3, w_3 : x, w_2 : ∀ x(p(x)  q)   w_3 : p(x),  w_2 : q

w_1 R w_2,  w_2 : ∀ x(p(x)  q)   w_2 : ∀ x p(x),  w_2 : q

w_1 R w_2,  w_2 : ∀ x(p(x) q)   w_2 : ∀ x p(x)  q

w_1 : ∀ x(p(x)  q)  (∀ x p(x)  q)



It is obvious that to finish this proof, we would need to instantiate the ∀ x quantifier in the labeled formula w_2 : ∀ x(p(x)  q) with x by applying the  rule. 
However, to do so, we would need to demonstrate that the world w_2 is reachable from w_3 where the domain atom w_3 : x resides. However w_2 is not reachable from w_3, so x is not available at w_2 to be used by  in this case. 




 §.§ The Domain Shift Rule 


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  with respect to the sequent semantics for the logic . Interestingly, this incompleteness only arises when the exclusion connective is involved – if one considers only the intuitionistic fragment of , these reachability rules are sufficient to prove completeness (see Lemma <ref> in Section <ref>). To see the issue with incompleteness, consider the formula in Example <ref>, which is semantically valid, and the following attempt at a (bottom-up) construction of a proof: 



w R u, u R v, u' R v, u: x, u' : p(x)  u': ∃ y. p(y), v:

w R u, u R v, u: x, v : p(x) ∃ y. p(y)   v:

w R u, u: x  u: (p(x) ∃ y. p(y))

w: ∀ x( (p(x) ∃ y. p(y)) )



We have so far applied only invertible rules,[We remark that invertibility is formally defined in  <ref>.] so the original sequent is provable the top sequent in the above derivation is provable. 
To proceed with the proof construction, one would need to instantiate the existential quantifier ∃ y with x. However, the only domain atom containing x is located at world u, which is not available to the world u' where the existential formula is located. 

It was not so obvious how the reachability rules for quantifiers could be amended to allow the above 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' for when u'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 ∀ x (p(x)  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  rule as shown in Figure <ref>. Using the  rule, the above derivation can now be completed to a proof: 





, u: x, u' : x, u' : p(x)  u': p(x), u': ∃ y. p(y), v:

, u: x, u' : x, u' : p(x)  u': ∃ y. p(y), v:

w R u, u R v, u' R v, u: x, u' : p(x)  u': ∃ y. p(y), v:




Note that the  rule can be applied only to atomic predicates, but not arbitrary formulas. This rules out an unsound instance, e.g., allowing the domain atom u:x to be introduced when u: p(x), which is clearly semantically not valid. It may be possible to relax the restriction to atomic predicates by, e.g., imposing some positivity conditions on the occurences of x, but we did not find this necessary – neither for the completeness, nor for cut-elimination. 



The  rule can be removed without affecting the cut-elimination result for . This raises the possibility of defining a first-order bi-intuitionistic logic that is strictly weaker than . It is unclear at this stage what the semantics for such a logic would look like. 































 §.§ Soundness and Completeness


 Let  be a sequent. If  is derivable in  (), then  is (-)valid.



 By induction on the height of the given derivation; see  <ref> for details.













We prove the cut-free completeness of  by showing that if a sequent of the form w : x⃗ w : ϕ(x⃗) is not provable, then a counter-model can be constructed witnessing the invalidity of the sequent. We focus on the proof for  as it is more involved than the similar proof for . Our proof 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  with the children nodes corresponding to the premises. We remark that a proof in  is a finite pseudo-derivation where all top sequents are instances of , , or . A branch  is defined to be a maximal path of sequents through a pseudo-derivation, starting from the conclusion. The following lemma is useful in our proof of completeness.

 Let ∈{, }. For each i ∈{0,1,2}, let _i = _i, _i, _i_i be a sequent.



  * If wu holds for the conclusion of a rule (r) in (), then wu holds for the premises of (r);


  * If w : p(t⃗) ∈_0, _0 and _0 is the conclusion of a rule (r) in () with _1 (and _2) the premise(s) of (r), then w : p(t⃗) ∈_1, _1 (and w : p(t⃗) ∈_2, _2, resp.);


  * If w : x ∈_0 and _0 is the conclusion of a rule (r) in () with _1 (and _2) the premise(s) of (r), then w : x∈_1 (and w : x ∈_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.

 
 If w : x⃗ w : ϕ(x⃗) is (-)valid, then w : x⃗ w : ϕ(x⃗) is derivable in  ().


 Outline. 
We assume that = w : x⃗ w : ϕ(x⃗) is not derivable in  and show that a model M can be defined which witnesses that  is invalid. To prove this, we first define a proof-search procedure  that bottom-up applies rules from  to w : x⃗ w : ϕ(x⃗). Second, we show how a model M can be extracted from failed proof-search. We now describe the proof-search procedure  and let ≺ be a well-founded, strict linear order over the set  of terms.


. Let us take w : x⃗ w : ϕ(x⃗) as input and continue to the next step. We show here some key selected steps; the complete  procedure can be found in Appendix <ref>. 

, , and . Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we halt the computation of  on each branch _i where _i is of the form , , or . If  is halted on each branch _i, then  returns  because a proof of the input has been constructed. However, if  did not halt on each branch _i with 1 ≤ i ≤ n, then let _j_1, …, _j_k be the remaining branches for which  did not halt. For each such branch, copy the top sequent above itself, and continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = ℛ𝒯, w_1 : p_1(t⃗_1), …, w_ℓ : p_ℓ(t⃗_ℓ)

where all atomic input formulae are displayed in _k+1 above. We successively consider each atomic input formula and bottom-up apply , yielding a branch extending _k+1 with a top sequent saturated under  applications. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.




. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , , w_1 : ∃ x_1ϕ_1, …, w_m : ∃ x_mϕ_m⊢

where all existential input formulae w_i : ∃ x_iϕ_i are displayed in _k+1 above. We consider each formula w_i : ∃ x_iϕ_i in turn, and bottom-up apply the  rule. These rule applications extend _k+1 such that

    , ', , w_1 : ϕ_1(y_1/x_1), …, w_n : ϕ_m(y_m/x_m) ⊢

is now the top sequent of the branch with y_1,…,y_m fresh variables and ' = , w_1 : y_1, …, w_m : y_m. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , ⊢ w_1 : ∃ x_1ϕ_1, …, w_m : ∃ x_mϕ_m,

 where all existential formulae w_i : ∃ x_iϕ_i are displayed in _k+1 above. We consider each labeled formula w_m : ∃ x_mϕ_i in turn, and bottom-up apply the  rule. Let w_ℓ+1 : ∃ x_ℓ+1ϕ_ℓ+1 be the current formula under consideration, and assume that w_1 : ∃ x_1ϕ_1, …, w_ℓ : ∃ x_ℓϕ_ℓ have already been considered. Recall that ≺ is a well-founded, strict linear order over the set  of terms. Choose the ≺-minimal term t ∈(X_w_ℓ+1) that has yet to be picked to instantiate w_ℓ+1 : ∃ x_ℓ+1ϕ_ℓ+1 and bottom-up apply the  rule, thus adding w_ℓ+1 : ϕ_ℓ+1(t/x_ℓ+1 ). After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.
 


The remaining rules are processed in a similar fashion, and thus, this completes our outline of . Next, we aim to show that if  does not return , then a model M, M-interpretation ι, and M-assignment  can be defined such that M, ι,. If  halts, i.e.  returns , then a proof of  may be obtained by `contracting'  all redundant inferences from the `, , and ' step of . Therefore, in this case, since a proof exists, we have obtained a contradiction to our assumption. As a consequence, we have that  does not halt, that is,  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 . We define a model M = (W,≤,U,D,,) by means of this branch as follows: 
Let us define the following (multi)sets, all of which are obtained by taking the union of each (multi)set of relational atoms, domain atoms, antecedent labeled formulae, and consequent labeled formulae (resp.) occurring within a sequent in :

    ^ = ⋃_(, , ) ∈    ^ = ⋃_(, , ) ∈


    ^ = ⋃_(, , ) ∈    ^ = ⋃_(, , ) ∈

We now define: (1) u ∈ W u ∈(^,^, ^, ^), (2) ≤ = {(u,v)  |  uRv ∈}^* where * denotes the reflexive-transitive closure, (3) t ∈ U there exists a label u ∈(^,^, ^, ^) such that t ∈(X_u), (4) t ∈ D(u) t ∈(X_u), and (5) (t_1, …, t_n) ∈(u,p) v,u ∈(^,^, ^, ^), v ↠^*_^ u, and v : p(t_1, …, t_n) ∈^.

It can be shown that M is indeed a model (see Appendix <ref>). Let us define  to be the M-assignment mapping every variable in U to itself and every variable in ∖ U arbitrarily. To finish the proof of completeness, we now argue the following by mutual induction on the complexity of ψ: (1) if u : ψ∈^, then M,u,⊩ψ, and (2) if u : ψ∈^, then M,u,⊮ψ. 
 Let ι to be the M-interpretation such that ι(u) = u for u ∈ W and ι(v) ∈ W for v ∉W. By the proof above, M,ι,w : x⃗ w : ϕ(x⃗), showing that if a sequent of the form w : x⃗ w : ϕ(x⃗) is not derivable in , then it is invalid, that is, every valid sequent of the form w : x⃗ w : ϕ(x⃗) is provable in .







 §.§ Intuitionistic Subsystems



We end this section by discussing two subsystems of  and  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), and in the latter, we obtain a new proof system for intuitionistic logic with constant domains. 






Let φ be an intuitionistic formula (i.e. a formula with no occurrences of ). Then φ is valid in  () iff w:φ is provable in  (respectively, ). 







The proof of Corollary <ref> is straightforward from the definition of the semantics of  (resp. ) in Definition <ref>. However, both  and  do not have a direct interpretation in the semantics in Definiton <ref>, which does not feature domain atoms. 
We shall show next how we can extract a purely intuitionistic fragment out of , where every sequent in the fragment is interpretable in the semantics without the existence predicate. 
We shall prove this via syntactic means, by showing how we can translate intuitionistic proofs in () to proofs in Gentzen's LJ <cit.>. A key idea is to first define a formula interpretation of a labeled polytree sequent, and then show that every inference rule corresponds to a valid implication in LJ. We start by defining a notion of intuitionistic (labeled polytree) sequent. 










    A sequent S = , , ΓΔ is an intuitionistic sequent iff  is a tree rooted at node u such that 
    
    
  * every formula in S is an intuitionistic formula (i.e. it contains no occurrences of ),   
    
  * for every labeled formula w : ϕ in S and for every variable x ∈ VT(ϕ), x is available for w, and
    
  * if w: x and z: x are in , then w = z. 
    






Let () denote the proof system () without the  rule, and where the sequents are restricted to intuitionistic sequents. The following lemma states an important property of , called the separation property, which was first discussed in the context of tense logics <cit.>. 




An intuitionistic sequent S is provable in () iff it is provable in ().


One direction, from () to () is trivial. For the other direction, suppose  is a proof of S in (). 
By induction on the structure of , it can be shown that there is a proof ' in () in which every sequent in ' is “almost” intuitionistic – it satisfies all the requirements in Definition <ref> except possibly the last condition (due to the possible use of the  rule). Then, from ' we can construct another derivation ” of S that does not use , by showing that one can always permute the rule  up until it disappears. Since all the rules of (), other than , preserve the property of being an intuitionistic sequent, it then follows that ” is a proof in ().


To translate a proof in () to LJ, we need to interpret a labeled polytree sequent as a formula. In the general case, this turns out to be quite difficult, due to the difficulty in interpreting the scopes of eigenvariables in 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 formulas 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 <ref>, except that in the second clause, x is either available for w, or it does not occur in . 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 that is not reachable from w. Given a multiset of labeled formulae Γ, we denote with Γ_u the labeled formulae in Γ that are labeled with u.



Given a quasi-intuitionistic sequent S=, , ΓΔ, we define its formula interpretation F(S) by induction on the height of the sequent tree as follows: suppose S is rooted at u.


  * If S is a flat sequent, then F(X) = ∀x⃗ (⋀Γ⋁Δ) where x⃗ are all the variables in .

  * Otherwise, suppose u has n successors: w_1, …, w_n. Then:

    F(S) = ∀x⃗ (⋀Γ_u  (⋁Δ_u  F(S_w_1) ⋯ F(S_w_n))).








Let S be an intuitionistic sequent. S is provable in () F(S) is provable in LJ. 


Outline. The proof is tedious, but not difficult and follows a general strategy to translate nested sequent proofs (which, recall, are notational variants of labeled 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 <cit.>. 
For every inference rule in () of the form:



S_1   ⋯   S_n
    S



we show that the formula F(S_1) ⋯ F(S_n)  F(S) is provable in LJ. Then given any proof in (), we simulate every inference step with its corresponding implication, followed by a cut. 
A more detailed proof will be made available in a forthcoming extended version of this paper. 


For intuitionistic logic with constant domains , as far as we know there is no formalization in the traditional Gentzen sequent calculus that admits cut-elimination. There is, however, a formalization in prefixed tableaux by Fitting <cit.>, which happens to be a syntactic variant of the intuitionistic fragment  (see <cit.>).












§ CUT-ELIMINATION











In this section, we show that  and  satisfy a sizable number of favorable properties culminating in syntactic cut-elimination, most of which necessitate non-trivial proofs. We explain here some key steps; the full details are available in Appendix <ref>. 

 and  can be seen as first-order extensions of Postniece's deep-nested sequent calculus for bi-intuitionistic logic DBiInt <cit.>. 
Cut-elimination for DBiInt <cit.> was proven in two stages. First, cut-elimination was proven for a “shallow” version of the nested sequent calculus LBiInt, which can be seen as a variant of a display calculus <cit.>. The cut-elimination proof for this shallow calculus follows from Belnap's generic cut-elimination for display calculi <cit.>. Second, it is shown that cut-free proofs in the shallow calculus can be translated to proofs in the deep-nested calculus. We do not have the corresponding shallow versions of  and , so we cannot rely on Belnap's generic cut-elimination. It may be possible to define shallow versions of  and , and then follow the same methodology outlined in <cit.> to prove cut-elimination, but we found that a direct cut-elimination proof is simpler, e.g., avoiding the need for proving admissibility of certain structural rules called the display postulates <cit.> that is needed as one transition from shallow to deep inference systems. 

Since our labeled polytree sequents are a restriction of ordinary labeled sequents, another possible approach to cut-elimination would be to apply the methodology for proving cut-elimination for labeled sequent calculi <cit.>. 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, i.e., given a proof π_1 and labels u and w, one can  construct another proof π_2 by replacing u with w everywhere in the proof and adjusting the inference rules accordingly. This is typically needed in showing 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., ). Such a substitution operation may not always preserve polytree structures. Another notable difference between our calculi and traditional labeled calculi is the absence of structural rules that manipulate relational atoms: the only changes to the relation atoms are through introduction rules. These differences mean that the cut-elimination techniques for labeled sequent calculi cannot be immediately applied in our setting. 

Our cut-elimination proof builds on an approach by Pinto and Uustalu <cit.>, which deals with a polytree labeled 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 <ref>. 
We illustrate some key transformations and why they are needed, through an example of a cut where  and  are applied to the cut formula. The formal details are available in the proof of Theorem <ref>. Suppose we have the following instance of cut: 





π_1
, Γ w: φψ, Δ
π_2
, Γ, w: φψΔ
cut
, ΓΔ



where π_1 is 



π_1'
, w R w', Γ, w':φ w': ψ, Δ

, Γ w: φψ, Δ



and π_2 is



π_3
, w : φψ, ΓΔ, u : φ
π_4
, Γ, w : φψ, u : ψΔ

, Γ, w : φψΔ



and wu.
A typical cut reduction strategy would be to cut π_1' with π_4 (with cut formula ψ), producing a derivation π_5, and then cut π_3 with π_5 (with cut formula φ). There are a couple of issues with this strategy: 


  * The cut formulas in both instances of cuts have mismatched labels, i.e., w' on one side and u on the other. 

  * The label w' and the relational atom w R w' are not present in either π_3 or π_4, so the contexts of the premises of the cuts do not match. 

To fix these issues, we would need to first transform π_1' to remove the label w' and its associated relational atom. Simply substituting w' with u may break the polytree shape of the sequent, e.g., if there is an v such that w R v and v R u are in , then replacing w' with u in w R w' would break the polytree shape of the sequent. So the relational atoms in the sequent also need to be modified. As we shall see later in the cut-elimination proof, a transformation that we use in this case is one that is represented by the rule : 



π_1'
, w R w', Γ, w':φ w': ψ, Δ

, Γ, w: φ w : ψ, Δ

, Γ, w:φψ, w: φ w : ψ, Δ



To allow cut to be applied to this derivation and π_4, we relax the cut rule to allow mismatched labels in the cut formula, as long as wu, yielding a derivation π_5 of , Γ, w: φψ, w:φΔ.  To complete the reduction, we also have to apply cut to π_5 and π_3. Here, however, we run into a problem: 



π_3
, w : φψ, ΓΔ, u : φ
π_5
, Γ, w: φψ, w:φΔ
cut
, Γ, w: φψΔ



This cut is not a valid instance, as the conditon uw does not hold. We would need another transformation to “lower” the label formula u: φ in π_3 to w:φ, using the  rule (which has the side condition wu). This gives us a valid proof π_6:



π_3
, w : φψ, ΓΔ, u : φ

, w : φψ, ΓΔ, w : φ
π_5
, Γ, w: φψ, w:φΔ
cut
, Γ, w: φψΔ



We can then finally can cut π_6 with π_2 to obtain a derivation of , ΓΔ.  Here we gloss over the termination arguments, but the details are available in the proof of Theorem <ref>.

The above example illustrates one among several proof transformations needed in cut-elimination. These transformations make use of the auxiliary rules in Figure <ref>. The bulk of the cut-elimination proof is really in showing that these auxiliary rules are 

(height-preserving (hp)) admissible, 
meaning if the premises of the rule have proofs (of heights h_1, …, h_n), then the conclusion of the rule has a proof (of height h ≤max{h_1, …, h_n}). If we let (r^-1) be the inverse of the rule (r) whose premise is the conclusion of (r) and conclusion is the premises of (r), then we say that (r) is (height-preserving) invertible, i.e. (hp-)invertible (r^-1) is (hp-)admissible. 

Whenever a rule is (hp-)admissible in both calculi, we only focus on the  case and we note that all admissible rules are assumed to preserve the polytree structure of sequents. With the exception of , all rules in  <ref> are shown to be hp-admissible. 









The first rule we focus on extends the  rule to all formulae.

 Let ∈{, }. For every ϕ∈, any sequent of the form ℛ𝒯Γ,wϕΔ,uϕ with wu is derivable in ().




This lemma is easily proved by induction on the structure of the formula φ. As an example, we consider the case φ=ψχ. We proceed as follows, where the dashed lines labeled with IH mark the use of the induction hypothesis.



.5





  rprem:= ℛ,vw𝒯Γ,vψ,vχΔ,uψχ,vχ












IH
ℛ,vw𝒯Γ,vψΔ,uψχ,vχ,vψ

IH
rprem

ℛ,vw𝒯Γ,vψΔ,uψχ,vχ

ℛ𝒯Γ,wψχΔ,uψχ


















For some labels w, u and v, assume wv and wu and vu in some ℛ. Then we know that (1) u and v are on two different paths passing through w of the polytree generated from ℛ, and (2) there is no vertex between v and w else we would be in presence of a cycle. In this scenario, the rule  (for branch forward) allows to move the branch rooted in v upward by connecting it to u instead of w. Similarly, with vw instead of wv, the rule  (for branch backward) expresses the possibility to move the branch rooted in v downward from u to w. These rules preserve the representability of sequents as polytrees, provability and height.



Let ∈{, }. The rules  and  are hp-admissible in ().





By changing wv to uv, we are effectively moving the branch rooted in v from w to u: we move from the left diagram to the right one below.




(0,0) node[point] (w0) [label=below:w];
(1.5,0) node[point](w1)[label=below:u];
(0.5,0.4) node[point](w2)[label=left:v];
(2.25,0) node ⇒;

[->] (w0) edge[dashed] (w1);
[->] (w0) edge (w2);
[-] (w2) edge[dashed] (1.1,0.3);
[-] (w2) edge[dashed] (1,0.8);
[-] (1.1,0.3) edge[dashed] (1,0.8);

(2.25,0) node ⇒;

(3,0) node[point] (w0) [label=below:w];
(4.5,0) node[point](w1)[label=below:u];
(5,0.4) node[point](w2)[label=left:v];

[->] (w0) edge[dashed] (w1);
[->] (w1) edge (w2);
[-] (w2) edge[dashed] (5.6,0.3);
[-] (w2) edge[dashed] (5.5,0.8);
[-] (5.6,0.3) edge[dashed] (5.5,0.8);




The crucial observation is that given that wu, this moving of the branch only extends the reachability relation: we have that for all w' and w”, if w'w” in ℛ,wv then w'w” in ℛ,uv. Consequently, we can see that  only expands reachability, and thus does not violate the reachability or availability conditions of any of the rules. Freshness is also not impacted. So, in all cases we can simply apply the induction hypothesis on the premises, and then the rule.

A similar argument can be provided for , where we move from the left diagram to the right one below.




(0,0) node[point] (w0) [label=above:w];
(1.5,0) node[point](w1)[label=above:u];
(1,-0.4) node[point](w2)[label=below:v];

[->] (w0) edge[dashed] (w1);
[->] (w2) edge (w1);
[-] (w2) edge[dashed] (0.4,-0.3);
[-] (w2) edge[dashed] (0.5,-0.8);
[-] (0.4,-0.3) edge[dashed] (0.5,-0.8);

(2.25,0) node ⇒;

(4,0) node[point] (w0) [label=above:w];
(5.5,0) node[point](w1)[label=above:u];
(3.5,-0.4) node[point](w2)[label=below:v];

[->] (w0) edge[dashed] (w1);
[->] (w2) edge (w0);
[-] (w2) edge[dashed] (2.9,-0.3);
[-] (w2) edge[dashed] (3,-0.8);
[-] (2.9,-0.3) edge[dashed] (3,-0.8);
































An acceptable operation on our sequents consists in the merging of two directly connected labels w and u, i.e. if wu or uw. Obviously, this merging preserves the representability of sequents as polytrees, and does not impact the availability, freshness or reachability conditions. The rules of our calculus corresponding to these operations, i.e.  and , are the rules nodemergeD and nodemergeU of Pinto and Uustalu <cit.>.


Let ∈{, }. The rules  and  are hp-admissible in ().
















As domains atoms are essentially used via availability, we can show the redundancy of a variable labeled by two labels such that one is reachable by the other: it suffices to keep the “lowest" label. A special case of importance is when the two labels are identical: then, the following rule is a contraction on domain atoms (as ww always holds).


Let ∈{, }. The  rule is hp-admissible in ().







This lemma is straightforwardly proved by induction on the height of proofs. To realize that we can simply apply the induction hypothesis on the premises of the rules, and then reapply the rule, it suffices to note that the deletion of ux does not impact reachability, freshness or even availability given that wu. So, any rule is reapplicable once we use the induction hypothesis.



Fortunately, term substitution is hp-admissible in our calculi. This result comes in handy in various places.


Let ∈{, }. The  rule is hp-admissible in ().




We reason by induction on the height of proofs, and consider the last rule applied. 

Obviously, the propositional rules are not impacted by the substitution. So, for these rules we simply need to apply the induction hypothesis on the premises of the rule, and then reapply the rule.

The rule  is treated straightforwardly: we apply the induction hypothesis on the proof of 
ℛ𝒯, wt⃗'⃗, wp(t⃗'⃗) to obtain a proof of ℛ𝒯'(t/x), wp(t⃗'⃗(⃗t⃗/⃗x⃗)⃗)(t/x) where 𝒯'=(𝒯, wt⃗'⃗)(t/x). Note that 𝒯' is such that any domain atom ux is replaced by ux_0,…,ux_m where x_0,…,x_m are the variables appearing in t. Consequently, all the variables appearing in the terms t⃗'⃗(⃗t⃗/⃗x⃗)⃗ are labeled by w in 𝒯'. Consequently, we can apply the rule  to obtain a proof of our goal, i.e. ℛ𝒯(t/x)(t/x), w : p(t⃗'⃗(⃗t⃗/⃗x⃗)⃗(t/x).

The cases of rules for quantifiers deserve more attention. We show the cases of  and , as the other rules can be treated in a similar way.

: we need to obtain a proof of ℛ(t/x)𝒯(t/x)Γ(t/x),w(∃ zϕ)(t/x)Δ(t/x), where we can safely assume that z is different from x and any variable appearing in t. First, we apply the induction hypothesis on the proof of ℛ𝒯,wyΓ,wϕ(y/z)Δ, the premise of the rule, to obtain a proof of no greater height of ℛ𝒯(y'/y),wy(y'/y)Γ(y'/y),wϕ(y/z)(y'/y)Δ(y'/y) with y' fresh and not appearing in t or x. Given that y was fresh, we have a proof of no greater height the sequent ℛ𝒯,wy'Γ,wϕ(y'/z)Δ. We can apply the induction hypothesis again here to obtain a proof of no greater height of ℛ𝒯(t/x),wy'(t/x)Γ(t/x),wϕ(y'/z)(t/x)Δ(t/x). Because of our choice of y', we have that the latter sequent is equal to ℛ𝒯(t/x),wy'Γ(t/x),wϕ(t/x)(y'/z)Δ(t/x). Thus, we can reapply the rule  on the latter to obtain a proof of ℛ(t/x)𝒯(t/x)Γ(t/x),w(∃ zϕ)(t/x)Δ(t/x).

: we need a proof of ℛ𝒯(t/x)Γ(t/x),w(∀ zϕ)(t/x)Δ(t/x) of no greater height, where we can safely assume that z is different from x and any variable appearing in t. We apply the induction hypothesis on the proof of ℛ𝒯Γ,w∀ zϕ,uϕ(t'/z)Δ, the premise of the rule, to obtain a proof of no greater height of ℛ𝒯(t/x)Γ,w(∀ zϕ)(t/x),uϕ(t'/z)(t/x)Δ(t/x). Note that the latter is equal to ℛ𝒯(t/x)Γ,w(∀ zϕ)(t/x),uϕ(t'(t/x)/z)Δ(t/x). Clearly, in this sequent we still have that wu. In addition to that, we have that t'(t/x) is available to u. We can argue this point by a case distinction on the presence or not of x in t'. If x does not appear in t', then t'(t/x)=t', which is available for u as initially given. If x does appear in t', then we have that there must be a v such that vx∈ and vu else t' would not be available in u. Consequently, we have that vx is replaced by {vx'| x' appears in t} in (t/x). This makes t'(t/x) available for u. So, as wu and t'(t/x) is available to u we can apply  to obtain a proof of ℛ𝒯(t/x)Γ(t/x),w(∀ zϕ)(t/x)Δ(t/x) of no greater height than the proof initially considered.






















The next lemma shows the admissibility of the weakening of labeled formulae, both on the left and right of a sequent.


Let ∈{, }. The  rule is hp-admissible in ().




The only problems that the addition of labeled formulae to a sequent can create have to do with the condition of freshness of a variable or a label. To make sure that there is no violation of these conditions, we can use Lemma <ref> and our view that isomorphic sequents are identical to avoid any overlap with these critical variables or labels. Thus, for all rules we can simply use these lemmas on the premises if needed, apply the induction hypothesis on the potentially modified premises and then reapply the rule.



Now, in the case of the calculus (), all the conditions on availability have disappeared from rules. So, the entirety of the labeled terms become unnecessary in this context. This point is captured by the following lemma, which is straightforwardly proved by induction on the height of proofs.


The  rule is hp-admissible in ().


Weakening of labeled variables is also hp-admissible.


Let ∈{, }. The  rule is hp-admissible in ().




The addition of a further labeled variable can only alter freshness of variable conditions. So, we only need to pay attention to the rules involving such conditions and apply Lemma <ref> before applying the induction hypothesis.











As one would expect, the presence of  (resp. ⊤) on the right (resp. left) is unnecessary. This is the essence of the next lemma.


Let ∈{, }. The rules  and  are hp-admissible in ().




We focus on  as  can be treated dually. By inspecting the rules, one can see that the deletion of w in the consequent of a sequent impacts the application of no rule. In particular, this deletion does not alter the reachability, availability or freshness conditions. As a consequence, a straightforward induction on the structure of the proof is sufficient to prove this statement: in the inductive cases, apply the induction hypothesis on the last rule applied, and then the rule.



Then, we proceed to show that we can modify the labels of formulae in a labeled sequent by looking at the polytree underlying it. More precisely, if wu we can both lower the label of uΔ on the right of the sequent to w, and lift the label of wΓ on the left of the sequent to u. This is the spirit of the rules  and , which we prove hp-admissible.


Let ∈{, }. The  rule is hp-admissible in ().




We reason by induction on the height of proofs, and consider the last rule applied.

Obviously, the “local" propositional rules (which do not involve a condition on reachability) and  are not impacted by the modification of the label, whether the principal formula is labeled by one of the labels under focus or not. For  we easily reach our goal by applying the induction hypothesis on the premise and then the rule as the principal formula cannot be the one under focus.
However, the other non-local rules require more care.

: then we have a proof of ℛ𝒯Γ,w'p(t⃗)Δ,u'p(t⃗) where w'u'. We proceed by case distinction on the equality between w and u'. If w=u', then we need to prove ℛ𝒯Γ,w'p(t⃗)Δ,up(t⃗). Now, note that we have w'u' and u'u by assumption as w=u'. Consequently, we have that w'u by transitivity. An application of the rule  leads us to our goal. If w≠ u', then we can simply reapply the rule as the two labeled formulae are not modified.

: then the last rule has the following form.


ℛ,w'u'𝒯,u'ϕ,u'ψ

ℛ𝒯,w'ϕψ


If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
As we have wu and not uu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,uu'𝒯,u'ϕ,u'ψ. Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,uϕψ of the adequate height. If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
 
: then the last rule has the following form.



ℛ𝒯,u'ϕψ,w'ϕ
ℛ𝒯,w'ψ,u'ϕψ

ℛ𝒯,u'ϕψ



If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w=u'.
As we have wu and w'w by the rule application, we get w'u by transitivity. This allows us to apply the induction hypothesis in both premises to obtain proofs of ℛ𝒯,uϕψ,w'ϕ and ℛ𝒯,w'ψ,uϕψ. Then, it suffices to reapply the rule to obtain a proof of adequate height of ℛ𝒯,uϕψ.

Let us now turn to the first order rules. For all the rules for quantifiers where the modified labeled formula cannot be principal, i.e. for  and , it suffices to apply the induction hypothesis in the premise, and then reapply the rule. So, we are left with the rules  and .

: then the last rule has the following form.


ℛ,w'u'𝒯,u'y,u'ϕ(y/x)

ℛ𝒯,w'∀ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
As we have wu and not uu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,uu'𝒯,u'y,u'ϕ(y/x). Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,u∀ xϕ of the adequate height. 

: then the last rule has the following form.


ℛ𝒯,w'∃ xϕ,w'ϕ(t/x)

ℛ𝒯,w'∃ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
Then, we can apply the induction hypothesis on the premise twice to obtain a proof of ℛ𝒯,u∃ xϕ,uϕ(t/x). Note that in this case, we have that t∈(X_u) as wu. So, we can apply the rule  to reach our goal.




















Let ∈{, }. The  rule is hp-admissible in ().




The proof of this lemma is very similar in spirit to the proof of Lemma <ref>. Dually, the problematic rules here are , , ,  and .

: then the last rule has the following form where u:p(t⃗) is the principal formula. 



π_1
, , Γ, u:p(t⃗),  u: t⃗Δ

, , Γ, u:p(t⃗) Δ



Applying the induction hypothesis to π_1, we get a proof π_2 of 
, , Γ, w:p(t⃗), u:t⃗Δ with the same height, from which we can obtain a proof of , , Γ, w : p(t⃗) Δ as follows:



, , Γ, w:p(t⃗), u:t⃗Δ

, , Γ, w:p(t⃗), w:t⃗, u:t⃗Δ

, , Γ, w:p(t⃗), w:t⃗Δ

, , Γ, w:p(t⃗) Δ



The instance of  above is applicable because wu. The hp-admissibility of  in this case then follows from Lemma <ref> and Lemma <ref>. 

: then the last rule has the following form.



ℛ𝒯,w'ϕψ,u'ϕ
ℛ𝒯,w'ϕψ,u'ψ

ℛ𝒯,w'ϕψ



If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
As we have wu and uu' by the rule application, we get wu' by transitivity. This allows us to apply the induction hypothesis in both premises to obtain proofs of ℛ𝒯,wϕψ,u'ϕ and ℛ𝒯,wϕψ,u'ψ. Then, it suffices to reapply the rule to obtain a proof of adequate height of ℛ𝒯,wϕψ.

: then the last rule has the following form.


ℛ,u'w'𝒯,u'ϕ,u'ψ

ℛ𝒯,w'ϕψ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
As we have wu and not wu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,u'w𝒯,u'ϕ,u'ψ. Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,wϕψ of the adequate height. 


: then the last rule has the following form.


ℛ𝒯,w'y,w'ϕ(y/x)

ℛ𝒯,w'∃ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
First, we can apply Lemma <ref> on the premise to obtain a proof of ℛ𝒯,wy,uy,uϕ(y/x). Then, as wu we apply Lemma <ref> to obtain a proof of ℛ𝒯,wy,uϕ(y/x). Finally, as all previous lemmas preserve height, it suffices to apply the induction hypothesis on this proof to obtain a proof of ℛ𝒯,wy,wϕ(y/x). A simple application of the rule  reaches our goal.

: then the last rule has the following form.


ℛ𝒯,w'∀ xϕ,u'ϕ(t/x)

ℛ𝒯,w'∀ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
Then, we can apply the induction hypothesis on the premise to obtain a proof of ℛ𝒯,w∀ xϕ,u'ϕ(t/x). Note that we have wu' as wu and uu'. So, we can apply the rule  to reach our goal.
















For each of the rules in the following lemma, we obtain a proof via an usual induction on the height of proofs. 


Let ∈{, }. The rules ,,, are hp-invertible in ().


The invertibility of the rules mentioned below essentially relies on the hp-admissibility of the weakening rule . 


Let ∈{, }. The rules , , ,  are hp-invertible in ().




For : given a proof of ℛ𝒯Γ,wϕψΔ, we can simply use height-preserving internal weakening (Lemma <ref>) to obtain proofs of ℛ𝒯Γ,wϕψΔ,uϕ and ℛ𝒯Γ,wϕψ,uψΔ of less or equal height.

For : given a proof of ℛ𝒯ΓΔ,w∃ xϕ, we can simply use height-preserving internal weakening (Lemma <ref>) to obtain a proof of ℛ𝒯ΓΔ,w∃ xϕ,wϕ(t/x) of less or equal height.



The invertibility of the rules  and  is proved by induction on the height of proofs. In some places, we need to use isomorphic labeled sequents to ensure the freshness of the label introduced by the rule.


Let ∈{, }. The rules  and  are hp-invertible in ().



When a rule crucially involves a freshness condition, we can use the Lemma <ref> to rename variables and ensure freshness of variables through some modifications. This is what we do in parts of the proofs of the next invertibility lemma.


Let ∈{, }. The rules  and  are hp-invertible in ().
























Let ∈{, }. The rules  and  are hp-admissible in ().




We simultaneously prove the hp-admissibility of the two rules. We reason by primary induction on the structure of ϕ (PIH) and secondary induction on the  height of derivations (SIH). In each case, we consider the last rule applied, and whether ϕ is principal in that rule. We omit the cases of initial rules as they are straightforward.



We start by the rule . If ϕ is not principal in the last rule, then we proceed as usual by applying SIH on ϕ in the premises of the rule, and then the rule. Note that all rules which have their principal formula on the right fall in this category.

If ϕ is principal, then for the rules  and  we use the invertibility lemmas proved previously, jointly with PIH. For the rules in which the principal formula is not deleted in the premises, i.e.  and , we simply use SIH to contract the principal formula. We give the case of  as an example.

: then the last rule has the following form, where ϕ=χψ.



ℛ𝒯,wχψ,wχψ,uχ
ℛ𝒯,wχψ,wχψ,uψ

ℛ𝒯,wχψ,wχψ



We can simply apply SIH on both premises to obtain proofs of ℛ𝒯,wχψ,uχ and ℛ𝒯,wχψ,uψ. A simple application of the  gives us the desired result.

Finally, we are left with the rules  and  which we treat individually.

: then the last rule has the following form, where ϕ=χψ.


ℛ,uw𝒯,uχ,wχψ,uψ

ℛ𝒯,wχψ,wχψ


Then, we proceed as follows.


ℛ,uw𝒯,uχ,wχψ,uψ
Lem.<ref>
ℛ,uw,vw𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,uw,vu𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,uw𝒯,uχ,uχ,uψ,uψ
PIH
ℛ,uw𝒯,uχ,uψ

ℛ𝒯,wχψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch vw to u and obtain vu. Third, we merge the points v and u using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.

: then the last rule has the following form, where ϕ=∃ xψ.


ℛ𝒯,wy,wψ(y/x),w∃ xψ

ℛ𝒯,w∃ xψ,w∃ xψ


Then, we proceed as follows.


ℛ𝒯,wy,wψ(y/x),w∃ xψ
Lem.<ref>
ℛ𝒯,wy,wz,wψ(y/x),wψ(z/x)
Lem.<ref>
ℛ𝒯,wy,wy,wψ(y/x),wψ(y/x)
Lem.<ref>
ℛ𝒯,wy,wψ(y/x),wψ(y/x)
PIH
ℛ𝒯,wy,wψ(y/x)

ℛ𝒯,w∃ xψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to rename the (fresh) variable z to y. Third, we contract the labeled variable wy using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.



Now, let us turn to the rule . If ϕ is not principal in the last rule, then we proceed as usual by applying SIH on ϕ in the premises of the rule, and then the rule. Note that this time, all rules which have their principal formula on the left fall in this category.

If ϕ is principal, then for the rules  and  we use the invertibility lemmas proved previously, jointly with PIH. For the rules in which the principal formula is not deleted in the premises, i.e. ,  and , we simply use SIH to contract the principal formula. We give the case of  as an example.

: then the last rule has the following form, where ϕ=χψ.



ℛ𝒯,wχψ,wχψ,uχ
ℛ𝒯,uψ,wχψ,wχψ

ℛ𝒯,wχψ,wχψ



We can simply apply SIH on both premises to obtain proofs of ℛ𝒯,wχψ,uχ and ℛ𝒯,uψ,wχψ. A simple application of the rule gives us the desired result.

Finally, we are left with the rules  and  which we treat individually.

: then the last rule has the following form, where ϕ=χψ.


ℛ,wu𝒯,uχ,uψ,wχψ

ℛ𝒯,wχψ,wχψ


Then, we proceed as follows.


ℛ,wu𝒯,uχ,uψ,wχψ
Lem.<ref>
ℛ,wu,wv𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,wu,uv𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,wu𝒯,uχ,uχ,uψ,uψ
PIH
ℛ,wu𝒯,uχ,uψ

ℛ𝒯,wχψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch wv to u and obtain uv. Third, we merge the points v and u using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.

: then the last rule has the following form, where ϕ=∀ xψ.


ℛ,wu𝒯,uy,uψ(y/x),w∀ xψ

ℛ𝒯,w∀ xψ,w∀ xψ


Then, we proceed as follows.


ℛ,wu𝒯,uy,uψ(y/x),w∀ xψ
Lem.<ref>
ℛ,wu,wv𝒯,uy,vz,uψ(y/x),vψ(z/x)
Lem.<ref>
ℛ,wu,uv𝒯,uy,vz,uψ(y/x),vψ(z/x)
Lem.<ref>
ℛ,wu𝒯,uy,uz,uψ(y/x),uψ(z/x)
Lem.<ref>
ℛ,wu𝒯,uy,uy,uψ(y/x),uψ(y/x)
Lem.<ref>
ℛ,wu𝒯,uy,uψ(y/x),uψ(y/x)
PIH
ℛ,wu𝒯,uy,uψ(y/x)

ℛ𝒯,w∀ xψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch wv to u and obtain uv. Third, we merge the points v and u using Lemma <ref>. Fourth, we use Lemma <ref> to rename the (fresh) variable z to y. Fifth, we contract the labeled variable wy using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.








Finally, we can prove the admissibility of the  rule. As our proof proceeds via local transformations of proofs, we are in fact obtaining a cut-elimination procedure from it.














The  rule is admissible in  and .





 
We proceed by primary induction (PIH) on the structure of the cut formula, and secondary induction (SIH) on the sum of the height of proofs of the premises of the cut. Assume that we have proofs of the following form, with wu.



π_1
r_1
ℛ𝒯,wϕ
   
π_2
r_2
ℛ𝒯,uϕ





We prove that there is a derivation of ℛ𝒯 by case distinction on r_1 and r_2, the last rules applied in the above proofs. We focus on the most interesting cases – see Appendix <ref> for other cases.

(I) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v_0p(t⃗)_0,v_1p(t⃗) where v_0v_1. 
If v_1p(t⃗) is wϕ, then we have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,v_0p(t⃗),up(t⃗) where =_0,v_0p(t⃗). Given that v_0v_1 and v_1u, we can apply Lemma <ref> on the latter to obtain a proof of ℛ𝒯_0,v_0p(t⃗),v_0p(t⃗). Consequently, we obtain a proof of ℛ𝒯_0,v_0p(t⃗), i.e. of ℛ𝒯, using Lemma <ref>. 
If v_1p(t⃗) is not wϕ, then we have that ℛ𝒯 is of the form ℛ𝒯_0,v_0p(t⃗)_0,v_1p(t⃗) where v_0v_1. The latter is easily provable using the rule .








(IV) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0, vp(t⃗),wϕ and we have a proof of ℛ𝒯, vt⃗_0, vp(t⃗),wϕ. 
Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0, vp(t⃗). We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0, vp(t⃗),uϕ.
We can apply Lemma <ref> repetitively on the proof of the latter to obtain a proof of 
ℛ𝒯, vt⃗_0, vp(t⃗),uϕ which we call S, while preserving height. Then, we proceed as follows.



ℛ𝒯, vt⃗_0, vp(t⃗),wϕ
S
SIH
ℛ𝒯, vt⃗_0, vp(t⃗)

ℛ𝒯_0, vp(t⃗)


Note that the instance of SIH is justified as the sum of the heights of the proofs of its premises is smaller than the one of the initial cut.

(XI) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ,wϕ and we a have proof of ℛ,v_0v𝒯_0,v_0ψ,wϕ,v_0χ. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,vψχ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,vψχ,uϕ. 
We apply Lemma <ref> on the proof of the latter sequent to obtain a proof of ℛ,v_0v𝒯_0,v_0ψ,uϕ,v_0χ, which we call S. Thus, we proceed as follows.


ℛ,v_0v𝒯_0,v_0ψ,wϕ,v_0χ

S

SIH
ℛ,v_0v𝒯_0,v_0ψ,v_0χ

ℛ𝒯_0,vψχ


Note that the instance of SIH is justified as the sum of the heights of the proofs of the premises is smaller than the one of the initial cut.

(XII) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ and we have proofs of ℛ𝒯_0,vψχ,v_0ψ and ℛ𝒯,v_0χ_0,vψχ where v_0v.

If wϕ is not vψχ, then we have proofs of ℛ𝒯_1,vψχ,v_0ψ,wϕ, which we call S_0, and ℛ𝒯,v_0χ_1,vψχ,wϕ, which we call S_1, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,vψχ. Then, we proceed as follows where π is the first proof displayed.



S_0
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,uϕ_1,vψχ,v_0ψ
SIH
ℛ𝒯_1,vψχ,v_0ψ




π

S_1
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,v_0χ,uϕ_1,vψχ
SIH
ℛ𝒯,v_0χ_1,vψχ


ℛ𝒯_1,vψχ



If wϕ is vψχ, then we have proofs of ℛ𝒯,vψχ,v_0ψ and ℛ𝒯,v_0χ,vψχ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uψχ. In this case, we need to consider the shape of r_2. If uψχ is not principal in r_2, then we use the proof of ℛ𝒯,vψχ with SIH to cut uψχ from the premises of r_2, and then reapply r_2 to reach our goal. If uψχ is principal in r_2, then the premise of r_2 is of the shape ℛ,v_1u𝒯,v_1ψ,v_1χ. Then, we proceed as follows where π_0 and π_1 are (in this order) the first proofs given.



ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_0ψ,vψχ
ℛ𝒯,uψχ,v_0ψ
SIH
ℛ𝒯,v_0ψ






ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_0χ,vψχ
ℛ𝒯,uψχ,v_0χ
SIH
ℛ𝒯,v_0χ
Lem.<ref>
ℛ𝒯,v_0ψ,v_0χ






π_0

ℛ,v_1u𝒯,v_1ψ,v_1χ
Lem.<ref>
ℛ,v_1v_0𝒯,v_1ψ,v_1χ
Lem.<ref>
ℛ𝒯,v_0ψ,v_0χ
π_1
PIH
ℛ𝒯,v_0ψ


PIH
ℛ𝒯






















(XIV) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v∃ xψ and we have a proof of ℛ𝒯_0,v∃ xψ,vψ(t/x) where t is available for v.

If wϕ is not v∃ xψ, then we have a proof of ℛ𝒯_1,v∃ xψ,vψ(t/x),wϕ, which we call S, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,v∃ xψ. Then, we proceed as follows.



S

ℛ𝒯,uϕ_1,v∃ xψ
Lem.<ref>
ℛ𝒯,uϕ_1,v∃ xψ,vψ(t/x)

SIH
ℛ𝒯_1,v∃ xψ,vψ(t/x)

ℛ𝒯_1,v∃ xψ



If wϕ is v∃ xψ, then we have proof a of ℛ𝒯,v∃ xψ,vψ(t/x), and ℛ𝒯,uϕ is of the form ℛ𝒯,u∃ xψ. In this case, we need to consider the shape of r_2. If u∃ xψ is not principal in r_2, then we use the proof of ℛ𝒯,v∃ xψ with SIH to cut u∃ xψ from the premises of r_2, and then reapply r_2 to reach our goal. If u∃ xψ is principal in r_2, then the premise of r_2 is of the shape ℛ𝒯,vy,vψ(y/x) where y is fresh. Then, we proceed as follows where π is the first proof given and x_0,…,x_n are all the variables appearing in t.



ℛ𝒯,v∃ xψ,vψ(t/x)
ℛ𝒯,u∃ xψ
Lem.<ref>
ℛ𝒯,u∃ xψ,vψ(t/x)
SIH
ℛ𝒯,vψ(t/x)






π

ℛ𝒯,vy,vψ(y/x)
Lem.<ref>
ℛ𝒯,vx_0,…,vx_n,vψ(t/x)
Lem.<ref>
ℛ𝒯,vψ(t/x)

PIH
ℛ𝒯


Note that the step involving Lemma <ref> is justified as t is available for v, which implies that we can push all its variables to the original labels making t available for v.
















































































§ CONCLUSION AND FUTURE WORK



We have provided a proof-theoretical analysis of two extensions of propositional bi-intuitionistic logic to the first-order setting:

the logic of constant domains  and the logic of increasing domains . While obtaining a sound and complete proof system for the former is relatively straightforward, the same cannot be said for the latter. As we have shown in the introduction, there is an inherent difficulty in formalizing a Hilbert system for  without collapsing the domains into a constant domain, since the natural and obvious formalization must necessarily entail the quantifier shift axiom, which in turn implies a constant domain model. This may explain why the proof theory for bi-intuitionistic logic with non-constant domains has not been previously studied and remained an open problem until now. 


The design of our proof system for  started with the analysis of a typical proof of the quantifier shift axiom, and uncovered a previously overlooked dependency between the residuation principle (that is core to bi-intuitionistic logic) and the existence assumption on quantified variables. This led us to the introduction of the existence predicates into our formalization of the proof system  for the logic . The proof system  is formalized as a labeled polytree sequent calculus, extended with an implicit notion of existence predicate (i.e. domain atoms). We proved cut-elimination, soundness, and completeness of  with respect to . 

Completeness was unexpectedly tricky, due to the rather intricate interaction between the exclusion operator and the existence predicate.  The use of a labeled polytree sequent calculus 

allows one to interpret a labeled polytree sequent as a formula. We have used this property to prove, syntactically, that  is conservative over first-order intuitionistic logic. 

Future work. Our initial analysis indicates that there may be two other 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 ≤ u then D(u) ≤ 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,” that is dual to the existence predicate, suggested by Restall <cit.>. This non-existence predicate may play a similar (but dual) role to the existence predicate in .
The other extension is motivated from the proof theoretical perspective. As mentioned in Remark <ref>, it seems that one can obtain a subsystem of  without the domain-shfit rule  that satisfies cut-elimination. As we discussed in Section <ref>, the  rule is crucial to ensure the completeness of  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. 
































ACM-Reference-Format












§ SOUNDNESS AND COMPLETENESS PROOFS





 §.§ Soundness


<ref>[Soundness] Let  be a sequent. If  is derivable in  (), then  is (-)valid.



 We argue the claim by induction on the height of the given derivation and consider the  case as the  case is similar.

Base case. It is straightforward to show that any instance of  or  is valid; hence, we focus on  and show that any instance thereof is valid. Let us consider the following instance of , where wu due to the side condition imposed on , that is, there exist v_1, …, v_n∈() such that wRv_1, …, v_nRu ∈.




ℛ𝒯Γ,wp(t⃗)Δ,up(t⃗)


Let us suppose ℛ𝒯Γ,wp(t⃗)Δ,up(t⃗) is invalid; in other words, a model M = (W,≤,U,D,,), M-interpretation ι, and M-assignment  exist such that the following hold: ι(w) ≤ι(v_1), …, ι(v_n) ≤ι(u), M, ι(w), ⊩ p(t⃗), and M, ι(u), ⊮p(t⃗). By the monotonicity condition  (see  <ref>), it must be that M, ι(u), ⊩ p(t⃗), giving a contradiction. Thus, every instance of  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.

. Suppose ℛ𝒯, wp(t⃗) is invalid with t⃗ = t_1, …, t_n. Then, there exists a model M, M-interpretation ι, and M-assignment  such that M, ι(w), ⊩ p(t⃗). Therefore, ((t_1),…,(t_n)) ∈(w,p), and since (w,p) ⊆ D(w)^n, we have that (t_i) ∈ D(ι(w)) for 1 ≤ i ≤ n. By the  and  conditions, we know that M, ι, wt⃗. Therefore, ℛ𝒯, wt⃗, wp(t⃗) is invalid as well.

. If we assume that ℛ𝒯Γ,wϕψΔ is invalid, then there exists a model M, M-interpretation ι, and M-assignment  such that M, ι(w), ⊩ϕψ, implying that M, ι(w), ⊩ϕ and M, ι(w), ⊩ψ, showing that the premise ℛ𝒯Γ,wϕ,wψΔ is invalid as well.

. Let us suppose that ℛ𝒯ΓΔ,wϕψ is invalid. Then, there exists an model M, M-interpretation ι, and M-assignment  such that M, ι(w), ⊮ϕψ. Hence, either M, ι(w), ⊮ϕ or M, ι(w), ⊮ψ. In the first case, the left premise of  is invalid, and in the second case, the right premise of  is invalid.

. Similar to the  case.

. Similar to the  case.

. Assume ℛ𝒯Γ,wϕψΔ is invalid and wu, i.e. a sequence w v_1, …, v_n u of relational atoms exist in . By our assumption, there exists a model M, M-interpretation ι, and M-assignment such that ι(w) ≤ι(v_1), …, ι(v_n) ≤ι(u) and M, ι(w), ⊩ϕψ. Because M, ι(w), ⊩ϕψ and ≤ is transitive, we know that either M, ι(u), ⊮ϕ or M,ι(u),⊩ψ. In the first case, the left premise of  is invalid, and in the second case, the right premise of  is invalid.

. Assume that ℛ𝒯ΓΔ,wϕψ is invalid. Then, there exists a model M, an M-interpretation ι, and an M-assignment  such that M, ι(w), ⊮ϕψ. Hence, there exists a world u such that ι(w) ≤ u, M, u, ⊩ϕ, and M, u, ⊮ψ. Let ι'(v) = ι(v) for all labels v ≠ u and ι'(u) = u otherwise. Then, M, ι', and  falsify the premise of , showing it invalid.

. Similar to the  case above. 

. Similar to the  case above. 

. Suppose that = ℛ𝒯Γ,w∃ xϕΔ is invalid. Then, there exists a model M, an M-interpretation ι, and an M-assignment  such that M, ι(w), ⊩∃ x ϕ. Therefore, there exists an ∈ D(ι(w)) such that M, ι(w), [/y] ⊩ϕ(y/x) with y not occurring in . Then, as y is fresh, M, ι, and [/y] falsify the premise of , showing it invalid.


. Suppose that = ℛ𝒯ΓΔ,w∃ xϕ is invalid. Then, there exists a model M, and M-interpretation ι, and M-assignment such that M, ι(w), ⊮∃ x ϕ. By the side condition on , we know that tX_w,, meaning there exist labels u_1, …, u_n∈() such that u_1 : x_1, …, u_n : x_n∈, t = {x_1, …, x_n}, and u_1w, …, u_nw. It follows that ι(u_1) ≤ι(w), …, ι(u_n) ≤ι(w) and (x_1) ∈ D(ι(u_1)), …, (x_n) ∈ D(ι(u_n)). By the increasing domain condition , we have that (x_1) ∈ D(ι(w)), …, (x_n) ∈ D(ι(w)). Therefore, by the  and  conditions, we know that (t) ∈ D(ι(w)), showing that M, ι(w), ⊮ϕ(t/x), and thus, the premise is invalid.

. Suppose that = ℛ𝒯,w∀ xϕ is invalid. Then, there exists a model M, and M-interpretation ι, and M-assignment  such that M, ι(w), ⊩∀ x ϕ. By the side condition on , we know that wu and tX_w,. By the latter fact, there exist labels v_1, …, v_n∈() such that v_1 : x_1, …, v_n : x_n∈, t = {x_1, …, x_n}, and v_1w, …, v_nw. It follows that ι(v_1) ≤ι(w), …, ι(v_n) ≤ι(w) and (x_1) ∈ D(ι(v_1)), …, (x_n) ∈ D(ι(v_n)). By the increasing domain condition , we have that (x_1) ∈ D(ι(w)), …, (x_n) ∈ D(ι(w)). Therefore, by the  and  conditions and our assumption, we know that (t) ∈ D(ι(w)), showing that M, ι(w), ⊩ϕ(t/x). By the fact that wu, we know ι(w) ≤ι(u) and (t) ∈ D(ι(u)), showing that M, ι(u), ⊩ϕ(t/x) by  <ref>. Thus, the premise is invalid.

. Let us assume that ℛ𝒯ΓΔ,w∀ xϕ is invalid. Then, there exists a model M, an M-interpretation ι, and an M-assignment  such that M, ι(w), ⊮∀ x ϕ. Thus, there exists a world u ∈ W such that ι(w) ≤ u, ∈ D(u), and M, u, [/y] ⊮ϕ(y/x). We define '(v) = (v) if v ≠ u and '(u) = u. Then, M, ι', and [/y] falsify the premise ℛ,w≤ u𝒯,uyΓΔ,uϕ(y/x), showing it invalid.







 §.§ Completeness


We prove the cut-free completeness of  by showing that if a sequent of the form w : x⃗ w : ϕ(x⃗) is not provable, then a counter-model can be constructed witnessing the invalidity of the sequent. We focus on the proof for  as it is more involved than the similar proof for . Our proof 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  with the children nodes corresponding to the premises. We remark that a proof in  is a finite pseudo-derivation where all top sequents are instances of , , or . A branch  is defined to be a maximal path of sequents through a pseudo-derivation, starting from the conclusion. The following lemma is useful in our proof of completeness.

<ref> Let ∈{, }. For each i ∈{0,1,2}, let _i = _i, _i, _i_i be a sequent.



  * If wu holds for the conclusion of a rule (r) in (), then wu holds for the premises of (r);


  * If w : p(t⃗) ∈_0, _0 and _0 is the conclusion of a rule (r) in () with _1 (and _2) the premise(s) of (r), then w : p(t⃗) ∈_1, _1 (and w : p(t⃗) ∈_2, _2, resp.);


  * If w : x ∈_0 and _0 is the conclusion of a rule (r) in () with _1 (and _2) the premise(s) of (r), then w : x∈_1 (and w : x ∈_2, resp.).




 Each claim can be seen to hold by inspecting the rules of ().


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

 
<ref>  If w : x⃗ w : ϕ(x⃗) is (-)valid, then w : x⃗ w : ϕ(x⃗) is derivable in  ().



 We assume that = w : x⃗ w : ϕ(x⃗) is not derivable in  and show that a model M can be defined which witnesses that  is invalid. To prove this, we first define a proof-search procedure  that bottom-up applies rules from  to w : x⃗ w : ϕ(x⃗). Second, we show how an M can be extracted from failed proof-search. We now describe the proof-search procedure  and let ≺ be a well-founded, strict linear order over the set  of terms.


. Let us take w : x⃗ w : ϕ(x⃗) as input and continue to the next step.


, , and . Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we halt the computation of  on each branch _i where _i is of the form , , or . If  is halted on each branch _i, then  returns  because a proof of the input has been constructed. However, if  did not halt on each branch _i with 1 ≤ i ≤ n, then let _j_1, …, _j_k be the remaining branches for which  did not halt. For each such branch, copy the top sequent above itself, and continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = ℛ𝒯, w_1 : p_1(t⃗_1), …, w_ℓ : p_ℓ(t⃗_ℓ)

where all atomic input formulae are displayed in _k+1 above. We successively consider each atomic input formula and bottom-up apply , yielding a branch extending _k+1 with a top sequent saturated under  applications. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , , w_1 : ϕ_1ψ_1, …, w_m : ϕ_mψ_m

 where all disjunctive formulae w_i : ϕ_iψ_i are displayed in _k+1 above. We consider each labeled formula w_i : ϕ_iψ_i in turn, and bottom-up apply the  rule, which gives 2^m new branches extending _k+1 such that each branch has a top sequent of the form _k+1 = , , , w_1 : χ_1…, w_m : χ_m with χ_i∈{ϕ_i,ψ_i} and 1 ≤ i ≤ n. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.
 
. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , ,  w_1 : ϕ_1ψ_1, …, w_m : ϕ_mψ_m,

 where all disjunctive formulae w_i : ϕ_iψ_i are displayed in _k+1 above. We consider each labeled formula w_i : ϕ_iψ_i in turn, and bottom-up apply the  rule. These  rule applications extend _k+1 such that , ,  w_1 : ϕ_1, w_1 :  ψ_1, …, w_m : ϕ_m, w_m : ψ_m, is now the top sequent of the branch. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.
 


. Similar to the  case above.



. Similar to the  case above.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , , w_1 : ϕ_1ψ_1, …, w_m : ϕ_mψ_m

 where all implicational formulae w_i : ϕ_iψ_i are displayed in _k+1 above. We consider each formula w_i : ϕ_iψ_i in turn, and bottom-up apply the  rule. Let w_ℓ + 1 : ϕ_ℓ+1ψ_ℓ+1 be the current formula under consideration, and assume that w_1 : ϕ_1ψ_1, …, w_ℓ : ϕ_ℓψ_ℓ have already been considered. For every label u such that w_ℓ + 1u, bottom-up apply the  rule. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , ,  w_1 : ϕ_1ψ_1, …, w_m : ϕ_mψ_m,

where all implicational formulae w_i : ϕ_iψ_i are displayed in _k+1 above. We consider each formula w_i : ϕ_iψ_i in turn, and bottom-up apply the  rule. These  rule applications extend _k+1 such that

    , w_1 u_1, …, w_m u_m, , , u_1 : ϕ_1, …, u_m : ϕ_m u_1 : ψ_1, …, u_m : ψ_m,

is now the top sequent of the branch with u_1, …, u_m fresh. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.



. Similar to the  case above.



. Similar to the  case above.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , , w_1 : ∃ x_1ϕ_1, …, w_m : ∃ x_mϕ_m⊢

where all existential input formulae w_i : ∃ x_iϕ_i are displayed in _k+1 above. We consider each formula w_i : ∃ x_iϕ_i in turn, and bottom-up apply the  rule. These  rule applications extend _k+1 such that

    , , w_1 : y_1, …, w_m : y_m, , w_1 : ϕ_1(y_1/x_1), …, w_n : ϕ_m(y_m/x_m) ⊢

is now the top sequent of the branch with y_1,…,y_m fresh variables. After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.



. Suppose _1, …, _n are all branches occurring in the current pseudo-derivation and let _1, …, _n be the top sequents of each respective branch. For each 1 ≤ i ≤ n, we consider _i and extend the branch with bottom-up applications of  rules. Let _k+1 be the current branch under consideration, and assume that _1,…,_k have already been considered. We assume that the top sequent in _k+1 is of the form

    _k+1 = , , ⊢ w_1 : ∃ x_1ϕ_1, …, w_m : ∃ x_mϕ_m,

 where all existential formulae w_i : ∃ x_iϕ_i are displayed in _k+1 above. We consider each labeled formula w_m : ∃ x_mϕ_i in turn, and bottom-up apply the  rule. Let w_ℓ+1 : ∃ x_ℓ+1ϕ_ℓ+1 be the current formula under consideration, and assume that w_1 : ∃ x_1ϕ_1, …, w_ℓ : ∃ x_ℓϕ_ℓ have already been considered. Recall that ≺ is a well-founded, strict linear order over the set  of terms. Choose the ≺-minimal term t ∈(X_w_ℓ+1) that has yet to be picked to instantiate w_ℓ+1 : ∃ x_ℓ+1ϕ_ℓ+1 and bottom-up apply the  rule, thus adding w_ℓ+1 : ϕ_ℓ+1(t/x_ℓ+1 ). After these operations have been performed for each branch _i with 1 ≤ i ≤ n, we continue to the next step.
 
 

. Similar to the  case above.



. Similar to the  and  cases above.



This concludes the description of .

 
We now argue that if  does not return , then a model M, M-interpretation ι, and M-assignment  can be defined such that M, ι,. If  halts, i.e.  returns , then a proof of  may be obtained by `contracting'  all redundant inferences from the `, , and ' step of , which contradicts our assumption. Therefore,  does not halt, that is,  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 . We define a model M = (W,≤,U,D,,) by means of this branch.

First, let us define the following (multi)sets, all of which are obtained by taking the union of each (multi)set of relational atoms, domain atoms, antecedent labeled formulae, and consequent labeled formulae (resp.) occurring within a sequent in :

    ^ = ⋃_(, , ) ∈    ^ = ⋃_(, , ) ∈    ^ = ⋃_(, , ) ∈    ^ = ⋃_(, , ) ∈







  * u ∈ W u ∈(^,^, ^, ^);


  * ≤ =  {(u,v)  |  uRv ∈}^* where * denotes the reflexive-transitive closure;


  * t ∈ U there exists a label u ∈(^,^, ^, ^) such that t ∈(X_u);


  * t ∈ D(u) t ∈(X_u);




  * (t_1, …, t_n) ∈(u,p) v,u ∈(^,^, ^, ^), v ↠^*_^ u, and v : p(t_1, …, t_n) ∈^.



We now verify that M is indeed a model. Observe that W ≠∅ since w ∈ W by definition and the relation ≤ is reflexive and transitive by definition. Furthermore, by definition, D(u) ⊆ U for each u ∈ W and U = ⋃_u ∈ W D(u). Also, since our language contains at least one constant symbol a (see  <ref>), we know that a ∈(X_u) for each u ∈ W, i.e. for each u ∈ W, D(u) ≠∅. Let us now argue that M satisfies the increasing domain condition , and assume u,v ∈ W, t ∈ D(u), and u ≤ v. Since t ∈ D(u), t ∈(X_u), and since u ≤ v, we know that u ↠^*_^ v. It follows that (X_u) ⊆(X_v) by  <ref>, showing that t ∈(X_v), and thus, t ∈ D(v). It is simple to confirm that  satisfies the  and  conditions as t ∈ D(u) t ∈(X_u), and (X_u) contains every constant and is closed under the formation of terms by definition. For each n-ary predicate p and world u ∈ W, (p,u) ⊆ D(u)^n. To show this, suppose that (t_1, …, t_n) ∈(p,u). Then, there exists a label v ∈(^,^, ^, ^) such that v ↠^*_^ u, and v : p(t_1, …, t_n) = v : p(t⃗) ∈^. By the  step of , we know that w : t⃗∈^. It follows that t_1, …, t_n∈(X_u), implying that (t_1, …, t_n) ∈ D(u)^n. Finally, we argue that M satisfies the monotonicity condition , and therefore, we assume u,v ∈ W, u ≤ v, and (t_1, …, t_n) ∈(p,u). Since u ≤ v, we know that there exist w_1, …, w_n∈(^,^, ^, ^) such that uRw_1, …, w_nRv, implying that u ↠^*_^ v. Since (t_1, …, t_n) ∈(p,u), there exists a v' such that v' ↠^*_^ u and v' : p(t_1, …, t_n) ∈^. Hence, v' ↠^*_^ v because v' ↠^*_^ u and u ↠^*_^ v, which shows that (t_1, …, t_n) ∈(p,v).
 
We have now confirmed that M is indeed a model. Let us define  to be the M-assignment mapping every variable in U to itself and every variable in ∖ U arbitrarily. To finish the proof of completeness, we now argue the following by mutual induction on the complexity of ψ: (1) if u : ψ∈^, then M,u,⊩ψ, and (2) if u : ψ∈^, then M,u,⊮ψ. We argue the cases where ψ is of the form p(t_1, …, t_n) or ∀ x χ, and omit the remaining cases as they are straightforward or similar.
 



  * u : p(t_1,…,t_n) ∈^. In this case, (t_1,…,t_n) ∈(p,u) by the definition of , implying that M,u,⊩ p(t_1,…,t_n).


  * u : p(t_1,…,t_n) ∈^. Observe that if a label v ∈(^,^, ^, ^) exists such that v ↠^*_^ u and v : p(t_1,…,t_n) ∈^, then due to the `, , and ' step of ,  would be finite. However, as this is not the case, it must be that no label v  ∈(^,^, ^, ^) exists such that v ↠^*_^ u and v : p(t_1,…,t_n) ∈^, showing that (t_1, …, t_n) ∉(u,p), i.e. M,u,⊮p(t_1,…,t_n).



  * u : ∀ x χ∈^. Suppose v ∈ W, t ∈ D(v), and u ≤ v. By the assumption that t ∈ D(v), we know that tX_u, holds for some sequent = ,, in . Let us suppose w.l.o.g. that  is the first such sequent in  for which this holds. By  <ref>, it follows that tX_w',' holds for every sequent = ', ', ' ' above  in . By the assumption that u ≤ v, we know that u ↠^*_^ v. Hence, at some point the  step of  will be applicable at or above  in , meaning v : χ(t/x) ∈^. By IH, we have that M,v,⊩χ(t/x), from which it follows that M,w,⊩∀ x χ by our assumptions.



  * u : ∀ x χ∈^. Due to the  step of , a  sequent of the form ℛ,uv𝒯,vy,vχ(y/x) with v and y fresh must occur in . By the definition of ≤ and D(v), as well as  <ref>, it follows that u ≤ v and y ∈ D(v). By IH and the definition of , M,v,⊮χ(y/x), and so, M,u,⊮∀ x χ.



 Let ι to be the M-interpretation such that ι(u) = u for u ∈ W and ι(v) ∈ W for v ∉W. By the proof above, M,ι,w : x⃗ w : ϕ(x⃗), showing that if a  sequent of the form w : x⃗ w : ϕ(x⃗) is not derivable in , then it is invalid, that is, every valid  sequent of the form w : x⃗ w : ϕ(x⃗) is provable in .

 
 
 
 
 
 
 
 
 






§ ADMISSIBILITY AND INVERTIBILITY PROOFS



<ref>[]
Let ∈{, }. The rules  and  are hp-admissible in ().



By changing wv to uv, we are effectively moving the branch rooted in v from w to u: we move from the left diagram to the right one below.




(0,0) node[point] (w0) [label=below:w];
(1.5,0) node[point](w1)[label=below:u];
(0.5,0.4) node[point](w2)[label=left:v];
(2.25,0) node ⇒;

[->] (w0) edge[dashed] (w1);
[->] (w0) edge (w2);
[-] (w2) edge[dashed] (1.1,0.3);
[-] (w2) edge[dashed] (1,0.8);
[-] (1.1,0.3) edge[dashed] (1,0.8);

(2.25,0) node ⇒;

(3,0) node[point] (w0) [label=below:w];
(4.5,0) node[point](w1)[label=below:u];
(5,0.4) node[point](w2)[label=left:v];

[->] (w0) edge[dashed] (w1);
[->] (w1) edge (w2);
[-] (w2) edge[dashed] (5.6,0.3);
[-] (w2) edge[dashed] (5.5,0.8);
[-] (5.6,0.3) edge[dashed] (5.5,0.8);




The crucial observation is that given that wu, this moving of the branch only extends the reachability relation: we have that for all w' and w”, if w'w” in ℛ,wv then w'w” in ℛ,uv. Consequently, we can see that  only expands reachability, and thus does not violate the reachability or availability conditions of any of the rules. Freshness is also not impacted. So, in all cases we can simply apply the induction hypothesis on the premises, and then the rule.

A similar argument can be provided for , where we move from the left diagram to the right one below.




(0,0) node[point] (w0) [label=above:w];
(1.5,0) node[point](w1)[label=above:u];
(1,-0.4) node[point](w2)[label=below:v];

[->] (w0) edge[dashed] (w1);
[->] (w2) edge (w1);
[-] (w2) edge[dashed] (0.4,-0.3);
[-] (w2) edge[dashed] (0.5,-0.8);
[-] (0.4,-0.3) edge[dashed] (0.5,-0.8);

(2.25,0) node ⇒;

(4,0) node[point] (w0) [label=above:w];
(5.5,0) node[point](w1)[label=above:u];
(3.5,-0.4) node[point](w2)[label=below:v];

[->] (w0) edge[dashed] (w1);
[->] (w2) edge (w0);
[-] (w2) edge[dashed] (2.9,-0.3);
[-] (w2) edge[dashed] (3,-0.8);
[-] (2.9,-0.3) edge[dashed] (3,-0.8);





























<ref>
Let ∈{, }. The rules  and  are hp-admissible in ().


Straightforward by induction on derivations. 


<ref>
Let ∈{, }. The  rule is hp-admissible in ().






This lemma is straightforwardly proved by induction on the height of proofs. To realize that we can simply apply the induction hypothesis on the premises of the rules, and then reapply the rule, it suffices to note that the deletion of ux does not impact reachability, freshness or even availability given that wu. So, any rule is reapplicable once we use the induction hypothesis.


<ref>
Let ∈{, }. The  rule is hp-admissible in ().



We reason by induction on the height of proofs, and consider the last rule applied. 

Obviously, the propositional rules are not impacted by the substitution. So, for these rules we simply need to apply the induction hypothesis on the premises of the rule, and then reapply the rule.

The rule  is treated straightforwardly: we apply the induction hypothesis on the proof of 
ℛ𝒯, wt⃗'⃗, wp(t⃗'⃗) to obtain a proof of ℛ𝒯'(t/x), wp(t⃗'⃗(⃗t⃗/⃗x⃗)⃗)(t/x) where 𝒯'=(𝒯, wt⃗'⃗)(t/x). Note that 𝒯' is such that any domain atom ux is replaced by ux_0,…,ux_m where x_0,…,x_m are the variables appearing in t. Consequently, all the variables appearing in the terms t⃗'⃗(⃗t⃗/⃗x⃗)⃗ are labeled by w in 𝒯'. Consequently, we can apply the rule  to obtain a proof of our goal, i.e. ℛ𝒯(t/x)(t/x), w : p(t⃗'⃗(⃗t⃗/⃗x⃗)⃗(t/x).

The cases of rules for quantifiers deserve more attention. We show the cases of  and , as the other rules can be treated in a similar way.

: we need to obtain a proof of ℛ(t/x)𝒯(t/x)Γ(t/x),w(∃ zϕ)(t/x)Δ(t/x), where we can safely assume that z is different from x and any variable appearing in t. First, we apply the induction hypothesis on the proof of ℛ𝒯,wyΓ,wϕ(y/z)Δ, the premise of the rule, to obtain a proof of no greater height of ℛ𝒯(y'/y),wy(y'/y)Γ(y'/y),wϕ(y/z)(y'/y)Δ(y'/y) with y' fresh and not appearing in t or x. Given that y was fresh, we have a proof of no greater height the sequent ℛ𝒯,wy'Γ,wϕ(y'/z)Δ. We can apply the induction hypothesis again here to obtain a proof of no greater height of ℛ𝒯(t/x),wy'(t/x)Γ(t/x),wϕ(y'/z)(t/x)Δ(t/x). Because of our choice of y', we have that the latter sequent is equal to ℛ𝒯(t/x),wy'Γ(t/x),wϕ(t/x)(y'/z)Δ(t/x). Thus, we can reapply the rule  on the latter to obtain a proof of ℛ(t/x)𝒯(t/x)Γ(t/x),w(∃ zϕ)(t/x)Δ(t/x).

: we need a proof of ℛ𝒯(t/x)Γ(t/x),w(∀ zϕ)(t/x)Δ(t/x) of no greater height, where we can safely assume that z is different from x and any variable appearing in t. We apply the induction hypothesis on the proof of ℛ𝒯Γ,w∀ zϕ,uϕ(t'/z)Δ, the premise of the rule, to obtain a proof of no greater height of ℛ𝒯(t/x)Γ,w(∀ zϕ)(t/x),uϕ(t'/z)(t/x)Δ(t/x). Note that the latter is equal to ℛ𝒯(t/x)Γ,w(∀ zϕ)(t/x),uϕ(t'(t/x)/z)Δ(t/x). Clearly, in this sequent we still have that wu. In addition to that, we have that t'(t/x) is available to u. We can argue this point by a case distinction on the presence or not of x in t'. If x does not appear in t', then t'(t/x)=t', which is available for u as initially given. If x does appear in t', then we have that there must be a v such that vx∈ and vu else t' would not be available in u. Consequently, we have that vx is replaced by {vx'| x' appears in t} in (t/x). This makes t'(t/x) available for u. So, as wu and t'(t/x) is available to u we can apply  to obtain a proof of ℛ𝒯(t/x)Γ(t/x),w(∀ zϕ)(t/x)Δ(t/x) of no greater height than the proof initially considered.



<ref>
Let ∈{, }. The  rule is hp-admissible in ().



The only problems that the addition of labeled formulae to a sequent can create have to do with the condition of freshness of a variable or a label. To make sure that there is no violation of these conditions, we can use Lemma <ref> and our view that isomorphic sequents are identical to avoid any overlap with these critical variables or labels. Thus, for all rules we can simply use these lemmas on the premises if needed, apply the induction hypothesis on the potentially modified premises and then reapply the rule.


<ref>
Let ∈{, }. The  rule is hp-admissible in ().



The addition of a further labeled variable can only alter freshness of variable conditions. So, we only need to pay attention to the rules involving such conditions and apply Lemma <ref> before applying the induction hypothesis.


<ref>
Let ∈{, }. The rules  and  are hp-admissible in ().



We focus on  as  can be treated dually. By inspecting the rules, one can see that the deletion of w in the consequent of a sequent impacts the application of no rule. In particular, this deletion does not alter the reachability, availability or freshness conditions. As a consequence, a straightforward induction on the structure of the proof is sufficient to prove this statement: in the inductive cases, apply the induction hypothesis on the last rule applied, and then the rule.



<ref>
Let ∈{, }. The  rule is hp-admissible in ().



We reason by induction on the height of proofs, and consider the last rule applied.

Obviously, the “local" propositional rules (which do not involve a condition on reachability) and  are not impacted by the modification of the label, whether the principal formula is labeled by one of the labels under focus or not. For  we easily reach our goal by applying the induction hypothesis on the premise and then the rule as the principal formula cannot be the one under focus.
However, the other non-local rules require more care.

: then we have a proof of ℛ𝒯Γ,w'p(t⃗)Δ,u'p(t⃗) where w'u'. We proceed by case distinction on the equality between w and u'. If w=u', then we need to prove ℛ𝒯Γ,w'p(t⃗)Δ,up(t⃗). Now, note that we have w'u' and u'u by assumption as w=u'. Consequently, we have that w'u by transitivity. An application of the rule  leads us to our goal. If w≠ u', then we can simply reapply the rule as the two labeled formulae are not modified.

: then the last rule has the following form.


ℛ,w'u'𝒯,u'ϕ,u'ψ

ℛ𝒯,w'ϕψ


If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
As we have wu and not uu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,uu'𝒯,u'ϕ,u'ψ. Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,uϕψ of the adequate height. If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
 
: then the last rule has the following form.



ℛ𝒯,u'ϕψ,w'ϕ
ℛ𝒯,w'ψ,u'ϕψ

ℛ𝒯,u'ϕψ



If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w=u'.
As we have wu and w'w by the rule application, we get w'u by transitivity. This allows us to apply the induction hypothesis in both premises to obtain proofs of ℛ𝒯,uϕψ,w'ϕ and ℛ𝒯,w'ψ,uϕψ. Then, it suffices to reapply the rule to obtain a proof of adequate height of ℛ𝒯,uϕψ.

Let us now turn to the first order rules. For all the rules for quantifiers where the modified labeled formula cannot be principal, i.e. for  and , it suffices to apply the induction hypothesis in the premise, and then reapply the rule. So, we are left with the rules  and .

: then the last rule has the following form.


ℛ,w'u'𝒯,u'y,u'ϕ(y/x)

ℛ𝒯,w'∀ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
As we have wu and not uu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,uu'𝒯,u'y,u'ϕ(y/x). Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,u∀ xϕ of the adequate height. 

: then the last rule has the following form.


ℛ𝒯,w'∃ xϕ,w'ϕ(t/x)

ℛ𝒯,w'∃ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that w'=w.
Then, we can apply the induction hypothesis on the premise twice to obtain a proof of ℛ𝒯,u∃ xϕ,uϕ(t/x). Note that in this case, we have that t∈(X_u) as wu. So, we can apply the rule  to reach our goal.















<ref>
Let ∈{, }. The  rule is hp-admissible in ().



The proof of this lemma is very similar in spirit to the proof of Lemma <ref>. Dually, the problematic rules here are , , ,  and .

: then the last rule has the following form where u:p(t⃗) is the principal formula. 



π_1
, , Γ, u:p(t⃗),  u: t⃗Δ

, , Γ, u:p(t⃗) Δ



Applying the induction hypothesis to π_1, we get a proof π_2 of 
, , Γ, w:p(t⃗), u:t⃗Δ with the same height, from which we can obtain a proof of , , Γ, w : p(t⃗) Δ as follows:



, , Γ, w:p(t⃗), u:t⃗Δ

, , Γ, w:p(t⃗), w:t⃗, u:t⃗Δ

, , Γ, w:p(t⃗), w:t⃗Δ

, , Γ, w:p(t⃗) Δ



The instance of  above is applicable because wu. The hp-admissibility of  in this case then follows from Lemma <ref> and Lemma <ref>. 

: then the last rule has the following form.



ℛ𝒯,w'ϕψ,u'ϕ
ℛ𝒯,w'ϕψ,u'ψ

ℛ𝒯,w'ϕψ



If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
As we have wu and uu' by the rule application, we get wu' by transitivity. This allows us to apply the induction hypothesis in both premises to obtain proofs of ℛ𝒯,wϕψ,u'ϕ and ℛ𝒯,wϕψ,u'ψ. Then, it suffices to reapply the rule to obtain a proof of adequate height of ℛ𝒯,wϕψ.

: then the last rule has the following form.


ℛ,u'w'𝒯,u'ϕ,u'ψ

ℛ𝒯,w'ϕψ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
As we have wu and not wu' because of the freshness of u', we can use Lemma <ref> to obtain a proof of ℛ,u'w𝒯,u'ϕ,u'ψ. Then, it suffices to apply the rule  to reach a proof of ℛ𝒯,wϕψ of the adequate height. 


: then the last rule has the following form.


ℛ𝒯,w'y,w'ϕ(y/x)

ℛ𝒯,w'∃ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
First, we can apply Lemma <ref> on the premise to obtain a proof of ℛ𝒯,wy,uy,uϕ(y/x). Then, as wu we apply Lemma <ref> to obtain a proof of ℛ𝒯,wy,uϕ(y/x). Finally, as all previous lemmas preserve height, it suffices to apply the induction hypothesis on this proof to obtain a proof of ℛ𝒯,wy,wϕ(y/x). A simple application of the rule  reaches our goal.

: then the last rule has the following form.


ℛ𝒯,w'∀ xϕ,u'ϕ(t/x)

ℛ𝒯,w'∀ xϕ


If the principal formula is not the one we intend to modify, then we can use the induction hypothesis in the premise and reapply the rule.
If the principal formula is the labeled formula we intend to modify, then we have that u=w'.
Then, we can apply the induction hypothesis on the premise to obtain a proof of ℛ𝒯,w∀ xϕ,u'ϕ(t/x). Note that we have wu' as wu and uu'. So, we can apply the rule  to reach our goal.














<ref>
Let ∈{, }. The rules , , ,  are hp-invertible in ().



For : given a proof of ℛ𝒯Γ,wϕψΔ, we can simply use height-preserving internal weakening (Lemma <ref>) to obtain proofs of ℛ𝒯Γ,wϕψΔ,uϕ and ℛ𝒯Γ,wϕψ,uψΔ of less or equal height.

For : given a proof of ℛ𝒯ΓΔ,w∃ xϕ, we can simply use height-preserving internal weakening (Lemma <ref>) to obtain a proof of ℛ𝒯ΓΔ,w∃ xϕ,wϕ(t/x) of less or equal height.



<ref>
Let ∈{, }. The rules  and  are hp-admissible in ().



We simultaneously prove the hp-admissibility of the two rules. We reason by primary induction on the structure of ϕ (PIH) and secondary induction on the  height of derivations (SIH). In each case, we consider the last rule applied, and whether ϕ is principal in that rule. We omit the cases of initial rules as they are straightforward.



We start by the rule . If ϕ is not principal in the last rule, then we proceed as usual by applying SIH on ϕ in the premises of the rule, and then the rule. Note that all rules which have their principal formula on the right fall in this category.

If ϕ is principal, then for the rules  and  we use the invertibility lemmas proved previously, jointly with PIH. For the rules in which the principal formula is not deleted in the premises, i.e.  and , we simply use SIH to contract the principal formula. We give the case of  as an example.

: then the last rule has the following form, where ϕ=χψ.



ℛ𝒯,wχψ,wχψ,uχ
ℛ𝒯,wχψ,wχψ,uψ

ℛ𝒯,wχψ,wχψ



We can simply apply SIH on both premises to obtain proofs of ℛ𝒯,wχψ,uχ and ℛ𝒯,wχψ,uψ. A simple application of the  gives us the desired result.

Finally, we are left with the rules  and  which we treat individually.

: then the last rule has the following form, where ϕ=χψ.


ℛ,uw𝒯,uχ,wχψ,uψ

ℛ𝒯,wχψ,wχψ


Then, we proceed as follows.


ℛ,uw𝒯,uχ,wχψ,uψ
Lem.<ref>
ℛ,uw,vw𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,uw,vu𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,uw𝒯,uχ,uχ,uψ,uψ
PIH
ℛ,uw𝒯,uχ,uψ

ℛ𝒯,wχψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch vw to u and obtain vu. Third, we merge the points v and u using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.

: then the last rule has the following form, where ϕ=∃ xψ.


ℛ𝒯,wy,wψ(y/x),w∃ xψ

ℛ𝒯,w∃ xψ,w∃ xψ


Then, we proceed as follows.


ℛ𝒯,wy,wψ(y/x),w∃ xψ
Lem.<ref>
ℛ𝒯,wy,wz,wψ(y/x),wψ(z/x)
Lem.<ref>
ℛ𝒯,wy,wy,wψ(y/x),wψ(y/x)
Lem.<ref>
ℛ𝒯,wy,wψ(y/x),wψ(y/x)
PIH
ℛ𝒯,wy,wψ(y/x)

ℛ𝒯,w∃ xψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to rename the (fresh) variable z to y. Third, we contract the labeled variable wy using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.



Now, let us turn to the rule . If ϕ is not principal in the last rule, then we proceed as usual by applying SIH on ϕ in the premises of the rule, and then the rule. Note that this time, all rules which have their principal formula on the left fall in this category.

If ϕ is principal, then for the rules  and  we use the invertibility lemmas proved previously, jointly with PIH. For the rules in which the principal formula is not deleted in the premises, i.e. ,  and , we simply use SIH to contract the principal formula. We give the case of  as an example.

: then the last rule has the following form, where ϕ=χψ.



ℛ𝒯,wχψ,wχψ,uχ
ℛ𝒯,uψ,wχψ,wχψ

ℛ𝒯,wχψ,wχψ



We can simply apply SIH on both premises to obtain proofs of ℛ𝒯,wχψ,uχ and ℛ𝒯,uψ,wχψ. A simple application of the rule gives us the desired result.

Finally, we are left with the rules  and  which we treat individually.

: then the last rule has the following form, where ϕ=χψ.


ℛ,wu𝒯,uχ,uψ,wχψ

ℛ𝒯,wχψ,wχψ


Then, we proceed as follows.


ℛ,wu𝒯,uχ,uψ,wχψ
Lem.<ref>
ℛ,wu,wv𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,wu,uv𝒯,uχ,vχ,uψ,vψ
Lem.<ref>
ℛ,wu𝒯,uχ,uχ,uψ,uψ
PIH
ℛ,wu𝒯,uχ,uψ

ℛ𝒯,wχψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch wv to u and obtain uv. Third, we merge the points v and u using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.

: then the last rule has the following form, where ϕ=∀ xψ.


ℛ,wu𝒯,uy,uψ(y/x),w∀ xψ

ℛ𝒯,w∀ xψ,w∀ xψ


Then, we proceed as follows.


ℛ,wu𝒯,uy,uψ(y/x),w∀ xψ
Lem.<ref>
ℛ,wu,wv𝒯,uy,vz,uψ(y/x),vψ(z/x)
Lem.<ref>
ℛ,wu,uv𝒯,uy,vz,uψ(y/x),vψ(z/x)
Lem.<ref>
ℛ,wu𝒯,uy,uz,uψ(y/x),uψ(z/x)
Lem.<ref>
ℛ,wu𝒯,uy,uy,uψ(y/x),uψ(y/x)
Lem.<ref>
ℛ,wu𝒯,uy,uψ(y/x),uψ(y/x)
PIH
ℛ,wu𝒯,uy,uψ(y/x)

ℛ𝒯,w∀ xψ


First, we use the invertibility Lemma <ref> on the initial premise. Second, we use Lemma <ref> to push the branch wv to u and obtain uv. Third, we merge the points v and u using Lemma <ref>. Fourth, we use Lemma <ref> to rename the (fresh) variable z to y. Fifth, we contract the labeled variable wy using Lemma <ref>. Once this is done, we can apply the induction hypothesis PIH and reapply the rule.



<ref>[Cut-elimination]
The  rule is admissible in  and .





 
We proceed by primary induction (PIH) on the structure of the cut formula, and secondary induction (SIH) on the sum of the height of proofs of the premises of the cut. Assume that we have proofs of the following form, with wu.



π_1
r_1
ℛ𝒯,wϕ
   
π_2
r_2
ℛ𝒯,uϕ





We prove that there is a derivation of ℛ𝒯 by case distinction on r_1 and r_2, the last rules applied in the above proofs.

(I) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v_0p(t⃗)_0,v_1p(t⃗) where v_0v_1. 
If v_1p(t⃗) is wϕ, then we have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,v_0p(t⃗),up(t⃗) where =_0,v_0p(t⃗). Given that v_0v_1 and v_1u, we can apply Lemma <ref> on the latter to obtain a proof of ℛ𝒯_0,v_0p(t⃗),v_0p(t⃗). Consequently, we obtain a proof of ℛ𝒯_0,v_0p(t⃗), i.e. of ℛ𝒯, using Lemma <ref>. 
If v_1p(t⃗) is not wϕ, then we have that ℛ𝒯 is of the form ℛ𝒯_0,v_0p(t⃗)_0,v_1p(t⃗) where v_0v_1. The latter is easily provable using the rule .

(II) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v,wϕ where =_0,v. Consequently, we know that that ℛ𝒯 is of the form ℛ𝒯_0,v. We straightforwardly prove the latter via a single application of .

(III) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v⊤. If wϕ is v⊤, then we have that ℛ𝒯,uϕ is of the form ℛ𝒯,u⊤. Thus, we obtain a proof of ℛ𝒯 using Lemma <ref>. If wϕ is not v⊤, then we have that ℛ𝒯 is of the form ℛ𝒯_0,v⊤. A single application of  gets us to our goal.




(IV) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0, vp(t⃗),wϕ and we have a proof of ℛ𝒯, vt⃗_0, vp(t⃗),wϕ. 
Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0, vp(t⃗). We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0, vp(t⃗),uϕ.
We can apply Lemma <ref> repetitively on the proof of the latter to obtain a proof of 
ℛ𝒯, vt⃗_0, vp(t⃗),uϕ which we call S, while preserving height. Then, we proceed as follows.



ℛ𝒯, vt⃗_0, vp(t⃗),wϕ
S
SIH
ℛ𝒯, vt⃗_0, vp(t⃗)

ℛ𝒯_0, vp(t⃗)


Note that the instance of SIH is justified as the sum of the heights of the proofs of its premises is smaller than the one of the initial cut.

(V) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ,wϕ and we have a proof of ℛ𝒯_0,vψ,vχ,wϕ. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,vψχ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,vψχ,uϕ. We apply Lemma <ref> on the proof of the latter  sequent to obtain a proof of ℛ𝒯_0,vψ,vχ,uϕ preserving height. Thus, we proceed as follows.


ℛ𝒯_0,vψ,vχ,wϕ
ℛ𝒯_0,vψ,vχ,uϕ
SIH
ℛ𝒯_0,vψ,vχ

ℛ𝒯_0,vψχ


Note that the instance of SIH is justified as the sum of the heights of the proofs of its premises is smaller than the one of the initial cut.


(VI) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ and we have proofs of ℛ𝒯_0,vψ and ℛ𝒯_0,vχ. 
If wϕ is vψχ, then we have proofs of ℛ𝒯,vψ and ℛ𝒯,vχ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uψχ. Then, we proceed as follows where π is the first proof.



ℛ𝒯,vχ
Lem.<ref>
ℛ𝒯,uψ,vχ
ℛ𝒯,uψχ
Lem.<ref>
ℛ𝒯,uψ,uχ
PIH
ℛ𝒯,uψ





ℛ𝒯,vψ

π

PIH
ℛ𝒯


If wϕ is not vψχ, then we have proofs of ℛ𝒯_1,vψ,wϕ and ℛ𝒯_1,vχ,wϕ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,vψχ. Then, we proceed as follows where π is the first proof displayed.




ℛ𝒯_1,vψ,wϕ
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,uϕ_1,vψ
SIH
ℛ𝒯_1,vψ






π

ℛ𝒯_1,vχ,wϕ
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,uϕ_1,vχ
SIH
ℛ𝒯_1,vχ


ℛ𝒯_1,vψχ




(VII) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ,wϕ and we have proofs of ℛ𝒯_0,vψ,wϕ and ℛ𝒯_0,vχ,wϕ. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,vψχ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,vψχ,uϕ. We apply Lemma <ref> on the proof of the latter  sequent to obtain proofs of ℛ𝒯_0,vψ,uϕ and ℛ𝒯_0,vχ,uϕ preserving height. Thus, we proceed as follows where π is the first proof.


ℛ𝒯_0,vχ,wϕ
ℛ𝒯_0,vχ,uϕ
SIH
ℛ𝒯_0,vχ





ℛ𝒯_0,vψ,wϕ
ℛ𝒯_0,vψ,uϕ
SIH
ℛ𝒯_0,vψ

π


ℛ𝒯_0,vψχ



Note that both instances of SIH are justified as the sum of the heights of the proofs of their premises is smaller than the one of the initial cut.

(VIII) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ and we have a proof of ℛ𝒯_0,vψ,vχ. 
If wϕ is vψχ, then we have a proof of ℛ𝒯,vψ,vχ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uψχ. Then, we proceed as follows where π is the first proof displayed.


ℛ𝒯,vψ,vχ

ℛ𝒯,uψχ
Lem.<ref>
ℛ𝒯,uχ
Lem.<ref>
ℛ𝒯,uχ,vψ

PIH
ℛ𝒯,vψ




π

ℛ𝒯,uψχ
Lem.<ref>
ℛ𝒯,uψ


PIH
ℛ𝒯


If wϕ is not vψχ, then we have a proof of ℛ𝒯_1,vψ,vχ,wϕ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,vψχ. Then, we proceed as follows.



ℛ𝒯_1,vψ,vχ,wϕ

ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,uϕ_1,vψ,vχ

SIH
ℛ𝒯_1,vψ,vχ

ℛ𝒯_1,vψχ




(IX) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ,wϕ and we have proofs of ℛ𝒯_0,vψχ,wϕ,v_0ψ and ℛ𝒯_0,vψχ,v_0χ,wϕ such that vv_0. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,vψχ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,vψχ,uϕ. Given that vv, we apply Lemma <ref> on the proof of the latter  sequent to obtain proofs of ℛ𝒯_0,vψχ,uϕ,vψ, which we call S_0, and ℛ𝒯_0,vψχ,vχ,uϕ, which we call S_1, preserving height. Thus, we proceed as follows where π is the first proof displayed.


ℛ𝒯_0,vψχ,wϕ,vψ
S_0
SIH
ℛ𝒯_0,vψχ,vψ





π
ℛ𝒯_0,vψχ,vχ,wϕ
S_1
SIH
ℛ𝒯_0,vψχ,vχ


ℛ𝒯_0,vψχ


Note that both instances of SIH are justified as the sum of the heights of the proofs of their premises is smaller than the one of the initial cut.

(X) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ and we have a proof of ℛ,vv_0𝒯,v_0ψ_0,v_0χ.

If wϕ is not vψχ, then we have a proof of ℛ,vv_0𝒯,v_0ψ_1,v_0χ,wϕ, which we call S, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,vψχ. Then, we proceed as follows.



S

ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ,vv_0𝒯,uϕ,v_0ψ_1,v_0χ

SIH
ℛ,vv_0𝒯,v_0ψ_1,v_0χ

ℛ𝒯_1,vψχ



If wϕ is vψχ, then we have a proof of ℛ,vv_0𝒯,v_0ψ,v_0χ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uψχ. In this case, we need to consider the shape of r_2. If uψχ is not principal in r_2, then we use the proof of ℛ𝒯,vψχ with SIH to cut uψχ from the premises of r_2, and then reapply r_2 to reach our goal. If uψχ is principal in r_2, then the premises of r_2 are of the shape ℛ𝒯,uψχ,v_1ψ and ℛ𝒯,uψχ,v_1χ where uv_1. Then, we proceed as follows where π_0 and π_1 are (in this order) the first proofs given.



ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_1ψ,vψχ
ℛ𝒯,uψχ,v_1ψ
SIH
ℛ𝒯,v_1ψ







ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_1χ,vψχ
ℛ𝒯,uψχ,v_1χ
SIH
ℛ𝒯,v_1χ






π_0

ℛ,vv_0𝒯,v_0ψ,v_0χ
Lem.<ref>
ℛ,v_1v_0𝒯,v_0ψ,v_0χ
Lem.<ref>
ℛ𝒯,v_1ψ,v_1χ
π_1
PIH
ℛ𝒯,v_1ψ


PIH
ℛ𝒯




(XI) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ,wϕ and we a have proof of ℛ,v_0v𝒯_0,v_0ψ,wϕ,v_0χ. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,vψχ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,vψχ,uϕ. 
We apply Lemma <ref> on the proof of the latter  sequent to obtain a proof of ℛ,v_0v𝒯_0,v_0ψ,uϕ,v_0χ, which we call S. Thus, we proceed as follows.


ℛ,v_0v𝒯_0,v_0ψ,wϕ,v_0χ

S

SIH
ℛ,v_0v𝒯_0,v_0ψ,v_0χ

ℛ𝒯_0,vψχ


Note that the instance of SIH is justified as the sum of the heights of the proofs of the premises is smaller than the one of the initial cut.

(XII) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,vψχ and we have proofs of ℛ𝒯_0,vψχ,v_0ψ and ℛ𝒯,v_0χ_0,vψχ where v_0v.

If wϕ is not vψχ, then we have proofs of ℛ𝒯_1,vψχ,v_0ψ,wϕ, which we call S_0, and ℛ𝒯,v_0χ_1,vψχ,wϕ, which we call S_1, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,vψχ. Then, we proceed as follows where π is the first proof displayed.



S_0
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,uϕ_1,vψχ,v_0ψ
SIH
ℛ𝒯_1,vψχ,v_0ψ




π

S_1
ℛ𝒯,uϕ_1,vψχ
Lem.<ref>
ℛ𝒯,v_0χ,uϕ_1,vψχ
SIH
ℛ𝒯,v_0χ_1,vψχ


ℛ𝒯_1,vψχ



If wϕ is vψχ, then we have proofs of ℛ𝒯,vψχ,v_0ψ and ℛ𝒯,v_0χ,vψχ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uψχ. In this case, we need to consider the shape of r_2. If uψχ is not principal in r_2, then we use the proof of ℛ𝒯,vψχ with SIH to cut uψχ from the premises of r_2, and then reapply r_2 to reach our goal. If uψχ is principal in r_2, then the premise of r_2 is of the shape ℛ,v_1u𝒯,v_1ψ,v_1χ. Then, we proceed as follows where π_0 and π_1 are (in this order) the first proofs given.



ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_0ψ,vψχ
ℛ𝒯,uψχ,v_0ψ
SIH
ℛ𝒯,v_0ψ






ℛ𝒯,vψχ
Lem.<ref>
ℛ𝒯,v_0χ,vψχ
ℛ𝒯,uψχ,v_0χ
SIH
ℛ𝒯,v_0χ
Lem.<ref>
ℛ𝒯,v_0ψ,v_0χ






π_0

ℛ,uv_0𝒯,v_1ψ,v_1χ
Lem.<ref>
ℛ,v_1v_0𝒯,v_1ψ,v_1χ
Lem.<ref>
ℛ𝒯,v_0ψ,v_0χ
π_1
PIH
ℛ𝒯,v_0ψ


PIH
ℛ𝒯



(XIII) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v∃ xψ,wϕ and we a have proof of ℛ𝒯,vx_0,vψ(y/x),wϕ, which we call S. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,v∃ψ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,v∃ xψ,uϕ. 
We apply Lemma <ref> on the proof of the latter  sequent to obtain a proof of ℛ𝒯,vz_0,vψ(z/x),uϕ. Thus, we proceed as follows.


S

ℛ𝒯,vz_0,vψ(z/x),uϕ
Lem.<ref>
ℛ𝒯,vy_0,vψ(y/x),uϕ

SIH
ℛ𝒯,vy_0,vψ(y/x)

ℛ𝒯_0,v∃ψ


Note that the instance of SIH is justified as the sum of the heights of the proofs of the premises is smaller than the one of the initial cut.

(XIV) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v∃ xψ and we have a proof of ℛ𝒯_0,v∃ xψ,vψ(t/x) where t is available for v.

If wϕ is not v∃ xψ, then we have a proof of ℛ𝒯_1,v∃ xψ,vψ(t/x),wϕ, which we call S, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,v∃ xψ. Then, we proceed as follows.



S

ℛ𝒯,uϕ_1,v∃ xψ
Lem.<ref>
ℛ𝒯,uϕ_1,v∃ xψ,vψ(t/x)

SIH
ℛ𝒯_1,v∃ xψ,vψ(t/x)

ℛ𝒯_1,v∃ xψ



If wϕ is v∃ xψ, then we have proof a of ℛ𝒯,v∃ xψ,vψ(t/x), and ℛ𝒯,uϕ is of the form ℛ𝒯,u∃ xψ. In this case, we need to consider the shape of r_2. If u∃ xψ is not principal in r_2, then we use the proof of ℛ𝒯,v∃ xψ with SIH to cut u∃ xψ from the premises of r_2, and then reapply r_2 to reach our goal. If u∃ xψ is principal in r_2, then the premise of r_2 is of the shape ℛ𝒯,vy,vψ(y/x) where y is fresh. Then, we proceed as follows where π is the first proof given and x_0,…,x_n are all the variables appearing in t.



ℛ𝒯,v∃ xψ,vψ(t/x)
ℛ𝒯,u∃ xψ
Lem.<ref>
ℛ𝒯,u∃ xψ,vψ(t/x)
SIH
ℛ𝒯,vψ(t/x)






π

ℛ𝒯,vy,vψ(y/x)
Lem.<ref>
ℛ𝒯,vx_0,…,vx_n,vψ(t/x)
Lem.<ref>
ℛ𝒯,vψ(t/x)

PIH
ℛ𝒯


Note that the step involving Lemma <ref> is justified as t is available for v, which implies that we can push all its variables to the original labels making t available for v.

(XV) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v∀ xψ,wϕ and we a have proof of ℛ𝒯_0,v∀ xψ,v_0ψ(t/x),wϕ where vv_0 and t is available for v_0. Consequently, we know that ℛ𝒯 is of the form ℛ𝒯_0,v∀ xψ. We also have that ℛ𝒯,uϕ is of the form ℛ𝒯_0,v∀ xψ,uϕ. 
We apply Lemma <ref> on the proof of the latter sequent to obtain a proof of ℛ𝒯_0,v∀ xψ,v_0ψ(t/x),uϕ, which we call S. Thus, we proceed as follows.


ℛ𝒯_0,v∀ xψ,v_0ψ(t/x),wϕ

S

SIH
ℛ𝒯_0,v∀ xψ,v_0ψ(t/x)

ℛ𝒯_0,v∀ψ


Note that the instance of SIH is justified as the sum of the heights of the proofs of the premises is smaller than the one of the initial cut.

(XVI) 𝐫_1=: Then ℛ𝒯,wϕ is of the form ℛ𝒯_0,v∀ xψ and we have a proof of ℛ,vv_0𝒯,v_0y_0,v_0ψ(y/x), which we call S, where y is fresh.

If wϕ is not v∀ xψ, then we have a proof of ℛ,vv_0𝒯,v_0y_1,v_0ψ(y/x),wϕ, and ℛ𝒯,uϕ is of the form ℛ𝒯,uϕ_1,v∀ xψ. Then, we proceed as follows where π is the first proof displayed.



S

ℛ𝒯,uϕ_1,v∀ xψ
Lem.<ref>
ℛ,vv_0𝒯,v_0y,uϕ_1,v_0ψ(y/x)

SIH
ℛ,vv_0𝒯,v_0y_1,v_0ψ(y/x)

ℛ𝒯_1,v∀ xψ



If wϕ is v∀ xψ, then we have proof a of ℛ,vv_0𝒯,v_0y,v_0ψ(y/x), and ℛ𝒯,uϕ is of the form ℛ𝒯,u∀ xψ. In this case, we need to consider the shape of r_2. If u∀ xψ is not principal in r_2, then we use the proof of ℛ𝒯,v∀ xψ with SIH to cut u∀ xψ from the premises of r_2, and then reapply r_2 to reach our goal. If u∀ xψ is principal in r_2, then the premise of r_2 is of the shape ℛ𝒯,u∀ xψ,v_1ψ(t/x), which we call S, where uv_1 and t is available for v_1. Then, we proceed as follows where π is the first proof given and x_0,…,x_n are all the variables appearing in t.


ℛ,vv_0𝒯,v_0y,v_0ψ(y/x)
Lem.<ref>
ℛ𝒯,vy,vψ(y/x)
Lem.<ref>
ℛ𝒯,vx_0,…,vx_n,vψ(t/x)
Lem.<ref>
ℛ𝒯,vψ(t/x)





π

ℛ𝒯,v∀ xψ
Lem.<ref>
ℛ𝒯,v_1ψ(t/x),v∀ xψ
S
SIH
ℛ𝒯,v_1ψ(t/x)

PIH
ℛ𝒯


Note that the step involving Lemma <ref> is justified as t is available for v, which implies that we can push all its variables to the original labels making t available for v. In addition to that, the use of PIH is justified by the holding of vv_1 which we infer from vu and uv_1.




