Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to prove uniform Lyndon interpolation. We close this gap by showing uniform Lyndon interpolation for the provability logic \(\mathsf{GLS}\). This logic was known to have uniform interpolation, but it was open whether it has uniform Lyndon interpolation (or at least non-uniform Lyndon interpolation). The methodology we provide is easy to adapt to other provability logics if a non-wellfounded sequent calculus is available for them. In addition, we offer an alternative proof of cut elimination for \(\mathsf{GLS}\) via non-wellfounded proofs.
Non-wellfounded proof theory provides a powerful machinery to study of logics with explicit fixpoints, see e.g. [@Brotherston; @thomasCK; @KokkinisStuder+2016+171+192; @saurin; @guillermo-CTL; @ill-founded-intui-linear-time; @das; @master-modality]. However, its use is not restricted to these logics. In particular, provability logics are closely connected to a simple class of non-wellfounded proof systems [@shamkanovGl; @shamkanovGrz; @justus; @coalgebraic; @proofth-interpretability; @bimodal-provability-proofth].
Non-wellfounded sequent calculi have been successfully applied to obtain many interpolation results. In particular, they have been used to establish Craig interpolation [@pdl-interpolation; @converse-pdl-interpolation], Lyndon interpolation [@shamkanovGl] and uniform interpolation [@interpolation-guillermo; @uip-interpretability]. Still, the combination of uniform and Lyndon interpolation (the so-called uniform Lyndon interpolation property [@Akbar; @Kurahashi]) has not been studied with these methods. This paper is the first investigation in that direction, using non-wellfounded proofs to establish uniform Lyndon interpolation of the logic \(\mathsf{GLS}\).
Solovay’s logic \(\mathsf{GLS}\) (also known simply as \(\mathsf{S}\)) is the provability logic corresponding to the provability predicate of \(\mathsf{PA}\) according to true arithmetic [@solovay], and it is known to have Craig interpolation [@boolos-GLS; @lev-GLS; @GLSprooftheory].2 No proof that it has Lyndon or uniform Lyndon interpolation is known. Usually for such a proof the use of non-wellfounded proof theory is beneficial, as non-wellfounded sequent calculi get rid of what is usually called the diagonal formula, which, in wellfounded proofs, does not preserve the polarity. In this paper we will show that, indeed, \(\mathsf{GLS}\) has uniform Lyndon interpolation using non-wellfounded proofs.
In this paper the contributions are three-fold.
An alternative proof of cut elimination for \(\mathsf{GLS}\) is provided using non-wellfounded proofs (the original proof using ideas from the wellfounded cut elimination of \(\mathsf{GL}\) can be found in [@lev-GLS] and more detailed in [@GLSprooftheory]).
The introduction of the concepts of Lyndon fixpoints and Lyndon equational systems, which are necessary to show that the uniform interpolant created via non-wellfounded proofs respects polarities.
The first proof that \(\mathsf{GLS}\) has uniform Lyndon interpolation.
In Section 2 we will introduce the concepts needed from non-wellfounded proof theory. In Section 3 we will give the definition of \(\mathsf{GLS}\) and its sequent calculi, with an alternative proof of cut elimination using non-wellfounded proofs. In Section 4 we will introduce the notions of Lyndon fixpoint and Lyndon equational system, which are at the heart of our proof of uniform Lyndon interpolation. We conclude by proving the promised result, uniform Lyndon interpolation for \(\mathsf{GLS}\).
Let us start by fixing the notions concerning trees. Given a set \(X\) we will write \(X^*\) (\(X^+\)) to mean the set of (non-empty) finite sequences of elements in \(X\), \(\epsilon\) will denote the empty sequence. As usual, we will write \(w \leq v\) to mean that \(w\) is an initial prefix of \(v\) and \((w,v]\) to mean the set \(\left\{u \in X^* \mid w < u \leq v\right\}\). A (finitely branching) tree on \(A\) is a function \(T\) whose image is contained in \(A\) and whose domain is a prefix-closed non-empty subset of \(\mathbb{N}^*\) such that for every \(w \in \mathrm{Dom}(T)\) there is an unique natural number \(k\) (called the arity of \(w\) in \(T\)) such that \(wi \in \mathrm{Dom}(T)\) iff \(i < k\). The \(wi \in \mathrm{Dom}(T)\) are also called the immediate successors of \(w\). Note that the domain of any tree always contains the word \(\epsilon\), which is called the root of \(T\).
The elements of \(\mathrm{Dom}(T)\) are also called the nodes of \(T\), the \(0\)-ary nodes are called leaves and the rest of the nodes are called interior nodes. Finally, an infinite branch in a tree \(T\) is sequence of nodes \((w_i)_{i \in \mathbb{N}}\) such that \(w_0 = \epsilon\) and for each \(i\) there is a \(j\) such that \(w_{i+1} = w_i j\).
Fix a set \(\text{Seq}\) whose elements we will call sequents, a sequent rule is a subset of \(\text{Seq}^+\). Given a rule \(R\), we say that \((S_0,\ldots,S_{n-1},S)\) is an instance of \(R\) with premises \(S_0,\ldots,S_{n-1}\) and conclusion \(S\) if \((S_0,\ldots,S_{n-1},S) \in R\). A rule \(R\) is said to be \(n\)-ary if \(R \subseteq \text{Seq}^{n+1}\). We introduce the kind of sequent calculi we are going to use, called local progress sequent calculi.
Definition 1. A local progress sequent calculus* is a pair \(\mathcal{G} = (\mathcal{R}, (L_R)_{R \in \mathcal{R}})\) where \(\mathcal{R}\) is a set of sequent rules and each \(L_R\) is a function that takes an instance \(r = (S_0,\ldots,S_{n-1},S)\) of \(R\) and returns a subset of \(\left\{0,\ldots,n-1\right\}\). \(\mathcal{G}\) is said to be wellfounded if each \(L_R\) is the constant function returning \(\varnothing\).*
We are prepared to define the notion of proof in a local progress calculus. From the defintion of proof we can infer that a wellfounded sequent calculus is just a sequent calculus in the usual (wellfounded) proof theory.
Definition 2. Given a local progress sequent calculus \(\mathcal{G} = (\mathcal{R}, (L_R)_{R \in \mathcal{R}})\), a preproof in \(\mathcal{G}\)* is a tree with labels in \(\text{Seq} \times \mathcal{R}\) such that for each node \(w\) with immediate successors \(w0,\ldots,w(n-1)\) we have that \((S_0,\ldots,S_{n-1},S) \in R\) where \(S\) is the sequent at \(w\), \(R\) is the rule at \(w\) and \(S_i\) is the sequent at \(wi\).*
Let \(w\) be a node in \(\pi\) with immediate successors \(w0,\ldots,w(n-1)\). We say that \(wi\) is a progressing node* if \(i \in L_R(r)\) where \(R\) is the rule at \(w\) and \(r = (S_0,\ldots,S_{n-1},S)\) where \(S\) is the sequent at \(w\) and \(S_i\) the sequent at \(wi\). A proof is a preproof in which any infinite branch has infinitely many progressing nodes.*
We will write \(\mathcal{G} \vdash S\) to mean that \(S\) is provable in \(\mathcal{G}\) and \(\pi \vdash_{\mathcal{G}} S\) to mean that \(\pi\) is a proof of \(S\) in \(\mathcal{G}\), omitting the subscript \(_\mathcal{G}\) when it is clear from context. It will be common to write an instance \((S_0,\ldots,S_{n-1},S)\) of a rule \(R\) as \[\AxiomC{\(S_0\)} \AxiomC{\(\cdots\)} \AxiomC{\(S_{n-1}\)} \RightLabel{\(R\)} \TrinaryInfC{\(S\)} \DisplayProof\] Given a proof \(\pi\) in \(\mathcal{G}\) we will define its main local fragment as the finite tree obtained from cutting the tree at the first progressing nodes from the root (in particular removing the progressing nodes). The local height of \(\pi\), denoted \(\mathrm{lhg}(\pi)\), is the height of its main local fragment. The local rules of \(\pi\), denoted \(\mathrm{lRul}(\pi)\), is the set of rules occuring in the main local fragment. We will say that \(\pi\) is locally \(R\)-free if \(R \not \in\mathrm{lRul}(\pi)\). We note that if \(\mathcal{G}\) is a wellfounded calculus the notion of local height agrees with the usual notion of height and the local rules is the set of rules occuring in the proof.
Given a local progress calculus \(\mathcal{G} = (\mathcal{R},(L_R)_{R \in \mathcal{R}})\) and a rule \(R'\) we define \(\mathcal{G} + R'\) as the local progress calculus with rules \(\mathcal{R} \cup\left\{R'\right\}\) and \(L_{R'}\) the constant function returning \(\varnothing\). Rules can interact with local progress calculi in different ways, the following definition introduce some of these ways and the theorem below shows that some of them are equivalent.
Definition 3. Let \(\mathcal{G}\) be a sequent calculus and \(R\) be a rule. We say that:
\(R\) is admissible if for any instance \((S_0,\ldots,S_{n-1},S) \in R\) we have that \(\pi_i \vdash_{\mathcal{G}} S_i\) for \(i < n\) implies the existence of \(\pi \vdash_{\mathcal{G}} S\). In addition we say that \(R\) is admissible preserving local height* if \(\mathrm{lhg}(\pi) \leq \max_{i < n}\mathrm{lhg}(\pi_i)\) and admissible preserving local rules if \(\mathrm{lRul}(\pi) \subseteq \bigcup_{i < n}\mathrm{lRul}(\pi_i)\).*
\(R\) is eliminable if \(\mathcal{G} + R\vdash S\) implies \(\mathcal{G} \vdash S\).3
\(R\) is locally admissible if for any instance \((S_0,\ldots,S_{n-1},S) \in R\) we have that if there are locally \(R\)-free \(\pi_i \vdash_{\mathcal{G}} S_i\) for \(i < n\) then there is a locally \(R\)-free \(\pi \vdash_{\mathcal{G}} S\).
An \(n\)-ary rule \(R\) is \(i\)-invertible in \(\mathcal{G}\) (where \(i < n\)) if the rule \(\left\{(S,S_i) \mid (S_0,\ldots,S_{n-1},S) \in R\right\}\) is admissible. \(R\) is invertible* if it is \(i\)-invertible for each \(i < n\).*
We will talk about invertibility preserving local height and/or local rules with the obvious meaning.
Given an admissible rule \(R\) in \(\mathcal{G}\) an instance \((S_0,\ldots,S_{n-1},S) \in R\) and proofs \(\pi_i \vdash_{\mathcal{G}} S_i\) for \(i < n\) we will write \(R(\pi_0,\ldots,\pi_{n-1})\) to mean a proof of \(S\) in \(\mathcal{G}\) that exists by admissibility. For the invertibility of a rule \(R\) we will write instead \(\mathrm{inv}{R}(\pi)\).
The following result allows an easy development of local progress proof theory (for the details see [@proofth-interpretability; @coalgebraic]).
Theorem 1. Let \(\mathcal{G}\) be a local progress sequent calculus, then \(R\) is eliminable in \(\mathcal{G}\) iff \(R\) is locally admissible in \(\mathcal{G}\). If \(\mathcal{G}\) is wellfounded, then both are equivalent to \(R\) is admissible in \(\mathcal{G}\).
Finally, sometimes we will need to work with non-wellfounded proofs that have a particular finite representation. To define this notion we introduce the notion of trees with backedges. A tree with backedges is an ordered pair \(\tau = (T,(\cdot)^\circ)\) such that \(T\) is a finite tree and \((\cdot)^\circ\) is a function from a subset of the leafs of \(\tau\) to the nodes of \(\tau\) such that if \(w\) is in the domain then \(w^\circ < w\), the nodes in the domain of \((\cdot)^\circ\) are called repeat nodes.
Definition 4. Given a local progress calculus \(\mathcal{G} = (\mathcal{R}, (L_R)_{R \in \mathcal{R}})\), a cyclic preproof in \(\mathcal{G}\)* is a tree with backedges \(\pi = (T, (\cdot)^\circ)\) on \(\text{Seq} \times \mathcal{R}\) such that for any non-repeat node \(w\) with immediate successors \(w0, \ldots, w(n-1)\), we have that \((S_0,\ldots,S_{n-1},S) \in R\) where \(S\) is the sequent at \(w\), \(R\) is the rule at \(w\) and \(S_i\) is the sequent at \(wi\). and for any repeat node \(w\), \(w\) and \(w^\circ\) have the same sequent and rule. A cyclic proof in \(\mathcal{G}\) is a cyclic preproof such that for any repeat node \(w\) there is a progressing node in \((w^\circ,w]\).*
In cyclic preproofs we will annotate repeat nodes with the word \(\mathrm{Rep}\) at the right, instead of the rule at the node.
We fix an infinite countable set \(\text{Var}\) whose elements are called propositional variables.
Definition 5. We define the language \(\mathcal{L}_{\nec}\) given by the following Backus-Naur form: \[\phi ::= p \mid \bot \mid \phi \to \phi \mid \nec \phi,\] where \(p \in \text{Var}\). The expressions of \(\mathcal{L}_{\nec}\) are called (modal) formulas. The complexity of a formula \(\phi\) is the number of logical connectives of \(\phi\), and will be denoted as \(|\phi|\).
Given a multisets of formulas \(\Gamma\), we will write \(\nec \Gamma\) to mean the multiset \(\left\{\nec \phi \mid \phi \in \Gamma\right\}\) and \(\necd \Gamma\) to mean the multiset \(\Gamma \cup\nec \Gamma\). Then, for a formula \(\phi\), \(\necd \phi\) will be the multiset with two elements \(\left\{\phi, \nec \phi\right\}\).
Definition 6. We define the logic \(\mathsf{GL}\) as the smallest set of formulas such that
every classical propositional tautology in \(\mathcal{L}_{\nec}\) is in \(\mathsf{GL}\),
\((\mathrm{K})\) \(\nec(\phi \to \psi) \to \nec \phi \to \nec \psi\) is in \(\mathsf{GL}\),
\((\mathrm{L})\) \(\nec(\nec \phi \to \phi) \to \nec \phi\) is in \(\mathsf{GL}\),
and that is closed under the rules \[\AxiomC{\(\phi\)} \AxiomC{\(\phi \to \psi\)} \RightLabel{\(\mathrm{MP}\)} \BinaryInfC{\(\psi\)} \DisplayProof \qquad \AxiomC{\(\phi\)} \RightLabel{\(\mathrm{NEC}\)} \UnaryInfC{\(\nec \phi\)} \DisplayProof\] The elements of \(\mathsf{GL}\) are also called the theorems of \(\mathsf{GL}\). We will write \(\mathsf{GL}\vdash \phi\) to mean \(\phi \in \mathsf{GL}\).
We define the logic \(\mathsf{GLS}\) as the smallest set of formulas such that
every theorem of \(\mathsf{GL}\) is in \(\mathsf{GLS}\),
\((\mathrm{T})\) \(\nec \phi \to \phi\) is in \(\mathsf{GLS}\),
and that is closed under the rule \((\mathrm{MP})\). The elements of \(\mathsf{GLS}\) are also called the theorems of \(\mathsf{GLS}\). We will write \(\mathsf{GLS}\vdash \phi\) to mean \(\phi \in \mathsf{GLS}\).
Now we will define sequent calculi for \(\mathsf{GLS}\). We start by fixing the notion of sequent we will work with. A sequent is a triple \((\Gamma, \Delta,i)\) where \(\Gamma, \Delta\) are multisets of formulas and \(i \in \left\{0,1\right\}\). We write \((\Gamma, \Delta, 0)\) as \(\Gamma \Rightarrow \Delta\) and \((\Gamma, \Delta, 1)\) as \(\Gamma \Rrightarrow \Delta\). We use \(\gg\), possibly with subindexes, to mean either \(\Rightarrow\) or \(\Rrightarrow\). Given a multiset \(\Sigma\), we let \(\Sigma^s\) be the set with the same elements as \(\Sigma\) (but without repetitions).
None
Figure 1: Sequent Rules.
We introduce some terminology related to the rules of Figure 1. In \((\bot\mathrm{R})\), \(({\to}\mathrm{L})\), \(({\to}\mathrm{R})\), \((\mathrm{T})\), \((\nec^{\mathsf{GL}})\) and \((\nec^{\mathsf{K4}})\) the displayed formula at the conclusion is called principal formula. In \((\nec^{\mathsf{GL}})\) and \((\nec^{\mathsf{K4}})\) the formulas at the conclusion in \(\nec \Sigma\) will be called auxiliary. In \((\nec^{\mathsf{GL}})\) the formula \(\nec \phi\) at the premise is called diagonal formula. In \((\mathrm{ax})\), \((\bot\mathrm{L})\), \((\nec^{\mathsf{GL}})\) and \((\nec^{\mathsf{K4}})\) the formulas in \(\Gamma\) and \(\Delta\) will be said to belong to the weakening part. Note that the weakneing part of any rule instance can be changed arbitrarily and still we will have a rule instance of the same rule.
Definition 7. We make the following definitions.
\(\mathcal{G}\mathsf{GLS}\) is the wellfounded calculus with rules \((\mathrm{ax})\), \((\bot\mathrm{L})\), \((\bot\mathrm{R})\), \(({\to}\mathrm{L})\), \(({\to}\mathrm{R})\), \((\nec^{\mathsf{GL}})\) and \((\mathrm{T})\).4
\(\mathcal{G}^\infty \mathsf{GLS}\) is the local progress calculus with rules \((\mathrm{ax})\), \((\bot\mathrm{L})\), \((\bot\mathrm{R})\), \(({\to}\mathrm{L})\), \(({\to}\mathrm{R})\), \((\nec^{\mathsf{K4}})\) and \((\mathrm{T})\). Progress only occurs at the premise of \((\nec^{\mathsf{K4}})\).
Lemma 1. For any formula \(\phi\) and multisets \(\Gamma, \Delta\) we have that
\(\mathcal{G}\mathsf{GLS} \vdash \phi, \Gamma \gg \phi, \Delta\) and \(\mathcal{G}^\infty \mathsf{GLS} \vdash \phi, \Gamma \gg \phi, \Delta\). We denote the use of this inside proofs as \((\mathrm{Ax})\).
The following rule is admissible in \(\mathcal{G}\mathsf{GLS}\; (+\mathrm{Cut})\) and in \(\mathcal{G}^\infty \mathsf{GLS}\; (+\mathrm{Cut})\): \[\AxiomC{\(\Gamma \Rightarrow \Delta\)} \RightLabel{\(\mathrm{Prom}\)} \UnaryInfC{\(\Gamma \Rrightarrow \Delta\)} \DisplayProof\]
Proof. The proof of 1.is by induction on \(\phi\) while the proof of 2.is by induction on the local height of the proof. ◻
None
Figure 2: Structural Rules.
In Figure 2 we can see some common structural rules. As usual, these rules behave well with the sequent calculi, as we record in the following lemma. The proof, which is omitted due to constraints of space, is just using induction on the local height and using Theorem 1 when needed.
Lemma 2. In \(\mathcal{G}\mathsf{GLS}\; (+\mathrm{Cut})\) and in \(\mathcal{G}^\infty \mathsf{GLS} (+\mathrm{Cut})\) we have that
\(\mathrm{Wk}\) is eliminable and admissible preserving local height and local rules,
\((\bot\mathrm{R})\), \(({\to}\mathrm{L})\), \(({\to}\mathrm{R})\) are invertible preserving local height and local rules,
\(\mathrm{Ctr}\) is admissible preserving local height and local rules.
Using the admissibility of structural rules is easy to show the following (see [@GLSprooftheory]).
Theorem 2. For any multisets \(\Gamma, \Delta\) we have that \[\mathcal{G}\mathsf{GLS} + \mathrm{Cut}\vdash \Gamma \Rightarrow \Delta \text{ iff }\mathsf{GL}\vdash \bigwedge \Gamma \to \bigvee \Delta \quad \text{and}\quad \mathcal{G}\mathsf{GLS} + \mathrm{Cut}\vdash \Gamma \Rrightarrow \Delta \text{ iff }\mathsf{GLS}\vdash \bigwedge \Gamma \to \bigvee \Delta.\]
To establish cut elimination for \(\mathcal{G}\mathsf{GLS}\) via cut elimination for \(\mathcal{G}^\infty \mathsf{GLS}\), we will need to be able to translate proofs between both calculi. In this section we define the necessary translations. The following lemma follows from using \((\mathrm{Cut})\) and \((\nec^{\mathsf{GL}})\).
Lemma 3 (Löb’s rule). The following rule is admissible in \(\mathcal{G}\mathsf{GLS} + \mathrm{Cut}\): \[\AxiomC{\(\necd \Sigma, \nec\phi \Rightarrow \phi\)} \RightLabel{\(\mathrm{L\ddot{o}b}\)} \UnaryInfC{\(\necd \Sigma \Rightarrow \phi\)} \DisplayProof\]
Lemma 4. If \(\mathcal{G}\mathsf{GLS} + \mathrm{Cut}\vdash \Gamma \Rightarrow \Delta\), then \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}\vdash \Gamma \Rightarrow \Delta\).
Proof. We define corecursively a function \(\alpha\) from proofs in \(\mathcal{G}\mathsf{GLS} + \mathrm{Cut}\) to proofs in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}\) by cases on the last rule of the input proof. It commutes with all rules different from \((\nec^{\mathsf{GL}})\), and for \((\nec^{\mathsf{GL}})\) it is defined as \[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma, \nec \phi \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{GL}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma \Rightarrow \nec\phi, \Delta\)} \DisplayProof \quad \overset{\alpha}{\longmapsto} \quad \AxiomC{\(\alpha(\mathrm{L\ddot{o}b}(\pi_0))\)} \noLine \UnaryInfC{\(\necd \Sigma\Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma \Rightarrow \nec\phi, \Delta\)} \DisplayProof\] We notice that \(\alpha(\pi)\) is indeed a proof and not a preproof, the corecursive call only increase in height if progress is made in the path from the root to the corecursive call. ◻
Definition 8. Let \(\phi\) be a formula. We define its set of subformulas, denoted \(\mathrm{Sub}(\phi)\), recursively on \(\phi\) as \[\begin{align} &\mathrm{Sub}(p) = \left\{p\right\}, &&\mathrm{Sub}(\bot) = \left\{\bot\right\}, \\ &\mathrm{Sub}(\phi_0 \to \phi_1) = \left\{\phi_0 \to \phi_1\right\} \cup\mathrm{Sub}(\phi_0) \cup\mathrm{Sub}(\phi_1), &&\mathrm{Sub}(\nec \phi_0) = \left\{\nec \phi_0\right\} \cup\mathrm{Sub}(\phi_0). \end{align}\] Given a multiset \(\Gamma\) we will write \(\mathrm{Sub}(\Gamma)\) to denote the set \(\bigcup_{\phi \in \Gamma} \mathrm{Sub}(\phi)\), and given a sequent \(\Gamma \gg \Delta\) we will write \(\mathrm{Sub}(\Gamma \gg \Delta)\) to denote \(\mathrm{Sub}(\Gamma) \cup\mathrm{Sub}(\Delta)\).
The following lemma follows by inspection of Figure 1.
Lemma 5 (Local subformula property). Let \[\AxiomC{\(S_0\)} \AxiomC{\(\cdots\)} \AxiomC{\(S_{n-1}\)} \RightLabel{\(R\)} \TrinaryInfC{\(S\)} \DisplayProof\] be an instance of a rule of \(\mathcal{G}\mathsf{GLS}\) or \(\mathcal{G}^\infty \mathsf{GLS}\). Then \(\mathrm{Sub}(S_i) \subseteq \mathrm{Sub}(S)\) for \(i < n\).
Lemma 6. For any finite set \(\Lambda\), we have that \(\mathcal{G}^\infty \mathsf{GLS} \vdash \Gamma \gg \Delta\) implies \(\mathcal{G}\mathsf{GLS} \vdash \nec \Lambda, \Gamma \gg \Delta\).
Proof. Let \(\pi \vdash \Gamma \gg \Delta\) in \(\mathcal{G}^\infty \mathsf{GLS}\), we proceed by induction on the measure \(\omega\cdot | \mathrm{Sub}(\Gamma \gg \Delta) \setminus \Lambda| + \mathrm{lhg}(\pi)\) and cases on the last rule of \(\pi\). If the last rule of \(\pi\) is not \(\nec^{\mathsf{K4}}\) then it suffices to apply the induction hypothesis and reapply the rule. Now assume that the last rule of \(\pi\) is \(\nec^{\mathsf{K4}}\), i.e., \(\pi\) is \[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma' \gg \nec\phi, \Delta'\)} \DisplayProof\] where \(\Gamma = \nec \Sigma, \Gamma'\) and \(\Delta = \nec \phi, \Delta'\). Let us denote the conclusion of \(\pi_0\) as \(S_0\) and the conclusion of \(\pi\) as \(S\). We proceed by cases. If \(\phi \in \Lambda\) the desired proof is obtained by using \((\mathrm{Ax})\), as \(\nec \phi\) will be in both sides of the sequent. Now assume that \(\phi \not \in \Lambda\), then \(|\mathrm{Sub}(S_0) \setminus (\Lambda \cup\left\{\phi\right\})| < |\mathrm{Sub}(S_0) \setminus \Lambda| \leq |\mathrm{Sub}(S) \setminus \Lambda|,\) so by the induction hypothesis we have a proof \(\tau \vdash \nec \phi, \nec \Lambda, \necd \Sigma \Rightarrow \phi\). The desired proof is then \[\AxiomC{\(\mathrm{Wk}(\tau)\)} \noLine \UnaryInfC{\(\nec \phi, \necd \Lambda, \necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{GL}}\)} \UnaryInfC{\(\nec \Lambda, \nec \Sigma, \Gamma' \Rightarrow \nec\phi, \Delta'\)} \DisplayProof\] ◻
Finally, we show local admissibility of \(\mathrm{Cut}\) in \(\mathcal{G}^\infty \mathsf{GLS}\) which implies its eliminability. Thanks to the translations of the previous subsection we also obtain cut elimination for \(\mathcal{G}\mathsf{GLS}\).
Theorem 3. \(\mathrm{Cut}\) is locally admissible in \(\mathcal{G}^\infty \mathsf{GLS}\). As a corollary, \(\mathrm{Cut}\) is eliminable in \(\mathcal{G}^\infty \mathsf{GLS}\).
Proof. Let \(\pi \vdash \Gamma \gg \Delta,\chi\) and \(\tau \vdash \chi, \Gamma \gg \Delta\) be locally cut free proofs in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}\). We proceed by induction on the measure \(\omega \cdot |\chi| + (\mathrm{lhg}(\pi) + \mathrm{lhg}(\tau))\). Most cases follow the usual cut reductions in cut elimination (for the details see Appendix 5), so we will consider only two special cases. Assume that \(\pi\) and \(\tau\) are of the following shape \[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \chi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma' \gg \nec\chi, \nec \phi, \Delta'\)} \DisplayProof \qquad \AxiomC{\(\tau_0\)} \noLine \UnaryInfC{\( \necd \chi, \necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec\chi, \nec \Sigma, \Gamma' \gg \nec \phi, \Delta'\)} \DisplayProof\] where \(\Gamma = \nec \Sigma, \Gamma'\), \(\Delta = \nec \phi, \Delta'\). We can assume that the auxiliary \(\nec\)-formulas on the left hand side are the same, since otherwise we can use \(\mathrm{Wk}\) on \(\pi_0\) and \(\tau_0\) preserving height and local cut freeness. Then, the desired proof is \[\AxiomC{\(\mathrm{Wk}(\pi_0)\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \phi, \chi\)} \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \chi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\chi, \necd \Sigma \Rightarrow \phi, \nec \chi\)} \AxiomC{\(\tau_0\)} \noLine \UnaryInfC{\(\necd \chi, \necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\mathrm{Cut}\)} \BinaryInfC{\(\chi, \necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\mathrm{Cut}\)} \BinaryInfC{\(\necd \Sigma \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma' \Rightarrow \nec\phi, \Delta'\)} \DisplayProof\] Notice that the proof is trivially locally cut free.
The other case is as follows. Assume \(\pi\) and \(\tau\) are of the following shape. \[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \chi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma' \Rrightarrow \nec\chi,\Delta\)} \DisplayProof \qquad \AxiomC{\(\tau_0\)} \noLine \UnaryInfC{\(\necd\chi, \nec \Sigma, \Gamma' \Rrightarrow \Delta\)} \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\nec\chi, \nec \Sigma, \Gamma' \Rrightarrow \Delta\)} \DisplayProof\] where \(\Gamma = \nec \Sigma, \Gamma'\). Then the desired proof is \[\AxiomC{\(\mathrm{Wk}(\mathrm{Prom}(\pi_0))\)} \noLine \UnaryInfC{\(\necd \Sigma,\Gamma' \Rrightarrow \chi, \Delta\)} \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma \Rightarrow \chi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\chi, \necd \Sigma, \Gamma' \Rrightarrow \nec\chi \Delta\)} \AxiomC{\(\mathrm{Wk}(\tau_0)\)} \noLine \UnaryInfC{\(\necd\chi, \necd \Sigma, \Gamma' \Rrightarrow \Delta\)} \RightLabel{\(\mathrm{Cut}\) (I.H.)} \BinaryInfC{\(\chi, \necd \Sigma, \Gamma' \Rrightarrow \Delta\)} \RightLabel{\(\mathrm{Cut}\) (I.H.)} \BinaryInfC{\(\necd \Sigma, \Gamma' \Rrightarrow \Delta\)} \doubleLine \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\nec \Sigma, \Gamma' \Rrightarrow \Delta\)} \DisplayProof\] where the double line denotes muliple aplpications of \((\mathrm{T})\). The first cut is justified by a smaller sum of local heights and the second cut by a smaller cut formula. ◻
Thanks to the translations of the previous subsection, we obtain the following.
Corollary 1. \(\mathrm{Cut}\) is eliminable in \(\mathcal{G}\mathsf{GLS}\).5
Corollary 2. Let \(\Gamma, \Delta\) be multisets. We have the following:
\(\mathsf{GL}\vdash \bigwedge \Gamma \to \bigvee \Delta \quad\text{iff}\quad \mathcal{G}\mathsf{GLS} \;(+\mathrm{Cut}) \vdash \Gamma \Rightarrow \Delta \quad\text{iff}\quad \mathcal{G}^\infty \mathsf{GLS} \;(+\mathrm{Cut})\vdash \Gamma \Rightarrow \Delta\).
\(\mathsf{GLS}\vdash \bigwedge \Gamma \to \bigvee \Delta \quad\text{iff}\quad \mathcal{G}\mathsf{GLS} \;(+\mathrm{Cut})\vdash \Gamma \Rrightarrow \Delta \quad\text{iff}\quad \mathcal{G}^\infty \mathsf{GLS} \;(+\mathrm{Cut})\vdash \Gamma \Rrightarrow \Delta\).
Having established the connection between the sequent and Hilbert calculi for \(\mathsf{GLS}\), we are ready to show uniform Lyndon interpolation for \(\mathsf{GLS}\). In order to respect the polarity of variables, it is necessary to avoid introducing the diagonal formula in the modal rule. Hence the use of \(\mathcal{G}^\infty \mathsf{GLS}\) instead of \(\mathcal{G}\mathsf{GLS}\) is essential.
To properly talk about uniform Lyndon interpolation, first we need to define the positive and negative vocabulary of a formula. From now on, with vocabulary we simply mean a set of variables.
Definition 9. Let \(\phi\) be a formula. We define its positive* and negative vocabulary, denoted \(\mathrm{Voc}_+(\phi)\) and \(\mathrm{Voc}_-(\phi)\) respectively, recursively by \[\begin{align} &\mathrm{Voc}_+(p) = \left\{p\right\}, &&\mathrm{Voc}_-(p) = \varnothing, \\ &\mathrm{Voc}_+(\bot) = \varnothing, &&\mathrm{Voc}_-(\bot) = \varnothing, \\ &\mathrm{Voc}_+(\phi_0 \to \phi_1) = \mathrm{Voc}_-(\phi_0) \cup\mathrm{Voc}_+(\phi_1), &&\mathrm{Voc}_-(\phi_0 \to \phi_1) = \mathrm{Voc}_+(\phi_0) \cup\mathrm{Voc}_-(\phi_1), \\ &\mathrm{Voc}_+(\nec\phi_0) = \mathrm{Voc}_+(\phi_0), &&\mathrm{Voc}_-(\nec\phi_0) = \mathrm{Voc}_-(\phi_0). \end{align}\] Given a multiset \(\Gamma\) we will write \(\mathrm{Voc}_+(\Gamma)\) to mean the set \(\bigcup_{\phi \in \Gamma} \mathrm{Voc}_+(\phi)\), and given a sequent \(\Gamma \gg \Delta\) we will write \(\mathrm{Voc}_+(\Gamma \gg \Delta)\) to mean \(\mathrm{Voc}_+(\Gamma) \cup\mathrm{Voc}_+(\Delta)\). We will use the same notation for \(\mathrm{Voc}_-\).*
We will write \(\overline{+}\) to mean \(-\) and \(\overline{-}\) to mean \(+\). The following lemma can be proved by induction on the complexity of \(\phi\) (although we omit the proof as it is highly technical and not particularly illuminating).
Lemma 7. Let \(p\) be a propositional variable and \(\phi(p_0,\ldots,p_{n-1}, q_0,\ldots,q_{m-1})\), \(\psi_0,\ldots,\psi_{n-1}\), and \(\chi_0,\ldots,\chi_{m-1}\) be formulas. If \(\mathrm{Voc}_-(\phi) \cap \left\{p_0,\ldots,p_{n-1}\right\} =\varnothing\) and \(\mathrm{Voc}_+(\phi) \cap \left\{q_0,\ldots,q_{m-1}\right\} = \varnothing\), then for \(b \in \left\{+,-\right\}\) \[\begin{gather} \mathrm{Voc}_b(\phi(\psi_0,\ldots,\psi_{n-1}, \chi_0,\ldots,\chi_{m-1})) \subseteq\\ \mathrm{Voc}_b(\phi) \setminus\left\{p_0,\ldots,p_{n-1},q_0,\ldots,q_{m-1}\right\} \cup\bigcup_{i < n} \mathrm{Voc}_b(\psi_i) \cup\bigcup_{j < m} \mathrm{Voc}_{\overline{b}}(\chi_j). \end{gather}\]
We are ready to recall the definition of uniform Lyndon interpolation.
Definition 10. A logic \(L\) has the Uniform Lyndon Interpolation Property* (or ULIP in short) if for any formula \(\phi\) and vocabularies \(V_+, V_-\), there is a formula \(\iota\) called uniform Lyndon interpolant such that*
\(\mathrm{Voc}_+(\iota) \subseteq V_+\) and \(\mathrm{Voc}_-(\iota) \subseteq V_-\),
\(L \vdash \phi \to \iota\), and
for any \(\psi\) such that \(\mathrm{Voc}_+(\psi) \subseteq V_+\) and \(\mathrm{Voc}_-(\psi) \subseteq V_-\) we have that \(L \vdash \phi \to \psi\) implies \(L \vdash \iota \to \psi\).
The rest of the paper will be dedicated to show that \(\mathsf{GLS}\) has the ULIP.
The first step towards calculating uniform Lyndon interpolants will be to solve equational systems of formulas. In addition, as the polarities of variables matters, we will need to keep track of them. We will do so by introducing the notions of Lyndon fixpoint and Lyndon equational system.
Definition 11 (Lyndon Fixpoints). Let \(\phi(p)\) and \(\psi\) be formulas. We say that \(\psi\) is a Lyndon fixpoint of \(\phi\) (with respect to \(p\)) in \(\mathsf{GLS}\)* if \(\mathrm{Voc}_{b}(\psi) \subseteq \mathrm{Voc}_b(\phi) \setminus \left\{p\right\}\) for \(b \in \left\{+,-\right\}\) and \(\mathsf{GLS}\vdash \psi \leftrightarrow \phi(\psi)\).*
A formula \(\phi\) is modalized in a variable \(p\) if all the occurences of \(p\) in \(\phi\) are under the scope of a \(\nec\).
Definition 12 (Lyndon equational systems). Let \(V_+,V_-\) be vocabularies and \(\bar{p} = (p_0,\ldots,p_{n-1})\) be a finite sequence of pairwise different variables not occuring in \(V_+ \cup V_-\). A Lyndon equational system over \((\bar{p},V_+,V_-)\)* is a collection of triples \(\mathcal{E} = \left\{(p_i,b_i,\phi_i) \mid i < n\right\}\) such that \(b_i \in \left\{+,-\right\}\), \(\phi_i\) is a formula, \(\mathrm{Voc}_{b_i}(\phi_i) \subseteq V_+ \cup B_+\) and \(\mathrm{Voc}_{\overline{b_i}}(\phi_i) \subseteq V_- \cup B_-\), where \(B_+ = \left\{p_i \mid b_i = +\right\}\) and \(B_- = \left\{p_i \mid b_i = -\right\}\). The elements of \(\bar{p}\) are called unknowns and those of \(\mathcal{E}\) are called equations.*
A solution in \(L\)* to \(\mathcal{E}\) is a sequence \((\psi_0,\ldots,\psi_{n-1})\) such that for each \(i \in n\), we have \(\mathrm{Voc}_{b_i}(\psi_i) \subseteq V_+\), \(\mathrm{Voc}_{\overline{b_i}}(\psi_i) \subseteq V_-\) and \(L \vdash \psi_i \leftrightarrow \phi_i[\psi_0/p_0,\ldots,\psi_{n-1}/p_{n-1}]\). \(\mathcal{E}\) is said to be*
2
**Solvable in \(L\)* if it has a solution in \(L\).*
**Simple* if \(\phi_i\) is a \(\nec\)-formula for \(i < n\).*
**Modalized* if \(\phi_{i}\) is modalized in \(p_0,\ldots,p_i\).*
**Positive* if \(b_i = {+}\) for \(i < n\).*
Given an equational system \(\mathcal{E}\) over \((\bar{p}, V_+, V_-)\) with solution \((\psi_0,\ldots,\psi_{n-1})\) we will also call the substitution \((\cdot)^*\) where \(p_i^* = \psi_i\) and \(q^* = q\) for \(q\) not in \(\bar{p}\) a solution of \(\mathcal{E}\).
Lemma 8. We have that
For any formula \(\phi(p)\), \(\nec \phi(\top)\) is a Lyndon fixpoint of \(\nec \phi(p)\) in \(\mathsf{GLS}\).
Simple Lyndon equational systems have a solution in \(\mathsf{GLS}\).
Proof. Proof 1. It is wellknown (e.g. see [@smorynski]) that \(\mathsf{GL}\vdash \nec \phi(\top) \leftrightarrow \nec \phi(\nec \phi (\top))\), so it is also a theorem of \(\mathsf{GLS}\). By the properties of substitution, we get \(\mathrm{Voc}_{b}(\phi(\top)) \subseteq \mathrm{Voc}_{b}(\phi) \setminus \left\{p\right\}\) for \(b \in \left\{+,-\right\}\).
Proof of 2. Let \(\mathcal{E} = \left\{(p_i,b_i,\nec \phi_i) \mid i < n\right\}\) be a simple Lyndon equational system over \((\bar{p}, V_+, V_-)\). We proceed by induction on \(n\), the number of unknowns. Take \(\nec \phi_0(p_0,\ldots,p_{n-1})\), we know that it has a Lyndon fixpoint \(\psi_0\) in \(\mathsf{GLS}\). Note that \(\mathcal{E}' = \left\{(p_i, b_i, \nec \phi_i[\psi_0/p_0]) \mid 1 \leq i < n\right\}\) is a simple Lyndon equational system solvable in \(\mathsf{GLS}\) by the induction hypothesis, let \((\chi_1,\ldots,\chi_n)\) be a solution in \(\mathsf{GLS}\) of it. Let us define \(\chi_0 = \psi_0[\chi_1/p_1,\ldots,\chi_n/p_n]\), then we claim that \((\chi_0,\ldots,\chi_n)\) is a solution of \(\mathcal{E}\).
First, note that we already have that \(\mathrm{Voc}_{b_i}(\chi_i) \subseteq V_+\) and \(\mathrm{Voc}_{\overline{b_i}}(\chi_i) \subseteq V_-\) for \(1 \leq i < n\). We notice that for \(1 \leq i < n\) we have that if \(b_i = b_0\) then \(p_i \not\in \mathrm{Voc}_-(\psi_0)\) and if \(b_i \neq b_0\) then \(p_i \not \in \mathrm{Voc}_+(\psi_0)\) (it suffices to do cases on \(b_i\) and \(b_0\)). Using Lemma 7 we have that \[\begin{align} \mathrm{Voc}_{b_0}(\chi_0) &\subseteq \mathrm{Voc}_{b_0}(\psi_0) \setminus \left\{p_1,\ldots,p_n\right\} \cup\bigcup_{\scriptstyle \begin{matrix} 1 \leq i < n \\ b_i = b_0 \end{matrix}} \mathrm{Voc}_{b_0}(\chi_i) \cup\bigcup_{\scriptstyle \begin{matrix} 1 \leq i < n \\ b_i \neq b_0 \end{matrix}} \mathrm{Voc}_{\overline{b_0}}(\chi_i) \\ &\subseteq \mathrm{Voc}_{b_0}(\nec \phi_0) \setminus \left\{p_0,\ldots,p_n\right\} \cup\bigcup_{\scriptstyle \begin{matrix} 1 \leq i < n \\ b_i = b_0 \end{matrix}} \mathrm{Voc}_{b_i}(\chi_i) \cup\bigcup_{\scriptstyle \begin{matrix} 1 \leq i < n \\ b_i \neq b_0 \end{matrix}} \mathrm{Voc}_{b_i}(\chi_i) \subseteq V_+. \end{align}\] where we used that \(\mathrm{Voc}_{b_0}(\nec \phi_0) \subseteq V_+ \cup B_+\). We have an anologous reasoning for \(\mathrm{Voc}_{\overline{b_0}}(\chi_0)\), so the desired polarity conditions hold.
Finally, we show the desired equivalences. We have \(\mathsf{GLS}\vdash \chi_i \leftrightarrow (\nec \phi_i[\psi_0/p_0])[\chi_1/p_1, \ldots, \chi_{n}/p_n]\) for \(1 \leq i < n\). Using that \(p_0 \neq p_i\) for \(1 \leq i < n\) we obtain that \[\begin{align} (\nec\phi_i[\psi_0/p_0])[\chi_1/p_1, \ldots, \chi_{n}/p_n] &= \nec\phi_i[\psi_0[\chi_1/p_1, \ldots, \chi_{n}/p_n]/p_0, \chi_1/p_1, \ldots, \chi_{n}/p_n]\\ &= \nec\phi_i[\chi_0/p_0,\chi_1/p_1, \ldots, \chi_{n}/p_n], \end{align}\] as desired. All left to show that \(\mathsf{GLS}\vdash \chi_0 \leftrightarrow \nec \phi_0[\chi_0/p_0, \ldots, \chi_{n}/p_n]\). We have that, as \(\psi_0\) is a fixpoint, \(\mathsf{GLS}\vdash \nec \psi_0 \leftrightarrow \nec \phi_0[\psi_0/p_0]\). As \(\mathsf{GLS}\) is closed under substitutions we obtain that \(\mathsf{GLS}\vdash \nec \chi_0 \leftrightarrow (\nec \phi_0[\psi_0/p_0])[\chi_1/p_1,\ldots,\chi_n/p_n]\), and we can use the same equalities as before since \(p_0 \neq p_i\) for \(1 \leq i < n\). ◻
We say that \(\phi\) is positive in \(p\) if \(p \not \in \mathrm{Voc}_-(\phi)\).
Theorem 4. We have that
Every formula positive and modalized in \(p\) has a Lyndon fixpoint in \(\mathsf{GLS}\).
Positive modalized Lyndon equational system are solvable in \(\mathsf{GLS}\).
Proof. Proof of 1.6 Let \(\phi(p)\) be a formula that is modalized in \(p\) and positive in \(p\). Then \(\phi(p)\) can be written as \(\phi'(\nec\psi_0(p),\ldots,\nec\psi_{n-1}(p),\nec\chi_0(p),\ldots,\nec\chi_{m-1}(p))\), where \(\phi'(q_0,\ldots,q_{n-1}, r_0,\ldots,r_{m-1})\) does not contain \(p\), and \(\left\{q_0,\ldots,q_{n-1}\right\} \subseteq \mathrm{Voc}_+(\phi') \setminus \mathrm{Voc}_-(\phi')\), \(\left\{r_0,\ldots,r_{m-1}\right\} \subseteq \mathrm{Voc}_-(\phi') \setminus \mathrm{Voc}_+(\phi')\). From this is easy to infer that for \(i < n\), \(j < m\) and \(b \in \left\{+,-\right\}\): \[\mathrm{Voc}_b(\psi_i) \subseteq \mathrm{Voc}_b(\phi), \quad \mathrm{Voc}_b(\chi_j) \subseteq \mathrm{Voc}_{\overline{b}}(\phi), \quad p \not \in \mathrm{Voc}_-(\psi_i)\quad \text{and}\quad p \not \in \mathrm{Voc}_+(\chi_j).\] Consider the following equational system \(\left\{(q_i, +,\nec \psi_i(\phi')) \mid i < n\right\} \cup\left\{(r_j,-, \nec\chi_j(\phi')) \mid j < m\right\}.\) This is a simple Lyndon \((\bar{q}\bar{r}, \mathrm{Voc}_+(\phi)\setminus \left\{p\right\}, \mathrm{Voc}_-(\phi)\setminus \left\{p\right\})\)-equational system. Thus, it has a solution \((\cdot)^* : \bar{q}\bar{r} \longrightarrow \mathcal{L}_{\nec}\) in \(\mathsf{GLS}\). Define \(\eta = \phi'(q^*_0, \ldots, q^*_{n-1}, r^*_0, \ldots,r^*_{m-1})\), by Lemma 7 we know that \(\mathrm{Voc}_+(\eta) \subseteq \mathrm{Voc}_+(\phi) \setminus \left\{p\right\}\) and \(\mathrm{Voc}_-(\eta) \subseteq \mathrm{Voc}_-(\phi)\). Also, since \((\cdot)^*\) is a solution of the equational system, we have that \(\mathsf{GLS}\vdash q^*_i \leftrightarrow \nec \psi_i(\eta)\) and \(\mathsf{GLS}\vdash r^*_j \leftrightarrow \nec \chi_j(\eta)\). So we obtain \[\mathsf{GLS}\vdash \eta \leftrightarrow \phi'(\nec\psi_0(\eta), \ldots,\nec\psi_{n-1}(\eta), \nec\chi_0(\eta), \ldots,\nec\chi_{m-1}(\eta)).\] In other words, \(L \vdash \eta \leftrightarrow \phi(\eta)\), so \(\eta\) is a Lyndon fixpoint of \(\phi\) with respect to \(p\).
Proof of 2. The proof is similar to the second point of Lemma 8 using that if \(\phi_i\) is modalised in \(p_0,\ldots,p_i\) then \(\phi_i[\psi/p_0]\) is also modalised in \(p_0,\ldots,p_i\). ◻
The fundamental result will be the second part of Theorem 4. When constructing an interpolant we will see that a positive modalized Lyndon equational system will arise. Solving it and using the solution on a particular formula will give us the uniform Lyndon interpolant.
It is common to relate uniform interpolation to proof search. We will make this connection explicit via defining interpolation templates, which is a proof search where we assume that we only have a part of the desired sequent. Since there is a rule in the system which increase the complexity of sequents (namely rule \((\mathrm{T})\)), we will need to base our proof search on a notion of saturation.
Definition 13. Let \(\Gamma \gg \Delta\) be a sequent. We say that a formula \(\phi\) is
2
**Left saturated in \(\Gamma \gg \Delta\)* if*
\(\phi\) is atomic,
\(\phi = \phi_0 \to \phi_1\) and \(\phi_0 \in \Delta\) or \(\phi_1 \in \Gamma\),
\(\phi = \nec \phi_0\) and \(\phi_0 \in \Gamma\) or \({\gg} = { \Rightarrow}\).
**Right saturated in \(\Gamma \gg \Delta\)* if*
\(\phi\) is atomic or a \(\nec\)-formula,
\(\phi = \phi_0 \to \phi_1\) and \(\phi_0 \in \Gamma\), \(\phi_1 \in \Delta\).
Given a sequent \(S = \Gamma \gg \Delta\) we define its saturation complexity, denoted \(|S|_{\mathrm{Sat}}\), as the multiset \[\left\{|\phi| \mid \phi \in \Gamma, \phi \text{ not left saturated in }S\right\} \cup\left\{|\phi| \mid \phi \in \Delta, \phi \text{ not right saturated in }S\right\}.\] We assume the saturation complexity comes with the multiset ordering attached to it, so \(|S|_{\mathrm{Sat}} < |S'|_{\mathrm{Sat}}\) means that \(|S|_{\mathrm{Sat}}\) is obtained from \(|S'|_{\mathrm{Sat}}\) by the process of taking out at least one element and replace it with a finite number of strictly smaller elements. We remember that the multiset ordering is wellfounded.
None
Figure 3: Interpolation Template Rules.
Definition 14. An interpolation template is a cyclic proof constructed in the local progress calculus whose rules are displayed in Figure 3 and progress is only made at the premises of \(\nec^{\mathsf{K4}}_{\mathrm{sat}}\).
It is easy to show the following lemma, the details of the proof can be found in the appendix.
Lemma 9. Every sequent has an interpolation template.
We will consider formulas on a expanded set of propositional variables. For each \(w \in \mathbb{N}^*\) we pick a new variable \(x_w\) different from the variables in \(\text{Var}\) and such that if \(w,v \in \mathbb{N}^*\) and \(w \neq v\) then \(x_w \neq x_v\). We define \(B = \left\{x_w \mid w \in \mathbb{N}^*\right\}\) and for a interpolation template \(T\) we define \(B_T = \left\{x_w \mid w \text{ repeat node of } T\right\}\). The elements of \(B\) will be called bound variables and the formulas on this expanded set of variables will be called pseudoformulas. For the rest of the subsection we fix two vocabularies \(V_+\) and \(V_-\) for which we want to calculate the uniform Lyndon interpolant.
Definition 15. Let \(T\) be an interpolation template and \(w\) a node of \(T\), let us denote the sequent at \(w\) in \(T\) as \(\Gamma_w \gg_w \Delta_w\). We will annotate each of the sequents of \(T\) with a pseudoformula \(\kappa\) called the preinterpolant at \(w\), denoted as \(\kappa : \Gamma_w \gg_w \Delta_w\). We proceed by recursion on the tree structure of \(T\) as follows. \[\AxiomC{\(\)} \RightLabel{\(\mathrm{ax}\)} \UnaryInfC{\(\bot : p, \Gamma \gg p, \Delta\)} \DisplayProof \quad \AxiomC{\(\)} \RightLabel{\(\bot\mathrm{L}\)} \UnaryInfC{\(\bot : \bot, \Gamma \gg \Delta\)} \DisplayProof \quad \AxiomC{\(\)} \RightLabel{\(\mathrm{Emp}\)} \UnaryInfC{\(\top : {\gg}\)} \DisplayProof \quad \AxiomC{} \RightLabel{\(\mathrm{Rep}\)} \UnaryInfC{\(x_w : \Gamma_w \gg_w \Delta_w\)} \DisplayProof \quad \AxiomC{\(\kappa : \necd \phi, \Gamma \Rrightarrow \Delta\)} \RightLabel{\(\mathrm{T}_{\mathrm{sat}}\)} \UnaryInfC{\(\kappa : \nec \phi, \Gamma \Rrightarrow \Delta\)} \DisplayProof\] \[\AxiomC{\(\kappa_0 : \phi \to \psi, \Gamma \gg \phi, \Delta\)} \AxiomC{\(\kappa_1 : \psi, \phi \to \psi, \Gamma \gg \Delta\)} \RightLabel{\({\to}\mathrm{L}_{\mathrm{sat}}\)} \BinaryInfC{\(\kappa_0 \vee \kappa_1 : \phi \to \psi, \Gamma \gg \Delta\)} \DisplayProof \quad \AxiomC{\(\kappa : \phi, \Gamma \gg \psi, \phi \to \psi, \Delta\)} \RightLabel{\({\to}\mathrm{R}_{\mathrm{sat}}\)} \UnaryInfC{\(\kappa : \Gamma \gg \phi \to \psi, \Delta\)} \DisplayProof\] \[\AxiomC{\(\kappa^{\nec} : \necd \Sigma \Rightarrow\)} \AxiomC{\([\kappa^{\pos}_\phi : \necd \Sigma \Rightarrow \phi]_{\phi \in \Theta}\)} \RightLabel{\(\nec^{\mathsf{K4}}_{\mathrm{sat}}\)} \BinaryInfC{\(\nec \kappa^{\nec} \wedge \bigwedge_{\phi \in \Theta} \pos \kappa^{\pos}_\phi \wedge \bigwedge (\Gamma \cap V_+) \wedge \neg (\Delta \cap V_-) : \nec \Sigma, \Gamma \gg \nec \Theta, \Delta\)} \DisplayProof\]
As promised, every interpolation template has an associated positive modalized equational system. The proof of this fact can be found in the appendix.
Lemma 10. For any interpolation template \(T\) and for any \(x_w \in B_T\) let us write \(\kappa_{x_w}\) to denote the preinterpolant of \(T\) at \(w^\circ\). There is an enumeration \(\bar{x} = (x_0,\ldots,x_{n-1})\) of \(B_T\) such that the equational system \(\mathcal{E}_T = \left\{(x_i, +, \kappa_{x_i}) \mid i < n\right\}\) is a positive modalized equational system over \((\bar{x}, V_+, V_-)\). As a corollary, \(\mathcal{E}_T\) is solvable in \(\mathsf{GLS}\).
Definition 16 (Interpolant). Let \(T\) be an interpolation template, \((\cdot)^*\) a solution of \(\mathcal{E}_T\) and for each node \(w\) of \(T\) let us denote the preinterpolant at \(w\) as \(\kappa_w\). The interpolant given by \(T\) is defined as \(\iota_T = \kappa_\epsilon^*\).
The interpolant given by an interpolation template \(T\) depends on the chosen solution of \(\mathcal{E}_T\). This does not matter to us, as in the end one can show that any two uniform interpolants are logically equivalent. Also note that, by definition of solution of a Lyndon equational system over \((\bar{x},V_+,V_-)\) we automatically have that each \(\iota_T\) is a formula (and not a pseudoformula) and \(\mathrm{Voc}_b(\iota_T) \subseteq V_b\) for \(b \in \left\{+,-\right\}\). Finally, to show that the interpolant has the necessary properties, we will need two additional lemmas.
Lemma 11. Let \(T\) be an interpolation template of \(\Gamma \gg \Delta\). Then \(\mathcal{G}^\infty \mathsf{GLS} \vdash \Gamma \gg \Delta, \iota_T\).
Proof. Given a node \(w\) of \(T\) let \(\Gamma_w \gg_{w} \Delta_w\) denote the sequent at \(w\) and \(\kappa_w\) be the preinterpolant of \(T\) at \(w\). The trick is to build a function \(\alpha\) such that given a node \(w\) of \(T\), \(\alpha(w)\) is a proof in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}+ \mathrm{Wk}+ \mathrm{Ctr}\) of \(\Gamma_w \gg_w \Delta_w, \kappa^*_w\). Since \(\mathrm{Ctr}\) is derivable with \(\mathrm{Cut}\), \(\mathrm{Wk}\) is eliminable in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}\) and \(\mathrm{Cut}\) is eliminable in \(\mathcal{G}^\infty \mathsf{GLS}\), we can obtain the desired proof in \(\mathcal{G}^\infty \mathsf{GLS}\). \(\alpha\) is defined in Appendix 6. ◻
Lemma 12. Let \(T\) be an interpolation template of \(\Gamma \gg \Delta\) and let \(\Phi \gg \Psi\) be a sequent such that \(\mathrm{Voc}_b(\Phi \gg \Psi) \subseteq V_b\) for \(b \in \left\{+,-\right\}\). Then \(\mathcal{G}^\infty \mathsf{GLS} \vdash \Gamma, \Gamma' \gg \Delta, \Delta'\) implies \(\mathcal{G}^\infty \mathsf{GLS} \vdash \iota_T, \Gamma' \gg \Delta'\).
Proof. Given a node \(w\) of \(T\) let \(\Gamma_w \gg_{w} \Delta_w\) denote the sequent at \(w\) and \(\kappa_w\) be the preinterpolant of \(T\) at \(w\). The trick is to build a function \(\beta\) such that given a node \(w\) of \(T\) and a proof \(\pi \vdash \Gamma_w, \Phi \gg_{w} \Delta_w, \Psi\) in \(\mathcal{G}^\infty \mathsf{GLS}\) such that \(\mathrm{Voc}_{b}(\Phi \gg_{w} \Psi) \subseteq V_b\) for \(b \in \left\{+,-\right\}\) , \(\beta(w,\pi)\) is a proof in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}+ \mathrm{Wk}+ \mathrm{Ctr}\) of \(\kappa_w^*, \Phi \gg_w \Psi\). Since \(\mathrm{Ctr}\) is derivable with \(\mathrm{Cut}\), \(\mathrm{Wk}\) is eliminable in \(\mathcal{G}^\infty \mathsf{GLS} + \mathrm{Cut}\) and \(\mathrm{Cut}\) is eliminable in \(\mathcal{G}^\infty \mathsf{GLS}\), we can obtain the desired proof in \(\mathcal{G}^\infty \mathsf{GLS}\). The definition of \(\beta\) can be found in Appendix 6. ◻
We finish the paper with the desired result.
Theorem 5. \(\mathsf{GLS}\) has uniform Lyndon interpolation.
Proof. Let \(T\) be an interpolation template for \(\phi \Rrightarrow\). It is easy to show using Lemmas 11 and 12 that \(\iota_T\) is the uniform Lyndon interpolant of \(\phi\) for given vocabularies \((V^+,V_-)\). ◻
The method to establish uniform Lyndon interpolation via non-wellfounded proofs can be applied to a plethora of provability logics, once sequent calculi for these logics have been developed. We leave it as future work to apply the methodology to other provability logics, such as unary interpretability or bimodal provability logics. In addition, there are two possible extensions of the method which need further exploration. One direction is to investigate logics without simple Lyndon fixpoints, such as interpretability logic \(\mathsf{IL}\), and see if it is still possible to solve positive modalized Lyndon equational systems. The other direction is to study whether the method is applicable to intuitionistic provability logics, where the resulting Lyndon equational system does not need to be positive.
We would like to thank Taishi Kurahashi for his interest in these methods and for bringing our attention to the problem of proving ULIP for \(\mathsf{GLS}\).
We display some possible cut reductions which were not consider at the proof of Theorem 3.
Weakening part. If \(\chi\) belongs to the weakening part of the last rule instance of \(\pi\) or \(\tau\) we can delete directly, as weakening parts can be modified arbitrarily. From now on we assume that \(\chi\) does not occur in the weakening part of the rule instances.
Axiomatic. Assume \(\pi\) ends in \((\mathrm{ax})\), the case for \(\tau\) is analogous. Then \(\chi = p\) for some variable \(p\) and the desired reduction is \[\AxiomC{\(\)} \RightLabel{\(\mathrm{ax}\)} \UnaryInfC{\(p, \Gamma' \gg \Delta, p\)} \DisplayProof \quad \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(p, p, \Gamma' \gg \Delta\)} \DisplayProof \longmapsto \AxiomC{\(\mathrm{Ctr}(\tau)\)} \noLine \UnaryInfC{\(p, \Gamma' \gg \Delta\)} \DisplayProof\] where \(\Gamma = p, \Gamma'\).
If \(\pi\) ends in \(\bot\mathrm{L}\) then \(\chi\) would belong to the weakening part, which is already covered. Assume \(\tau\) ends in \(\bot\mathrm{L}\), so \(\chi = \bot\). \[\AxiomC{\(\pi\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta, \bot\)} \DisplayProof \quad \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(\bot, \Gamma \gg \Delta\)} \DisplayProof \longmapsto \AxiomC{\(\mathrm{inv}_{\bot\mathrm{R}}(\pi)\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta\)} \DisplayProof\]
From now own we assume that neither \(\pi\) nor \(\tau\) end in \((\mathrm{ax})\) or \((\bot\mathrm{L})\).
\(\bot\mathrm{R}\) case. Asssume \(\pi\) ends in an application of \((\bot\mathrm{R})\), the case for \(\tau\) is analogous. If \(\bot\) is the cut formula, the desired cut reduction is obtained taking the immediate subproof of \(\pi\). If \(\bot\) is not the cut formula, the desired cut reduction is \[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta', \chi\)} \RightLabel{\(\bot\mathrm{R}\)} \UnaryInfC{\(\Gamma \gg \bot, \Delta', \chi\)} \DisplayProof \quad \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(\chi, \Gamma \gg \bot, \Delta'\)} \DisplayProof \longmapsto \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta', \chi\)} \AxiomC{\(\mathrm{inv}_{\bot\mathrm{R}}(\tau)\)} \noLine \UnaryInfC{\(\chi, \Gamma \gg \Delta'\)} \RightLabel{\(\mathrm{Cut}\text{(I.H.)}\)} \BinaryInfC{\(\Gamma \gg \Delta'\)} \DisplayProof\] where \(\Delta = \bot, \Delta'\).
From now own we assume that neither \(\pi\) nor \(\tau\) end in \((\bot\mathrm{R})\).
Principal cut reduction. Assume \(\chi\) is principal in \(\pi\) and \(\tau\). Then either \(\chi\) is an implication or a \(\nec\)-formula. The second case is covered at the proof of Theorem 3, so we just show the cut reduction for the first. \[\begin{gather} \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\chi_0, \Gamma \gg \Delta, \chi_1\)} \RightLabel{\({\to}\mathrm{R}\)} \UnaryInfC{\(\Gamma \gg \Delta, \chi_0 \to \chi_1\)} \DisplayProof \quad \AxiomC{\(\tau_0\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta, \chi_0\)} \AxiomC{\(\tau_1\)} \noLine \UnaryInfC{\(\chi_1, \Gamma \gg \Delta\)} \RightLabel{\({\to}\mathrm{L}\)} \BinaryInfC{\(\chi_0 \to \chi_1, \Gamma \gg \Delta\)} \DisplayProof\\ \\ \longmapsto \AxiomC{\(\mathrm{Wk}(\tau_0)\)} \noLine \UnaryInfC{\(\Gamma \gg \Delta, \chi_1, \chi_0\)} \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\chi_0, \Gamma \gg \Delta, \chi_1\)} \RightLabel{\(\mathrm{Cut}\text{(I.H.)}\)} \BinaryInfC{\(\Gamma \gg \Delta, \chi_1\)} \AxiomC{\(\tau_1\)} \noLine \UnaryInfC{\(\chi_1, \Gamma \gg \Delta\)} \RightLabel{\(\mathrm{Cut}\text{(I.H.)}\)} \BinaryInfC{\(\Gamma \gg \Delta\)} \DisplayProof \end{gather}\]
Commutative cut reduction. Finally, assume that the cut formula is not principal in either \(\pi\) or \(\tau\). Assume that the cut formula is not principal in \(\pi\) and the last rule of \(\pi\) is \(({\to}\mathrm{R})\), the cases where the rule is instead \(({\to}\mathrm{R})\) or \((\mathrm{T})\), or where any of these occurs at \(\tau\) are analogous. The desired cut reduction is
\[\AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\phi, \Gamma \Rightarrow \psi, \Delta', \chi\)} \RightLabel{\({\to}\mathrm{R}\)} \UnaryInfC{\(\Gamma \Rightarrow \phi \to \psi, \Delta', \chi\)} \DisplayProof \quad \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(\chi, \Gamma \Rightarrow \phi \to \psi, \Delta'\)} \DisplayProof \longmapsto \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\phi, \Gamma \Rightarrow \psi, \Delta', \chi\)} \AxiomC{\(\mathrm{inv}_{{\to}\mathrm{R}}(\tau)\)} \noLine \UnaryInfC{\(\chi, \phi, \Gamma \Rightarrow \psi, \Delta'\)} \RightLabel{\(\mathrm{Cut}\text{ (I.H.)}\)} \BinaryInfC{\(\phi, \Gamma \Rightarrow \psi, \Delta'\)} \RightLabel{\({\to}\mathrm{R}\)} \UnaryInfC{\( \Gamma \Rightarrow \phi \to \psi, \Delta'\)} \DisplayProof\] where \(\Delta = \phi \to \psi, \Delta'\)
Finally, we have that the cut formula is not principal in either \(\pi\) or \(\tau\) with last rule \((\nec^{\mathsf{K4}})\). We notice that this cannot occur in \(\pi\), as then the cut formula would belong to the weakening part, so it must occur in \(\tau\). To make the cut formula not belong to the weakening part it must be the case that \(\chi = \nec \chi_0\). If \(\chi\) where not principal in \(\pi\), then we would be in one of the cases which we already covered, so we can assume it is prinicipal in \(\pi\), so \(\pi\) must end in \((\nec^{\mathsf{K4}})\). This case was covered at the proof of Theorem 3.
We will show that we can obtain a cyclic preproof, this preproof will be a proof since all the rules strictly lower the saturation complexity of sequents from conclusion to premises except for \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\) (so to repeat a sequent we must at least apply \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\) once, as otherwise the repeated sequent would have strictly saturation complexity than itself). Take the sequent \(\Gamma \gg \Delta\) and start applying the rules of Figure 3 as possible (note that for any sequent it is always possible to apply at least one), and whenever a repetition in the same branch is found make the leaf a repetition node. If we show that in this process no infinite branch is generated we would finish.
Assume otherwise, so there is a branch without repetitions. As the only rule which not strictly lowers the saturation complexity is \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\), it must be the case that \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\) is applied infinitely often. We notice that the rules of Figure 3 fulfill the subformula property, so all the formulas occuring on the branch must be in the set \(\mathrm{Sub}(\Gamma \gg \Delta)\). Also, the premises of \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\) are determined by choosing a formula (or nothing in the case of the left-most premise) and a set of formulas, so in fact the possible number of such premises is not bigger than \((k+1)2^k\), where \(k\) is the cardinality of \(\mathrm{Sub}(\Gamma \gg \Delta)\). Since there is infinitely many nodes in the branch which are premises of \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\), and only finitely many possibilities, there must be a repetition, absurd.
Given a node \(w\) of \(T\) let \(\mathrm{hg}(w)\) denote the height of \(w\), i.e., the height of the subtree generated by \(w\) (then leafs have height \(0\) and the root has the same height as the tree). If \(\mathrm{hg}(T) = H\), let \(\bar{x}_i\) for \(i \leq H\) be an arbitrary linear ordering of \(\left\{x_{w} \mid w \text{ repeat node and } \mathrm{hg}(w^\circ) = i\right\}\). Consider the enumeration of \(B_T\) defined as \(\bar{x}_T = \bar{x}_0 \cdots \bar{x}_H\) and let us show that \(\mathcal{E}_T\) is an positive modalized equational system over \((\bar{x}_T, V_+, V_-)\).
The positivy of \(\mathcal{E}_T\) is straightforward by definition. In addition, one can check that for any node \(w\), \(\mathrm{Voc}_+(\kappa_w) \subseteq V_+ \cup B_+\) and \(\mathrm{Voc}_-(\kappa_w) \subseteq V_-\) by induction on the length of \(w\). So all left to show is that it is modalized, let \(\bar{x}_T = (x_0,\ldots,x_{n-1})\) and for each \(i < n\) let us write \(w_i\) to mean the repeat node such that \(x_i = x_{w_i}\). First, we notice three facts.
If \(w\) is a repeat node and \(v \not \leq w\) then \(x_w\) does not occur in \(\kappa_w\).
If \(w\) is the conclusion of a \(\nec^{\mathsf{K4}}_{\mathrm{sat}}\) rule, then \(\kappa_w\) is modalized in all the variables of \(B_T\).
For any \(x \in B_T\), if \(w\) is a non-repeat node with immediate successors \(w0, \ldots, w(n-1)\) and \(\kappa_{w0}\), …, \(\kappa_{w(n-1)}\) are modalized in \(x\) then \(\kappa_w\) is modalized in \(\kappa_{w}\).
Additionally, thanks to the definition of \(\bar{x}_T\) we have that if \(i \leq j\) then either \(w^\circ_j \leq w^\circ_i\) or \(w^\circ_j\) and \(w^\circ_i\) are incomparable. Using this with the previous facts gives that for any \(i \leq j\) we have that \(\kappa_{w^\circ_j}\) is modalised in \(x_i\), as desired.
We will define \(\alpha\) corecursively, that \(\alpha(w)\) is a preproof will be trivial from construction. When the definition is finished we will show that it is indeed a proof. We proceed by cases on the shape of \(w\).
Case \(w\) is \((\mathrm{ax})\) or \((\bot\mathrm{L})\). \(\alpha(w)\) is obtained by applying rule \((\mathrm{ax})\) or \((\bot\mathrm{L})\), respectively.
Case \(w\) is \((\mathrm{Emp})\). \(\alpha(w)\) is a proof of \(\gg_w \top\), which is straightforward to obtain.
Case \(w\) is \((\mathrm{T}_{\mathrm{sat}})\). Then the function is defined as \[\AxiomC{\(w0\)} \noLine \UnaryInfC{\(\kappa : \necd \phi, \Gamma'_w \Rrightarrow \Delta_w\)} \RightLabel{\(\mathrm{T}_{\mathrm{sat}}\)} \UnaryInfC{\(\kappa : \nec \phi, \Gamma'_w \Rrightarrow \Delta_w\)} \DisplayProof \qquad \overset{\alpha}{\longmapsto} \qquad \AxiomC{\(\alpha(w0)\)} \noLine \UnaryInfC{\(\necd \phi, \Gamma'_w \Rrightarrow \Delta_w, (\kappa)^*\)} \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\nec \phi, \Gamma'_w \Rrightarrow \Delta_w, (\kappa)^*\)} \DisplayProof\] where \(\kappa_w = \kappa\), \({\gg}_w = {\Rrightarrow}\) and \(\Gamma_w = \nec\phi, \Gamma'_w\).
Case \(w\) is \(({\to}\mathrm{L}_{\mathrm{sat}})\) or \(({\to}\mathrm{R}_{\mathrm{sat}})\). Analogous to the \((\mathrm{T}_{\mathrm{sat}})\) case.
Case \(w\) is \((\mathrm{Rep})\). The function is defined as \[\AxiomC{\(\)} \RightLabel{\(\mathrm{Rep}\)} \UnaryInfC{\(x_w : \Gamma_w \gg_w \Delta_w\)} \DisplayProof \quad \overset{\alpha}{\longmapsto} \quad \AxiomC{\(\alpha(w^\circ)\)} \noLine \UnaryInfC{\(\Gamma_w \gg_w \Delta_w, \kappa_{w^\circ}^*\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\Gamma_w \gg_w \Delta_w, x^*_w, \kappa_{w^\circ}^*\)} \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(\kappa_{w^\circ}^*, \Gamma_w \gg_w \Delta_w, x^*_w\)} \RightLabel{\(\mathrm{Cut}\)} \BinaryInfC{\(\Gamma_w \gg_w \Delta_w, x^*_w\)} \DisplayProof\] where \(\tau\) is a proof of \(\kappa_{w^\circ}^*, \Gamma_w \gg_w \Delta_w, x^*_w\) in \(\mathcal{G}^\infty \mathsf{GLS}\) which exists since \(\mathsf{GLS}\vdash x^*_w \leftrightarrow \kappa^*_{w^\circ}\).
Case \(w\) is \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\). Then \(w\) is of shape \[\AxiomC{\(\begin{matrix} w^{\nec} \\ \kappa^{\nec} : \necd \Sigma^s \Rightarrow \end{matrix}\)} \AxiomC{\(\left[\begin{matrix} w^{\pos}_\phi \\ \kappa^{\pos}_\phi : \necd \Sigma^s \Rightarrow \phi\end{matrix}\right]_{\phi \in \Theta}\)} \RightLabel{\(\nec^{\mathsf{K4}}_{\mathrm{sat}}\)} \BinaryInfC{\(\nec \kappa^{\nec} \wedge \bigwedge_{\phi \in \Theta} \pos \kappa^{\pos}_\phi \wedge \bigwedge (\Gamma'_w \cap V_+) \wedge \neg (\Delta'_w \cap V_-) : \nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w\)} \DisplayProof\] where \(\kappa_w =\nec \kappa^{\nec} \wedge \bigwedge_{\phi \in \Theta} \pos \kappa^{\pos}_\phi \wedge \bigwedge (\Gamma'_w \cap V_+) \wedge \neg (\Delta'_w \cap V_-)\), \({\gg_w} = {\gg}\), \(\Gamma_w = \nec \Sigma, \Gamma'_w\) and \(\Delta_w = \nec \Theta, \Delta'_w\). Since \((\cdot)^* : B_T \longrightarrow \mathcal{L}_{\nec}\) and \(B_T \cap\text{Var} = \varnothing\) we have that \[\kappa^*_w = \nec (\kappa^{\nec})^* \wedge \bigwedge_{\phi \in \Theta} \pos (\kappa^{\pos}_\phi)^* \wedge \bigwedge (\Gamma'_w \cap V_+) \wedge \neg (\Delta'_w \cap V_-).\] So to build a preproof of \(\Gamma_w \gg_w \Delta, \kappa^*_w\) we build a preproof for each of the conjuncts and join them using \(({\wedge}\mathrm{R})\).
Proof for \(\nec\kappa^{\nec}\) and \(\pos \kappa^{\nec}_\phi\) for \(\phi \in \Theta\). \(\alpha(w)\) is respectively: \[\AxiomC{\(\alpha(w^{\nec})\)} \noLine \UnaryInfC{\(\necd \Sigma^s \Rightarrow (\kappa^{\nec})^*\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w, \nec(\kappa^{\nec})^*\)} \DisplayProof \qquad \AxiomC{\(\alpha(w^{\pos}_\phi)\)} \noLine \UnaryInfC{\(\necd \Sigma^s \Rightarrow \phi, (\kappa^{\pos}_\phi)^*\)} \RightLabel{\({\neg}\mathrm{L}+ \mathrm{Wk}\)} \UnaryInfC{\(\necd\neg (\kappa^{\pos}_\phi)^*, \necd \Sigma^s \Rightarrow \phi \)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \neg (\kappa^{\pos}_\phi)^*, \nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w\)} \RightLabel{\({\neg}\mathrm{R}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w, \pos(\kappa^{\pos}_\phi)^*\)} \DisplayProof\]
Proof for \(p \in \Gamma'_w \cap V_+\) and \(\neg q\) where \(q \in \Delta'_w \cap V_-\). In each case the preproof is, respectively: \[\AxiomC{\(\)} \RightLabel{\(\mathrm{ax}\)} \UnaryInfC{\( \nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w, p\)} \DisplayProof \qquad \AxiomC{\(\)} \RightLabel{\(\mathrm{ax}\)} \UnaryInfC{\(q, \nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w\)} \RightLabel{\({\neg}\mathrm{R}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w, \neg q\)} \DisplayProof\]
To each node \(w\) assign the measure \((|\Gamma_w \gg_w \Delta_w|_{\mathrm{sat}}, \mathrm{lgh}(w))\) with the lexicographic order. We notice that in each case the measure decreases from \(w\) to its corecursive calls, except when \(w\) is \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\). However, in this case there is an application of \(\nec^{\mathsf{K4}}\) from the root of \(\alpha(w)\) to the corecursive calls, guaranteeing progress.
We will define \(\beta\) corecursively. That \(\beta(w, \pi)\) is a preproof will be trivial from construction, when the definition is finished we will show that it is indeed a proof. We proceed by cases on the shape of \(w\).
Case \(w\) is \((\mathrm{ax})\) or \((\bot\mathrm{L})\). \(\beta(w,\pi)\) is obtained by applying rule \((\bot\mathrm{L})\).
Case \(w\) is \((\mathrm{Emp})\). \(\beta(w,\pi)\) is obtained from \(\pi\) by applying the weakening rule.
Case \(w\) is \((\mathrm{T}_{\mathrm{sat}})\). Then the function is defined as \[\left(\AxiomC{\(w0\)} \noLine \UnaryInfC{\(\kappa : \necd \phi, \Gamma'_w \Rrightarrow \Delta_w\)} \RightLabel{\(\mathrm{T}_{\mathrm{sat}}\)} \UnaryInfC{\(\kappa : \nec \phi, \Gamma'_w \Rrightarrow \Delta_w\)} \DisplayProof, \quad \AxiomC{\(\pi\)} \noLine \UnaryInfC{\(\nec \phi, \Gamma'_w, \Phi \Rrightarrow \Delta_w, \Psi\)} \DisplayProof\right) \qquad \overset{\beta}{\longmapsto} \qquad \AxiomC{\(\beta(w0,\mathrm{Wk}(\pi))\)} \noLine \UnaryInfC{\(\kappa^*, \Phi \Rrightarrow \Psi\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\kappa^*, \Phi \Rrightarrow \Psi\)} \DisplayProof\] where \(\kappa_w = \kappa\), \({\gg}_w = {\Rrightarrow}\) and \(\Gamma_w = \nec\phi, \Gamma'_w\).
Case \(w\) is \(({\to}\mathrm{L}_{\mathrm{sat}})\) or \(({\to}\mathrm{R}_{\mathrm{sat}})\). Analogous to the \((\mathrm{T}_{\mathrm{sat}})\) case.
Case \(w\) is \((\mathrm{Rep})\). The function is defined as \[\AxiomC{\(\)} \RightLabel{\(\mathrm{Rep}\)} \UnaryInfC{\(x_w : \Gamma_w \gg_w \Delta_w\)} \DisplayProof, \quad \AxiomC{\(\pi\)} \noLine \UnaryInfC{\(\Gamma_w, \Phi \gg_w \Delta_w, \Psi\)} \DisplayProof \quad \overset{\beta}{\longmapsto} \quad \AxiomC{\(\tau\)} \noLine \UnaryInfC{\(x^*_w, \Phi \gg_w \Psi, \kappa_{w^\circ}^*\)} \AxiomC{\(\beta(w^\circ, \pi)\)} \noLine \UnaryInfC{\(\kappa^*_{w^\circ}, \Phi \gg_w \Psi\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\kappa^*_{w^\circ},x^*_w, \Phi \gg_w \Psi\)} \RightLabel{\(\mathrm{Cut}\)} \BinaryInfC{\( x^*_w, \Phi \gg_w \Psi\)} \DisplayProof\] where \(\tau\) is a proof of \(x^*_w, \Phi \gg_w \Psi, \kappa_{w^\circ}^*\) in \(\mathcal{G}^\infty \mathsf{GLS}\) which exists since \(\mathsf{GLS}\vdash x^*_w \leftrightarrow \kappa^*_{w^\circ}\).
Case \(w\) is \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\). Then \(w\) is of shape \[\AxiomC{\(\begin{matrix} w^{\nec} \\ \kappa^{\nec} : \necd \Sigma^s \Rightarrow \end{matrix}\)} \AxiomC{\(\left[\begin{matrix} w^{\pos}_\phi \\ \kappa^{\pos}_\phi : \necd \Sigma^s \Rightarrow \phi\end{matrix}\right]_{\phi \in \Theta}\)} \RightLabel{\(\nec^{\mathsf{K4}}_{\mathrm{sat}}\)} \BinaryInfC{\(\nec \kappa^{\nec} \wedge \bigwedge_{\phi \in \Theta} \pos \kappa^{\pos}_\phi \wedge \bigwedge (\Gamma'_w \cap V_+) \wedge \neg (\Delta'_w \cap V_-) : \nec \Sigma, \Gamma'_w \gg \nec \Theta, \Delta'_w\)} \DisplayProof\] where \(\kappa_w =\nec \kappa^{\nec} \wedge \bigwedge_{\phi \in \Theta} \pos \kappa^{\pos}_\phi \wedge \bigwedge (\Gamma'_w \cap V_+) \wedge \neg (\Delta'_w \cap V_-)\), \({\gg_w} = {\gg}\), \(\Gamma_w = \nec \Sigma, \Gamma'_w\) and \(\Delta_w = \nec \Theta, \Delta'_w\). We proceed by further case analysis in the last rule applied to \(\pi\).
Last rule is \(\mathrm{ax}\). We have that a propositional variable \(p\) must occur at the left and right side of the sequent. Since \((\Gamma'_w \cap\Delta'_w) \cap\text{Var} = \varnothing\) we have three options. If \(p \in \Phi \cap\Psi\) then the desired proof is just \(\mathrm{ax}\). If \(p \in \Gamma'_w \cap\Psi\), then \(p \in \Psi\) implies that \(p \in V_+\) and the desired proof is using that \(p\) is a conjunct of \(\kappa^*_w\). If \(p \in \Phi \cap\Delta'_w\), then \(p \in \Phi\) implies that \(p \in V_-\) and the desired proof is using that \(\neg p\) is a conjunct of \(\kappa^*_w\).
Last rule is \(\bot\mathrm{L}\). Since \(\bot \not \in \Gamma'_w\) (by definition of \(\nec^{\mathsf{K4}}_{\mathrm{sat}}\)), it must be the case that \(\bot \in \Phi\). Then the desired preproof is obtained using \(\bot\mathrm{L}\).
Last rule is \(\bot\mathrm{R}\). If \(\bot \in \Delta'_w\) then \(\Delta'_w = \bot, \Delta''_w\). We define \(\beta\) as \[\left(w,\quad \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \Theta, \Delta''_w, \Psi\)} \RightLabel{\(\bot\mathrm{R}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \Theta, \bot, \Delta''_w, \Psi\)} \DisplayProof \right) \quad \overset{\beta}{\longmapsto} \quad \AxiomC{\(\beta(w,\mathrm{Wk}(\pi_0))\)} \noLine \UnaryInfC{\(\kappa^*_w, \Phi \gg \Psi\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\kappa^*_w, \Phi \gg \Psi\)} \DisplayProof\] If \(\bot \not \in \Delta'_w\) then \(\bot \in \Psi\) so \(\Psi = \bot, \Psi'\). We define \(\beta\) as \[\left(w,\quad \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \Theta, \Delta'_w, \Psi'\)} \RightLabel{\(\bot\mathrm{R}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \Theta, \Delta''_w, \bot, \Psi'\)} \DisplayProof \right) \quad \overset{\beta}{\longmapsto} \quad \AxiomC{\(\beta(w,\pi_0)\)} \noLine \UnaryInfC{\(\Phi \gg \Psi'\)} \RightLabel{\(\bot\mathrm{R}\)} \UnaryInfC{\(\Phi \gg \bot,\Psi'\)} \DisplayProof\]
Last rule is \((\mathrm{T})\). If the principal formula \(\nec\phi\) of \((\mathrm{T})\) is in \(\nec \Sigma\), then we know by saturation that \(\phi \in \nec \Sigma, \Gamma'_w\). Let \(\Sigma' = \phi, \Sigma\), we define \(\beta\) as \[\left( w, \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \phi, \nec \Sigma', \Gamma'_w, \Phi \Rrightarrow \nec \Theta, \Delta'_w, \Psi\)} \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\nec \phi, \nec \Sigma', \Gamma'_w, \Phi \Rrightarrow \nec \Theta, \Delta'_w, \Psi\)} \DisplayProof \right) \overset{\beta}{\longmapsto} \AxiomC{\(\beta(w,\mathrm{Ctr}(\pi_0))\)} \noLine \UnaryInfC{\(\kappa^*_w, \Phi \Rrightarrow \Psi\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\kappa^*_w, \Phi \Rrightarrow \Psi\)} \DisplayProof\] where we contract \(\pi_0\) to get rid of one instance of \(\phi\) at the left. If the principal formula \(\nec \phi\) of \((\mathrm{T})\) is not in \(\nec \Sigma\), it must be in \(\Phi\), so let \(\Phi = \nec \phi, \Phi'\). We define \(\beta\) as \[\left( w, \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \necd \phi, \Phi' \Rrightarrow \nec \Theta, \Delta'_w, \Psi\)} \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \nec\phi,\Phi' \Rrightarrow \nec \Theta, \Delta'_w, \Psi\)} \DisplayProof \right) \overset{\beta}{\longmapsto} \AxiomC{\(\beta(w,\pi_0)\)} \noLine \UnaryInfC{\(\kappa^*_w, \necd \phi, \Phi' \Rrightarrow \Psi\)} \RightLabel{\(\mathrm{T}\)} \UnaryInfC{\(\kappa^*_w, \nec \phi, \Phi' \Rrightarrow \Psi\)} \DisplayProof\]
Last rule is \(({\to}\mathrm{L})\) or \(({\to}\mathrm{R})\). Analogous to \((\mathrm{T})\) case (with cases on where the principal formula occurs and possibly needed to use admissibility of contraction and weakening at proof \(\pi\)).
Last rule is \(\nec^{\mathsf{K4}}\). If the principal formula \(\nec \phi\) of \(\nec^{\mathsf{K4}}\) is in \(\nec \Theta\), then let \(\nec \Theta = \nec \phi, \nec \Theta'\). We define \(\beta\) as \[\left( w, \quad \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma', \necd \Phi_{\nec} \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \phi, \nec \Theta', \Delta'_w, \Psi\)} \DisplayProof \right) \quad \overset{\beta}{\longmapsto} \quad \AxiomC{\(\beta\left(w^{\pos}_\phi, \mathrm{Wk}(\pi_0)\right)\)} \noLine \UnaryInfC{\((\kappa^{\pos}_\phi)^*, \necd \Phi_{\nec} \Rightarrow \)} \RightLabel{\({\neg}\mathrm{R}\)} \UnaryInfC{\(\necd \Phi_{\nec} \Rightarrow \neg (\kappa^{\pos}_\phi)^*\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\Phi \gg \nec \neg (\kappa^{\pos}_\phi)^*, \Psi\)} \RightLabel{\({\neg}\mathrm{L}\)} \UnaryInfC{\(\pos (\kappa^{\pos}_\phi)^*, \Phi \gg \Psi\)} \doubleLine \RightLabel{\(\mathrm{Wk}+ {\wedge}\mathrm{L}\)} \UnaryInfC{\(\kappa^*_w, \Phi \gg \Psi\)} \DisplayProof\] where \(\Sigma' \subseteq \Sigma\), \(\nec\Phi_{\nec} \subseteq \Phi\) and we applied weakening on \(\pi_0\) to obtain the full \(\necd \Sigma\) instead of \(\necd \Sigma'\). If the principal formula \(\nec \phi\) of \(\nec^{\mathsf{K4}}\) is in \(\Psi\), then let \(\Psi = \nec \phi, \Psi'\). We define \(\beta\) as \[\left( w, \quad \AxiomC{\(\pi_0\)} \noLine \UnaryInfC{\(\necd \Sigma', \necd \Phi_{\nec} \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec \Sigma, \Gamma'_w, \Phi \gg \nec \Theta, \Delta'_w, \nec \phi,\Psi'\)} \DisplayProof \right) \quad \overset{\beta}{\longmapsto} \quad \AxiomC{\(\beta(w^{\nec}, \mathrm{Wk}(\pi_0))\)} \noLine \UnaryInfC{\((\kappa^{\nec})^*, \necd \Phi_{\nec} \Rightarrow \phi\)} \RightLabel{\(\mathrm{Wk}\)} \UnaryInfC{\(\necd (\kappa^{\nec})^*, \necd \Phi_{\nec} \Rightarrow \phi\)} \RightLabel{\(\nec^{\mathsf{K4}}\)} \UnaryInfC{\(\nec(\kappa^{\nec})^*, \Phi \gg \nec\phi, \Psi'\)} \doubleLine \RightLabel{\(\mathrm{Wk}+ {\wedge}\mathrm{L}\)} \UnaryInfC{\(\kappa^*_w, \Phi \gg \nec \phi, \Psi'\)} \DisplayProof\] where \(\Sigma' \subseteq \Sigma\), \(\nec\Phi_{\nec} \subseteq \Phi\) and we applied weakening on \(\pi_0\) to obtain the full \(\necd \Sigma\) instead of \(\necd \Sigma'\).
To each pair \((w,\pi)\) assign the measure \((|\Gamma_w \gg_w \Delta_w|_{\mathrm{sat}}, \mathrm{lgh}(w), \mathrm{lhg}(\pi))\) with the lexicographic order. We notice that in each case the measure decreases from \((w,\pi)\) to its corecursive calls, except when \(w\) is \((\nec^{\mathsf{K4}}_{\mathrm{sat}})\) and \(\pi\) ends in the \((\nec^{\mathsf{K4}})\) rule. However, in this case there is an application of \((\nec^{\mathsf{K4}})\) from the root of \(\alpha(w)\) to the corecursive calls, guaranteeing progress.
[@*]
Research supported by the Swiss National Science Foundation project 200021_214820.↩︎
Uniform interpolation for \(\mathsf{GLS}\) follows easily from the fact that \(\mathsf{GL}\) has uniform interpolation, by the same proof as in [@lev-GLS]. Note though that the translation between \(\mathsf{GL}\) and \(\mathsf{GLS}\) described in that paper does not yield Lyndon interpolation, as it does not preserve the polarity of variables.↩︎
In the proof-theoretic tradition, it is common to study the concept of effective cut elimination, i.e. to study who to get rid of the cut rule in proofs using computable (effective) means. Often, cut-elimination is understood as effective cut-elimination and non-effective cut-elimination is called cut admissibility. This is justified since eliminablity and admissibility, as given in Definition 3, are equivalent for wellfounded proofs. However, this equivalence does not hold for non-wellfounded proofs. The best approximation we can get is Theorem 1. For this reason, we will not follow the tradition. For us, a rule being eliminable means exactly what it says: that the rule can be eliminated from the calculus without affecting the provability of sequents. In case we want to talk about the effectiveness of our methodology, we will say effective cut elimination explicitely.↩︎
This calculus is an minor variation of the ones appearing in [@lev-GLS; @GLSprooftheory].↩︎
In fact, this cut elimination procedure can be made effective (see the footnote on page ) since a finite approximation of the non-wellfounded proof will suffice to compute each of the steps.↩︎
This proof follows the proof in [@lindstrom] for \(\mathsf{GL}\), with the addition of the condition on the polarity of variables.↩︎