| Izvestiya: Mathematics |
|
|
|
|
|
This article is cited in 1 scientific paper (total in 1 paper) A realization theorem for the modal logic of transitive closure D. S. Shamkanovab a Steklov Mathematical Institute of Russian Academy of Sciences, Moscow b National Research University Higher School of Economics, Moscow
Bibliographic databases:
    § 1. IntroductionIt is worth to recall that justification logics are a family of epistemic systems whose language feature is the replacement of modal expressions $\Box A$ with $[h]A$, where $[h]A$ is interpreted as “$h$ is a justification for $A$”. A lot of research on justification logics has been undertaken since Artemov introduced the logic of proofs $\mathsf{LP}$ [2], where $[h] A$ is understood as “$h$ is a proof for $A$”. Among other things established by Artemov, a realization theorem relating $\mathsf{LP}$ and the standard modal logic $\mathsf{S4}$ has attracted considerable attention. This result involves the following notion of forgetful translation (or projection). For any formula $B$ of $\mathsf{LP}$, the forgetful translation of $B$ is obtained from the given formula by replacing all subformulas of the form $[h]C$ with $\Box C$. It is easy to see that the forgetful translation of every formula provable in $\mathsf{LP}$ is provable in $\mathsf{S4}$. The realization theorem states the converse: any formula $A$ provable in $\mathsf{S4}$ turns out to be the forgetful translation of a formula $B$ provable in $\mathsf{LP}$. Due to the theorem, the logic $\mathsf{LP}$ is called a justification counterpart of $\mathsf{S4}$. To date, justification counterparts of many modal logics have been found and corresponding realization theorems have been obtained. However, the epistemically important case of the modal logic of common knowledge still needs to be explored. The concept of common knowledge is captured in this logic according to the so-called fixed-point account, i.e., common knowledge of $A$ is defined as the greatest fixed-point of the mapping
$$
\begin{equation*}
X \mapsto (\text{everybody knows }A\text{ and everybody knows }X).
\end{equation*}
\notag
$$
Thus, the logic of common knowledge is a member of the family of modal fixed-point logics and, like other logics from the family, is difficult to study in many respects. Although Bucheli, Kuznets and Studer introduced a justification logic similar to the logic of common knowledge, whether one can prove the realization theorem remains to be an open question [6], [4]. Notice that, for the modified concept of common knowledge known as generic common knowledge, the corresponding modal logic has been shown to be realizable [1], [3]. This article focuses on the case of the logic of transitive closure $\mathsf{K}^+$, which is very similar to the case of the logic of common knowledge. The system $\mathsf{K}^+$ [8], [7], [9] is a Kripke-complete modal propositional logic whose language contains modal connectives $\Box$ and $\Box^+$. Like the logic of common knowledge, $\mathsf{K}^+$ belongs to the family of modal fixed-point logics, which can be explained as follows: in any $\mathsf{K^+}$-algebra $\mathcal{A}$, an element $\Box^+ a$ is the greatest fixed-point of a mapping $z \mapsto \Box a\wedge \Box z$. It is therefore not surprising that $\mathsf{K^+}$ is not valid in its canonical Kripke frame and is not strongly complete with respect to its Kripke semantics. In the given article, we present a justification counterpart of $\mathsf{K}^+$ and establish the corresponding realization theorem by means of a sequent calculus allowing non-well-founded proofs. We have chosen to work with $\mathsf{K^+}$ rather than the modal logic of common knowledge in order to reduce the number of syntactic details under consideration. At the same time, we believe that the methods of the article can be applied to the case of common knowledge logic as well. It remains to emphasize that, in addition to the result of this article, we know only one theorem about normal realization for a logic that is not Kripke canonical, namely, a realization theorem for the Gödel–Löb provability logic $\mathsf{GL}$ (see [11]). § 2. Logics $\mathsf{K}^+$ and $\mathsf{J}^+$In this section, we briefly recall some facts about the bimodal logic $\mathsf{K}^+$ (see [8] and [7]) and define a justification logic $\mathsf{J}^+$, which will be proved to be a counterpart of $\mathsf{K}^+$. We also prove some properties of $\mathsf{J}^+$ in order to use them later. Formulas of $\mathsf{K}^+$ are built from propositional variables $p_0, p_1, \dotsc$ and the constant $\bot$ by means of propositional connectives $\to$, $\Box$ and $\Box^+$. We consider other Boolean connectives as abbreviations: $\neg A:= A\to \bot$, $\top := \neg \bot$, $A \wedge B := \neg (A \to \neg B)$, $A \vee B := (\neg A\to B)$. The size of a formula $A$, denoted by $\operatorname{sz} (A)$, is defined inductively in the following way:
$$
\begin{equation*}
\begin{gathered} \, \operatorname{sz}(p):=1, \qquad \operatorname{sz}(\bot):=1, \qquad \operatorname{sz} (A\to B):= \operatorname{sz}(A)+\operatorname{sz}(B)+1, \\ \operatorname{sz}(\Box A):=\operatorname{sz}(A)+1,\qquad \operatorname{sz}(\Box^+ A):=\operatorname{sz}(A)+1. \end{gathered}
\end{equation*}
\notag
$$
The Frege–Hilbert calculus of the logic $\mathsf{K}^+$ is given by the following axioms and inference rules. Axioms:
Inference rules:
$$
\begin{equation*}
\textsf{mp}\frac{A \quad A\to B}{B}, \qquad \mathsf{nec}\frac{A}{\Box^+ A}.
\end{equation*}
\notag
$$
Recall that a bimodal Kripke frame $(W,R,S)$ is a $\mathsf{K}^+$-frame if the relation $S$ is the transitive closure of $R$. Proposition 1 (see [8], [7], [9]). The logic $\mathsf{K}^+$ is sound and weakly complete with respect to the class of $\mathsf{K}^+$-frame. Now we define a justification logic $\mathsf{J}^+$. The language of $\mathsf{J}^+$ contains three sorts of expressions: two sorts of terms and one sort of formulas. Justification terms of both sorts are simultaneously built from the disjoint countable sets of variables $\mathrm{JV}_1 =\{x_0, x_1, \dotsc \}$ and $\mathrm{JV}_2 =\{y_0, y_1, \dotsc \}$ and constants $\mathrm{JC}_2 =\{c_0, c_1, \dotsc \}$ according to the grammar:
$$
\begin{equation*}
\begin{aligned} \, w &::= x_i \mid (w \cdot w) \mid \mathsf{head}(s) \mid \mathsf{tail}(s) \mid (w+w), \\ s &::= y_i \mid c_i \mid (s \cdot s) \mid \mathsf{ind}(w,s) \mid (s+s), \end{aligned}
\end{equation*}
\notag
$$
where $w$ and $s$ stand for justification terms of the first and second sort, respectively. The corresponding sets of terms are denoted by $\mathrm{JT}_1$ and $\mathrm{JT}_2$. We call a justification term ground if it does not contain variables. Justification formulas are given by the grammar:
$$
\begin{equation*}
A::= p_i \mid \bot \mid (A \to A) \mid [w] A\mid [ s]_\mathsf{tc} \,A.
\end{equation*}
\notag
$$
We denote the set of justification formulas by $\mathrm{JF}$. The logic $\mathsf{J}^+_0$ is defined by the following axioms and the following inference rule. Axioms:
Inference rule: We introduce the logic $\mathsf{J}^+$ by adding the set of new axioms
$$
\begin{equation*}
\{ [c ]_\mathsf{tc} \,A \mid c \in \mathrm{JC}_2 \text{ and $A$ is an axiom of $\mathsf{J}^+_0$} \}
\end{equation*}
\notag
$$
to $\mathsf{J}^+_0$. Subsets of the given set of axioms are called constant specifications. For a constant specification $\mathrm{cs}$, let $\mathsf{J}^+_\mathrm{cs}$ be the fragment of $\mathsf{J}^+$ in which all axioms of the form $[c ]_\mathsf{tc} \,A $ are taken from $\mathrm{cs}$. Note that $\mathsf{J}^+_\varnothing$ is the same as $\mathsf{J}^+_0$. Additionally, we define the set of constants $\operatorname{Con}(\mathrm{cs})$ by setting $c\in \operatorname{Con}(\mathrm{cs})$ if and only if $[c ]_\mathsf{tc} \,A$ belongs to $\mathrm{cs} $ for some formula $A$. A constant specification $\mathrm{cs}$ is called injective if, for any $[c_i ]_\mathsf{tc} \,A$ and $[c_i ]_\mathsf{tc} \,B$ from $\mathrm{cs}$, the formulas $A$ and $B$ coincide. In other words, different axioms of $\mathsf{J}^+_0$ are associated with different constants in $\mathrm{cs}$. For a proof $\pi$ of $\mathsf{J}^+$, we denote the set of all axioms of the form $[c ]_\mathsf{tc} \,A$ in $\pi$ by $\mathrm{cs}(\pi)$. The proof $\pi$ is called injective if the constant specification $\mathrm{cs}(\pi)$ is injective. Note that any proof of $\mathsf{J}^+_\mathrm{cs}$, where $\mathrm{cs}$ is injective, is also injective. Further note that $\sigma(\mathrm{cs})= \{\sigma (C)\mid C\in \mathrm{cs}\} $ is an injective constant specification for any injective constant specification $\mathrm{cs}$ and any substitution
$$
\begin{equation*}
\sigma =[h_1/x_{i_1}, \dotsc, h_n/x_{i_n}, t_1/y_{j_1}, \dotsc, t_m/y_{j_m}],
\end{equation*}
\notag
$$
where $h_1,\dotsc, h_n$ ($t_1,\dotsc, t_m$) are justification terms of the first (second) sort. Lemma 1 (substitution). If $\mathsf{J}^+_\mathrm{cs} \vdash A$, then $\mathsf{J}^+_{\sigma(\mathrm{cs})} \vdash \sigma(A)$ for any substitution In particular, if $A$ has an injective proof in $\mathsf{J}^+ $, then so does $\sigma (A)$. Proof. The assumption $\mathsf{J}^+_\mathrm{cs} \vdash A$ immediately implies $\mathsf{J}^+_{\sigma(\mathrm{cs})} \vdash \sigma(A)$. In addition, if $A$ has an injective proof $\pi$ in $\mathsf{J}^+ $, then $\mathsf{J}^+_{\mathrm{cs}(\pi)} \vdash A$ and the constant specification $\mathrm{cs}(\pi)$ is injective. Therefore, $\sigma (\mathrm{cs}(\pi))$ is injective. Since $\mathsf{J}^+_{\sigma(\mathrm{cs})} \vdash \sigma(A)$, the formula $\sigma (A)$ has an injective proof in $\mathsf{J}^+_{\sigma(\mathrm{cs})}$ and in $\mathsf{J}^+ $. $\Box$ Lemma 2 (axiom internalization). Suppose $\mathsf{J}^+_{\mathrm{cs}_0} \vdash A$, where $\mathrm{cs}_0$ is a finite constant specification and $A$ is an axiom of $\mathsf{J}^+$. Then there exist a finite superset $\mathrm{cs}_1$ of $\mathrm{cs}_0$ and a ground justification term $s$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s]_\mathsf{tc} \, A$. Moreover, if $\mathrm{cs}_0$ is injective, then the same holds for $\mathrm{cs}_1$. Proof. If $A$ is an axiom of $\mathsf{J}^+_0$, then $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [c_i]_\mathsf{tc} \, A$, where $c_i$ is the first justification constant not belonging to $\operatorname{Con}(\mathrm{cs}_0)$ and $\mathrm{cs}_1:= \mathrm{cs}_0\cup \{[c_i]_\mathsf{tc} \, A\}$. If $A$ has the form $[c]_\mathsf{tc} \, B$, then $\mathsf{J}^+_{\mathrm{cs}_0} \vdash [ c]_\mathsf{tc}\, B \to [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B$. In this case, $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [c_i]_\mathsf{tc} \, ([ c]_\mathsf{tc}\, B \to [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B)$, where $c_i$ is the first justification constant not belonging to $\operatorname{Con}(\mathrm{cs}_0)$ and $\mathrm{cs}_1:= \mathrm{cs}_0\cup \{[c_i]_\mathsf{tc} \, ([ c]_\mathsf{tc}\, B \to [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B)\}$. Since $\mathsf{J}^+_{\mathrm{cs}_0} \vdash [ c]_\mathsf{tc}\, B$, we have $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [ c]_\mathsf{tc}\, B$ and $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B$. Therefore, $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B\wedge [c_i]_\mathsf{tc} \, ([ c]_\mathsf{tc}\, B \to [\mathsf{tail}(c)] [ c]_\mathsf{tc}\, B)$. Applying Axiom (ix), we obtain $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [\mathsf{ind}(\mathsf{tail}(c),c_i)]_\mathsf{tc}\, [ c]_\mathsf{tc}\, B$, i.e., $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [\mathsf{ind}(\mathsf{tail}(c),c_i)]_\mathsf{tc} \,A$. Trivially, in both cases, $\mathrm{cs}_1$ is injective if $\mathrm{cs}_0$ is injective. $\Box$ Lemma 3 (internalization). Suppose $\mathsf{J}^+_{\mathrm{cs}_0} \vdash A$, where $\mathrm{cs}_0$ is a finite constant specification. Then there exist a finite superset $\mathrm{cs}_1$ of $\mathrm{cs}_0$ and a ground justification term $s$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s]_\mathsf{tc} \, A$. Moreover, if $\mathrm{cs}_0$ is injective, then the same holds for $\mathrm{cs}_1$. Proof. Assume $\mathsf{J}^+_{\mathrm{cs}_0} \vdash A$ and consider a proof $\pi$ of $A$ in $\mathsf{J}^+_{\mathrm{cs}_0} $. Let $B_1, \dotsc, B_n$ be the axioms of $\mathsf{J}^+_{\mathrm{cs}_0} $ that mark the leaves of $\pi$. Successively applying the previous lemma to the formulas $B_1, \dotsc, B_n$ and expanding the resulting constant specifications, we find a finite superset $\mathrm{cs}_1$ of $\mathrm{cs}_0$ and ground justification terms $s_1,\dotsc, s_n$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s_i]_\mathsf{tc} \, B_i$ for $i\in\{1,\dotsc, n\}$. Moreover, $\mathrm{cs}_1$ is injective if $\mathrm{cs}_0$ is injective. Notice that $\pi$ is a tree whose leaves are marked by axioms $B_1, \dotsc, B_n$ and that is constructed according to the rule ($\mathsf{mp}$). Consequently, moving from the leaves of $\pi$ to its root and applying Axiom (vi), we can find, for each node $b$, a ground justification term $s_b$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s_b]_\mathsf{tc} \, C_b$, where $C_b$ is the formula of the node $b$. Therefore, there is a ground justification term $s$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s]_\mathsf{tc} \, A$. $\Box$ Lemma 4 (lifting lemma). Suppose Then there exists a justification term $h(z_1, \dotsc, z_n, y_1, \dotsc, y_m)$ depending only on the explicitly displayed variables such that for arbitrary variables $z_1, \dotsc, z_n$ of the first sort. Moreover, if the original proof is injective, the same holds for the later proof. Proof. Assume that
$$
\begin{equation*}
\mathsf{J}^+ \vdash A_1\wedge\dotsb \wedge A_n\wedge B_1\wedge\dotsb \wedge B_m \wedge [s_1]_\mathsf{tc}\, B_1\wedge\dotsb \wedge [s_m]_\mathsf{tc}\, B_m \to C.
\end{equation*}
\notag
$$
Then this formula is provable in $\mathsf{J}^+_{\mathrm{cs}_0}$ for some finite constant specification $\mathrm{cs}_0$. Therefore,
$$
\begin{equation*}
\mathsf{J}^+_{\mathrm{cs}_0} \vdash A_1\to (A_2 \to \dotsb (B_1\to \dotsb ([s_1]_\mathsf{tc}\, B_1\to \dotsb ([s_m]_\mathsf{tc}\, B_m \to C)\cdots).
\end{equation*}
\notag
$$
By Lemma 3, there exist a finite superset $\mathrm{cs}_1$ of $\mathrm{cs}_0$ and a ground justification term $t$ such that
$$
\begin{equation*}
\mathsf{J}^+_{\mathrm{cs}_1} \vdash [t]_\mathsf{tc} \, (A_1\to (A_2 \to \dotsb (B_1\to \dotsb ([s_1]_\mathsf{tc}\, B_1\to \dotsb ([s_m]_\mathsf{tc}\, B_m \to C)\cdots)).
\end{equation*}
\notag
$$
From Axiom (vii), it follows that
$$
\begin{equation*}
\mathsf{J}^+_{\mathrm{cs}_1} \vdash [\mathsf{head}(t)] (A_1\to (A_2 \to \dotsb (B_1\to \dotsb ([s_1]_\mathsf{tc}\, B_1\to \dotsb ([s_m]_\mathsf{tc}\, B_m \to C)\cdots)).
\end{equation*}
\notag
$$
Applying Axiom (iv) successively, we obtain
$$
\begin{equation*}
\begin{aligned} \, &\mathsf{J}^+_{\mathrm{cs}_1} \vdash [z_1]A_1\to ([z_2]A_2 \to \dotsb ([\mathsf{head}(s_1)]B_1\to \dotsb ([\mathsf{tail}(s_1)][s_1]_\mathsf{tc}\, B_1 \\ &\qquad\to \dotsb ([\mathsf{tail}(s_m)][s_m]_\mathsf{tc}\, B_m \to [h(z_1, \dotsc, z_n, s_1, \dotsc, s_m)] C)\cdots), \end{aligned}
\end{equation*}
\notag
$$
where $h(z_1, \dotsc, z_n, y_1, \dotsc, y_m)$ is equal to
$$
\begin{equation*}
(\cdots(\mathsf{head}(t)\cdot z_1) \cdots z_n) \cdot \mathsf{head}(y_1)) \cdots \mathsf{head}(y_m))\cdot \mathsf{tail}(y_1)) \cdots \mathsf{tail}(y_m).
\end{equation*}
\notag
$$
Hence, the formula
$$
\begin{equation*}
\begin{aligned} \, &[z_1]A_1\wedge\dotsb \wedge [z_n]A_n\wedge [\mathsf{head}(s_1)]B_1\wedge\dotsb \wedge [\mathsf{head}(s_m)]B_m \wedge [\mathsf{tail}(s_1)][s_1]_\mathsf{tc}\, B_1 \\ &\qquad\wedge\dotsb \wedge [\mathsf{tail}(s_m)][s_m]_\mathsf{tc}\, B_m \to [h(z_1, \dotsc, z_n, s_1, \dotsc, s_m)]C \end{aligned}
\end{equation*}
\notag
$$
is provable in $\mathsf{J}^+_{\mathrm{cs}_1}$. Applying Axiom (vii) and Axiom (viii), we conclude Note that the constant specifications $\mathrm{cs}_0$ and $\mathrm{cs}_1$ can be chosen to be injective if the original proof was injective. $\Box$ Lemma 5. If $\mathsf{J}^+ \vdash B \to [w] (A \wedge B)$, then there exists a justification term $t (x_0)$ depending only on $x_0$ such that $\mathsf{J}^+ \vdash B \to [t(w)]_\mathsf{tc} \, A$. Moreover, if the original proof is injective, the same holds for the later proof. Proof. Assume $\mathsf{J}^+ \vdash B \to [w] (A \wedge B)$. Then $\mathsf{J}^+_{\mathrm{cs}_0} \vdash B \to [w] (A \wedge B)$ for some finite constant specification $\mathrm{cs}_0$. We have $\mathsf{J}^+_{\mathrm{cs}_0} \vdash A\wedge B \to [w] (A \wedge B)$. By Lemma 3, there are a finite superset ${\mathrm{cs}_1}$ of ${\mathrm{cs}_0}$ and a ground term $s_0$ such that $\mathsf{J}^+_{\mathrm{cs}_1} \vdash [s_0]_\mathsf{tc} \, (A \wedge B \to [w] (A \wedge B))$. Hence, $\mathsf{J}^+_{\mathrm{cs}_1} \vdash B \to ([w] (A \wedge B) \wedge [s_0]_\mathsf{tc} \, (A \wedge B \to [w] (A \wedge B)))$. Applying Axiom (ix), we obtain $\mathsf{J}^+_{\mathrm{cs}_1} \vdash B \to [\mathsf{ind}(w,s_0)]_\mathsf{tc} \, (A \wedge B)$. Besides, $\mathsf{J}^+_{\mathrm{cs}_1} \vdash A\wedge B \to A$. From Lemma 3, there are a finite superset ${\mathrm{cs}_2}$ of ${\mathrm{cs}_1}$ and a ground term $s_1$ such that $\mathsf{J}^+_{\mathrm{cs}_2} \vdash [s_1]_\mathsf{tc} \, (A \wedge B \to A)$. Applying Axiom (vi), we obtain $\mathsf{J}^+_{\mathrm{cs}_2} \vdash B \to [s_1 \cdot \mathsf{ind}(w,s_0)]_\mathsf{tc} \, A$. It remains to note that $\mathrm{cs}_2$ can be chosen to be injective if $\mathrm{cs}_0$ is injective. $\Box$
§ 3. A non-well-founded sequent calculusThis section examines a sequent calculus for the logic $\mathsf{K}^+$, where non-well-founded proofs are allowed. The given system, denoted by $\mathsf{S}$, is a version of the calculus from [5] adapted for the case of transitive closure. Below we provide a semantic proof that each theorem of $\mathsf{K}^+$ is provable in $\mathsf{S}$. We present the argument in full detail, although semantic proofs of the given sort are not new (see [5] and [7]). We also stress that the established connection between two calculi can be proved in a pure syntactic way (see § 8 in [10]). Sequents are defined as expressions of the form $\Gamma \Rightarrow \Delta$, where $\Gamma$ and $\Delta$ are finite multisets of formulas. Multisets are often written without any curly braces, and the comma in the expression $\Gamma, \Delta$ means the multiset union. For a multiset of formulas $\Gamma = A_1,\dotsc, A_n$, we put $\Box \Gamma := \Box A_1,\dotsc, \Box A_n$ and $\Box^+ \Gamma := \Box^+ A_1,\dotsc, \Box^+ A_n$. If we remove all repetitions in a multiset $\Gamma$, then the resulting multiset is denoted by $\Gamma^s$. For example, $\Gamma^s= p,q, \Box^+ (p \to q)$ if $\Gamma= p,p, p,q, \Box^+ (p \to q), \Box^+ (p \to q)$. We denote the sequent calculus for the logic $\mathsf{K}^+$ by $\mathsf{S}$ and define its inference rules as follows:
$$
\begin{equation*}
\begin{gathered} \, \frac{\quad}{\Gamma, p \Rightarrow p, \Delta}, \qquad \frac{\quad}{\Gamma, \bot \Rightarrow \Delta}, \\ \to_{\mathsf L}\! \frac{\Gamma, B \Rightarrow \Delta \quad \Gamma \Rightarrow A, \Delta}{\Gamma, A\to B \Rightarrow \Delta}, \qquad \to_\mathsf{R} \!\frac{\Gamma, A\Rightarrow B,\Delta}{\Gamma \Rightarrow A\to B,\Delta}, \\ \Box\frac{\Sigma, \Pi, \Box^+ \Pi \Rightarrow A}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A, \Lambda}, \qquad \Box^+ \frac{\Sigma, \Pi, \Box^+ \Pi \Rightarrow A\quad \Sigma, \Pi, \Box^+ \Pi \Rightarrow \Box^+ A}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box^+ A,\Lambda}. \end{gathered}
\end{equation*}
\notag
$$
The last two inference rules of the sequent calculus are called modal rules. For the modal rule ($\Box$) (or ($\Box^+$)), the formula $\Box A$ (or $\Box^+ A$) is the principal formula of the corresponding inference. An $\infty$-proof is a possibly infinite tree whose nodes are marked by sequents and that is constructed according to the rules of the sequent calculus. Besides, every infinite branch in an $\infty$-proof must contain a tail satisfying the conditions: all applications of the rule ($\mathsf{\Box^+}$) in the tail have the same principal formula $\Box^+ A$; the tail passes through the right premise of the rule ($\mathsf{\Box^+}$) infinitely many times; the tail does not pass through the left premise of the rule ($\mathsf{\Box^+}$); there are no applications of the rule ($\Box$) in the tail. An $\infty$-proof is called regular if it contains only finitely many non-isomorphic subtrees with respect to the marking of sequents. A sequent $\Gamma \Rightarrow \Delta$ is provable in $\mathsf{S}$ if there is a regular $\infty$-proof $\pi$ with the root marked by $\Gamma \Rightarrow \Delta$. For example, consider the regular $\infty$-proof
$$
\begin{equation*}
\begin{gathered} \, \pi \\ \vdots \\ \Box^+\frac{{\displaystyle\begin{matrix}\\p, H, \Box^+ H \Rightarrow p\end{matrix}}\qquad {\displaystyle \to_\mathsf{L}\!\frac{p, \Box p, \Box^+ H \Rightarrow \Box^+ p \qquad p, \Box^+ H \Rightarrow p, \Box^+ p}{p, H, \Box^+ H \Rightarrow \Box^+}}}{p, \Box p, \Box^+ H \Rightarrow \Box^+ p}, \end{gathered}
\end{equation*}
\notag
$$
where $H= p \to \Box p$ and the subtree $\pi$ is isomorphic to the whole $\infty$-proof. Here a unique infinite branch passes through alternate applications of inference rules ($\mathsf{\to_L}$) and ($\mathsf{\Box^+}$) infinitely many times. If we consider the given branch as its own tail, then we immediately see that this branch satisfies the required conditions on infinite branches in $\infty$-proofs. We call a sequent $\Gamma \Rightarrow \Delta$ valid if the formula $\bigwedge\Gamma\to \bigvee\Delta$ is valid in any bimodal Kripke frame $(W,R,R^+)$, where $R^+$ is the transitive closure of $R$. In the rest of the section, we show that any valid sequent is provable in $\mathsf{S}$. Let us consider the following auxiliary rules ($\mathsf{\to_{L1}}$) and ($\mathsf{\to_{L2}}$)
$$
\begin{equation*}
\to_{\mathsf{L1}}\!\frac{\Gamma, B \Rightarrow \Delta}{\Gamma, A\to B \Rightarrow \Delta}, \qquad \to_\mathsf{{L2}}\! \frac{\Phi \Rightarrow C, \Psi}{\Phi, C \to D \Rightarrow \Psi}
\end{equation*}
\notag
$$
with the side conditions: the sequent $\Gamma \Rightarrow A, \Delta$ (the sequent $\Phi, D \Rightarrow \Psi$) is provable in $\mathsf{S}$. Furthermore, we consider the rule ($\boxtimes$)
$$
\begin{equation*}
\boxtimes\frac{\textrm{Prem}_1 \quad \textrm{Prem}_2}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A_1, \dotsc,\Box A_n, \Box^+ B_1, \dotsc, \Box^+ B_m,\Lambda},
\end{equation*}
\notag
$$
where the multisets $\Upsilon$ and $\Lambda$ contain only propositional variables and the constant $\bot$. Besides, $\textrm{Prem}_1$ and $\textrm{Prem}_2$ are two (possibly empty) groups of premises such that
In addition, the rule ($\boxtimes$) has the side condition: any sequent of the form $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow B_j$ or $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow \Box^+ B_j$ that does not belong to $\textrm{Prem}_2$ is provable in $\mathsf{S}$. A sequent $\Gamma \Rightarrow \Delta$ is called saturated if $\Gamma$ and $\Delta$ do not contain formulas of the form $A \to B$. A saturation tree is a finite tree of unprovable sequents constructed according to the rules ($\mathsf{\to_{R}}$), ($\mathsf{\to_{L}}$), ($\mathsf{\to_{L1}}$) and ($\mathsf{\to_{L2}}$), where all leaves are marked by saturated sequents. Lemma 6. For any unprovable sequent $\Gamma \Rightarrow \Delta$, there is a saturation tree with the root marked by $\Gamma \Rightarrow \Delta$. Proof. For a sequent $\Phi \Rightarrow \Psi$, we define its size as the sum of sizes of all formulas from $\Phi$ and $\Psi$ with respect to repetitions.
Now assume we have an unprovable sequent $\Gamma \Rightarrow \Delta$. We prove that there exists the required saturation tree for $\Gamma \Rightarrow \Delta$ by induction on the size of $\Gamma \Rightarrow \Delta$. If the sequent $\Gamma \Rightarrow \Delta$ is saturated, then the tree consisting of one node marked by $\Gamma \Rightarrow \Delta$ is a saturation tree for $\Gamma \Rightarrow \Delta$. Otherwise, there is a formula $(A\to B)\in \Gamma \cup \Delta$. Suppose $\Delta= A\to B, \Delta'$. Then the sequent $\Gamma \Rightarrow \Delta$ can be obtained from an unprovable sequent $\Gamma, A\Rightarrow B, \Delta'$ by an application of the rule ($\mathsf{\to_{R}}$). In addition, the size of $\Gamma, A\Rightarrow B, \Delta'$ is strictly less than the size of $\Gamma \Rightarrow \Delta$. Thus, by the induction hypothesis for $\Gamma, A\Rightarrow B, \Delta'$, there exists a saturation tree $\xi$ for the sequent $\Gamma, A\Rightarrow B, \Delta'$. We see that
$$
\begin{equation*}
\begin{gathered} \, \xi \\ \vdots \\ \to_{\mathsf{R}}\!\frac{\Gamma, A\Rightarrow B, \Delta'}{\Gamma \Rightarrow A\to B, \Delta'} \end{gathered}
\end{equation*}
\notag
$$
is a saturation tree with the root marked by $\Gamma \Rightarrow \Delta$.
Suppose $\Gamma= \Gamma', A\to B$. Then the sequent $\Gamma \Rightarrow \Delta$ can be obtained from $\Gamma', B \Rightarrow \Delta$ and $\Gamma' \Rightarrow A, \Delta$ by an application of the rule ($\mathsf{\to_{L}}$). Consequently, one or both of these sequents are unprovable. Note that the sizes of $\Gamma', B \Rightarrow \Delta$ and $\Gamma' \Rightarrow A, \Delta$ are strictly less than the size of $\Gamma \Rightarrow \Delta$. Hence, by the induction hypothesis, there exists a saturation tree for one or both of these sequents. Similarly to the previous case, we obtain a saturation tree for $\Gamma \Rightarrow \Delta$ from the given saturation tree(s) by an application of the rule ($\mathsf{\to_{L1}}$), ($\mathsf{\to_{L2}}$) or ($\mathsf{\to_{L}}$). $\Box$ A refutation tree is a tree of unprovable sequents constructed according to the rules ($\mathsf{\to_{R}}$), ($\mathsf{\to_{L}}$), ($\mathsf{\to_{L1}}$), ($\mathsf{\to_{L2}}$) and ($\boxtimes$). A refutation tree is called regular if it contains only finitely many non-isomorphic subtrees with respect to the marking of sequents. Lemma 7. For any unprovable sequent $\Gamma \Rightarrow \Delta$, there exists a regular refutation tree with the root marked by $\Gamma \Rightarrow \Delta$. Proof. Assume we have an unprovable sequent $\Gamma \Rightarrow \Delta$. Let $\operatorname{Sub} (\Gamma \Rightarrow \Delta)$ be the set of all subformulas of the formulas from $\Gamma \cup \Delta$. Let $S_0$ be the set of unprovable sequents of the form $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$ (or $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow \Box^+C$), where $\Sigma^s \subset \operatorname{Sub}(\Gamma \Rightarrow \Delta)$, $ \Pi^s \subset \operatorname{Sub}(\Gamma \Rightarrow \Delta)$ and $ C \in \operatorname{Sub}(\Gamma \Rightarrow \Delta)$ (or $ \Box^+ C \in \operatorname{Sub}(\Gamma \Rightarrow \Delta)$). We put $S:= S_0\cup \{\Gamma \Rightarrow \Delta\} $. Notice that $S$ if finite.
Applying Lemma 6, for any sequent $\alpha$ from $S$, we fix a saturation tree $\xi_\alpha$ with the root marked by $\alpha$. Notice that each leaf $a$ of the saturation tree $\xi_\alpha$ is marked by a saturated unprovable sequent $\Phi_a \Rightarrow \Psi_a$, where $\Phi^s_a \subset \operatorname{Sub}(\Gamma \Rightarrow \Delta)$ and $\Psi^s_a \subset \operatorname{Sub}(\Gamma \Rightarrow \Delta)$. Since $\Phi_a \Rightarrow \Psi_a$ is unprovable, any application of the rule ($\Box$) or ($\Box^+$) that draws $\Phi_a \Rightarrow \Psi_a$ must contain an unprovable sequent among its premises. It follows that $\Phi_a \Rightarrow \Psi_a$ can be obtained from unprovable sequents by an application of the rule ($\boxtimes$). Moreover, this application is uniquely determined. For $\alpha\in S$, let $\delta_\alpha$ be the tree of sequents obtained from $\xi_\alpha$ by extending each leaf of $\xi_\alpha$ with the corresponding application of ($\boxtimes$). We see that all premises of all application of ($\boxtimes$) in $\delta_\alpha$ belong to $S$. Now, starting from the root of $\delta_{\Gamma \Rightarrow \Delta}$ and travelling upwards, we successively extend each premise $\alpha$ of ($\boxtimes$) with the tree $\delta_\alpha$ and define a refutation tree for $\Gamma \Rightarrow \Delta$ by co-recursion. Since $S$ is finite, the obtained refutation tree is regular. $\Box$ Lemma 8. In any regular refutation tree with the root marked by $\Gamma \Rightarrow \Box^+ C, \Delta$, there is an application of the rule ($\boxtimes$) with a premise of the form $\Theta \Rightarrow C$. Proof. Assume we have a regular refutation tree $\delta$ with the root marked by $\Gamma \Rightarrow \Box^+ C, \Delta$. We prove the required assertion by reductio ad absurdum.
Suppose that, in the tree $\delta$, there is no application of the rule ($\boxtimes$) with a premise of the form $\Theta \Rightarrow C$. If we consider any application of the rule ($\boxtimes$) from $\delta$
$$
\begin{equation*}
\boxtimes\frac{\textrm{Prem}_1\quad \textrm{Prem}_2}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A_1, \dotsc,\Box A_n, \Box^+ B_1, \dotsc, \Box^+ B_m, \Box^+ C,\Lambda},
\end{equation*}
\notag
$$
where the succedent of the conclusion contains $\Box^+ C$, then we see that $\textrm{Prem}_2$ must contain the premise $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow \Box^+ C$ since it can not contain the sequent $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$. From the side condition for ($\boxtimes$), we also see that the sequent $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$ is provable in $\mathsf{S}$. Also, we note that, for any application of the rule ($\mathsf{\to_{R}}$), ($\mathsf{\to_{L}}$), ($\mathsf{\to_{L1}}$) or ($\mathsf{\to_{L2}}$), the succedent of each premise contains $\Box^+ C$ whenever the succedent of the conclusion contains $\Box^+ C$.
Now we define the tree of sequents $\delta'$ from the tree $\delta$ by travelling along $\delta$ from conclusions to premises and prunning each application of the rule ($\boxtimes$) of the form
$$
\begin{equation*}
\boxtimes\frac{\textrm{Prem}_1\quad \textrm{Prem}_2}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A_1, \dotsc,\Box A_n, \Box^+ B_1, \dotsc, \Box^+ B_m,\Box^+ C,\Lambda}
\end{equation*}
\notag
$$
to
$$
\begin{equation*}
\boxtimes'\frac{\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow \Box^+ C}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A_1, \dotsc,\Box A_n, \Box^+ B_1, \dotsc, \Box^+ B_m,\Box^+ C, \Lambda}.
\end{equation*}
\notag
$$
We see that the succedent of each sequent from $\delta'$ contains $\Box^+ C$ and there remain no applications of the rule ($\boxtimes$) in $\delta'$. In addition, since the refutation tree $\delta$ is regular, the obtained tree $\delta'$ contains only finitely many non-isomorphic subtrees with respect to the marking of sequents.
For any application of the rule ($\mathsf{\to_{L1}}$) or ($\mathsf{\to_{L2}}$) in the tree $\delta'$
$$
\begin{equation*}
\to_{\mathsf{L1}}\!\frac{\Phi, B \Rightarrow \Psi}{\Phi, A\to B \Rightarrow \Psi},\qquad \to_{\mathsf{L2}}\!\frac{\Phi \Rightarrow A, \Psi}{\Phi, A\to B \Rightarrow \Psi},
\end{equation*}
\notag
$$
from the side conditions of the rules, we see that the sequent $\Phi \Rightarrow A, \Psi$ or $\Phi, B \Rightarrow \Psi$ is provable in $\mathsf{S}$. Also, we see that, for any transformed application of the rule ($\boxtimes$) in the tree $\delta'$
$$
\begin{equation*}
\boxtimes'\frac{\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow \Box^+ C}{\Upsilon, \Box \Sigma, \Box^+ \Pi \Rightarrow \Box A_1, \dotsc,\Box A_n, \Box^+ B_1, \dotsc, \Box^+ B_m,\Box^+ C, \Lambda},
\end{equation*}
\notag
$$
the sequent $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$ is provable in $\mathsf{S}$. In the tree $\delta'$, there are only finitely many (non-identical) applications of the rule ($\mathsf{\to_{L1}}$), ($\mathsf{\to_{L2}}$) or ($\boxtimes'$), and so we have finitely many corresponding provable sequents of the form $\Phi \Rightarrow A, \Psi$, $\Phi, B \Rightarrow \Psi$ or $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$.
Now we transform each application of the rule ($\mathsf{\to_{L1}}$), ($\mathsf{\to_{L2}}$) or ($\boxtimes'$) in the tree $\delta'$ into an application of ($\mathsf{\to_{L}}$) or ($\Box^+$) by adding the missing premise of the form $\Phi \Rightarrow A, \Psi$, $\Phi, B \Rightarrow \Psi$ or $\Sigma^s, \Pi^s, \Box^+ \Pi^s \Rightarrow C$ and extending this premise with a regular $\infty$-proof. If we extend identical premises with identical regular $\infty$-proofs, we obtain a regular $\infty$-proof with the root marked by $\Gamma \Rightarrow \Box^+ C, \Delta$. However, the sequent $\Gamma \Rightarrow \Box^+ C, \Delta$ occurs in the refutation tree $\delta$ and must be unprovable (by the definition of refutation tree), which is a contradiction. Consequently, there exists an application of the rule ($\boxtimes$) in the refutation tree $\delta$ with a premise of the form $\Theta \Rightarrow C$. $\Box$ Lemma 9. If there is a regular refutation tree with the root marked by $\Gamma \Rightarrow \Delta$, then $\Gamma \Rightarrow \Delta$ is invalid. Proof. Assume we have a regular refutation tree $\delta$ with the root marked by $\Gamma \Rightarrow \Delta$. For any node $c$ of $\delta$, let us denote the sequent of the node $c$ by $\Phi_c \Rightarrow \Psi_c$.
Now we define a Kripke frame, which will be used to invalidate the sequent $\Gamma \Rightarrow \Delta$. We denote the set of nodes of $\delta$ that are conclusions of applications of the rule ($\boxtimes$) by $W$. For $a, b \in W$, we put $a \prec b$ if $b$ is a descendant of $a$ and there is exactly one application of ($\boxtimes$) in between $a$ and $b$. Besides, we denote the transitive closure of $\prec$ by $\prec^+$. We obtain the bimodal frame $(W, \prec, \prec^+)$. For this frame, we define the truth relation by letting For a node $c $ of $\delta$ and $a \in W$, we set $a \in \mathsf{sat} (c)$ if and only if $a$ is a descendant of $c$ in the tree $\delta$ and there are no applications of the rule ($\boxtimes$) in between $c$ and $a$. We claim that, for any formula $F$ and any node $c $ of $\delta$,
$$
\begin{equation*}
\begin{gathered} \, F \in \Phi_c \Longrightarrow \forall\, a\in \mathsf{sat}(c) \ a\vDash F, \\ F \in \Psi_c \Longrightarrow \forall\, a\in \mathsf{sat}(c) \ a\nvDash F. \end{gathered}
\end{equation*}
\notag
$$
The claim is established by induction on $\operatorname{sz} (F)$.
Suppose $F=\bot$. Since the sequent $\Phi_c \Rightarrow \Psi_c$ is unprovable (by the definition of refutation tree), we have $\bot \notin \Phi_c$. We also see that $a \nvDash \bot$ for any $a \in \mathsf{sat} (c)$. The aforementioned assertion holds. Suppose $F=p$. If $p \in \Phi_c$, then $p \in \Phi_a$ for any $a \in \mathsf{sat} (c)$. Consequently, $a \vDash p$ from the choice of the truth relation $\vDash$. Now if $p \in \Psi_c$, then $p \in \Psi_a$ for any $a \in \mathsf{sat} (c)$. Since the sequent $\Phi_a \Rightarrow \Psi_a$ is unprovable, we have $p \notin \Phi_a$. It follows that $a \nvDash p$ by the definition of the truth relation $\vDash$. Suppose $F = A\to B$. If $(A \to B) \in \Phi_c$, then, on the path from $c$ to each $a\in \mathsf{sat} (c)$, we can find a node $a'$ such that $B \in \Phi_{a'}$ or $A \in \Psi_{a'}$. Notice that $a \in \mathsf{sat} (a')$. From the induction hypothesis, we see that $a \vDash B$ or $a \nvDash A$. Consequently, $a \vDash A\to B$. If $(A \to B) \in \Psi_c$, then, on the path from $c$ to each $a\in \mathsf{sat} (c)$, we can find a node $a'$ such that $A \in \Phi_{a'}$ and $B \in \Psi_{a'}$. Notice that $a \in \mathsf{sat} (a')$. From the induction hypothesis, we see that $a \vDash A$ and $a \nvDash B$. It follows that $a \nvDash A\to B$. Suppose $F$ has the form $\Box A$. If $\Box A\in \Phi_c$, then $\Box A\in \Phi_a$ for any $a \in \mathsf{sat} (c)$. In order to show that $a \vDash \Box A$, let us consider any $b\in W$ such that $a \prec b$. Recall that there is a unique application of the rule ($\boxtimes$) in between $a$ and $b$ and $a$ is the conclusion of the application. Moreover, there is a premise $a'$ of the given application such that $b \in \mathsf{sat}(a')$. We see that $A \in \Phi_{a'}$ and $b \vDash A$ by the induction hypothesis for $A$. We obtain that $a \vDash \Box A$. Now if $\Box A\in \Psi_c$, then $\Box A\in \Psi_a$ for any $a \in \mathsf{sat} (c)$. Recall that $a$ is the conclusion of an application of the rule ($\boxtimes$) in $\delta$. Hence there is a premise $a'$ of the given application such that $A \in \Psi_{a'}$. Since $\mathsf{sat} (a') \neq \varnothing$, there is a node $b \in \mathsf{sat} (a')$. By the induction hypothesis for $A$, we have $b \nvDash A$. We see that $a\prec b$, $b \nvDash A$ and $a \nvDash \Box A$. Suppose $F = \Box^+ A$. Let us check that $a \vDash \Box^+ A$ for $a\in \mathsf{sat} (c)$ if $\Box^+ A\in \Phi_c$. Consider any node $a \in \mathsf{sat} (c)$ and an arbitrary sequence $a=a_0 \prec a_1 \prec \dotsb \prec a_n \prec a_{n+1}$. From $\Box^+ A\in \Phi_c$, we have $\Box^+ A\in \Phi_{a_i}$ for all $i\in \{0,\dotsc, n+1\}$. We recall that $a_n$ is the conclusion of an application of the rule ($\boxtimes$) in $\delta$. Therefore there is a premise $a'_n$ of the given application such that $a_{n+1} \in \mathsf{sat} (a'_n)$. In addition, we have $A \in \Phi_{a'_n}$. From the induction hypothesis for $A$, we obtain $a_{n+1}\vDash A$. Consequently, $a \vDash \Box^+ A$. If $\Box^+ A\in \Psi_c$, then $\Box^+ A\in \Psi_a$ for any $a \in \mathsf{sat} (c)$. Applying Lemma 8 for $C=A$, in the subtree of $\delta$ determined by $a$, we can find a node $a'$ such that $A \in \Psi_{a'}$. Also, there is an application of the rule ($\boxtimes$) in between $a$ and $a'$. Since $\mathsf{sat} (a')\neq \varnothing$, there is a node $a'' \in \mathsf{sat} (a')$. By the induction hypothesis for $A$, we have $a'' \nvDash A$. We also see that $a \prec^+ a''$. Therefore $a \nvDash \Box^+ A$. The claim is established. Now let $r$ be the root of $\delta$. Since $\mathsf{sat} (r) \neq \varnothing$, there is a node $r' \in \mathsf{sat} (r)$. We see that $\Phi_r=\Gamma$, $\Psi_r=\Delta$, $r' \vDash \bigwedge \Gamma$ and $r' \nvDash \bigvee \Delta$. Thus the sequent $\Gamma \Rightarrow \Delta$ is invalid. $\Box$ Proof. Assume we have a valid sequent $\Gamma \Rightarrow \Delta$. We show that the sequent $\Gamma \Rightarrow \Delta$ is provable in the sequent calculus $\mathsf{S}$ by reductio ad absurdum. If $\Gamma \Rightarrow \Delta$ is unprovable, then there exists a regular refutation tree with the root marked by $\Gamma \Rightarrow \Delta$ from Lemma 7. Therefore, the sequent $\Gamma \Rightarrow \Delta$ is invalid by Lemma 9, which is a contradiction. Consequently, the sequent $\Gamma \Rightarrow \Delta$ is provable in $\mathsf{S}$. $\Box$ Corollary 1. If $\mathsf{K}^+\vdash \bigwedge \Gamma \to \bigvee\Delta$, then the sequent $\Gamma \Rightarrow \Delta$ is provable by a regular $\infty$-proof. § 4. Cyclic proofs and annotationsIn order to facilitate our prove of the realization theorem, we introduce annotated versions of sequents and inference rules of the sequent calculus $\mathsf{S}$. We also define useful finite representations of regular $\infty$-proofs called cyclic (or circular) proofs. An annotated formula is a formula of $\mathsf{K}^+$ in which any occurrence of a modal connective is labelled with a natural number. These labelled modal connectives are denoted by $\Box_i$ and $\Box^+_i$, where $i\in \mathbb{N}$. A modal formula is called properly annotated if distinct occurrences of $\Box$ in it are labelled with distinct natural numbers, and the same holds for the occurrences of $\Box^+$. An annotated sequent is an expression of the form $\Gamma \Rightarrow_\alpha \Delta$, where all formulas in $\Gamma$ and $\Delta$ are annotated and $\alpha$ is an annotated formula of the form $\Box^+_n C$ or an auxiliary sign $\ast$. In addition, if $\alpha$ is a formula, then the multiset $\Delta$ must contain $\alpha$. We also require that negative occurrences of modal connectives in $\Gamma \Rightarrow_\alpha \Delta$ (i.e., in $\bigwedge \Gamma \to \bigvee \Delta$) are labelled with even natural numbers and positive ones are labelled with odd numbers. An annotated sequent $\Gamma \Rightarrow_\alpha \Delta$ is called properly annotated if the formula $\bigwedge \Gamma \to \bigvee \Delta$ is properly annotated. Here is an example of a properly annotated sequent:
$$
\begin{equation*}
\Box_1 p \to r, q \to \Box^+_2 (p \to \Box_6 \bot) \Rightarrow_{\Box^+_1 p} \Box^+_1 p, \bot.
\end{equation*}
\notag
$$
Annotated versions of inference rules are defined as
$$
\begin{equation*}
\begin{gathered} \, \frac{\quad}{\Gamma, p \Rightarrow_\alpha p, \Delta}, \qquad \frac{\quad}{\Gamma, \bot \Rightarrow_\alpha \Delta}, \\ \to_\mathsf{L}\! \frac{\Gamma, B \Rightarrow_\alpha \Delta\quad \Gamma \Rightarrow_\alpha A, \Delta}{\Gamma, A\to B \Rightarrow_\alpha \Delta},\qquad \to_\mathsf{R}\! \frac{\Gamma, A\Rightarrow_\alpha B,\Delta}{\Gamma \Rightarrow_\alpha A\to B,\Delta}, \\ \Box_m \frac{A_1,\dotsc,A_k, B_1, \dotsc, B_l, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast C}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\alpha \Box_m C, \Lambda}, \\ \Box^+_n\frac{\Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast C\quad \Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n C} \Box^+_n C}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\alpha \Box^+_n C, \Lambda}, \end{gathered}
\end{equation*}
\notag
$$
where $\Sigma= \{A_1,\dotsc,A_k\}$ and $\Pi=\{B_1, \dotsc, B_l\}$. An annotated $\infty$-proof is a (possibly infinite) tree whose nodes are marked by annotated sequents and that is constructed according to annotated versions of inference rules. Moreover, every infinite branch in it must contain a tail such that all sequents in the tail are annotated with the same subscript formula $\Box^+_n C$ and the tail intersects an application of the rule ($\Box^+_n$) on the right premise infinitely many times. An annotated $\infty$-proof is regular if it contains only finitely many non-isomorphic subtrees with respect to annotations. Also, we call an annotated $\infty$-proof properly annotated if its root is marked by a properly annotated sequent. Notice that if we erase all annotations in an annotated $\infty$-proof, then the resulting tree is an ordinary $\infty$-proof. Let us prove the converse. Lemma 10. Any $\infty$-proof $\pi$ can be properly annotated. Moreover, the obtained annotated $\infty$-proof can be chosen to be regular if $\pi $ is regular. Proof. Note that, for any application of an inference rule of $\mathsf{S}$ and any annotation of its conclusion, one can annotate its premises and obtain an application of the annotated version of the rule. However, the choice of annotations for the premises is not unique. Let us fix, for any application of an inference rule of $\mathsf{S}$, some way of propagating annotations from the conclusion of the rule to its premises. We also require that this way of propagation, when moving from the conclusion of the rule ($\Box^+$) to its right premise, preserves, whenever possible, the subscript formula $\Box^+_n C$.
Now assume we have an $\infty$-proof $\pi$ and an arbitrary proper annotation of its root. Starting from the root, we annotate $\pi$ according to the chosen way of propagating annotations and denote the resulting tree of annotated sequents by $\pi'$. We claim that the given tree $\pi'$ is an annotated $\infty$-proof. It is sufficient to check that $\pi'$ satisfies the required condition on infinite branches. Suppose there is an infinite branch in $\pi'$. Then, by the definition of $\infty$-proof, this branch contains a tail that does not intersect applications of the rule ($ \Box$) and applications of the rule ($\Box^+$) on the left premise. Moreover, all applications of the rule ($\Box^+$) in the tail have the same principal formula $\Box^+ A$ disregarding annotations. Note also that the tail intersects the rule ($\Box^+$) infinitely many times. Consequently, after the first application of the rule ($\Box^+$), all right-hand sides of sequents in the tail contain the formula $\Box^+ A$ disregarding annotations. According to the chosen way of propagating annotations, from now on all annotated sequents in the tail have the same subscript formula $\Box^+_n C$ and all applications of the rule ($\Box^+$) have the same principal formula $\Box^+_n C$, where $\Box^+_n C$ is an annotated version of the formula $\Box^+ A$. Therefore, every infinite branch of $\pi'$ satisfies the required condition, and $\pi'$ is an annotated $\infty$-proof. We now assume that the $\infty$-proof $\pi$ is regular, and show that $\pi'$ is also regular by reductio ad absurdum. Suppose there is an infinite sequence of pairwise non-isomorphic subtrees of $\pi'$. Since $\pi'$ is obtained from a regular $\infty$-proof, there are only finitely many non-isomorphic subtrees disregarding annotations in $\pi'$. Therefore, there is a subsequence $(\mu_i)_{i\in \mathbb{N}}$ of the given sequence, where all members are isomorphic disregarding annotations. We see that the roots of $(\mu_i)_{i\in \mathbb{N}}$ are marked by non-identical annotated sequents obtained from a single unannotated sequent $\Gamma \Rightarrow \Delta$. However, any annotated formula occurring in $\pi'$ is a subformula of the annotated sequence of the root. Consequently, there can be only finitely many non-identical annotated sequents obtained from $\Gamma \Rightarrow \Delta$ in $\pi'$, which is a contradiction. We conclude that the annotated $\infty$-proof $\pi'$ is regular. $\Box$ A cyclic annotated proof is a pair $(\kappa, d)$, where $\kappa$ is a finite tree of annotated sequents constructed in accordance with annotated versions of inference rules of the system $\mathsf{S}$, while leaves of $\kappa$ are allowed to be marked not only by sequents of the form $\Gamma,p\Rightarrow_\alpha p,\Delta$ or $\Gamma, \bot \Rightarrow_\alpha \Delta $, and $d$ is a function with the following properties: the domain of $d$ is included in the set of all leaves of $\kappa$; $d$ is defined at each leaf of $\kappa$ that is not marked by a sequent of the form $\Gamma,p\Rightarrow_\alpha p,\Delta$ or $\Gamma, \bot \Rightarrow_\alpha \Delta $; the image $d(a)$ of a leaf $a$ lies on the path from the root of $\kappa$ to the leaf $a$ and is not equal to $a$; $d(a)$ and $a$ are marked by the same sequents; all sequents on the path from $d(a)$ to $a$ have the same subscript formula $\Box^+_n C$; this path intersects an application of the rule ($\Box^+_n$) on the right premise. If the function $d$ is defined at a leaf $a$, then we say that the nodes $a$ and $d(a)$ are connected by a back-link. Obviously, every cyclic annotated proof can be unravelled into a regular one. We prove the converse. Lemma 11. Any regular annotated $\infty$-proof can be obtained by unravelling of a cyclic annotated proof. Proof. Assume we have a regular annotated $\infty$-proof $\pi$. Notice that each node $a$ of this tree determines the subtree $\pi_a$ with the root $a$. Let $m$ denote the number of non-isomorphic subtrees of $\pi$. Consider any branch $a_0, a_1, \dotsc, a_m$ in $\pi$ that starts at the root of $\pi$ and has length $m + 1$. This branch defines the sequence of subtrees $\pi_{a_0},\pi_{a_1}, \dotsc,\pi_{a_m}$. Since $\pi$ contains precisely $m$ non-isomorphic subtrees, the branch contains a pair of different nodes $b$ and $c$ determining isomorphic subtrees $\pi_b$ and $\pi_c$. Without loss of generality, assume that $c$ is farther from the root than $b$. Note that all sequents on the path form $b$ to $c$ have the same subscript formula of the form $\Box^+_n C$ and this path intersects an application of the rule ($\Box^+_n$) on the right premise, because otherwise there is an infinite branch in $\pi$ that violates the corresponding condition on infinite branches of annotated $\infty$-proofs. We cut the branch under consideration at the node $c$ and connect $c$, which has become a leaf, with $b$ by a back-link. By applying a similar operation to each of the remaining branches of length $m + 1$, we ravel the regular annotated $\infty$-proof $\pi$ into the desired cyclic annotated proof. $\Box$
§ 5. Realization theoremIn this section, we establish the realization theorem connecting the modal logic $\mathsf{K}^+$ and the justification logic $\mathsf{J}^+$. Note that all realizations constructed in the proof will be normal. Let us define the forgetful translation from the language of $\mathsf{J}^+$ into the language of $\mathsf{K}^+$. Given a justification formula $A$, its forgetful translation $A^\circ$ is defined inductively by
$$
\begin{equation*}
\begin{gathered} \, p^\circ :=p, \qquad \bot^\circ :=\bot, \qquad (A\to B)^\circ:= (A^\circ \to B^\circ),\\ ([ w] A)^\circ:= \Box A^\circ,\qquad ([s]_\mathsf{tc}\, A)^\circ:= \Box^+ A^\circ. \end{gathered}
\end{equation*}
\notag
$$
Obviously, the forgetful translation of any theorem of $\mathsf{J}^+$ is a theorem of $\mathsf{K}^+$. The converse statement, which we give in a slightly stronger form, is called a realization theorem. A justification formula $B$ is a realization of a modal formula $A$ if the formula $B$ is obtained from $A$ by replacing every occurrence of $\Box$ ($\Box^+$) in $A$ with an arbitrary justification term of the first (second) sort. The realization $B$ is called normal if distinct negative occurrences of $\Box$ ($\Box^+$) in $A$ are replaced with distinct justification variables of the first (second) sort. Theorem 2 (normal realization). For any theorem $A$ of the logic $\mathsf{K}^+$, there exists its normal realization $B$ such that $B$ has an injective proof in $\mathsf{J}^+$. A cyclic annotated proof is called prepared if, in the given proof, each occurrence of a modal rule is labelled with an additional natural number so that different occurrences of ($\Box_m$) are labelled with different natural numbers. Further, two different occurrences of ($\Box^+_n$) are labelled with the same natural number if and only if all sequents on the shortest path connecting the right premises of these occurrences have the same subscript formula $\Box^+_n C$. We denote occurrences of ($\Box_m$) and ($\Box^+_m$) labelled with a natural number $i$ by ($\Box_{m,i}$) and ($\Box^+_{m,i}$). A function $g \colon \mathbb{N} \to \mathbb{N}$ is called a bounding function for a prepared proof $\pi$ if, for every application of ($\Box_{m,i}$) in $\pi$, we have $i< g(m-1)$. In addition, for every application of ($\Box^+_{n,j}$), we require that $j< g(n)$. Now we extend the sets of justification variables $\mathrm{JV}_1 =\{x_0, x_1, \dotsc \}$ and $\mathrm{JV}_2 =\{y_0, y_1, \dotsc \}$ with provisional variables of the form $x_{m,i}$ and $y_{n,j}$. A substitution
$$
\begin{equation*}
\theta = [w_1 / x_{m_1,i_1},\dotsc, w_k/x_{m_k,i_k}, s_1 / y_{n_1,j_1},\dotsc, s_l/y_{n_l,j_l} ]
\end{equation*}
\notag
$$
is called finalizing if the terms $w_1,\dotsc, w_k$ and $s_1, \dotsc, s_l$ do not contain provisional variables. In this case, we denote the set
$$
\begin{equation*}
\{x_{m_1,i_1}, \dotsc,x_{m_k,i_k}, y_{n_1,j_1},\dotsc, y_{n_l,j_l}\}
\end{equation*}
\notag
$$
by $\operatorname{Dom}(\theta)$. A finalizing substitution $\theta$ is called adequate for a prepared cyclic annotated proof $\pi$ if $\operatorname{Dom}(\theta)= \{x_{m_1,i_1}, \dotsc,x_{m_k,i_k}, y_{n_1,j_1},\dotsc, y_{n_l,j_l}\}$ and the finite sequences $(\Box_{m_1,i_1}), \dotsc, (\Box_{m_k,i_k})$ and $(\Box^+_{n_1,j_1}), \dotsc, (\Box^+_{n_l,j_l})$ contain precisely all annotated modal rules of $\pi$. For an arbitrary function $g \colon \mathbb{N} \to \mathbb{N}$, we define the following translation of annotated modal formulas to justification ones: $p^g :=p$, $\bot^g :=\bot$, $(A\to B)^g:= (A^g \to B^g)$, $(\Box_{2m} A)^g:= [x_{2m}] A^g$, $(\Box^+_{2m} A)^g:= [y_{2m}] A^g$,
$$
\begin{equation*}
\begin{aligned} \, (\Box_{2m+1} A)^g &:= \begin{cases} [x_{2m+1}] A^g & \text{if }g(2m)=0, \\ [x_{2m+1,0}+\dotsb + x_{2m+1,g(2m)-1}] A^g & \text{if }g(2m)\neq 0, \end{cases} \\ (\Box^+_{2n+1} A)^g &:= \begin{cases} [y_{2n+1}]_\mathsf{tc}\, A^g & \text{if }g(2n+1)=0, \\ [y_{2n+1,0}+\dotsb + y_{2n+1,g(2n+1)-1}]_\mathsf{tc}\, A^g & \text{if }g(2n+1)\neq0. \end{cases} \end{aligned}
\end{equation*}
\notag
$$
Note that, for a formula $A$ occurring in a prepared cyclic annotated proof $\pi $ and a bounding function $g$ for $\pi$, the formula $\theta (A^g)$ can contain provisional variables even if $\theta$ is a finalizing substitution adequate for $\pi$. However, $\theta (A^g)$ does not contain provisional variables if, in addition, the following conditions hold: the labelling of occurrences of ($\Box_m$) in $\pi$ has no gaps (i.e., for any occurrence ($\Box_{m,j}$) and any natural number $i<j$, there exists an occurrence ($\Box_{m,i}$) in $\pi$); similarly, the labelling of occurrences of ($\Box^+_n$) in $\pi$ has no gaps; finally, the bounding function $g$ is pointwise the least possible. This remark will play a role in the proof of Theorem 2. For a prepared proof $\pi = (\kappa, d)$, we denote the root of $\kappa$ by $r(\pi)$. Also, for a node $c$ of $\kappa$, by $F_c$, we denote the formula $\bigwedge \Phi_c \to \bigvee \Psi_c$, where $\Phi_c \Rightarrow_\alpha \Psi_c$ is the sequent of the node $c$. Lemma 12. Suppose $\pi$ is a prepared cyclic annotated proof of $\Gamma \Rightarrow_\alpha \Delta$ and $g$ is a bounding function for $\pi$. Then there exists a finalizing substitution $\theta$ adequate for $\pi$ such that the formula $\theta (F^g_{r(\pi)} )$ has an injective proof in $\mathsf{J}^+$. Proof.
The lemma is proved by induction on the number of nodes in $\pi=(\kappa,d)$. Note that the function $g$ will be a bounding function for all prepared cyclic annotated proofs considered below.
Case 1. If $\kappa$ consists of a single node, then $\Gamma \Rightarrow_\alpha \Delta$ has the form $\Gamma', p \Rightarrow_\alpha p, \Delta'$ or $\Gamma', \bot \Rightarrow_\alpha \Delta$. Trivially, $\mathsf{J}^+_0\vdash F^g_{r(\pi)} $. Consequently, the formula $ F^g_{r(\pi)}$ has an injective proof in $\mathsf{J}^+$. We define $\theta$ as the identity substitution. Case 2. Suppose $\Delta = A\to B, \Delta'$ and $\pi$ has the form
$$
\begin{equation*}
\begin{gathered} \, \pi' \\ \vdots \\ \to_\mathsf{R}\! \frac{\Gamma, A\Rightarrow_\alpha B,\Delta'}{\Gamma \Rightarrow_\alpha A\to B,\Delta'} \end{gathered}
\end{equation*}
\notag
$$
for a prepared cyclic annotated proof $\pi'$. By the induction hypothesis, there is a finalizing substitution $\theta'$ adequate for $\pi'$ such that the formula $\theta' (F^g_{r(\pi')} )$ has an injective proof in $\mathsf{J}^+$. We also have $\mathsf{J}^+_0\vdash\theta' (F^g_{r(\pi')}) \to \theta' (F^g_{r(\pi)})$. Consequently, the formula $\theta' (F^g_{r(\pi)})$ has an injective proof in $\mathsf{J}^+$. We see that $\theta'$ is adequate for $\pi$, and we set $\theta := \theta'$.
Case 3. Suppose $\Gamma = \Gamma', A\to B$ and $\pi$ has the form
$$
\begin{equation*}
\begin{gathered} \, \quad \ \pi'\qquad\qquad\quad \ \pi'' \\ \ \ \vdots\qquad\qquad\qquad \vdots \\ \to_\mathsf{L}\!\frac{\Gamma', B \Rightarrow_\alpha \Delta\quad \Gamma' \Rightarrow_\alpha A, \Delta}{\Gamma', A\to B \Rightarrow_\alpha \Delta}, \end{gathered}
\end{equation*}
\notag
$$
where $\pi'$ and $\pi''$ are prepared cyclic annotated proofs. Suppose also that, for any occurrences ($\Box^+_{n,i}$) and ($\Box^+_{n,j}$), one from $\pi'$ and one from $\pi''$, we have $i \neq j$. In other words, there is no simple path intersecting $r(\pi)$ and connecting right premises of ($\Box^+_n$) such that all sequents on the path have the same subscript $\alpha$. Applying the induction hypothesis for $\pi'$ and $\pi''$, we find a finalizing substitution $\theta'$ adequate for $\pi'$ and a finalizing substitution $\theta''$ adequate for $\pi''$ such that $\theta' (F^g_{r(\pi')} )$ and $\theta'' (F^g_{r(\pi'')} )$ are provable in $\mathsf{J}^+$ by injective proofs. Notice that $\mathsf{J}^+_{\mathrm{cs}'}\vdash \theta' (F^g_{r(\pi')} )$ and $\mathsf{J}^+_{\mathrm{cs}''}\vdash \theta'' (F^g_{r(\pi'')} )$ for some finite injective constant specifications $\mathrm{cs}'$ and $\mathrm{cs}''$. We assume that the sets $\operatorname{Con} (\mathrm{cs}')$ and $\operatorname{Con} (\mathrm{cs}'')$ are disjoint. Otherwise, we can make them disjoint by renaming the constants from $\mathrm{cs}'$ and modifying appropriately the substitution $\theta'$. Since $\operatorname{Con} (\mathrm{cs}') \cap \operatorname{Con} (\mathrm{cs}'')=\varnothing$, the set $\mathrm{cs}'\cup\mathrm{cs}''$ is a finite injective constant specification. Moreover, $\mathsf{J}^+_{\mathrm{cs}' \cup\mathrm{cs}''}\vdash \theta' (F^g_{r(\pi')} ) \wedge \theta'' (F^g_{r(\pi'')} )$. We see that $ \theta' (F^g_{r(\pi')} ) \wedge \theta'' (F^g_{r(\pi'')} )$ has an injective proof in $\mathsf{J}^+$.
Note that $\operatorname{Dom}(\theta')\cap \operatorname{Dom}(\theta'')=\varnothing$, because, for any occurrences ($\Box^+_{n,i}$) and ($\Box^+_{n,j}$), one from $\pi'$ and one from $\pi''$, we have $i \neq j$. In addition, $\theta' \circ \theta''=\theta''\circ \theta'$ since $\operatorname{Dom}(\theta')\cap \operatorname{Dom}(\theta'')=\varnothing$. We set $\theta:=\theta'\circ\theta''$. Applying the substitution $\theta$ to $\theta' (F^g_{r(\pi')} ) \wedge\theta'' (F^g_{r(\pi'')} )$, we obtain $\theta (F^g_{r(\pi')} )\wedge\theta (F^g_{r(\pi'')} )$. This formula has an injective proof in $\mathsf{J}^+$ by Lemma 1. Since $\mathsf{J}^+_0\vdash \theta (F^g_{r(\pi')}) \wedge \theta (F^g_{r(\pi'')} ) \to\theta (F^g_{r(\pi)} )$, the formula $\theta (F^g_{r(\pi)} )$ has an injective proof in $\mathsf{J}^+$. Besides, the substitution $\theta$ is adequate for $\pi$. Case 4. Suppose that $\pi$ has the form
$$
\begin{equation*}
\begin{gathered} \, \ \pi' \\ \vdots \\ \Box_{m,i}\frac{A_1,\dotsc,A_k, B_1, \dotsc, B_l, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast D}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\alpha \Box_m D, \Lambda}, \end{gathered}
\end{equation*}
\notag
$$
where $\pi'$ is a prepared cyclic annotated proof. By the induction hypothesis, there is a finalizing substitution $\theta'$ adequate for $\pi'$ such that $\theta' (F^g_{r(\pi')} )$ has an injective proof in $\mathsf{J}^+$. The formula $\theta'(F^g_{r(\pi')})$ has the form
$$
\begin{equation*}
\begin{aligned} \, &\theta' (A^g)\wedge\dotsb \wedge \theta'(A^g_k) \\ &\qquad\wedge \theta'(B^g_1)\wedge\dotsb \wedge \theta'(B^g_l)\wedge [y_{j_1}]_\mathsf{tc}\, \theta'(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \theta'(B^g_l) \to \theta'(D^g). \end{aligned}
\end{equation*}
\notag
$$
From Lemma 4, there is a term $h$ depending only on $\{x_{i_1}, \dotsc, x_{i_k}\}$ and $\{y_{j_1}, \dotsc, y_{j_l}\}$ such that the formula
$$
\begin{equation}
[x_{i_1}]\theta' (A^g)\wedge\dotsb \wedge [x_{i_k}]\theta'(A^g_k) \wedge [y_{j_1}]_\mathsf{tc}\, \theta'(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \theta'(B^g_l) \to [h] \theta'(D^g)
\end{equation}
\tag{1}
$$
has an injective proof in $\mathsf{J}^+$. Note that $x_{m,i} \notin \operatorname{Dom}(\theta')$, i.e., $\theta'(x_{m,i})=x_{m,i}$. We put $\theta:= [h/ x_{m,i}] \circ \theta'$. Applying the substitution $[h/ x_{m,i}]$ to (1), we obtain
$$
\begin{equation}
[x_{i_1}]\theta (A^g)\wedge\dotsb \wedge [x_{i_k}]\theta(A^g_k) \wedge [y_{j_1}]_\mathsf{tc}\, \theta(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \theta(B^g_l) \to [h] \theta(D^g),
\end{equation}
\tag{2}
$$
which has an injective proof in $\mathsf{J}^+$ by Lemma 1. In addition, the formula
$$
\begin{equation*}
[h] \theta(D^g)\to [\theta(x_{m,0})+\dotsb + \theta(x_{m,i-1})+ h+\theta(x_{m,i+1})+ \dotsb +\theta(x_{m,g(m-1)-1})] \theta(D^g)
\end{equation*}
\notag
$$
is provable in $\mathsf{J}^+_0$, i.e., $\mathsf{J}^+_0\vdash [h] \theta(D^g)\to \theta ((\Box_m D)^g)$. Now we see that (2) implies $\theta (F^g_{r(\pi)} )$ in $\mathsf{J}^+_0$. Therefore, the formula $\theta (F^g_{r(\pi)} )$ has an injective proof in $\mathsf{J}^+$. Note also that $\theta$ is a finalizing substitution adequate for $\pi$.
Case 5. Suppose that there is a leaf of $\pi$ connected by a back-link with the root. In this case, all sequents on the path from the root to the leaf have the same subscript $\alpha$, and $\alpha= \Box^+_n D$ for some formula $D$. Let $R$ denote the following set of nodes of $\pi=(\kappa,d)$: $b\in R$ if and only if every sequent lying on the path from the root of $\pi$ to the node $b$ has the subscript formula $\Box^+_n D$. Note that, for any $b\in R$, the sequent of the node $b$ has the form $\Gamma_b\Rightarrow_{\Box^+_n D}\Delta_b, \Box^+_n D$. We set $G_b:= \bigwedge \Gamma_b\wedge \neg \bigvee \Delta_b$ and $H:= \bigvee \{G_b\mid b\in R \}$. Trivially, $\mathsf{K}^+\vdash \bigwedge \Gamma_b\to \bigvee (\Delta_b\cup \{H\})$ and $\mathsf{J}^+_0\vdash (\bigwedge \Gamma_b\to \bigvee (\Delta_b\cup \{H\}))^g$. For any $b\in R$, we define its rank $\operatorname{rk}(b) $ as follows. We put $\operatorname{rk}(b):= 0$ whenever $b$ is the conclusion of a modal rule or is a leaf of $\kappa$ that is not connected by a back-link. We set $\operatorname{rk}(b):= \operatorname{rk}(b')+1$ whenever $b$ is a conclusion of the rule ($\to_\mathsf{R}$) and $b'$ is the corresponding premise. Analogously, $\operatorname{rk}(b):= \max \{\operatorname{rk}(b')+1, \operatorname{rk}(b'')+1\}$ if $b$ is a conclusion of the rule ($\mathsf{\to_L}$) with the premises $b'$ and $b''$. If $b$ is a leaf of $\kappa$ connected by a back-link with a node $c$, then we put $\operatorname{rk}(b):= \operatorname{rk}(c)+1$. Let $R_0:= \{a\in R \mid \operatorname{rk}(a)=0\}$. For each $a\in R_0$, we define a finalizing substitution $\sigma_a$ and a justification term $o_a$ such that $o_a$ does not contain provisional variables, $\operatorname{Dom}(\sigma_a)\cap \operatorname{Dom}(\sigma_b)=\varnothing$ for any two different nodes $a$ and $b$ from $R_0$ and the formula
$$
\begin{equation*}
\sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g))
\end{equation*}
\notag
$$
has an injective proof in $\mathsf{J}^+$. In what follows, we denote the subtree of $\kappa$ with the root $a$ by $\kappa_a$.
Suppose $a$ is a leaf of $\kappa$ and is not connected by a back-link with another node of $\kappa$. In this case, the node $a$ is marked by a sequent of the form $\Gamma'_a, p \Rightarrow_{\Box^+_n D} p, \Delta'_a, \Box^+_n D $ or $\Gamma'_a, \bot \Rightarrow_{\Box^+_n D} \Delta_a, \Box^+_n D$. We define $\sigma_a$ as the identity substitution and put $o_a:= x_0$. We see that $\mathsf{J}^+_0\vdash \neg G^g_a $ and $\mathsf{J}^+_0\vdash \neg \sigma_a (G^g_a) $. Consequently, $\mathsf{J}^+_0\vdash \sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g)) $. Suppose $a$ is the conclusion of a modal rule and $\kappa_a$ has the form
$$
\begin{equation*}
\begin{gathered} \, \kappa'_a \\ \vdots \\ \Box_{m,i}\frac{A_1,\dotsc,A_k, B_1, \dotsc, B_l, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast E}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n D} \Box_m E, \Lambda, \Box^+_n D}. \end{gathered}
\end{equation*}
\notag
$$
Since there are no applications of the rule ($\Box$) between two nodes connected by a back-link, the tree $\kappa'_a$, together with the function $d$ restricted to the leaves of $\kappa'_a$, defines a prepared cyclic annotated proof $\pi'_a$. Consider the following prepared cyclic annotated proof:
$$
\begin{equation*}
\begin{gathered} \, \pi'_a \\ \vdots \\ \Box_{m,i}\frac{A_1,\dotsc,A_k, B_1, \dotsc, B_l, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast E}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\ast} \Box_m E, \Lambda}, \end{gathered}
\end{equation*}
\notag
$$
which we denote by $\pi'$. Note that $a$ is different from the root of $\pi$. Therefore, $\pi'$ contains fewer nodes than $\pi$. Applying the induction hypothesis, we find a finalizing substitution $\sigma_a$ adequate for $\pi'$ such that $\sigma_a (F^g_{r(\pi')} )$ has an injective proof in $\mathsf{J}^+$. We see that $\mathsf{J}^+_0\vdash \sigma_a(F^g_{r(\pi')})\to \neg \sigma_a(G^g_a) $. Hence, $\neg \sigma_a (G^g_a) $ is provable in $\mathsf{J}^+$ by an injective proof. Now we put $o_a:= x_0$ and obtain that $ \sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g)) $ has an injective proof in $\mathsf{J}^+$.
Suppose $a$ is the conclusion of a modal rule and $\kappa_a$ has the form
$$
\begin{equation*}
\begin{gathered} \, \ \ \kappa'_a\qquad\qquad\qquad\quad \kappa''_a \\ \vdots\qquad\qquad\qquad\qquad\vdots \\ \Box^+_{m,j}\frac{\Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast E\quad \Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_m E} \Box^+_m E}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n D} \Box^+_m E, \Lambda, \Box^+_n D}, \end{gathered}
\end{equation*}
\notag
$$
where $\Sigma= \{A_1,\dotsc,A_k\}$, $\Pi=\{B_1, \dotsc, B_l\}$ and $\Box^+_m E \neq \Box^+_n D$. Since the path between any two nodes connected by a back-link cannot intersect the application ($\Box^+_{m,j}$), the trees $\kappa'_a$ and $\kappa''_a$, together with the function $d$ restricted to the corresponding sets of leaves, define prepared cyclic annotated proofs $\pi'_a$ and $\pi''_a$. Consider the following prepared cyclic annotated proof:
$$
\begin{equation*}
\begin{gathered} \, \ \ \pi'_a\qquad\qquad\qquad\quad \pi''_a \\ \vdots\qquad\qquad\qquad\qquad\vdots \\ \Box^+_{m,j}\frac{\Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast E\quad \Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_m E} \Box^+_m E}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_m E} \Box^+_m E, \Lambda}, \end{gathered}
\end{equation*}
\notag
$$
which we denote by $\pi'$. Since $a$ is different from the root of $\pi$, the proof $\pi'$ contains fewer nodes than $\pi$. By the induction hypothesis, there is a finalizing substitution $\sigma_a$ adequate for $\pi'$ such that $\sigma_a (F^g_{r(\pi')} )$ has an injective proof in $\mathsf{J}^+$. Note that $\mathsf{J}^+_0\vdash \sigma_a(F^g_{r(\pi')})\to \neg \sigma_a(G^g_a) $. Therefore, $\neg \sigma_a (G^g_a) $ has an injective proof in $\mathsf{J}^+$. We put $o_a:= x_0$ and obtain that $ \sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g)) $ is provable in $\mathsf{J}^+$ by an injective proof.
Suppose $a$ is the conclusion of a modal rule and $\kappa_a$ has the form
$$
\begin{equation*}
\begin{gathered} \, \ \ \kappa'_a\qquad\qquad\qquad\quad \kappa''_a \\ \vdots\qquad\qquad\qquad\qquad\vdots \\ \Box^+_{n,j}\frac{\Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast D\quad \Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n D} \Box^+_n D}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n D} \Box^+_n D, \Lambda}, \end{gathered}
\end{equation*}
\notag
$$
where $\Sigma= \{A_1,\dotsc,A_k\}$ and $\Pi=\{B_1, \dotsc, B_l\}$. We see that the tree $\kappa'_a$, together with the function $d$ restricted to the set of leaves of $\kappa'_a$, defines a prepared cyclic annotated proof $\pi'_a$. By the induction hypothesis, there is a finalizing substitution $\sigma_a$ adequate for $\pi'_a$ such that $\sigma_a (F^g_{r(\pi'_a)} )$ has an injective proof in $\mathsf{J}^+$. The formula $\sigma_a(F^g_{r(\pi'_a)})$ has the form
$$
\begin{equation*}
\begin{aligned} \, &\sigma_a (A^g_1)\wedge\dotsb \wedge \sigma_a(A^g_k) \\ &\qquad\wedge \sigma_a(B^g_1)\wedge\dotsb \wedge \sigma_a(B^g_l)\wedge [y_{j_1}]_\mathsf{tc}\, \sigma_a(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \sigma_a(B^g_l) \to \sigma_a(D^g). \end{aligned}
\end{equation*}
\notag
$$
From the definition of $H$, we have
$$
\begin{equation*}
\begin{aligned} \, &\mathsf{J}^+_0\vdash\sigma_a (A^g_1)\wedge\dotsb \wedge \sigma_a(A^g_k)\wedge\sigma_a(B^g_1)\wedge\dotsb \wedge \sigma_a(B^g_l) \\ &\qquad\wedge [y_{j_1}]_\mathsf{tc}\, \sigma_a(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \sigma_a(B^g_l) \to \sigma_a(H^g). \end{aligned}
\end{equation*}
\notag
$$
Hence, the formula
$$
\begin{equation*}
\begin{aligned} \, &\sigma_a (A^g_1)\wedge\dotsb \wedge \sigma_a(A^g_k)\wedge\sigma_a(B^g_1)\wedge\dotsb \wedge \sigma_a(B^g_l) \\ &\qquad\wedge [y_{j_1}]_\mathsf{tc}\, \sigma_a(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \sigma_a(B^g_l) \to \sigma_a(D^g) \wedge \sigma_a(H^g) \end{aligned}
\end{equation*}
\notag
$$
has an injective proof in $\mathsf{J}^+$. By Lemma 4, there is a term $o_a$ depending only on $\{x_{i_1}, \dotsc, x_{i_k}\}$ and $\{y_{j_1}, \dotsc, y_{j_l}\}$ such that the formula
$$
\begin{equation}
\begin{aligned} \, &[x_{i_1}]\sigma_a (A^g_1)\wedge\dotsb \wedge [x_{i_k}]\sigma_a(A^g_k) \nonumber \\ &\qquad\wedge [y_{j_1}]_\mathsf{tc}\, \sigma_a(B^g_1)\wedge\dotsb \wedge [y_{j_l}]_\mathsf{tc}\, \sigma_a(B^g_l) \to [o_a] (\sigma_a(D^g) \wedge \sigma_a (H^g)) \end{aligned}
\end{equation}
\tag{3}
$$
has an injective proof in $\mathsf{J}^+$. Note that (3) implies $ \sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g)) $ in $\mathsf{J}^+_0$.
Now the finalizing substitution $\sigma_a$ and the justification term $o_a$ are well defined for any $a\in R_0$. Moreover, for each $a\in R_0$, the formula
$$
\begin{equation}
\sigma_a (G_a^g)\to [o_a] (\sigma_a(D^g)\wedge \sigma_a(H^g))
\end{equation}
\tag{4}
$$
is provable in $\mathsf{J}^+_{\mathrm{cs}_a}$ for some finite injective constant specification $\mathrm{cs}_a$. We assume that all sets $\operatorname{Con}(\mathrm{cs}_a)$ are pairwise disjoint. Otherwise, we make them disjoint by renaming the constants and modifying appropriately substitutions $\sigma_a$ and terms $o_a$. Note that $\sigma_a\circ \sigma_b=\sigma_b\circ \sigma_a$ for any two different nodes $a$ and $b$ since $\operatorname{Dom}(\sigma_a)\cap \operatorname{Dom}(\sigma_b)=\varnothing$. Let $\sigma$ be the composition of all substitutions $\sigma_a$ for $a\in R_0$. Obviously, $\sigma$ is finalizing. Now we put $\mathrm{cs}:= \bigcup \{\sigma (\mathrm{cs}_a)\mid a\in R_0\}$. Since the sets $\operatorname{Con}(\sigma(\mathrm{cs}_a))= \operatorname{Con}(\mathrm{cs}_a)$ are pairwise disjoint, $\mathrm{cs}$ is a finite injective constant specification.
We claim that, for each $b\in R$, there is a justification term $v_b$ such that $v_b$ does not contain provisional variables and the formula
$$
\begin{equation}
\sigma (G^g_b)\to [v_b] (\sigma(D^g)\wedge \sigma(H^g)),
\end{equation}
\tag{5}
$$
is provable in $\mathsf{J}^+_\mathrm{cs}$. We proceed by subinduction on $\operatorname{rk}(b)$.
Case A. Suppose $ \operatorname{rk}(b)=0$, i.e., $b\in R_0$. Applying $\sigma$ to (4), we obtain
$$
\begin{equation*}
\sigma (G^g_b)\to [v_b] (\sigma(D^g)\wedge \sigma(H^g)),
\end{equation*}
\notag
$$
where $v_b=o_b$. This formula is provable in $\mathsf{J}^+_{\sigma(\mathrm{cs}_b)}$ by Lemma 1. Therefore, it is provable in $\mathsf{J}^+_{\mathrm{cs}}$.
Case B. Suppose $b$ is a leaf of $\kappa$ connected by a back-link with a node $c$. From the induction hypothesis for $c$, the formula $\sigma (G_{c}^g)\to [v_{c}] (\sigma(D^g)\wedge \sigma(H^g)) $ is provable in $\mathsf{J}^+_{\mathrm{cs}}$ for some term $v_{c}$. In addition, $v_c$ does not contain provisional variables. Note that $\sigma (G_{b}^g)$ coincides with $\sigma (G_{c}^g)$. Therefore, the formula $\sigma(G_b^g)\to [v_b] (\sigma(D^g)\wedge \sigma(H^g)) $ is provable in $\mathsf{J}^+_{\mathrm{cs}}$ for $v_b:= v_{c}$, and $v_b$ does not contain provisional variables. Case C. Suppose the tree $\kappa_b$ has the form
$$
\begin{equation*}
\begin{gathered} \, \kappa'_b \\ \vdots \\ \to_\mathsf{R}\! \frac{\Gamma_b, A\Rightarrow_{\Box^+_n D} B,\Delta'_b, \Box^+_n D}{\Gamma_b \Rightarrow_{\Box^+_n D} A\to B,\Delta'_b, \Box^+_n D}. \end{gathered}
\end{equation*}
\notag
$$
In this case, $G_b $ coincides with $\bigwedge \Gamma_b \wedge \neg \bigvee \{ A\to B\}\cup \Delta'_b$. Let us denote the child of $b$ by $b'$. Note that $\operatorname{rk}(b')< \operatorname{rk}(b)$. By the subinduction hypothesis, there is a term $v_{b'}$ without occurrences of provisional variables such that the formula $\sigma (G_{b'}^g)\to [v_{b'}] (\sigma(D^g)\wedge \sigma(H^g)) $ is provable in $\mathsf{J}^+_{\mathrm{cs}}$. Since $\mathsf{J}^+_0\vdash \sigma (G_{b}^g) \to \sigma (G_{b'}^g)$, we obtain $\mathsf{J}^+_\mathrm{cs}\vdash \sigma (G_b^g)\to [v_b] (\sigma(D^g)\wedge \sigma(H^g)) $ for $v_b:= v_{b'}$. We see that $v_b$ does not contain provisional variables.
Case D. Suppose the tree $\kappa_b$ has the form
$$
\begin{equation*}
\begin{gathered} \, \ \kappa'_b\qquad\qquad\quad\ \kappa''_b \\ \vdots\qquad\qquad\qquad\vdots \\ \to_\mathsf{L}\! \frac{\Gamma'_b, B \Rightarrow_{\Box^+_n D} \Delta_b, \Box^+_n D\quad \Gamma'_b \Rightarrow_{\Box^+_n D} A, \Delta_b,\Box^+_n D}{\Gamma'_b, A\to B \Rightarrow_{\Box^+_n D} \Delta_b, \Box^+_n D}. \end{gathered}
\end{equation*}
\notag
$$
In this case, $G_b $ coincides with $\bigwedge \Gamma'_b\cup \{ A\to B\} \wedge \neg \bigvee \Delta_b$. Let $b'$ and $b''$ be the children of $b$. We see that $\operatorname{rk}(b')< \operatorname{rk}(b)$ and $\operatorname{rk}(b'')< \operatorname{rk}(b)$. By the subinduction hypotheses for $b'$ and $b''$, there are terms $v_{b'}$ and $v_{b''}$ without occurrences of provisional variables such that the formulas $\sigma (G_{b'}^g)\to [v_{b'}] (\sigma(D^g)\wedge \sigma(H^g)) $ and $\sigma (G_{b''}^g)\to [v_{b''}] (\sigma(D^g)\wedge \sigma(H^g)) $ are provable in $\mathsf{J}^+_{\mathrm{cs}}$. Since $\mathsf{J}^+_0\vdash \sigma (G_{b}^g) \to \sigma (G_{b'}^g)\vee \sigma (G_{b''}^g)$, we obtain $\mathsf{J}^+_\mathrm{cs}\vdash \sigma (G_b^g)\to [v_{b'} + v_{b''}] (\sigma(D^g)\wedge \sigma(H^g)) $. It remains to set $v_b:= v_{b'}+ v_{b''}$.
We see that, for any $b\in R$, there is a justification term $v_b$ such that $v_b$ does not contain provisional variables and formula (5) is provable in $\mathsf{J}^+_{\mathrm{cs}}$. The claim is checked. We define $v$ as the sum of the terms $v_b$ (in any order) for $b\in R$. From Axiom (v), we have $\mathsf{J}_0^+\vdash [v_b](\sigma(D^g)\wedge \sigma (H^g)) \to [v] (\sigma(D^g)\wedge \sigma (H^g))$. Consequently, $\sigma (G_b^g)\to [v] (\sigma(D^g)\wedge \sigma (H^g))$ is provable in $\mathsf{J}^+_{\mathrm{cs}}$. Since $H:= \bigvee \{G_b\mid b\in R \}$, the formula has an injective proof in $\mathsf{J}^+$. Now, by Lemma 5, there is a term $t$ such that $t$ does not contain provisional variables and the formula has an injective proof in $\mathsf{J}^+$. Recall that in the case under consideration there is a leaf of $\pi$ connected by a back-link with the root. From the definition of cyclic annotated proof, the path from the root of $\pi$ to this leaf intersects an application of the rule ($\Box^+_{n,j}$). Furthermore, all applications of the rule ($\Box^+$) whose right premises belong to $R$ are labelled with the same indices $n$ and $j$. Note that $y_{n,j}\notin \operatorname{Dom}(\sigma)$ since $\operatorname{Dom}(\sigma)= \bigcup \{\operatorname{Dom}(\sigma_a)\mid a\in R_0\}$. We define the substitution $\theta$ so that the value of $\theta$ coincides with the value of $\sigma$ on every justification variable except $y_{n,j}$ and $\theta (y_{n,j})= t$. Applying $[t/y_{n,j}]$ to $\sigma (H^g)\to [t]_\mathsf{tc} \,\sigma(D^g)$, we obtain the formula $\theta (H^g)\to [t]_\mathsf{tc} \,\theta(D^g)$, which, by Lemma 1, has an injective proof in $\mathsf{J}^+$. In addition, the formulas $ \theta (G^g_{r(\pi)}) \to \theta (H^g)$ and
$$
\begin{equation*}
[t]_\mathsf{tc} \, \theta(D^g)\to [\theta(y_{n,0})+\dotsb + \theta(y_{n,j-1})+ t+\theta(y_{n,j+1})+ \dotsb +\theta(y_{n,g(n)-1})]_\mathsf{tc} \, \theta(D^g)
\end{equation*}
\notag
$$
are provable in $\mathsf{J}^+_0$. Therefore, $\theta ((G_{r(\pi)} \to \Box^+_n D)^g)$ has an injective proof in $\mathsf{J}^+$. Notice that $\theta ((G_{r(\pi)} \to \Box^+_n D)^g)$ is equivalent to the formula $\theta (F_{r(\pi)}^g)$ in $\mathsf{J}^+_0 $. Consequently, $\theta (F_{r(\pi)}^g)$ is provable in $\mathsf{J}^+$ by an injective proof. We also see that $\theta$ is adequate substitution for $\pi$.
Case 6. Suppose the lowermost application of an inference rule in $\pi$ has the form
$$
\begin{equation*}
\Box^+_{n,j}\frac{\Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\ast D\quad \Sigma, \Pi, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_{\Box^+_n D} \Box^+_n D}{\Upsilon, \Box_{i_1} A_1, \dotsc, \Box_{i_k} A_k, \Box^+_{j_1} B_1,\dotsc, \Box^+_{j_l} B_l \Rightarrow_\alpha \Box^+_n D, \Lambda},
\end{equation*}
\notag
$$
where $\Sigma= \{A_1,\dotsc,A_k\}$ and $\Pi=\{B_1, \dotsc, B_l\}$. Without loss of generality, we assume that $\alpha= \Box^+_n D$. Otherwise, we replace $\alpha$ with $\Box^+_n D$ and obtain a prepared cyclic annotated proof with the same number of nodes as the proof $\pi$, and with the same formula of the root $F_{r(\pi)}$.
From this point on, the argument repeats what happened in Case 5. The required substitution $\theta$ is defined in exactly the same way as before. Therefore, we omit further details. Case 7. Suppose $\Gamma = \Gamma', A\to B$ and $\pi$ has the form
$$
\begin{equation*}
\begin{gathered} \, \ \pi'_b\qquad\qquad\quad \ \pi''_b \\ \vdots\qquad\qquad\qquad\vdots \\ \to_\mathsf{L}\! \frac{\Gamma', B \Rightarrow_\alpha \Delta\quad \Gamma' \Rightarrow_\alpha A, \Delta}{\Gamma', A\to B \Rightarrow_\alpha \Delta}, \end{gathered}
\end{equation*}
\notag
$$
where $\pi'$ and $\pi''$ are prepared cyclic annotated proofs. Suppose also that there are two distinct occurrences of ($\Box^+_{n}$), one from $\pi'$ and one from $\pi''$, labelled with the same natural number $j$. We see that $\alpha$ has the form $\Box^+_n D$ and there is a path intersecting $r(\pi)$ and connecting right premises of ($\Box^+_n$) such that all sequents on the path have the subscript $\Box^+_n D$.
Now we repeat what happened in Case 5 and define the required substitution $\theta$ in the same way as before. $\Box$ Proof of Theorem 2. Assume $\mathsf{K}^+\vdash A$. There exists a regular $\infty$-proof of the sequent $\Rightarrow A$ by Corollary 1. Applying Lemma 10 to this $\infty$-proof, we find a regular properly annotated $\infty$-proof of $\Rightarrow_\alpha B$, where $B^\circ= A$. From Lemma 11, there exists a cyclic annotated proof $\eta$ for the properly annotated sequent $\Rightarrow_\alpha B$.
Using $\eta$, we define a prepared cyclic annotated proof $\pi$ and a bounding function $g$ for this proof $\pi$ as follows. If $\eta$ contains $k$ applications of the rule ($\Box_{2m+1}$), then we enumerate these applications starting from $0$ to $k-1$ and set $g(2m) = k$; if $\eta$ does not contain applications of ($\Box_{2m+1}$), then we set $g(2m) = 0$. Two applications of ($\Box^+_{2n+1}$) in the proof $\eta$ are called equivalent if all sequents on the shortest path connecting the right premises of the applications have the same subscript formula $\Box^+_{2n+1} D$. If $\eta$ contains $l$ equivalence classes of applications of the rule ($\Box^+_{2n+1}$), then we enumerate these classes starting from $0$ to $l-1$ and set $g(2n+1) = l$; if $\eta$ does not contain applications of ($\Box^+_{2n+1}$), then we set $g(2n+1) = 0$. We label each occurrence of the rule ($\Box^+_{2n+1}$) from the $i$th class by $i$. In this way, we obtain a prepared cyclic annotated proof $\pi$ with a bounding function $g$. From Lemma 12, there is a finalizing substitution $\theta$ such that the formula $\theta (B^g)$ has an injective proof in $\mathsf{J}^+$. We also see that $\theta (B^g)$ does not contain provisional variables. It remains to note that $\theta (B^g)$ is a normal realization for $A$. $\Box$ AcknowledgementsI thank the anonymous referee for his attention and comments on the article. I also heartily thank my wife Mariya Shamkanova for her constant and warm support.
Citation in format AMSBIB
\Bibitem{Sha25} |
|
|||||||||||||||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|