| Izvestiya: Mathematics |
|
|
|
|
|
On provability logics of Niebergall arithmetic L. V. Dvorkin Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Bibliographic databases:
    § 1. IntroductionNiebergall [1] proposed a consistent theory extending Peano arithmetic $\mathrm{PA}$, in which a natural formalization of the statement of self-consistency is provable. We call it Niebergall arithmetic and denote $\mathrm{NA}$. $\mathrm{NA}$ is constructed as the intersection of two extensions of $\mathrm{PA}$: $T_1 \,{:=}\, \mathrm{PA} + \operatorname{Tr}_{\Pi_1}$ and $T_2 := \mathrm{PA} + \operatorname{Con}(T_1)$ (where $\operatorname{Tr}_{\Pi_1}$ is the set of all true in the standard model $\Pi_1$ sentences, and $\operatorname{Con}(T)$ is a formula naturally expressing the consistency of $T$). Since $T_2$ is recursively enumerable (r.e.) and consistent, $\operatorname{Con}(T_2) \in \operatorname{Tr}_{\Pi_1}$, and $T_1 \vdash \operatorname{Con}(T_2)$. It is also obvious that $T_2 \vdash \operatorname{Con}(T_1)$ and $\mathrm{PA} \vdash \operatorname{Con}(T_j) \to \operatorname{Con}(T_1 \cap T_2)$ for $j = 1, 2$. Therefore, both theories prove $\operatorname{Con}(\mathrm{NA})$ and $\mathrm{NA} \vdash \operatorname{Con}(\mathrm{NA})$. Niebergall’s example deserves further study for several reasons. According to Gödel’s second incompleteness theorem, in a consistent r.e. theory containing a sufficiently strong fragment of arithmetic, a natural formalization of the statement of self-consistency is unprovable. Well-known counterexamples are typically associated with the construction of artificial (pathological) provability predicates (cf. [2] and [3]). On the other hand, there are examples of very weak r.e. theories for which the conclusion of Gödel’s second incompleteness theorem is violated [4]. In connection with this, we would like to mention a recent result by Pakhomov [5], who gave an example of a weak set theory in which one can formulate and prove a natural statement expressing its own consistency. Niebergall’s theory is an example of another kind, namely the simplest non-r.e. theory extending $\mathrm{PA}$ in which its own consistency is provable. The arithmetical formula expressing the provability in $\mathrm{NA}$ is natural. However, Niebergall’s theory does not satisfy the Hilbert–Bernays–Löb derivability conditions, and the properties of provability in it differ significantly from those of the studied arithmetical theories. Provability logics describe the properties of provability in a given theory expressible by formulas of modal propositional logic, that can be justified by means of a meta-theory (see, for example, [6]–[8]). The well-known theorem of Solovey [9] states that, for r.e. arithmetically correct theories $T$ satisfying the conditions of Gödel’s second theorem, the logic of provability is described by the Gödel–Löb system $\mathrm{GL}$ (in this case, we consider $T$ itself as a meta-theory). Thus, for all theories in the considered broad class, the logic of provability is the same. For Niebergall arithmetic, the corresponding logic is different, and the question of its explicit description is of interest. In this paper, we have started investigating this question and have obtained a partial answer to it. Note that provability logics for various types of “pathological” provability predicates (Rosser’s, Feferman’s and others) have been extensively studied, in particular, by Smorinsky [7], Visser [10], and Shavrukov [11] and [12]. In some cases, a complete axiomatization of such logics was obtained. It turns out that the provability logics of Niebergall arithmetic are related to modal logics satisfying weakened versions of the transitivity axiom. For many such systems, the question of their algorithmic decidability remains open for a long time. The logics considered in this paper will be shown to be decidable. In this paper, we investigate the provability logics of Niebergall arithmetic with respect to three theories: Peano arithmetic, all arithmetical sentences true in the standard model, and $\mathrm{NA}$ itself. At the moment, there is no explicit axiomatization for any of these logics, but we will provide their description in terms of Kripke semantics. The paper is organized as follows: In § 2, we provide necessary definitions and facts from modal logic, formal arithmetic, and provability logic. Section 3 is devoted to the Kripke semantics of the provability logic of $\mathrm{NA}$ with respect to $\mathrm{PA}$. This logic is called $\mathrm{Nie}$. We prove that $\mathrm{Nie}$ is finitely approximable and describe the class of all its Kripke frames. The search for an explicit axiomatization of $\mathrm{Nie}$ seems to be a challenging task. However, this problem can be circumvented by extending the language. In § 4, we consider the logic $\mathrm{Nie}_\flat$, which is a conservative extension of $\mathrm{Nie}$ in the language with an additional propositional constant. This extension preserves completeness with respect to (enriched) finite $\mathrm{Nie}$-frames. At the same time, we obtain a finite axiomatization for it. Section 5 is devoted to the description of the truth provability logic of $\mathrm{NA}$ and the provability logic of $\mathrm{NA}$ with respect to $\mathrm{NA}$ itself. For both logics, we obtain a complete semantics in terms of Kripke models. In addition, we present a finite axiomatization of the truth provability logic over $\mathrm{Nie}$. In § 6, we describe the variable free fragments of the logics under consideration. For each of them, we prove a normal form theorem and construct a universal Kripke model. In § 7, we will show that $\mathrm{Nie}$ does not satisfy the Craig interpolation property and derivability problem in the investigated logics is $\mathrm{PSpace}$-complete. § 2. Basic conceptsThe language of modal logic with modalities $\Box_1, \dots, \Box_n$ includes the countable set of propositional variables $\mathrm{PVar} = \{ p_1, p_2, \dots \}$, boolean connectives $\to$ and $\bot$, and one-place modal connectives $\Box_1, \dots, \Box_n$. Other boolean and dual modal connectives $\Diamond_1, \dots, \Diamond_n$ are considered as abbreviations. The set of all formulas in this language is denoted by $\mathrm{Fm}(\Box_1, \dots, \Box_n)$. The set of all subformulas of a formula $\varphi$ is denoted by $\operatorname{Sub}(\varphi)$. By a modal logic we mean a set of formulas $\Lambda \subset \mathrm{Fm}(\Box_1, \dots, \Box_n)$ containing all tautologies and closed under the rules of modus ponens and substitution. A modal logic is called normal if it contains the axioms
$$
\begin{equation*}
\Box_i(p \to q) \to (\Box_i p \to \Box_i q),\qquad i = 1, \dots, n,
\end{equation*}
\notag
$$
and is closed under necessitation rules $\Lambda \vdash \varphi \Rightarrow \Lambda \vdash \Box_i\varphi$ for each modality $\Box_i$. We say that a (normal) logic $\Lambda$ is given by some set of axioms if $\Lambda$ is the smallest (normal) logic containing them. By arithmetical theories we mean first-order theories in the language of Peano arithmetic containing $\mathrm{PA}$. We denote the set of formulas in the language of Peano arithmetic by $\mathrm{Fm}(Ar)$. The provability predicate of an arithmetical theory $T$ is a formula $\mathrm{Pr}(x) \in \mathrm{Fm}(Ar)$ such that $\mathbb{N} \vDash \mathrm{Pr}(\ulcorner\varphi\urcorner) \Leftrightarrow T \vdash \varphi$, where $\ulcorner\varphi\urcorner$ is the Gödel number of the formula $\varphi$. For the theories considered in this paper, the provability predicate is naturally formulated based on their definitions. We denote by $\mathrm{Pr}_0$ and $\mathrm{Pr}_1$ the natural provability predicates for $\mathrm{PA}$ and $\mathrm{PA} + \operatorname{Tr}_{\Pi_1}$ respectively (cf. [13]). Let $\xrightarrow{\cdot}$ be the p.r. term mapping the Gödel numbers of the formulas $\varphi$ and $\psi$ to $\ulcorner\varphi \to \psi\urcorner$. Then $\mathrm{Pr}_0(\ulcorner\neg \mathrm{Pr}_1(\ulcorner\bot\urcorner) \urcorner \xrightarrow{\cdot} x)$ is a natural provability predicate for $\mathrm{PA}+\operatorname{Con}(\mathrm{PA}+ \operatorname{Tr}_{\Pi_1})$. Therefore,
$$
\begin{equation*}
\mathrm{Pr}_{\mathrm{NA}}(x) := \mathrm{Pr}_1(x) \wedge \mathrm{Pr}_0\bigl(\ulcorner\neg \mathrm{Pr}_1(\ulcorner\bot\urcorner) \urcorner \xrightarrow{\cdot} x\bigr)
\end{equation*}
\notag
$$
is a natural provability predicate for Niebergall arithmetic. An arbitrary mapping $f \colon \mathrm{PVar} \to \mathrm{Fm}(Ar)$ is called an arithmetical valuation. Suppose that, for some arithmetical theories $T_1, \dots, T_n$, we have fixed the provability predicates $\mathrm{Pr}_1, \dots, \mathrm{Pr}_n$. The arithmetical translation $\widehat f$ of modal formulas with respect to theories $T_1, \dots, T_n$ and valuation $f$ is defined as follows: $\widehat f(p) = f(p)$, $\widehat f(\bot) = \bot$, $\widehat f(\varphi \to \psi) =\widehat f(\varphi) \to \widehat f(\psi)$, $\widehat f(\Box_i\varphi) = \mathrm{Pr}_i(\ulcorner\widehat f(\varphi)\urcorner)$ for all variables $p$, formulas $\varphi, \psi \in \mathrm{Fm}(\Box_1, \dots, \Box_n)$ and all $i = 1, \dots, n$. The provability logic of the theories $T_1, \dots, T_n$ with provability predicates $\mathrm{Pr}_1, \dots, \mathrm{Pr}_n$ with respect to some arithmetical theory $U$ is a set of formulas $\varphi \in \mathrm{Fm}(\Box_1, \dots, \Box_n)$ such that $U \vdash \widehat f(\varphi)$ for every arithmetical valuation $f$. Obviously, this set of formulas is a modal logic according to the above definition (however, in general, this logic is not normal). In this paper, we consider theories with fixed provability predicates. This allows us to talk about the provability logic of theories $T_1, \dots, T_n$ with respect to $U$ and use the notation $\mathrm{PL}_U(T_1, \dots, T_n)$. The logic of provability with respect to the set of all true in the standard model arithmetical sentences is called the truth provability logic and denoted by $\mathrm{PL}_\mathbb{N}(T_1, \dots, T_n)$. According to Ignatyev [14], $\mathrm{PL}_{\mathrm{PA}}(\mathrm{PA}, \mathrm{PA} + \operatorname{Tr}_{\Pi_1})$ coincides with the bimodal fragment $\mathrm{GLB}$ of the polymodal logic of Japaridze [15], [16]. Recall that $\mathrm{GLB}$ is a normal modal logic in the language with modalities $\Box_0$ and $\Box_1$ given by the following set of axioms: 1. $\Box_i(\Box_i p \to p) \to \Box_i p$, $i = 0, 1$; 2. $\Diamond_0 p \to \Box_1\Diamond_0 p$; 3. $\Box_0 p \to \Box_1 p$. In the same work, it was shown that the logic $\mathrm{PL}_\mathbb{N}(\mathrm{PA}, \mathrm{PA} + \operatorname{Tr}_{\Pi_1})$ can be described in terms of $\mathrm{GLB}$ in two ways. Firstly, it is the smallest (non-normal) modal logic containing $\mathrm{GLB}$ and the axiom $\Box_1 p \to p$. Secondly, it is the set of formulas $\varphi \in \mathrm{Fm}(\Box_0, \Box_1)$ such that $\mathrm{GLB} \vdash S(\varphi) \to \varphi$, where $S(\varphi)$ is the conjunction of implications $\Box_0\psi \to \psi$ and $\Box_1\eta \to \eta$ for all $\Box_0\psi, \Box_1\eta \in \operatorname{Sub}(\varphi)$. In the case of an r.e. theory $T$, all possible logics $\mathrm{PL}_U(T)$ are described (see [6]). Since $\mathrm{NA}$ is not r.e., its provability logics do not fit into this classification. In this paper, three of them are investigated: $\mathrm{PL}_{\mathrm{PA}}(\mathrm{NA})$, $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$, and $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. Using the above facts, it is not difficult to translate the problem of investigating these logics into the language of modal logic. Specifically, consider the translation
$$
\begin{equation*}
\begin{aligned} \, {}^* \colon \mathrm{Fm}(\Box) &\to \mathrm{Fm}(\Box_0, \Box_1), \\ \Box\psi &\mapsto \Box_1\psi^* \wedge \Box_0(\neg\Box_1\bot \to \psi^*) \end{aligned}
\end{equation*}
\notag
$$
(variables, constants, and boolean connectives commute with ${}^*$). Proposition 2.1. The provability logics of $\mathrm{NA}$ can be described in terms of $\mathrm{GLB}$ as follows: Proof. It is clear that, for every arithmetical valuation $f$ and formula $\varphi \in \mathrm{Fm}(\Box)$, where $\widehat f_{\mathrm{NA}}$ and $\widehat f_{\mathrm{PA}, \mathrm{PA} + \operatorname{Tr}_{\Pi_1}}$ are arithmetical translations with respect to the corresponding theories and valuation $f$ and $\equiv$ denotes the graphical equality of formulas. From Ignatiev’s results, we have the first two statements. The third one follows from the second, since, for all arithmetical theories $T$, $\Box$ In what follows, we will rely heavily on Kripke semantics. Recall that a Kripke frame is a non-empty set $W$, whose elements are called possible worlds, with binary relations $\mathbin{R}_1, \dots, \mathbin{R}_n$. A mapping $\vartheta \colon \mathrm{PVar} \to \mathcal{P}(W)$ is called a valuation on the frame $\mathcal{F}$. A frame with fixed valuation on it is called a Kripke model. As usual, we inductively define whether a formula $\varphi \in \mathrm{Fm}(\Box_1, \dots, \Box_n)$ is true at a given world of a model $\mathcal{M}$: $\bot$ is false at all worlds; variable $p \in \mathrm{PVar}$ is true at worlds belonging to $\vartheta(p)$ and only at them; the implication is true at a world if and only if the conclusion is true at it or the premise is false; a formula of the form $\Box_i\psi$ is true at the world $w$ if and only if $\psi$ is true at all the worlds from $\mathbin{R}_i(w) := \{ v \in W \mid w \mathbin{R}_i v\}$ (such worlds are called accessible from from $w$ over $\mathbin{R}_i$). The fact that a formula $\varphi$ is true at the world $w$ of the model $\mathcal{M}$ is denoted by $\mathcal{M}, w \vDash \varphi$. If a formula $\varphi$ is true at all worlds of $\mathcal{M}$, it is said to be true in the model $\mathcal{M}$, and we denote this by $\mathcal{M} \vDash \varphi$. A formula is valid on a frame $\mathcal{F}$ if it is true in the model $(F, \vartheta)$ for all valuations $\vartheta$ on $\mathcal{F}$. More detailed explanation of the modal logical concepts used in this paper can be found, for example, in [17]. Let us note the connection between translation ${}^*$ and Kripke semantics. Lemma 2.2. Let $(W, \mathbin{R_0}, \mathbin{R_1}, \vartheta)$ be a Kripke model. Let the relation $\mathbin{R}$ be defined by: Then, for each world $w \in W$ and formula $\varphi \in \mathrm{Fm}(\Box)$, This result can be easily obtained by induction on the construction of $\varphi$. § 3. Kripke semantics for $\mathrm{Nie}$Definition. A Kripke frame $\mathcal{F} = (W, \succ)$ is called an $\mathrm{N}$-frame if the set of its worlds can be represented as $W = T \sqcup L$ (we call the elements $t \in T$ stem nodes and $l \in L$ leaf nodes or, simply, leaves) so that the following conditions are satisfied: (Fund). The relation ${\prec} = {\succ}^{-1}$ is well-founded. (Trans). Transitivity for stem nodes:
$$
\begin{equation*}
\forall\, w_1, w_2 \in W\quad \forall\, t \in T\quad (w_1 \succ w_2 \succ t \Rightarrow w_1 \succ t).
\end{equation*}
\notag
$$
(EL). Existence of a leave: $\forall\, t \in T\ \exists\, l \in L \ (t \succ l)$. (LL). Inaccessibility of leaves from each other: $\forall\, l_1, l_2 \in L\ (l_1 \nsucc l_2)$. (TL). Coordination between stem and leaf nodes: We emphasize some aspects of our notation. Firstly, we use $\succ$ for the accessability relation, so $w \succ v$ means that the world $v$ is accessible from $w$ (intuitively, $\succ$ is an arrow directed from $w$ to $v$). Secondly, $\prec$ is not a strict partial order, since it is not transitive. Thirdly, leaves $l \in L$ in $\mathrm{N}$-frames are not $\prec$-minimal; on the contrary, the set $\{ w \in W \mid w \succ l \}$ does not contain worlds that are accessible from each other. In the definition of an $\mathrm{N}$-frame, we postulate that there exists a partition of the set of worlds into stem and leaf nodes. It is easy to show that such a partition is unique. Proposition 3.1. Let $\mathcal{F} = (W, \succ)$ be an $\mathrm{N}$-frame. Then the partition $W = T \sqcup L$ satisfying (EL) and (TL) is unique. Proof. Suppose that there are two different partitions $W = T_1 \sqcup L_1 = T_2 \sqcup L_2$. Denote $D := T_1 \cap L_2 \cup T_2 \cap L_1$. Since the partitions are distinct, $D$ is not empty. Hence by (Fund), there is a $\prec$-minimal world $w$ in $D$. Suppose, without loss of generality, that $w \in T_1 \cap L_2$. Then, by (EL), there is a leaf $l \in L_1$ accessible from $w$. Since $l \prec w$, $l$ is not in $D$, therefore, $l \in L_2$. Thus, by (LL) $w \in T_2$, contradicting $w \in L_2$. $\Box$ An appropriate frame is shown in Fig. 1. We show leaf nodes by circles and stem nodes by squares. The accessibility relation is defined in terms of two auxiliary relations: the solid relation, represented by solid arrows, and the dashed one, which is the transitive closure of dashed arrows. $w \succ v$ holds if and only if at least one of the following conditions is satisfied:
If a leaf $l$ is accessible by $\succ$ from a stem node $t$, we say that it is attached to $t$. In an $\mathrm{N}$-frame, in general, there can be leaves attached to several stem nodes simultaneously (like $l_8$ in the example), as well as those (like $l_3$) not attached to any node (therefore, according to (LL), inaccessible from all worlds of the frame). Definition. We say that an $\mathrm{N}$-frame $\mathcal{F} = (T \sqcup L, \succ)$ is fine if it satisfies (Fine) Each leaf is attached to exactly one stem node: $\forall\, l \in L\ \exists!\,t \in T \ (t \succ l)$. Proposition 3.2. For an arbitrary $\mathrm{N}$-frame $\mathcal{F}$, there exists a fine $\mathrm{N}$-frame $\vec{\mathcal{F}}$ such that $\mathcal{F}$ is a generated subframe of a $p$-morphic image of $\vec{\mathcal{F}}$. Moreover, if $\mathcal{F}$ is finite, then $\vec{\mathcal{F}}$ can also be chosen finite. Proof. We first note that an arbitrary $\mathrm{N}$-frame $\mathcal{F} = (W, \succ)$, $W = T \sqcup L$, is a generated subframe of some (finite if initial frame was finite) $\mathrm{N}$-frame, in which every leaf is attached to at least one stem node.
Indeed, let $T' := T \sqcup \{ t_l \mid l \in L \}$ and extend $\succ$ to $T' \sqcup L$ by
$$
\begin{equation*}
\forall\, l \in L\ \forall\, w \in W\ (t_l \succ w \Leftrightarrow l \succeq w).
\end{equation*}
\notag
$$
The nodes $t_l$ are inaccessible by $\succ$. It is easy to see that $\mathcal{F}' {=}\, (T' \sqcup L, \succ )$ is an $\mathrm{N}$-frame, $\mathcal{F}$ is its generated subframe, and
Consider
$$
\begin{equation*}
\begin{gathered} \, \vec W := T' \sqcup \vec L,\qquad \vec L := \{(t, l) \mid t \in T',\, l \in L,\, t \succ l\}, \\ \pi \colon \vec W \to T' \sqcup L,\qquad \pi(t) = t\ \text{ for }\ t \in T',\qquad \pi((t, l)) = l\ \text{ for }\ (t, l) \in \vec L, \\ w \mathrel{\succ\kern-6pt\succ} t \ \Leftrightarrow\ \pi(w) \succ t \ \text{ for }\ w \in \vec W, \ t \in T', \\ w \mathrel{\succ\kern-6pt\succ} (t, l)\ \Leftrightarrow\ w = t \ \text{ for }\ w \in \vec W, \ (t, l) \in \vec L. \end{gathered}
\end{equation*}
\notag
$$
It is clear that $\vec{\mathcal{F}} := (\vec W, \mathrel{\succ\kern-6pt\succ} )$ is an $\mathrm{N}$-frame satisfying (Fine). That $\pi$ is surjective follows from (2). Let us show that $\pi$ is a $\mathrm{p}$-morphism of $\vec{\mathcal{F}}$ onto $\mathcal{F}'$. Consider $w_1, w_2 \in \vec W$ such that $w_1 \mathrel{\succ\kern-6pt\succ} w_2$. If $w_2 \in T'$, then $\pi(w_1) \succ w_2 = \pi(w_2)$. If $w_2 = (t, l) \in \vec L$, then $w_1 = t$ and $\pi(w_1) = t \succ l = \pi((t, l))$. Consider $w \in \vec W$ and $v \in W$ such that $\pi(w) \succ v$. If $v \in T'$, then $v \in \vec W$, $w \mathrel{\succ\kern-6pt\succ} v$, and $\pi(v) = v$. If $v \in L$, then $\pi(w) \in T'$ by (LL), therefore, $w \in T'$, $(w, v) \in \vec L$, $w \mathrel{\succ\kern-6pt\succ} (w, v)$, and $\pi((w, v)) = v$. $\Box$ Corollary 3.3. If a formula $\varphi$ is valid in all (finite) fine $\mathrm{N}$-frames, then it is valid in all (finite) $\mathrm{N}$-frames. It is worth noting that fine $\mathrm{N}$-frames can be equivalently defined as Kripke frames $\mathcal{F} = (W, \succ)$ obtained from triples $(T, \succ_T, \mathcal{L})$, where
3.1. The logic $\mathrm{J}$ and its framesThe logic $\mathrm{J}$ was introduced by Beklemishev in [18] as a suitable approximation to the polymodal provability logic $\mathrm{GLP}$ with finite model property. We need only its bimodal fragment, which we will call $\mathrm{J}$ in the following part of the paper. Definition. $\mathrm{J}$ is a normal logic given by the following axioms: 1. $\Box_i(\Box_i p \to p) \to \Box_i p$, $i = 0, 1$; 2. $\Diamond_0 p \to \Box_1\Diamond_0 p$; 3. $\Box_0 p \to \Box_1\Box_0 p$; 4. $\Box_0 p \to \Box_0\Box_1 p$. Note that $\mathrm{J} \subset \mathrm{GLB}$. Indeed, the first two axioms of the logic $\mathrm{J}$ are also $\mathrm{GLB}$ axioms. To prove the latter two in $\mathrm{GLB}$, one should use the monotonicity axiom $\Box_0 p \to \Box_1 p$ and the well-known fact that Löb’s axiom $\Box_0(\Box_0 p \to p) \to \Box_0 p$ implies the transitivity $\Box_0 p \to \Box_0\Box_0 p$. Definition. Let $\mathcal{F} = (W, \mathbin{R_0}, \mathbin{R_1})$ be a Kripke frame with transitive conversely well-founded relations $\mathbin{R_0}$ and $\mathbin{R_1}$. Denote by $\sim_\pi$ the reflexive symmetric closure of $\mathbin{R_1}$. The equivalence class under $\sim_\pi$ of a world $w \in W$ is called its plane and is denoted by $\pi(w)$; $\mathcal{F}$ is called a stratified $\mathrm{J}$-frame if $\sim_\pi$ is a congruence on $(W, \mathbin{R_0})$, that is, for all $w_1, w_2 \in W$, We set $(\Pi, {\mathbin{R_0}}_\pi) := (W, \mathbin{R_0}) / \sim_\pi$. For all worlds $w_1, w_2 \in W$,
$$
\begin{equation}
w_1 \mathbin{R_0} w_2\ \Leftrightarrow\ \pi(w_1) \mathbin{R_0}_\pi \pi(w_2).
\end{equation}
\tag{3}
$$
In what follows, the subscript $\pi$ for $\mathbin{R_0}$ will be omitted. It follows from (3) that, in order to define $\mathbin{R_0}$ on a $\mathrm{J}$-frame, it suffices to specify it on its planes. Definition. Let $\mathcal{F} = (W, R_0, R_1)$ be a stratified $\mathrm{J}$-frame, $\Pi$ be the set of its planes. A world $t$ is called the root of a plane $\pi \in \Pi$ if $\pi = \{t\} \cup R_1(t)$. A plane $\pi_0 \in \Pi$ is called the root plane of $\mathcal{F}$ if $\Pi = \pi_0 \cup R_0(\pi_0)$. We say that $\mathcal{F}$ is hereditarily rooted if it has a root plane and each of its planes has a root. In this case, it is clear that the whole frame $\mathcal{F}$ is generated by the root of its root plane, which we call the root of the frame $\mathcal{F}$. In Fig. 2, we give an example of a stratified hereditarily rooted $\mathrm{J}$-model with six planes $\pi_0, \dots, \pi_5$. The valuation can be arbitrary, for example,
$$
\begin{equation*}
\vartheta(p) := \{t_{\pi_0}, w_4, w_8\},\qquad \vartheta(q) := \{t_{\pi_2}, w_1\}
\end{equation*}
\notag
$$
(in all examples, we suppose that the valuation of all variables other than $p$ and $q$ is empty). In [18], Beklemishev proved the following three theorems, which will be actively used in the present paper. Theorem 3.5 (completeness). If $\varphi \in \mathrm{Fm}(\Box_0, \Box_1)$ is not derivable in $\mathrm{J}$, then there exists a finite hereditarily rooted $\mathrm{J}$-frame at the root of which $\varphi$ is false. Given a formula $\varphi \in \mathrm{Fm}(\Box_0, \Box_1)$, we set
$$
\begin{equation*}
M(\varphi) := \bigwedge_{\Box_0\psi \in \operatorname{Sub}(\varphi)} \Box_0\psi \to \Box_1\psi,\qquad \boxdot\varphi := \varphi \wedge \Box_0\varphi \wedge \Box_1\varphi.
\end{equation*}
\notag
$$
Theorem 3.6 (a translation of $\mathrm{GLB}$ into $\mathrm{J}$). For every formula $\varphi \in \mathrm{Fm}(\Box_0, \Box_1)$, 3.2. Transformation of $\mathrm{N}$-models into $\mathrm{J}$-models. Soundness theoremLet $\mathcal{M} = (W, \succ, \vartheta)$, $W = T \sqcup L$ be a fine $\mathrm{N}$-model. We construct a $\mathrm{J}$-model $\mathcal{M} = (W, \mathbin{R_0}, \mathbin{R_1}, \vartheta)$ from it. We let the relation $\mathbin{R_1}$ connect stem nodes and leaves attached to them:
$$
\begin{equation*}
w \mathbin{R_1} v \ \Leftrightarrow\ w \succ v \wedge w \in T \wedge v \in L.
\end{equation*}
\notag
$$
By (Fine), each plane under this relation contains exactly one stem node and leaves attached to it. Let $\mathbin{R_0}$ be defined on the planes by
$$
\begin{equation*}
\pi(t) \mathbin{R_0} \pi(t') \ \Leftrightarrow\ t \succ t'.
\end{equation*}
\notag
$$
$\mathbin{R_0}$ is conversely well-founded and transitive by (Trans) and (Fund), and for $\mathbin{R_1}$ these properties are clear since $\mathbin{R}_1^2 = \varnothing$. Figure 3 provides an example of the transformation from an $\mathrm{N}$-model into a $\mathrm{J}$-model. Here we suppose that the valuations in both models are the same. Proposition 3.7. For every formula $\varphi \in \mathrm{Fm}(\Box)$ and world $w\in W$, and Proof. Note that ${\succ} = {\mathbin{R}}$, were $\mathbin{R}$ is given by (1) for the model $\mathcal{M}^*$. Therefore, the first claim follows from Lemma 2.2. Since it follows that the implications in $M(\varphi^*)$ have the form It is easy to see that $\mathcal{M}^* \vDash \Box_1\Box_1\bot$, therefore, all the implications of this form are trivially true in $\mathcal{M}^*$. $\Box$ The soundness of $\mathrm{Nie}$ follows immediately from Proposition 3.7. Proof. Suppose that a formula $\varphi$ is false at a world $w$ of a fine $\mathrm{N}$-frame $\mathcal{M}$ (by Corollary 3.3 we can consider only such frames). By Proposition 3.7, $\mathcal{M}^*, w \nvDash \varphi^*$ and $\mathcal{M}^* \vDash M(\varphi^*)$, therefore, $\mathcal{M}^*, w \nvDash \boxdot M(\varphi^*) \to \varphi^*$. By Theorems 3.4 and 3.6, $\mathrm{GLB} \nvdash \varphi^*$. Hence $\mathrm{Nie} \nvdash \varphi$ by Proposition 2.1. $\Box$ 3.3. Transformation of $\mathrm{J}$-models into $\mathrm{N}$-models. Completeness theoremLet $\mathcal{M} = (W, \mathbin{R_0}, \mathbin{R_1}, \vartheta)$ be a stratified hereditarily rooted $\mathrm{J}$-model with root $w_0$. We denote by $\Pi^\circ$ the set of its planes containing more then one world (such planes will be called essential). Let
$$
\begin{equation*}
T := \{ t_\pi \}_{\pi \in \Pi^\circ},\quad L := \bigcup_{\pi \in \Pi^\circ} L_\pi,\quad L_\pi := \{ w \in \pi \mid R_{1}(w) = \varnothing \},
\end{equation*}
\notag
$$
where $t_\pi$ is the root of $\pi$. Note that all $L_\pi$ are not empty, since $\mathbin{R_1}$ is conversely well-founded, and $L_\pi \,{\cap}\, T \,{=}\, \varnothing$ for $\pi\in\Pi^\circ$. Consider $\mathcal{M}^\circ := (W^\circ, \mathbin{R}|_{W^\circ}, \vartheta|_{W^\circ})$, where $W^\circ := T \sqcup L$ and $\mathbin{R}$ is given by (1). One can easily check that this is a fine $\mathrm{N}$-model. In the $\mathrm{J}$-model $\mathcal{M}_1$ from Fig. 2 only the planes $\pi_0$, $\pi_1$, $\pi_3$ and $\pi_5$ are essential,
$$
\begin{equation*}
L_{\pi_0} = \{ w_2, w_3\},\quad L_{\pi_1} = \{ w_5\},\quad L_{\pi_3} = \{ w_7\},\quad L_{\pi_5} = \{ w_8\}.
\end{equation*}
\notag
$$
The corresponding $\mathrm{N}$-model $\mathcal{M}_1^\circ$ is shown in Fig. 4. The valuation $\vartheta^\circ$ in the resulting model is determined by the valuation in $\mathcal{M}_1$:
$$
\begin{equation*}
\vartheta^\circ(p) = \{t_{\pi_0}, w_8\},\qquad \vartheta^\circ(q) = \varnothing.
\end{equation*}
\notag
$$
Proposition 3.9. Let $\mathcal{M}$ be a stratified hereditarily rooted $\mathrm{J}$-model. If $M(\varphi^*)$ is true in $\mathcal{M}$ for some $\varphi \in \mathrm{Fm}(\Box)$, then $\forall\,\psi \,{\in}\, \operatorname{Sub}(\varphi)$, $w \,{\in}\, W^\circ$ From Proposition 3.9 we immediately obtain the completeness theorem. Theorem 3.10 (completeness). For every formula $\varphi\,{\in}\,\mathrm{Fm}(\Box)$ non-derivable in $\mathrm{Nie}$, there is a finite $\mathrm{N}$-model $\mathcal{M}$ such that $\mathcal{M} \nvDash \varphi$. Proof. Suppose $\mathrm{Nie} \nvdash \varphi$. By Proposition 2.1, $\mathrm{GLB} \nvdash \varphi^*$, and, by Theorem 3.6, $\mathrm{J} \,{\nvdash}\, \boxdot M(\varphi^*) \to \varphi^*$. By Theorem 3.10, there is a finite stratified hereditarily rooted $\mathrm{J}$-model $\mathcal{M}$ with a root $w_0$ such that $\mathcal{M}, w_0 \vDash \boxdot M(\varphi^*)$ and $\mathcal{M}, w_0 \nvDash \varphi^*$. Since $W = \{ w_0\} \cup \mathbin{R_0}(w_0) \cup \mathbin{R_1}(w_0)$, $\mathcal{M} \vDash M(\varphi^*)$. If the plane $\pi(w_0)$ is essential, then, by Proposition 3.9, $\varphi$ is false in the world $w_0$ of the finite fine $\mathrm{N}$-model $\mathcal{M}^\circ$.
Otherwise, we extend $\mathcal{M}$ to the model $\mathcal{M}'$ by adding a new root $t_0$ in the plane $\pi(w_0)$:
$$
\begin{equation*}
W' := W \sqcup \{ t_0 \}, \quad \mathbin{R_0}(t_0) := \mathbin{R_0}(w_0) = W \setminus \{ w_0 \}, \quad \mathbin{R_1}(t_0) := \{ w_0 \}.
\end{equation*}
\notag
$$
Since $\mathcal{M}$ is a generated submodel of $\mathcal{M}'$, $\mathcal{M}', w_0 \nvDash \varphi$. Further, $\mathcal{M}', t_0 \vDash \Box_1\Box_1\bot$, therefore, as noted in the proof of Proposition 3.7, $M(\varphi^*)$ is true at $t_0$, whence in the whole model $\mathcal{M}'$. By Proposition 3.9, $\mathcal{M}'^\circ, w_0 \nvDash \varphi$. $\Box$ Let us now return to the proof of Proposition 3.9. Suppose that $M(\varphi^*)$ is true in a stratified hereditarily rooted $\mathrm{J}$-model $\mathcal{M}$. Lemma 3.11. For every $\Box\psi \in \operatorname{Sub}(\varphi)$ and world $w \in W$, if $\mathcal{M}, w \nvDash (\Box\psi)^*$, then there is a world $v \in W^\circ$ such that $w \mathbin{R} v$ and $\mathcal{M}, v \nvDash \psi^*$. Proof. Since $\mathbin{R}$ is conversely well-founded, there is a world $v \in W$ such that $w \mathbin{R} v$ and $\mathcal{M}, v \nvDash \psi^*$ from which other worlds with the same properties are inaccessible by $\mathbin{R}$. From the definition of $\mathbin{R}$, it follows that the plane $\pi(v)$ is essential. We will show that $v \in W^\circ$.
Assume the converse. Let $t$ be the root of $\pi(v)$. Since $v \notin W^\circ$, $t \mathbin{R_1} v$ and $\mathcal{M}, v \nvDash \Box_1\bot$, therefore, $\mathcal{M}, t \nvDash \Box_1(\Box_1\bot \vee \psi^*)$. By the assumption, $\mathcal{M} \vDash M(\varphi^*)$. Hence $\mathcal{M}, t \nvDash \Box_0(\Box_1\bot \vee \psi^*)$, that is, there is a world $u \in W$ such that $t \mathbin{R_0} u$, $\mathbin{R_1}(u) \neq \varnothing$, and $\mathcal{M}, u \nvDash \psi^*$. Since $t$ and $v$ are in the same plane, $v \mathbin{R_0} u$. Furthermore, $w \mathbin{R_0} u$ (if $w \mathbin{R_1} v$, then $\mathbin{R_0}(w) = \mathbin{R_0}(v)$, otherwise $w \mathbin{R_0} v \mathbin{R_0} u$ and $w \mathbin{R_0} u$ by transitivity). Since $\mathbin{R_1}(u) \neq \varnothing$, it follows that $v \mathbin{R} u$ and $w \mathbin{R} u$, so the world $u$ has all the properties of $v$ and is accessible from it, contradicting the choice of $v$. $\Box$ Now let us prove Proposition 3.9. It is easy to see that $\mathcal{M}^\circ$ is a fine $\mathrm{J}$-model. Let us check that, for all $\psi \in \operatorname{Sub}(\varphi)$,
$$
\begin{equation*}
(W, \mathbin{R}, \vartheta), w \vDash \psi \ \Leftrightarrow\ \mathcal{M}^\circ, w \vDash \psi.
\end{equation*}
\notag
$$
The proof is by induction on the construction of $\psi$. Since $\mathcal{M}^\circ$ is a submodel of $(W, \mathbin{R}, \vartheta)$, all the cases except $\psi \equiv \Box\eta$, and, more specifically
$$
\begin{equation*}
\mathcal{M}^\circ, w \vDash \Box\eta\quad \Longrightarrow\quad (W, \mathbin{R}, \vartheta) \vDash \Box\eta,
\end{equation*}
\notag
$$
are trivial. This implication follows from Lemma 3.11. 3.4. Unravelling. Completeness with respect to finite treelike framesIt follows from Corollary 3.3 that $\mathrm{Nie}$ is complete with respect to fine $\mathrm{N}$-frames. In fact, the completeness holds even for the following narrower class of frames. Definition. Let $\succ$ be a binary relation on a finite set $T$. Suppose that $(T, \succ )$ has a root, that is, a node $t_0 \in T$ such that $T$ is generated by $t_0$. Let the immediate successor relation $ \mathrel{\kern2pt \succ{\kern-12pt\cdot\kern6pt}} $ be defined on $T$ by A path in $(T, \succ)$ is a finite sequence of nodes $t_0, \dots, t_n$ such that $t_0$ is the root and $t_i \mathrel{\kern2pt \succ{\kern-12pt\cdot\kern6pt}} t_{i+1}$ for all $i < n$; $(T, \succ)$ is a tree if, for all $t \in T$, there exists a unique path $(t_0, \dots, t_n)$ with $t_n = t$. We say that a finite fine $\mathrm{N}$-frame $\mathcal{F} = (T \sqcup L, \succ)$ has a root $t_0$ if $t_0$ is the root of $(T, {\succ}|_T)$; it is treelike if $(T, {\succ}|_T)$ is a tree. Proposition 3.12. If $\varphi \in \mathrm{Fm}(\Box)$ is not derivable in $\mathrm{Nie}$, then there is a finite fine $\mathrm{N}$-model $\mathcal{M}$ with root $t_0$ such that either $\mathcal{M}, t_0 \nvDash \varphi$, or there is a unique leaf $l_0$ attached to $t_0$ and $\mathcal{M}, {l_0} \nvDash \varphi$. Proof. By Theorem 3.10 and Corollary 3.3, there is a fine $\mathrm{N}$-model $\mathcal{M}_0$ with a world $w$ such that $\mathcal{M}_0, w \nvDash \varphi$. If $w$ is a stem node, then it suffices to take the submodel generated by $w$. Otherwise, in addition to the submodel of $\mathcal{M}_0$ generated by $w$, we keep in $\mathcal{M}$ the stem node $t$ to which $w$ is attached. $\Box$ Proposition 3.13. Let $\mathcal{F} = (T \sqcup L, \succ)$ be a finite fine $\mathrm{N}$-frame with root $t_0 \in T$. Then there exists a treelike frame $\vec{\mathcal{F}}$ such that $\mathcal{F}$ is its $p$-morphic image. Proof. Let $\vec T$ denote the set of all paths in $(T, {\succ}|_T)$. Consider
$$
\begin{equation*}
\vec L := \{ (\vec t, l) \mid \vec t = (t_0, \dots, t_n) \in \vec T,\, l \in L,\, t_n \succ l \},\qquad \vec W := \vec T \sqcup \vec L.
\end{equation*}
\notag
$$
For convenience, we set $\tau(\vec l\,)=\vec t$ if $\vec l = (\vec t, l)$. Let us define the relation $ \mathrel{\succ\kern-6pt\succ} $
$$
\begin{equation*}
\begin{gathered} \, \forall\, \vec t_1, \vec t_2 \in \vec T \ (\vec t_1 \mathrel{\succ\kern-6pt\succ} \vec t_2 \Leftrightarrow \vec t_1 \text{ is a prefix of } \vec t_2 \text{ and } \vec t_1 \neq \vec t_2), \\ \forall\, \vec t \in \vec T,\, \vec l \in \vec L\, (\vec t \mathrel{\succ\kern-6pt\succ} \vec l \Leftrightarrow \tau(\vec l\,) = \vec t\,), \\ \forall\, \vec l \in \vec L,\, \vec t \in \vec T\ (\vec l \mathrel{\succ\kern-6pt\succ} \vec t \Leftrightarrow \tau(\vec l\,) \mathrel{\succ\kern-6pt\succ} \vec t\,). \end{gathered}
\end{equation*}
\notag
$$
It is obvious that $\vec{\mathcal{F}} := (\vec T \sqcup \vec L, \mathrel{\succ\kern-6pt\succ} )$ is a treelike $\mathrm{N}$-frame. Consider the function Let us check that $\pi$ is a $p$-morphism of $\vec{\mathcal{F}}$ onto $\mathcal{F}$. It is surjective, since $\mathcal{F}$ is a finite model with the root $t_0$.
For all $\vec t, \vec t_1, \vec t_2 \in \vec T$, $\vec l \in \vec L$, $t \in T$, and $l \in L$, we have:
3.5. Logic $\mathrm{Nie}'$ and the class of all $\mathrm{Nie}$-framesIn this section, we will show that the class of all $\mathrm{Nie}$-frames coincides with the class of $\mathrm{N}$-frames. This is done as follows. We introduce an auxiliary logic $\mathrm{Nie}' \subseteq \mathrm{Nie}$ given by the specific set of axioms. Next, we establish that all $\mathrm{Nie}'$-frames are $\mathrm{N}$-frames, and, as a consequence, we obtain the desired fact for $\mathrm{Nie}$. Consider the normal logic $\mathrm{Nie}'$ given by the following axioms: [Löb]. $\Box(\Box(p \vee \Box p) \to p) \to \Box p$; [TL]. $\Box(\Box p \to \Diamond\Box p) \vee \Box(p \vee \Box p)$. Similarly to $\mathrm{GL}$, one can derive an analogue of the transitivity axiom from [Löb]: [Trans]. $\Box p \to \Box^2(p \vee \Box p)$. Proof. We set $A := \Box(p \vee \Box p) \wedge p$. Since $A \to p$ By normality and [Löb], as claimed. $\Box$ Lemma 3.16. Let $\mathcal{M} = (T \sqcup L, \succ, \vartheta)$ be an $\mathrm{N}$-model. If, for some formula $\varphi \in \mathrm{Fm}(\Box)$ and world $w$, then $\mathcal{M}, w \vDash \Box(\varphi \vee \Box\varphi)$. Proof. If $w$ is a stem node and $l$ is a leaf attached to it, then by (LL) and (Trans) $\mathcal{M}, l \vDash \Box\varphi$. In the stem nodes accessible from $w$, $\varphi$ is true by assumption. Thus, $\mathcal{M}, w \vDash \Box(\varphi \vee \Box\varphi)$. $\Box$ Proof. It is sufficient to check that the axioms of $\mathrm{Nie}'$ are true in an arbitrary $\mathrm{N}$-model $\mathcal{M} = (W, \succ, \vartheta)$.
[Löb]. Suppose $\mathcal{M}, w \nvDash \Box p$. If there is a stem node acessible from $w$ at which $p$ is false, then, by (Fund) and (Trans), there exists $t \in T$ such that $w \succ t$, $\mathcal{M}, t \nvDash p$, and $\forall\, t' \in T (t \succ t' \Rightarrow \mathcal{M}, t' \vDash p)$. Therefore, $\mathcal{M}, t \vDash \Box(p \vee \Box p)$ by Lemma 3.16. Otherwise, $p$ is false at some leaf $l$ attached to $w$ and $\mathcal{M}, l \vDash \Box p$ by (LL) and (Trans). In any case, there is a world accessible from $w$ at which $\Box(p \vee \Box p)$ is true and $p$ is false, that is, $\mathcal{M}, w \nvDash \Box(\Box(p \vee \Box p) \to p)$. [TL]. Suppose $\mathcal{M}, w \nvDash \Box(\Box p \to \Diamond\Box p)$. Then there is a world $l$ accessible from $w$ such that $\mathcal{M}, l \vDash \Box p \wedge \neg\Diamond\Box p$. Let us show that $l \in L$. Indeed, otherwise there exists a leaf $l'$ attached to it, at which, by (LL) and (Trans), $\Box p$ is true. Thus, $l \in L$ and, by (LL), $w \in T$. $p$ is true at all worlds accessible from $l$, therefore, by (TL), at all stem nodes accessible from $w$. By Lemma 3.16, $\mathcal{M}, w \vDash \Box(p \vee \Box p)$. $\Box$ Since $\mathrm{Nie}'$ is complete with respect to $\mathrm{N}$-frames, the following result is immediate. Definition. Let $(W, \succ)$ be a Kripke frame such that the relation $\prec$ is well-founded. Let the depth of a world $w \in W$ (the function $d\colon W \,{\to}\, \mathrm{Ord}$) be defined recursively by If the set is empty, the set $d(w) = 0$. It is well known that every ordinal can be represented as $\gamma = \omega \alpha + n$, where $n < \omega$. We set $\mathfrak{d}(w) = n$ if $d(w) = \omega \alpha + n$. Note that if the depth of the world $w$ is greater then some ordinal $\gamma$, then there is a world $v$ accessible from $w$ by the transitive closure of $\succ$ whose depth is equal to $\gamma$ (to obtain it one can take a $\prec$-minimal element in the set of the worlds accessible from $w$ by the transitive closure of $\succ$ whose depth is greater than or equal to $\gamma$). Proposition 3.19. If $\mathrm{Nie}'$ is valid in a Kripke frame $\mathcal{F} = (W, \succ)$, then this frame is an $\mathrm{N}$-frame. Proof. First of all, let us show that $\prec$ is well-founded. Suppose this is not the case. Then there is an infinite decreasing sequence of worlds Consider the model $\mathcal{M} = (W, \vartheta)$ with the valuation $\vartheta(p) := W \setminus \{ w_i \mid i \in \omega \}$. The formula $\Box(p \vee \Box p)$ is false at every world from the sequence and $p$ is true at all other worlds, therefore, $\mathcal{M} \vDash \Box(p \vee \Box p) \to p$, so $\mathcal{M}, w_0 \vDash \Box(\Box(p \vee \Box p) \to p)$. At the same time, $\mathcal{M}, w_0 \nvDash \Box p$, contradicting the fact that [Löb] is valid in $\mathcal{M}$.
Let $T := \{ w \in W \mid \mathfrak{d}(w) \text{ is odd} \}$, and $L := W \setminus T$. We need to check that this partition satisfies all the conditions of an $\mathrm{N}$-frame. First, let us show that (EL) is satisfied. If $t \in T$, then $\mathfrak{d}(t)$ is odd and $d(t)$ is not a limit ordinal. Therefore, there is $ l \prec t$ such that $ d(t) = d(l) + 1$. Since $\mathfrak{d}(l)$ is even, $l \in L$. The proof of the remaining conditions is by induction over $\prec$. Suppose that (Trans), (TL) and (LL), are satisfied for all worlds accessible from $w \in W$ by the transitive closure of $\succ$. Let us show that the same conditions are satisfied if we allow worlds to be equal to $w$. We need the following two facts for the proof: 1. Intransitivity: If $w \succ v_1 \succ \dots \succ v_n$, where $n \geqslant 2$ and $v_n \in L$, then $w \nsucc v_n$. Consider the valuation $\vartheta(p) := T \setminus \{ v_1, v_2\}$. We have $(\mathcal{F}, \vartheta), w \nvDash \Box(p \vee \Box p)$, therefore, by [TL] $(\mathcal{F}, \vartheta), w \vDash \Box(\Box p \to \Diamond\Box p)$. By the induction hypothesis, (LL), and (EL), $\Box p$ is true and $\Diamond\Box p$ is false at $v_n$ ($v_1$ and $v_2$ are not accessible by well-foundness). Thus, $w \nsucc v_n$ 2. Coherence: If $w \succ l$ and $w \succ t$, where $l \in L$ and $t \in T$, then $l \succ t$. Consider the valuation $\vartheta(p) := T \setminus \{ t \}$. We use the induction hypothesis several times. By (EL), $(\mathcal{F}, \vartheta), t \nvDash \Box p$, therefore, $\Box(p \vee \Box p)$ is false at $w$, hence, by [TL], $(\mathcal{F}, \vartheta), l \vDash \Box p \to \Diamond\Box p$. By (LL) and (EL), $\Diamond\Box p$ is false at $l$. Thus, $(\mathcal{F}, \vartheta), l \nvDash \Box p$ and $l \succ t$ by (LL). Now we are ready to make the induction step: (Trans). Suppose $v \in W$ and $t \in T$ are such that $w \succ v \succ t$. By (EL), there is a leaf $l$ attached to $t$. Consider the valuation $\vartheta(p) := W \setminus \{ t, l \}$. We have $(\mathcal{F}, \vartheta), w \nvDash \Box^2(p \vee \Box p)$, therefore, by [Trans] $(\mathcal{F}, \vartheta), w \nvDash \Box p$, that is, $w \succ t$ or $w \succ l$. The latter is impossible by intransitivity. (TL). If $w, t \in T$, $l \in L$, $w \succ l$, and $w \succ t$, then $l \succ t$ by coherence. (LL). Suppose that $w, l \in L$ and $w \succ l$. Then $d(w) > d(l)$ and, since $\mathfrak{d}(w)$ and $\mathfrak{d}(l)$ are even, $d(w) > d(l) + 1$. There is a world $t$ accessible from $w$ by the transitive closure of $\succ$ such that $d(t) = d(l) + 1$. Since $\mathfrak{d}(l) + 1$ is odd, $t \in T$ and $w \succ t$ by (Trans), which is already proved for the induction step. Thus, $l \succ t$ by coherence for $w$, $l$, and $t$, which is impossible, since $d(t) > d(l)$. $\Box$ Proof. If $\mathcal{F} \vDash \mathrm{Nie}$, then $\mathcal{F} \vDash \mathrm{Nie}'$ by Corollary 3.18. If $\mathcal{F} \vDash \mathrm{Nie}'$, then, by Proposition 3.19, $\mathcal{F}$ is an $\mathrm{N}$-frame. Finally, if $\mathcal{F}$ is an $\mathrm{N}$-frame, then $\mathcal{F} \vDash \mathrm{Nie}$ by Theorem 3.8. $\Box$ At the same time, as we will show in § 7.1, $\mathrm{Nie}'$ does not coincide with $\mathrm{Nie}$ and, therefore, is not Kripke complete. § 4. Logic $\mathrm{Nie}_\flat$In this section, we consider the logic $\mathrm{Nie}_\flat$, which is a conservative extension of $\mathrm{Nie}$ in the language with additional propositional constant $\flat$. We will see that it is sound and complete with respect to $\mathrm{N}$-frames, assuming that $\flat$ is true in leaf nodes and only in them, and obtain its explicit finite axiomatization. We denote by $\mathrm{Fm}(\Box; \flat)$ the set of all formulas constructed from variables, $\bot$, and $\flat$, using $\to$ and $\Box$. Extend the translation ${}^*$ to $\mathrm{Fm}(\Box; \flat)$ by letting $\flat^* := \Box_1\bot$. We consider the logic
$$
\begin{equation*}
\mathrm{Nie}_\flat := \{ \varphi \in \mathrm{Fm}(\Box; \flat) \mid \mathrm{GLB} \vdash \varphi^* \}.
\end{equation*}
\notag
$$
It is easy to see that $\mathrm{Nie}_\flat$ is a normal modal logic conservatively extending $\mathrm{Nie}$, that is,
$$
\begin{equation*}
\forall\,\varphi \in \mathrm{Fm}(\Box) (\mathrm{Nie} \vdash \varphi \Leftrightarrow \mathrm{Nie}_\flat \vdash \varphi).
\end{equation*}
\notag
$$
A Kripke frame in the language with the constant $\flat$ is a triple $(W, \mathbin{R}, L)$, where $W$ is a non-empty set, $\mathbin{R}$ is a binary relation on $W$, and and $L$ is a subset of $W$. A Kripke model is a frame $\mathcal{F} = (W, \mathbin{R}, L)$ with the valuation of variables $\vartheta\colon \mathrm{PVar} \to \mathcal{P}(W)$. We define whether a formula $\varphi \in \mathrm{Fm}(\Box; \flat)$ is true at a world of such model, as usual, by induction on the construction of $\varphi$ with an extra base case for $\varphi \equiv \flat$:
$$
\begin{equation*}
\mathcal{M}, w \vDash \flat \ \Leftrightarrow\ w \in L.
\end{equation*}
\notag
$$
In the case of $\mathrm{N}$-frame $\mathcal{F} = (W, \succ)$, we always assume that $L$ is the set of its leaves. Moreover, as noted in Proposition 3.1, $L$ is determined uniquely by $(W, \succ)$. Thus, we may consider $\mathrm{N}$-frames as frames for $\mathrm{Nie}_\flat$. 4.1. Soundness and completeness with respect to Kripke frames Proposition 4.1. Let $\mathcal{M} = (W, \succ, \vartheta)$ be a fine $\mathrm{N}$-model. Then, for all formulas $\varphi \in \mathrm{Fm}(\Box; \flat)$ and worlds $w \in W$, Proof. The proof is by induction on the construction of $\varphi$. The only new case compared to Proposition 3.7 is $\varphi \equiv \flat$. In this case, for every world $w \in W$
$$
\begin{equation*}
\mathcal{M}, w \vDash \flat \ \Leftrightarrow\ w \in L \ \Leftrightarrow\ \mathcal{M}^*, w \vDash \Box_1\bot.
\end{equation*}
\notag
$$
To prove that $M(\varphi^*)$ is true in $\mathcal{M}^*$ for all $\varphi \in \mathrm{Fm}(\Box; \flat)$, we can repeat exactly the same arguments as in Proposition 3.7, since all formulas of the form $\Box_0\eta \in \operatorname{Sub}(\varphi^*)$ are, as before, $\Box_0(\Box_1\bot \vee \psi^*)$ for $\Box\psi \in \operatorname{Sub}(\varphi)$. $\Box$ Proposition 4.2. Let $\mathcal{M} = (W, \mathbin{R_0}, \mathbin{R_1}, \vartheta)$ be a stratified hereditarily rooted $\mathrm{J}$-model. If, for a formula $\varphi \in \mathrm{Fm}(\Box; \flat)$, $\mathcal{M} \vDash M(\varphi^*)$, then $\forall\,\psi \in \operatorname{Sub}(\varphi)$, $w \in W^\circ$, Proof. We proceed by induction on the construction of $\psi$. The only one new case compared to Proposition 3.9 is $\psi \equiv \flat$. In this case, for all $w \in W^\circ$, $\Box$ Using the last two propositions and arguing as in Theorems 3.8 and 3.10 we arrive at Theorems 4.3 and 4.4. Theorem 4.4 (completeness). $\mathrm{Nie}_\flat$ is compete with respect to finite $\mathrm{N}$-frames. Note that $p$-mophisms used in Propositions 3.2 and 3.13 glue together leaves with leaves and stem nodes with stem nodes, therefore, they preserve truth values of formulas with $\flat$. Thus, $\mathrm{Nie}_\flat$ is complete with respect to fine and, moreover, treelike $\mathrm{N}$-frames. 4.2. AxiomatizationConsider the normal modal logic $\mathrm{Nie}_\flat'$ given by the following axioms: [Löb$_\flat$]. $\Box(\Box(\neg\flat \to p) \to p) \to \Box p$; [LL-EL$_\flat$]. $\flat \leftrightarrow \Box\neg\flat$; [TL$_\flat$]. $\Box(\flat \to \neg\Box p) \vee \Box(\neg\flat \to p)$. We will prove that $\mathrm{Nie}_\flat' = \mathrm{Nie}_\flat$, thus the above formulas provide an axiomatization of $\mathrm{Nie}_\flat$. Similarly to Proposition 3.15, one can derive in $\mathrm{Nie}_\flat'$ an analogue of the transitivity axiom. [Trans$_\flat$]. $\Box p \to \Box^2(\neg\flat \to p)$. Note that the axioms involve expressions of the form $\Box_L \varphi := \Box(\flat\,{\to}\, \varphi)$ and $\Box_T \varphi := \Box(\neg\flat \to \varphi)$. Since $\flat$ is true at leaves and only at them, the modalities $\Box_L$ and $\Box_T$ correspond to accessible leaves and stem nodes, respectively. Proof. Since $\mathrm{Nie}_\flat$ is complete with respect to $\mathrm{N}$-frames, it is sufficient to show that the axioms of $\mathrm{Nie}_\flat'$ are true in every $\mathrm{N}$-model $\mathcal{M} = (W,\succ, \vartheta)$, $W = T \sqcup L$.
[Löb$_\flat$]. Suppose that $\Box(\Box(\neg\flat \to p) \to p)$ is true and $\Box p$ is false at a world $w \in W$. Then there exists $v \prec w$ such that $\mathcal{M},v \nvDash p$ and $\mathcal{M}, v \nvDash \Box(\neg\flat \to p)$, so there is a stem node accessible from $v$ at which $p$ is false. By (Fund) and (Trans), there is $t \in T$ such that $v \succ t$, $\mathcal{M}, t \nvDash p$, and $p$ is true at all stem nodes accessible from $t$, that is, $\mathcal{M}, t \vDash \Box(\neg\flat \to p)$. At the same time, $w \succ v \succ t$, whence, by (Trans), $w \succ t$ and $\mathcal{M}, t \vDash \Box(\neg\flat \to p) \to p$. A contradiction. [LL-EL$_\flat$]. The left-to-right implication follows from (LL), and the converse one is secured by (EL). [TL$_\flat$]. Suppose that $\Box(\flat \to \neg\Box p)$ and $\Box(\neg\flat \to p)$ are false at a world $w$ at the same time. Then there are $l \in L$ and $t \in T$ accessible from $w$ such that $\mathcal{M}, l \vDash \Box p$ and $\mathcal{M}, t \vDash \neg p$. By (LL) and (TL), $w \in T$ and $l \succ t$, contradicting $\Box p$ being true at $l$. $\Box$ To establish that $\mathrm{Nie}_\flat = \mathrm{Nie}_\flat'$, we need to check the completeness of $\mathrm{Nie}_\flat'$ with respect to $\mathrm{N}$-frames. For this purpose, we use the standard method of selective filtration of the canonical model (see § 5.5 in [17]). Let $W^c$ be the collection of all maximal $\mathrm{Nie}_\flat'$-consistent subsets of $\mathrm{Fm}(\Box; \flat)$,
$$
\begin{equation*}
L^c := \{ w \in W^c \mid \flat \in w \},\qquad T^c := W^c \setminus L^c.
\end{equation*}
\notag
$$
Next, let the relation $\mathbin{R}^c$ on $W^c$ be defined by
$$
\begin{equation*}
w \mathbin{R}^c v \ \Leftrightarrow\ \forall\,\varphi \in \mathrm{Fm}(\Box; \flat) (\Box\varphi \in w \Rightarrow \varphi \in v),
\end{equation*}
\notag
$$
and the valuation $\vartheta^c$: The frame $\mathcal{F}^c = (W^c, \mathbin{R}^c, L^c)$ is called the canonical frame, and the model $\mathcal{M}^c = (\mathcal{F}^c, \vartheta^c)$ is called the canonical model of $\mathrm{Nie}_\flat'$. The following properties of the canonical model can be verified in the standard way:
Proof. (Trans). Consider $w_1, w_2 \in W^c$ and $t \in T^c$ such that $w_1 \mathbin{R}^c w_2 \mathbin{R}^c t$. We will show that $w_1 \mathbin{R}^c t$. In fact, if $\mathcal{M}^c, w_1 \vDash \Box\varphi$, then, by [Trans$_\flat$] $\mathcal{M}^c, w_1 \vDash \Box^2(\neg\flat \to \varphi)$. Therefore, $\mathcal{M}^c, t \vDash \neg\flat \to \varphi$, and hence $\mathcal{M}^c, t \vDash \varphi$.
(EL) and (LL) immediately follow from [LL-EL$_\flat$]. (TL). Consider $t, t' \in T^c$ and $l \in L^c$ such that $t \mathbin{R}^c l$ and $t \mathbin{R}^c t'$. We will show that $l \mathbin{R}^c t'$. In fact, if $\mathcal{M}^c, l \vDash \Box\varphi$, then $\mathcal{M}^c, t \nvDash \Box(\flat \to \neg\Box\varphi)$, therefore, by [TL$_\flat$] $\mathcal{M}^c, t \vDash \Box(\neg\flat \to \varphi)$ and $\mathcal{M}^c, t' \vDash \varphi$. $\Box$ Lemma 4.7. Suppose that $w \in W^c$ and $\varphi \in \mathrm{Fm}(\Box)$ are such that $\mathcal{M}^c, w \nvDash \Box\varphi$. Hence Proof. Since $\mathcal{M}^c, w \nvDash \Box\varphi$, there is a world $v \in \mathbin{R}^c(w)$ at which $\varphi$ is false. If $\mathcal{M}^c, w \vDash \Box(\neg\flat \to \varphi)$, then $v \in L^c$.
If $\mathcal{M}^c, w \nvDash \Box(\neg\flat \to \varphi)$, then, by [Löb$_\flat$], $\mathcal{M}^c, w \nvDash \Box(\Box(\neg\flat \to \varphi) \to (\neg\flat \to \varphi))$. Thus, there is a world $t \in T^c$ accessible from $w$, where $\Box(\neg\flat \to \varphi)$ is true and $\varphi$ is false. $\Box$ Note that the worlds $l$ and $t$ from Lemma 4.7 are irreflexive, since
$$
\begin{equation*}
\mathcal{M}^c, l \vDash \Box\neg\flat,\quad \mathcal{M}^c, t \vDash \Box(\neg\flat \to \varphi),\text{ and } \mathcal{M}^c, t \nvDash \neg\flat \to \varphi.
\end{equation*}
\notag
$$
Corollary 4.8. If a formula $\varphi$ is not derivable in $\mathrm{Nie}_\flat'$, then there is an irreflexive world $w_0 \in W^c$ in which $\varphi$ is false. Proof. Suppose that $\mathrm{Nie}_\flat' \nvdash \varphi$. Then $\{ \neg\varphi \}$ is a $\mathrm{Nie}_\flat'$-consistent set and, by Lindenbaum’s lemma, there is $w \in W^c$, where $\varphi$ is false. If $w$ is irreflexive, then we are done. Otherwise, $\mathcal{M}^c, w \nvDash \Box\varphi$, thus, by Lemma 4.7, there is an irreflexive world $w_0 \prec w$ in which $\varphi$ is false. $\Box$ Theorem 4.9 (completeness). The logic $\mathrm{Nie}_\flat'$ is complete with respect to finite $\mathrm{N}$-frames. Proof. Let $\mathrm{Nie}_\flat' \nvdash \varphi$ and let $\Phi$ be the set consisting of $\varphi$, $\Box\neg\flat$, and all their subformulas.
We will extract a finite $\mathrm{N}$-model from $\mathcal{M}^c$ in which $\varphi$ is falsified. For this, we construct a sequence of subsets of $W^c$: $W^{(1)} \subseteq \dots \subseteq W^{(k)} \subseteq \dots \subset W^c$, which stabilizes at the set of the worlds of an $\mathrm{N}$-model. For convenience, we also construct a sequence of sets of stem nodes $\Delta T^{(k)} \subset T^c$. Using Corollary 4.8, we take an irreflexive world $w_0 \in W^c$ in which $\varphi$ is false. Consider two cases: $w_0 \in T^c$ and $w_0 \in L^c$. In the first case, let $W^{(1)} = \Delta T^{(1)} := \{ w_0 \}$. In the second case, we need an extra step: let $\Box\eta_1, \dots, \Box\eta_m$ be all the formulas of the form $\Box\eta$ in $\Phi \setminus w_0$. By [LL-EL$_\flat$], we have $\mathcal{M}^c, w_0 \vDash \Box\neg\flat$, and, therefore, for $j = 1, \dots, m$, $\Box(\neg\flat \to \eta_j)$ are also false at $w_0$. Thus, by Lemma 4.7, there are irreflexive stem nodes $t_1, \dots, t_m \in T^c$ accessible from $w_0$ such that $\eta_j$ is false and $\Box(\neg\flat \to \eta_j)$ is true at $t_j$ for all $j = 1, \dots, m$. Let $W^{(1)} := \{ w_0, t_1, \dots, t_m \}$ and $\Delta T^{(1)} = \{ t_1, \dots, t_m \}$. Suppose that, for some $n \geqslant 1$, $W^{(n)}$ and $\Delta T^{(n)}$ are constructed. For each $t \in \Delta T^{(n)}$, consider all formulas of the form $\Box\xi$ in $\Phi \setminus t$. Let us divide them into two groups: formulas $\Box\xi \in \Phi\setminus t$ such that $\mathcal{M}^c, w \vDash \Box(\neg\flat \to \xi)$, and the remain ones. We denote by $\Box\psi_1, \dots, \Box\psi_n$ the formulas in the first group and by $\Box\eta_1, \dots, \Box\eta_m$ the formulas in the second group. Using Lemma 4.7, we take leaves $l_1, \dots, l_n$ and stem nodes $t_1, \dots, t_m$ accessible from $w$ such that $\psi_i$ is false at $l_i$, $\eta_j$ is false at $t_j$, and $\Box(\neg\flat \to \eta_j)$ is true at $t_j$ for all $i$ and $j$. We set $\Delta L(t) := \{ l_1, \dots, l_n \}$, $\Delta T(t) := \{ t_1, \dots, t_m \}$, and define
$$
\begin{equation*}
W^{(n+1)} := W^{(n)} \cup \bigcup_{t \in \Delta T^{(n)}} (\Delta L(t) \cup \Delta T(t)), \qquad \Delta T^{(n+1)} := \bigcup_{t \in \Delta T^{(n)}} \Delta T(t).
\end{equation*}
\notag
$$
Let us show that the sequence $W^{(k)}$ stabilizes. For $t \in T^c$, consider the set of formulas $\Xi(t) := \{ \xi \mid \Box\xi \in \Phi \text{ and } \mathcal{M}^c, t \nvDash \Box(\neg\flat \to \xi) \}$. Since the worlds $t_j \in \Delta T(t)$ are accessible from $t$, we have $\Xi(t) \supseteq \Xi(t_j)$ by [Trans$_\flat$]. Moreover, there is a formula $\Box\eta_j \in \Phi$ such that $\Box(\neg\flat \to \eta_j) \in t_j \setminus t$, so the inclusion $\Xi(t) \supset \Xi(t_j)$ is strict. Since $\Phi$ is finite, the maximal cardinality of $\Xi(t)$ for all $t\in\Delta T^{(k)}$ strictly decreases with increasing $k$. Therefore, there is a number $k_0 \in\omega$ such that $\Xi(t) = \varnothing$ for all $t \in \Delta T^{(k_0)}$. In this case, $\Delta T^{(k_0+1)}=\varnothing$. Thus, $W^{(n)} = \bigcup_{k \in \omega} W^{(k)}$ for $n = k_0 + 1$. We set $W := W^{(n)}$. Now define an $\mathrm{N}$-model $\mathcal{M} = (W, \succ, \vartheta)$, $W = T \sqcup L$: the sets of stem and leaf nodes, relation $\succ$ and valuation $\vartheta$ are restrictions to $W$ of the sets $T^c$ and $L^c$, relation $\mathbin{R}^c$ and valuation $\vartheta^c$, respectively. To end the proof, we need to show that $\mathcal{F} = (W, \succ)$ is an $\mathrm{N}$-frame and $\mathcal{M}, w_0 \nvDash \varphi$. (Trans), (TL) and (LL) follow from Lemma 4.6. (Fund). Since the frame is finite, $\prec$ is well-founded if and only if there is no cycle in $(W, \succ)$. Suppose that $w_1, \dots, w_n \in W$ are such that $w_1 \succ w_2 \succ \dots \succ w_n \succ w_1$. If $w_1 \in T$, then by (Trans) $w_1 \succ w_1$, which is impossible, since only irreflexive worlds were taken. If $w_1 \in L$, then by (LL) $w_2 \in T$, which analogously leads us to the contradiction. (EL). Consider the stem node $t \in T$. By [LL-EL$_\flat$], $\mathcal{M}^c, t \nvDash \Box\neg\flat$. Since $\Box\neg\flat \in \Phi$ and $\mathcal{M}^c, t \vDash \Box(\neg\flat \to \neg\flat)$, $\Box\neg\flat \equiv \Box\psi_i$ for some $i$ and the leaf $l_i \in \Delta L(t) \subseteq L$ is accessible from $t$. Now let us check that, for all formulas $\xi \in \Phi$ and worlds $w \in W$,
$$
\begin{equation*}
\mathcal{M}, w \vDash \xi \ \Leftrightarrow \ \mathcal{M}^c, w \vDash \xi
\end{equation*}
\notag
$$
(substituting $\varphi$ for $\xi$ in this equivalence completes the proof).
We argue by induction on the construction of $\xi$. Consider the case $\xi \equiv \Box\zeta$. If $\mathcal{M}^c, w \vDash \Box\zeta$, then we obviously have $\mathcal{M}, w \vDash \Box\zeta$, since $\mathcal{M}$ is a submodel of $\mathcal{M}^c$. Suppose that $\mathcal{M}^c, w \nvDash \Box\zeta$. There are three cases to consider. 1) $w \in T$. By construction, either in $\Delta T(w)$ or in $\Delta L(w)$ there is a world $v$ accessible from $w$ at which $\zeta$ is false. 2) $w \in L$ and $w \neq w_0$. We have $w \in \Delta L(t)$ for some stem node $t \in T$ and $t \succ w$. There is $v \in \mathbin{R}^c(w)$ at which $\zeta$ is false. Now we use Lemma 4.6 several times. By (LL) and (Trans), $v \in T$ and $t \mathbin{R}^c v$, therefore, $\mathcal{M}, t \nvDash \Box(\neg\flat \to \zeta)$. Thus, when we considered the node $t$, we have $\zeta \equiv \eta_j$ for some $j$, so $t_j \in \Delta T(t)$ is such that $t \mathbin{R}^c t_j$ and $\mathcal{M}^c, t_j \nvDash \zeta$. By (TL), $w \mathbin{R}^c t_j$. 3) $w = w_0 \in L$. By construction, there is a world $t_j \in W^{(1)}$ accessible from $w_0$ at which $\zeta$ is false. In all three cases, we found a world $v \in W$ accessible from $w$ such that $\mathcal{M}^c, v \nvDash \zeta$. Thus, by the induction hypothesis, $\mathcal{M}, v \nvDash \zeta$ and $\mathcal{M}, w \nvDash \Box\zeta$. $\Box$ Corollary 4.10. $\mathrm{Nie}_\flat' = \mathrm{Nie}_\flat$, that is, $\mathrm{Nie}_\flat$ is finitely axiomatizable and is given by [Löb$_\flat$], [LL-EL$_\flat$], [TL$_\flat$]. § 5. Provability logics of $\mathrm{NA}$ with respect to $\mathrm{NA}$ and truth arithmeticIn this section, we consider the provability logics of Niebergall arithmetic with respect to all sentences true in the standard model and $\mathrm{NA}$ itself. Recall that, by Proposition 2.1, $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ can be characterized by translation into $\mathrm{GLB}$:
$$
\begin{equation*}
\mathrm{PL}_\mathbb{N}(\mathrm{NA}) = \{ \varphi \in \mathrm{Fm}(\Box) \mid \mathrm{GLB} \vdash S(\varphi^*) \to \varphi^* \}.
\end{equation*}
\notag
$$
Taking into account Theorem 3.6 and the fact that $M(S(\varphi^*) \to \varphi^*) \equiv M(\varphi^*)$, we obtain, for all $\varphi \in \mathrm{Fm}(\Box)$,
$$
\begin{equation*}
\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \varphi \ \Leftrightarrow \ \mathrm{J} \vdash S(\varphi^*) \wedge \boxdot M(\varphi^*) \to \varphi^*.
\end{equation*}
\notag
$$
By Proposition 2.1, we also have, for all $\varphi \in \mathrm{Fm}(\Box)$,
$$
\begin{equation*}
\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash \varphi \ \Leftrightarrow\ \mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \Box\varphi.
\end{equation*}
\notag
$$
5.1. Kripke semantics for truth provability logic of $\mathrm{NA}$Definition. Let $\mathcal{M} = (W, \succ, \vartheta)$, $W = T \sqcup L$ be a fine $\mathrm{N}$-model with root $t_0$, $L_0$ be the set of leaves attached to the root, $\pi_0 := \{ t_0 \} \cup L_0$. Extend the set of the worlds $W$ to $SW$ by adding the “tail” of worlds: Let all stem nodes $t \in T$ be accessible by $\succ$ from new worlds, and for all $n, m \leqslant \omega$, $v \in \pi_0$, and $l \in L_0$. Take the valuation of variables at $(n, v)$ from $v$. We call the resulting model $\mathcal{SM} = (SW, \succ, S\vartheta)$ a tail $\mathrm{N}$-model (the conditions on $\mathrm{N}$-model for $\mathcal{SM}$ are obviously satisfied). An example of a tail $\mathrm{N}$-model is shown in Fig. 5. Original model $\mathcal{M}_3$ is indicated by a brace in the same figure. If the valuation in $\mathcal{M}_3$ is
$$
\begin{equation*}
\vartheta(p) := \{t_0, t_1\},\qquad \vartheta(q) := \{l_2, l_4\},
\end{equation*}
\notag
$$
then it is extended to $\mathcal{SM}_3$ in the following way:
$$
\begin{equation}
S\vartheta(p) = \vartheta(p) \cup \{(n, t_0) \mid n \leqslant \omega\},\qquad S\vartheta(q) = \vartheta(q) \cup \{(n, l_2) \mid n \leqslant \omega\}.
\end{equation}
\tag{4}
$$
We will show that the logic $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ is sound and complete with respect to tail $\mathrm{N}$-models in the following sense: a formula $\varphi \in \mathrm{Fm}(\Box)$ is derivable in $\mathrm{PL}_{\mathbb N}(\mathrm{NA})$ if and only if it is true at the root of every tail $\mathrm{N}$-model. Lemma 5.1 (stabilization). For every formula $\varphi \in \mathrm{Fm}(\Box)$, there exists $n_\varphi \in \omega$ such that in an arbitrary tail $\mathrm{N}$-model $\mathcal{SM}$ for all $n \geqslant n_\varphi$ and all $v \in \pi_0$, Proof. We proceed by induction on the construction of $\varphi$. Consider the case $\varphi \equiv \Box\eta$. Let $n_\varphi = n_\eta + 1$. The right-to-left implication is trivial.
Suppose that $\mathcal{SM}, (n, l) \vDash \Box\eta$ for some $n \geqslant n_\varphi$ and $l \in L_0$. Then $\eta$ is true at all stem nodes $t \in T$ and $(m, t_0)$ with $m < n$. Since $n_\eta < n_\varphi \leqslant n$, $(n_\eta, t_0) \vDash \eta$ and, by the induction hypothesis, $\eta$ is also true at the worlds $(m, t_0)$ for all $m \geqslant n > n_\eta$. Thus, $(\omega, l) \vDash \Box\eta$. Now let $\mathcal{SM}, (n, t_0) \vDash \Box\eta$. Then $\eta$ is true at all stem nodes $t \in T$ and $(m, t_0)$ with $m < n$ and also at leaves $(n, l)$, $l \in L_0$. Similarly, we have $\mathcal{SM}, (m, t_0) \vDash \eta$ for $m \geqslant n$. Moreover, since $n > n_\eta$ and $\eta$ is true at $(n, l)$, by the induction hypothesis, $\mathcal{SM}, (\omega, l) \vDash \eta$. Thus, $(\omega, t_0) \vDash \Box\eta$. $\Box$ Proposition 5.2. For each fine tail $\mathrm{N}$-model $\mathcal{M}$ with root $t_0$, there exists a stratified $\mathrm{J}$-model $\mathcal{S^*M}$ with root $w_0$ such that, for all $\varphi \in \mathrm{Fm}(\Box)$ Proof. Let $\mathcal{M}$ be a fine $\mathrm{N}$-model, $\mathcal{SM}$ be the tail model, constructed from $\mathcal{M}$. Add to the $\mathrm{J}$-model $(\mathcal{SM})^*$ a new world $w_0$ in the plane $\pi((\omega, t_0))$: $S^* W := (SW)^* \sqcup \{ w_0 \}$, $w \mathbin{R_1} v$ for all $v$ in the plane of $(\omega, t_0)$ in $(\mathcal{SM})^*$. Take the valuation of variables at $w_0$ from $(\omega, t_0)$. Denote the resulting $\mathrm{J}$-model by $\mathcal{S^*M}$. Since $(\mathcal{SM})^*$ is its generated submodel, by Proposition 3.7, for all $\varphi \in \mathrm{Fm}(\Box)$ and $w \in SW$,
We claim that, for all $\varphi \in \mathrm{Fm}(\Box)$,
$$
\begin{equation}
\mathcal{S^*M}, w_0 \vDash \varphi^* \ \Leftrightarrow\ \mathcal{S^*M} (\omega, t_0) \vDash \varphi^*.
\end{equation}
\tag{7}
$$
The proof is by induction on the construction of $\varphi$. Consider the case $\varphi \equiv \Box\eta$. The left-to-right implication is trivial. Suppose that $\mathcal{S^*M}, (\omega, t_0) \vDash (\Box\eta)^*$. Then, by (5), $\mathcal{SM}, (\omega, t_0) \vDash \Box\eta$, therefore, $\mathcal{SM}, (n_\eta, t_0) \vDash \eta$. By Lemma 5.1, $\mathcal{SM}, (\omega, t_0) \vDash \eta$ and, by (5) $\mathcal{S^*M}, (\omega, t_0) \vDash \eta^*$, thus $\mathcal{S^*M}, w_0 \vDash (\Box\eta)^*$.
$$
\begin{equation*}
\mathcal{S^*M}, w_0 \vDash \varphi^* \ \Leftrightarrow\ \mathcal{SM}, (\omega, t_0) \vDash \varphi.
\end{equation*}
\notag
$$
Taking into account (6), we only need to check that $\mathcal{S^*M}, w_0 \vDash M(\varphi^*) \wedge S(\varphi^*)$. Recall that subformulas of $\varphi^*$ whose outermost connective is a modality are
$$
\begin{equation*}
\Box_1\psi^*,\quad \Box_0(\Box_1\bot \vee \psi^*),\quad \Box_1\bot\quad \text{for }\ \psi \in \operatorname{Sub}(\varphi).
\end{equation*}
\notag
$$
Therefore, we need to check that the following formulas are true at $w_0$:
$$
\begin{equation*}
\Box_1\psi^* \to \psi^*,\quad \Box_0(\Box_1\bot \vee \psi^*) \to \Box_1(\Box_1\bot \vee \psi^*) \wedge \psi^*\quad \text{for }\ \psi \in \operatorname{Sub}(\varphi)
\end{equation*}
\notag
$$
($\Box_1\bot \to \bot$ is obviously true at $w_0$). If $\mathcal{S^*M}, w_0 \vDash \Box_1\psi^*$, then $\mathcal{S^*M}, (\omega, t_0) \vDash \psi^*$ and, by (7) $\mathcal{S^*M}, w_0 \vDash \psi^*$. Suppose that $\mathcal{S^*M}, w_0 \vDash \Box_0(\Box_1\bot \vee \psi^*)$. Then $\mathcal{S^*M}, (n_\psi, t_0) \vDash \psi^*$ and, by (5), we have $\mathcal{SM}, (n_\psi, t_0) \vDash \psi$. Hence by Lemma 5.1, $\mathcal{SM}, (\omega, t_0) \vDash \psi$, thus, by (5) $\mathcal{S^*M}, (\omega, t_0) \vDash \psi^*$ and, by (7) $\mathcal{S^*M}, w_0 \vDash \psi^*$. Taking into account that all nodes accessible by $\mathbin{R_1}$ from $w_0$ are $(\omega, t_0)$ and leaves, at which $\Box_1\bot$ is true, we obtain $\mathcal{S^*M}, w_0 \vDash \Box_1(\Box_1\bot \vee \psi^*)$. $\Box$ Figure 6 shows the $\mathrm{J}$-model $\mathcal{S^*M}_3$ corresponding to the model $\mathcal{M}_3$ from Fig. 5. The valuation in $\mathcal{S^*M}_3$ is as follows:
$$
\begin{equation*}
S^*\vartheta(p) = S\vartheta(p) \cup \{w_0\},\qquad S^*\vartheta(q) = S\vartheta(q),
\end{equation*}
\notag
$$
where $S\vartheta$ is defined in (4). Theorem 5.3 (soundness). The logic $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ is true at the roots of all $\mathrm{N}$-models. Proof. Suppose that $\mathcal{SM}, (\omega, t_0) \nvDash \varphi$ for some fine $\mathrm{N}$-model $\mathcal{M}$. Then, by Proposition 5.2 $\mathcal{S^*M}, (\omega, t_0) \nvDash \boxdot M(\varphi^*) \wedge S(\varphi^*) \to \varphi^*$, therefore, by Theorem 3.4, we have $\mathrm{J} \nvdash \boxdot M(\varphi^*) \wedge S(\varphi^*) \to \varphi^*$. As noted above, $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \nvdash \varphi$. $\Box$ Proposition 5.4. Let $\mathcal{M}$ be a stratified hereditarily rooted $\mathrm{J}$-model with root $t_0$, the root plane of which is essential. If a formula $\varphi \in \mathrm{Fm}(\Box)$ is such that then $S(\mathcal{M}^\circ), (\omega, t_0) \vDash \varphi$. Proof. Let $\pi_0 := \pi(t_0)$. Extend $\mathcal{M}$ by the planes
Let all planes of $\mathcal{M}$ be accessible from the new planes by $\mathbin{R_0}$ and $\sigma_n \mathbin{R_0} \sigma_m \Leftrightarrow n > m$. We define $\mathbin{R_1}$ and the valuation of variables in the new planes as in $\pi_0$:
$$
\begin{equation*}
(n, v) \mathbin{R_1} (n, u) \ \Leftrightarrow v \ \mathbin{R_1} u, \quad(n, v) \vDash p \ \Leftrightarrow \ v \vDash p.
\end{equation*}
\notag
$$
We denote the resulting model by
$$
\begin{equation*}
\mathcal{SM} := (SW, \mathbin{R_0}, \mathbin{R_1}, \vartheta),\qquad SW := W \sqcup \bigsqcup_{n \leqslant \omega}\sigma_n.
\end{equation*}
\notag
$$
Let us show that, for all $\psi \in \operatorname{Sub}(\varphi^*), n \leqslant \omega$, and $v \in \pi_0$,
$$
\begin{equation*}
\mathcal{SM}, (n, v) \vDash \psi \ \Leftrightarrow\ \mathcal{M}, v \vDash \psi.
\end{equation*}
\notag
$$
The proof is by induction on the construction of $\psi$. Consider the cases $\psi \equiv \Box_0\eta$ and $\psi \equiv \Box_1\eta$.
For $\psi \equiv \Box_0\eta$ the left-to-right implication is obvious. Conversely, if $\mathcal{M}, v \vDash \Box_0\eta$, then $\mathcal{M}, t_0 \vDash \Box_0\eta$, since $v \in \pi(t_0)$. Therefore, by (8), $\mathcal{M}, t_0 \vDash \Box_1\eta \wedge \eta$, that is, $\eta$ is true at all worlds $u \in \pi_0$. By the induction hypothesis,
$$
\begin{equation*}
\forall\, m \leqslant \omega,\ u \in \pi_0\ (\mathcal{SM}, (m, u) \vDash \eta).
\end{equation*}
\notag
$$
Since all worlds $w \in W \setminus \pi_0$ are accessible from $v$ by $\mathbin{R_0}$, $\eta$ is also true at them. Thus, $\mathcal{SM}, (n, v) \vDash \Box_0\eta$.
For $\psi \equiv \Box_1\eta$, the proof is even simpler: for all $n \leqslant \omega$ and $v \in \pi_0$,
$$
\begin{equation*}
\begin{aligned} \, \mathcal{SM}, (n, v) \vDash \Box_1\eta &\ \Leftrightarrow\ \forall\, u \in \mathbin{R_1}(v) (\mathcal{SM}, (n, u) \vDash \eta) \\ &\ \Leftrightarrow\ \forall\, u \in \mathbin{R_1}(v) (\mathcal{M}, u \vDash \eta) \text{ by induction hypothesis} \\ &\ \Leftrightarrow\ \mathcal{M}, v \vDash \Box_1\eta. \end{aligned}
\end{equation*}
\notag
$$
Thus, we have $\mathcal{SM}, (\omega, t_0) \vDash \varphi^*$. Now let us show that $\mathcal{SM} \vDash M(\varphi^*)$. In the worlds $w \in W$, $M(\varphi^*)$ is true by (8). In the new worlds $(n, v)$, $n \leqslant \omega$, $v \in \pi_0$,
$$
\begin{equation*}
\begin{aligned} \, \mathcal{SM}, (n, v) \vDash \Box_0\psi &\ \Rightarrow\ \forall\, u \in \pi_0 (\mathcal{SM}, u \vDash \psi) \\ &\ \Rightarrow\ \forall\, u \in \pi_0 (\mathcal{SM}, (n, u) \vDash \psi) \\ &\ \Rightarrow\ \mathcal{SM}, (n, v) \vDash \Box_1\psi. \end{aligned}
\end{equation*}
\notag
$$
Hence $(\mathcal{SM})^\circ, (\omega, t_0) \vDash \varphi$ by Proposition 3.9. It remains to note that $(\mathcal{SM})^\circ = S(\mathcal{M}^\circ)$, which completes the proof. $\Box$ Figure 7 shows the $\mathrm{J}$-models $\mathcal{M}_4$ and $\mathcal{SM}_4$ (on the left), the $\mathrm{N}$-models $\mathcal{M}_4^\circ$ and $(\mathcal{SM}_4)^\circ \equiv S(\mathcal{M}_4^\circ)$ (on the right). The valuation in $\mathcal{M}_4$ determines the valuations in the remaining models. For example, if the valuation in $\mathcal{M}_4$ is
$$
\begin{equation*}
\vartheta(p) := \{t_0, w_4\},\qquad \vartheta(q) := \{t_2, w_1\},
\end{equation*}
\notag
$$
then valuations in $\mathcal{SM}_4$, $\mathcal{M}_4^\circ$ and $S(\mathcal{M}_4^\circ)$ are, respectively,
$$
\begin{equation*}
\begin{alignedat}{2} S\vartheta(p) &= \vartheta(p) \cup \{(n, t_0) \mid n \leqslant \omega\}, &\qquad S\vartheta(q) &= \vartheta(q) \cup \{(n, w_1) \mid n \leqslant \omega\}, \\ \vartheta^\circ(p) &= \{t_0\}, &\qquad \vartheta^\circ(q) &= \{t_2\}, \\ S\vartheta^\circ(p) &= \vartheta^\circ(p) \cup \{(n, t_0) \mid n \leqslant \omega\}, &\qquad S\vartheta^\circ(q) &= \vartheta^\circ(q). \end{alignedat}
\end{equation*}
\notag
$$
Theorem 5.5 (completeness). If a formula $\varphi\in\mathrm{Fm}(\Box)$ is not derivable in $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$, then there exists a finite fine $\mathrm{N}$-model $\mathcal{M}$ such that $\varphi$ is false at the root of the tail model $\mathcal{SM}$. Proof. If $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \nvdash \varphi$, then $\mathrm{J} \nvdash S(\varphi^*) \wedge \boxdot M(\varphi^*) \to \varphi^*$. By Theorem 3.5 (on completeness of $\mathrm{J}$), there is a finite stratified hereditarily rooted $\mathrm{J}$-model $\mathcal{M}$ with root $t_0$ such that
$$
\begin{equation*}
\mathcal{M}, t_0 \vDash S(\varphi^*) \wedge \boxdot M(\varphi^*) \wedge \neg\varphi^*.
\end{equation*}
\notag
$$
If $\varphi$ does not contain $\Box$, everything is trivial. Otherwise $\Box_1\bot \to \bot$ is one of the implications in $S(\varphi^*)$, therefore, $\mathcal{M}, t_0 \vDash \Diamond_1\top$ and the plane $\pi(t_0)$ is essential. By Proposition 5.4, $S(\mathcal{M}^\circ), (\omega, t_0) \nvDash \varphi$. $\Box$ 5.2. Syntactic description of the truth provability logic of $\mathrm{NA}$Definition. Denote by $\mathrm{Nie}S$ the minimal (not normal) logic containing $\mathrm{Nie}$ and the axiom [S] $\Box(p \vee \Box p) \to p$. For a formula $\varphi \in \mathrm{Fm}(\Box)$, denote Lemma 5.6. Suppose that $\varphi \in \mathrm{Fm}(\Box)$ and $\mathcal{F} = (W, \succ)$ is a fine $\mathrm{N}$-frame with root $t_0$ such that there is only one leaf $l_0$ attached to $t_0$. If $(\mathcal{F}, \vartheta), {l_0} \vDash S(\varphi) \wedge \varphi$ under some valuation $\vartheta$, then the valuation at $t_0$ can be changed to make $S(\varphi) \wedge \varphi$ true at $t_0$. Proof. Let the valuation of variables at $t_0$ be as at $l_0$: Clearly, this does not change truth values of formulas at the worlds other than $t_0$. We denote by $\mathcal{M}'$ the resulting model $(\mathcal{F}, \vartheta')$. By induction on the construction of $\psi \in \operatorname{Sub}\varphi)$, we show that Consider the case $\psi \equiv \Box\eta$. The left-to-right implication is trivial. If $\mathcal{M}', l_0 \vDash \Box\eta$, then $\mathcal{M}', l_0 \vDash \eta$, since $S(\varphi)$ is true at $l_0$, therefore $\mathcal{M}', t_0 \vDash \Box\eta$.
So, $\mathcal{M}', t_0 \vDash \varphi$. To complete the proof we need to verify that $\mathcal{M}', t_0 \vDash S(\varphi)$. Suppose that $\mathcal{M}', t_0 \vDash \Box(\psi \vee \Box\psi)$ for $\Box\psi \in \operatorname{Sub}(\varphi)$. Then either $\psi$ or $\Box\psi$ is true at $l_0$. Since $S(\varphi)$ is true at ${l_0}$, in both cases $\mathcal{M}', l_0 \vDash \psi$, therefore, by the above, $\mathcal{M}', t_0 \vDash \psi$. $\Box$ Lemma 5.7. Suppose that $\varphi \in \mathrm{Fm}(\Box)$ and $\mathcal{M} = (W, \succ, \vartheta)$, $W = T \sqcup L$ is a fine $\mathrm{N}$-model with root $t_0$. If $\mathcal{M}, t_0 \vDash S(\varphi) \wedge \varphi$, then $\mathcal{SM}, (\omega, t_0) \vDash \varphi$. Proof. As before, denote by $L_0$ the set of leaves attached to $t_0$, $\pi_0 := \{ t_0\} \cup L_0$. By induction on the construction of $\psi \in \operatorname{Sub}(\varphi)$, we show that $\forall\, n \leqslant \omega$, $v \in \pi_0$ Consider the case $\psi \equiv \Box\eta$. The left-to-right implication is trivial.
Suppose that $\mathcal{M}, t_0 \vDash \Box\eta$. Since $S(\varphi)$ is true at $t_0$, we have $\mathcal{M}, t_0 \vDash \eta$. Hence $\eta$ is true at all worlds in $T \cup L_0$, and, by the induction hypothesis,
$$
\begin{equation*}
\forall\, m \leqslant \omega \ \ \forall\, u \in \pi_0 (\mathcal{SM}, (m, u) \vDash \eta).
\end{equation*}
\notag
$$
All worlds accessible from $(n, t_0)$ are $t \in T$, $(m, t_0)$ with $m < n$, and $(n, l),$ $l \in L_0$. Thus, $\mathcal{SM}, (n, t_0) \vDash \Box\eta$.
If $\Box\eta$ is true at some ${l_0} \in L_0$, then $\eta$ is true at all $t \in T \setminus \{t_0\}$ and $\Box\eta$ is true at all $l \in L_0$, therefore, $\mathcal{M}, t_0 \vDash \Box(\eta \vee \Box\eta)$. Since $S(\varphi)$ is true at $t_0$, $\mathcal{M}, t_0 \vDash \eta$. By the induction hypothesis, Since all worlds accessible from $(n, l_0)$ are stem nodes, $\mathcal{SM}, (n, l_0) \vDash \Box\eta$. $\Box$Theorem 5.8. For a formula $\varphi \in \mathrm{Fm}(\Box)$, the following conditions are equivalent: 1. $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \varphi$; 2. $\mathrm{Nie} \vdash S(\varphi) \to \varphi$; 3. $\mathrm{Nie}S \vdash \varphi$. Proof. $1 \Rightarrow 2$. Suppose that $\mathrm{Nie} \nvdash S(\varphi) \to \varphi$. By Proposition 3.12, there is a fine $\mathrm{N}$-model $\mathcal{M} = (W, \succ, \vartheta)$, $W = T \sqcup L$ with root $t_0$ such that either $\mathcal{M}, t_0 \vDash S(\varphi) \wedge \neg\varphi$, or there is only one leaf $l_0$ attached to $t_0$ and $\mathcal{M}, l_0 \vDash S(\varphi) \wedge \neg\varphi$. By Lemma 5.6, one can reduce the second case to the first one by changing the valuation at the root of $\mathcal{M}$. By Lemma 5.7, $\mathcal{SM}, (\omega, t_0) \nvDash \varphi$ and, by Theorem 5.3, $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \nvdash \varphi$.
The implication $2 \Rightarrow 3$ is trivial, since $\mathrm{Nie}S$ contains all theorems of $\mathrm{Nie}$, $S(\varphi)$, and is closed under modus ponens. $3 \Rightarrow 1$. In view of Theorem 5.5, it is sufficient to show that $\mathcal{SM}, (\omega, t_0) \vDash \mathrm{Nie}S$ for each fine $\mathrm{N}$-model $\mathcal{M}$ with root $t_0$. We only need to check that $S$ is true, since $\mathrm{Nie}$ is true in all $\mathrm{N}$-models. Suppose that, for a formula $\varphi \in \mathrm{Fm}(\Box)$, $\mathcal{SM}, (\omega, t_0) \vDash \Box(\varphi \vee \Box\varphi)$. Then $\mathcal{SM}, (n_\varphi + 1, t_0) \vDash \varphi \vee \Box\varphi$, therefore, $\varphi$ is true either at $(n_\varphi + 1, t_0)$ or at $(n_\varphi, t_0)$. In both cases, $\mathcal{SM}, (\omega, t_0) \vDash \varphi$ by Lemma 5.1. So, $\mathcal{SM}, (\omega, t_0) \vDash S$. 5.3. The logic of provability of $\mathrm{NA}$ with respect to $\mathrm{NA}$With the known semantics for $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ and the fact that, for all $\varphi \in \mathrm{Fm}(\Box)$,
$$
\begin{equation*}
\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash \varphi \ \Leftrightarrow \ \mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \Box\varphi,
\end{equation*}
\notag
$$
one can easily obtain a semantic description of $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. Theorem 5.9 (soundness). Let $\mathcal{M}$ be a fine $\mathrm{N}$-model with root $t_0$. Then $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ is true at all stem nodes of $\mathcal{M}$, and, for each leaf $l$ attached to $t_0$, $\mathcal{SM}, (\omega, l) \vDash \mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. Proof. Suppose that $\varphi \in \mathrm{Fm}(\Box)$ is derivable in $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. Then $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \Box\varphi$ and, by Theorem 5.3, $\mathcal{SM}, (\omega, t_0) \vDash \Box\varphi$. Therefore, $\mathcal{SM}, (\omega, l) \vDash \varphi$. Moreover, every stem node $t$ of the model $\mathcal{M}$ is accessible from $(\omega, t_0)$ and $\mathcal{M}$ is a generated subframe of $\mathcal{SM}$. Thus, $\mathcal{M}, t \vDash \varphi$. $\Box$ Theorem 5.10 (completeness). Let $\varphi$ be a formula not derivable in $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. Then there exists a finite fine $\mathrm{N}$-model $\mathcal{M}$ with root $t_0$ such that either $\mathcal{M}, t_0 \nvDash \varphi$ or, for some leaf $l$ attached to $t_0$, $\mathcal{SM}, (\omega, l) \nvDash \varphi$. Proof. Suppose that $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \nvdash \varphi$. Then $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \nvdash \Box\varphi$ and, by Theorem 5.5, there is a fine finite $\mathrm{N}$-model $\mathcal{M}$ with root $t_0$ such that $\mathcal{SM}, (\omega, t_0) \nvDash \Box\varphi$. If $\varphi$ is false at some leaf $(\omega, l)$ attached to $(\omega, t_0)$, we are done. Otherwise, $\varphi$ is false at a stem node of $\mathcal{SM}$. It suffices to take the submodel generated by this node. $\Box$ Notice that the semantics can not be limited to only stem nodes: the formula $\Box p \to \Diamond\Box p$ can not be falsified at a stem node of any $\mathrm{N}$-model in view of (EL) and (TL), but it is false at the leaves of a tail model $\mathcal{SM}$ if $\vartheta(p) = T$. The logic $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ is not normal: it contains the consistency formula $\neg\Box\bot$, but does not contain $\Box\neg\Box\bot$. Corollary 5.11. $\mathrm{PL}_{\mathrm{PA}}(\mathrm{NA}) \,{=}\, \mathrm{Nie} \,{\subset}\, \mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \,{\subset}\, \mathrm{Nie}S \,{=}\, \mathrm{PL}_\mathbb{N}(\mathrm{NA})$. Proof. We provide two proofs of this fact.
First of all, these inclusions are obvious from the proof-theoretic point of view: $\mathrm{NA}$ extends $\mathrm{PA}$ and all its theorems are true in the standard model. Thus, if every arithmetical interpretation of $\varphi$ is derivable in $\mathrm{PA}$, then it is derivable in $\mathrm{NA}$, and if it is derivable in $\mathrm{NA}$, then it is true in $\mathbb{N}$. However, now we can obtain the same result without using the arithmetical interpretation. Suppose that $\mathrm{Nie} \vdash \varphi$. By Theorem 3.8, $\varphi$ is valid in all $\mathrm{N}$-frames, in particular, it is true at all stem nodes and leaves attached to the root nodes of all tail models. Thus, by Theorem 5.10, $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash \varphi$. Now suppose that $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash \varphi$. By Theorem 5.9, $\varphi$ is true, particularly, at all stem nodes of $\mathrm{N}$-models, therefore, at the roots of all tail models. Thus $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \varphi$ by Theorem 5.5. Moreover, both inclusions are strict: § 6. Variable free fragmentsIn this section, we consider the variable free fragments of the logics related to the provability in $\mathrm{NA}$: $\mathrm{Nie} = \mathrm{PL}_{\mathrm{PA}}(\mathrm{NA})$, $\mathrm{Nie}_\flat$, and $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$. The variable free fragment of $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ is trivial: since $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \supset \mathrm{Nie}$ and $\mathrm{PL}_\mathbb{N}(\mathrm{NA}) \vdash \Diamond^n \top$ for all $n\in\omega$, every variable free formula in $\mathrm{PL}_\mathbb{N}(\mathrm{NA})$ is equivalent to $\top$ or $\bot$. Consider the $\mathrm{N}$-model $\mathcal{M}^u = (\mathcal{F}^u, \vartheta)$ (see Fig. 8), where $\vartheta(p) = \varnothing$ for each variable $p$ and $\mathcal{F}^u = (W^u, \succ)$, where $W^u = T^u \sqcup L^u$, $T^u = \{(n, 1) \mid n \in \omega\}$, $L^u = \{(n, 0) \mid n \in \omega\}$, and the relation $\succ$ is defined as follows:
$$
\begin{equation*}
\begin{aligned} \, (n, m) \succ (n', 1) &\ \Leftrightarrow\ n > n', \\ (n, m) \succ (n', 0) &\ \Leftrightarrow\ n = n' \wedge m = 1. \end{aligned}
\end{equation*}
\notag
$$
One can easily check that $\mathcal{F}^u$ satisfies the conditions on $\mathrm{N}$-frame. Notice that every world $(n, m) \in W^u$ is uniquely determined by the number $d = 2n + m$. For a variable free formula $\varphi$, we set
$$
\begin{equation*}
D(\varphi) = \{ 2n + m \mid \mathcal{M}^u, (n, m) \vDash \varphi \}.
\end{equation*}
\notag
$$
Proof. From the definition of $\succ$, we have whence, by induction on $k$, we get the required equality. $\Box$ For each of the logics mentioned above, we will prove that every variable free formula is equivalent to the unique normal form and the model $\mathcal{M}^u$ is universal for their variable free fragments in some sense. 6.1. The variable free fragment of $\mathrm{Nie}$For all $n\in\omega$, we call the formulas $\Diamond^n \top$ atomic and the formulas $\bot$, $\Diamond^n \top$, and $\Diamond^n \top \wedge \Box^{n+1}\bot$ elementary conjunctions. Note that, even in the minimal normal logic $K$, we have the following lemma. Lemma 6.2. If a variable free formula $\varphi$ is a boolean combination of atomic formulas, then it is equivalent to a disjunction of some elementary conjunctions. Proof. We bring $\varphi$ to a disjunctive form and reduce all false/true conjunctions. For formulas $\Box^n \bot$, we apply the following equivalence: $\Box$ Proof. We need to derive only two implications: since the remaining ones are derivable in $K$.
The proof is by induction on $n$. Suppose that $n \in \omega$ is even and we have the implications for all $k < n$. It is clear that
$$
\begin{equation*}
K \vdash \Box^{n+1}\bot \to \Box\bigvee_{k < n}(\Diamond^k \top \wedge \Box^{k+1}\bot).
\end{equation*}
\notag
$$
By the induction hypothesis, for even $k < n$,
$$
\begin{equation*}
\mathrm{Nie}' \vdash \Diamond(\Diamond^k \top \wedge \Box^{k+1}\bot) \to \Box^{k+2}\bot,
\end{equation*}
\notag
$$
therefore,
$$
\begin{equation}
\mathrm{Nie}' \vdash \Diamond^n \top \wedge \Box^{n+1}\bot \to \Box\bigvee_{k < n,\, k \not{}\kern2pt\mathrel{\scriptscriptstyle\vdots}\, 2}(\Diamond^k \top \wedge \Box^{k+1}\bot).
\end{equation}
\tag{9}
$$
We set
$$
\begin{equation*}
\varphi := \bigvee_{k < n,\, k \not{}\kern2pt\mathrel{\scriptscriptstyle\vdots}\, 2} (\Diamond^k \top \wedge \Box^{k + 1} \bot).
\end{equation*}
\notag
$$
Notice that, for odd $k < n$,
$$
\begin{equation*}
\begin{aligned} \, K \vdash \Diamond^k \top \wedge \Box^{k+1} \bot & \to \Diamond(\Diamond^{k-1} \top \wedge \Box^k \bot) \\ & \to \neg\Box\varphi. \end{aligned}
\end{equation*}
\notag
$$
Thus, $K \vdash \varphi \to \neg\Box\varphi$. From (9), by normality,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}' \vdash \Diamond(\Diamond^n \top \wedge \Box^{n+1}\bot) &\to \Diamond\Box\varphi \\ & \to \Diamond(\Box\varphi \wedge \neg\Diamond\Box\varphi). \end{aligned}
\end{equation*}
\notag
$$
By [TL], since $K \vdash \varphi \to \Box^n \bot$,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}' \vdash \Diamond(\Diamond^n \top \wedge \Box^{n+1}\bot) & \to \Box(\varphi \vee \Box\varphi) \\ & \to \Box^{n+2}\bot. \end{aligned}
\end{equation*}
\notag
$$
Now consider an odd $n$. By [Löb],
$$
\begin{equation*}
\mathrm{Nie}' \vdash \Box(\Box(\Box^{n-1} \bot \vee \Box^n \bot) \to \Box^{n-1}\bot) \to \Box^n \bot.
\end{equation*}
\notag
$$
By normality, this is equivalent to By the induction hypothesis, $\mathrm{Nie}' \vdash \Diamond(\Diamond^{n-1} \top \wedge \Box^n \bot) \to \Box^{n+1}\bot$, therefore, $\Box$ Theorem 6.4. Each variable free formula $\varphi \in \mathrm{Fm}(\Box)$ is equivalent in $\mathrm{Nie}'$ to a disjunction of elementary conjunctions. Proof. We use an induction on the construction of $\varphi$ replacing subformulas of the form $\Box\psi$ by $\neg\Diamond\neg\psi$. The base case and the step for boolean connectives are given by Lemma 6.2. For $\varphi \equiv \Diamond\psi$, since $\Diamond$ distributes over disjnctions, we can assume, without loss of generality, that $\psi$ is an elementary conjunction. If $\psi \equiv \Diamond^n \top$ or $\psi \equiv \bot$, there is nothing to prove. If $\psi \equiv \Diamond^n \top \wedge \Box^{n+1} \bot$, then $\Diamond\psi$ is equivalent to elementary conjunction by Lemma 6.3. $\Box$ Definition. A normal form is a formula of the form where $N \geqslant 0$, $0 \leqslant k_1 < \dots < k_N$, and $k > k_N + 1$. For $N = 0$, we assume that the empty disjunction is $\bot$ and the condition $k > k_N + 1$ is satisfied. Notice that
$$
\begin{equation*}
\begin{aligned} \, D\biggl(\bigvee_{1 \leqslant j \leqslant N}(\Diamond^{k_j}\top \wedge \Box^{k_j + 1}\bot)\biggr) &= \{ k_1, \dots, k_N\}, \\ D\biggl(\bigvee_{1 \leqslant j \leqslant N}(\Diamond^{k_j}\top \wedge \Box^{k_j + 1}\bot) \vee \Diamond^k \top\biggr) &= \{ k_1, \dots, k_N\} \cup \{ d \mid d \geqslant k \}, \end{aligned}
\end{equation*}
\notag
$$
and, by the constraints, for different normal forms $\varphi$ and $\psi$, we have $D(\varphi) \neq D(\psi)$. Proposition 6.5. Every variable free formula in $\mathrm{Nie}$ and $\mathrm{Nie}'$ is equivalent to the unique normal form. Proof. We have already proved that every variable free formula is equivalent to a disjunction of elementary conjunctions. Now bring it to the normal form. First of all, since $K \vdash \Diamond^k \top \to \Diamond^l \top$ for $l < k$, we can leave only one atomic formula of the form $\Diamond^k \top$ in which $k$ is maximal and exclude disjuncts of the form $\Diamond^m \top \wedge \Box^{m+1} \bot$ with $m > k$. If we order disjuncts $\Diamond^{k_j} \top \wedge \Box^{k_j + 1} \bot$ by increasing of $k_j$, all conditions, except $k > k_N + 1$, will be satisfied. It remains to notice that
Now prove the uniqueness. As noted above, for distinct normal forms $\varphi$ and $\psi$, $D(\varphi) \neq D(\psi)$. Thus, there is a world $w$ such that $\mathcal{M}^u, w \nvDash \varphi \leftrightarrow \psi$. By soundness, $\mathrm{Nie} \nvdash \varphi \leftrightarrow \psi$. $\Box$ Corollary 6.6. The model $\mathcal{M}^u$ is universal for the variable free fragments of $\mathrm{Nie}$ and $\mathrm{Nie}'$, that is, for all variable free formulas $\varphi \in \mathrm{Fm}(\Box)$ Proof. Suppose that $\mathcal{M}^u \vDash \varphi$. We bring $\varphi$ to the normal form $\varphi'$. We have $D(\varphi') = \omega = D(\top)$, therefore, $\varphi' \equiv \top$ and $\mathrm{Nie}' \vdash \varphi$. To complete the proof, we recall that $\mathrm{Nie}'$ is a subset of $\mathrm{Nie}$, and $\mathcal{M}^u$ is an $\mathrm{N}$-model. $\Box$ Corollary 6.7. The variable free fragments of the logics $\mathrm{Nie}$ and $\mathrm{Nie}'$ are the same. 6.2. The variable free fragment of $\mathrm{Nie}_\flat$For all $n\in\omega$, $c \in \{ \flat, \neg\flat \}$, the formulas $\flat$ and $\Diamond^n \top$ are called $\flat$-atomic, and the formulas $\bot$, $\Diamond^n \top \wedge c$, and $\Diamond^n \top \wedge \Box^{n+1} \bot \wedge c$ are called $\flat$-elementary conjunctions. Similarly to Lemma 6.2, one can establish the following result (here we also do not need anything from $\mathrm{Nie}_\flat$, except its normality). Lemma 6.8. If a variable free formula $\varphi \,{\in}\, \mathrm{Fm}(\Box; \flat)$ is a boolean combination of $\flat$-atomic formulas, then it is equivalent to a disjunction of some $\flat$-elementary conjunctions. Consider an auxiliary function $\mathfrak b(n)$ mapping even $n\in\omega$ to $\flat$ and odd $n$ to $\neg\flat$. Proof. We prove by induction on $n$. Suppose that the required statement holds for all $k < n$.
If $n$ is even, then, by the induction hypothesis, $\mathrm{Nie}_\flat \vdash \Diamond^{n-1} \top \wedge \Box^n \bot \to \neg\flat$, therefore, by normality,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}_\flat \vdash \Diamond^n \top \wedge \Box^{n+1} \bot & \to \Diamond(\Diamond^{n-1} \top \wedge \Box^n \bot) \\ & \to \Diamond(\Diamond^{n-1} \top \wedge \neg\flat). \end{aligned}
\end{equation*}
\notag
$$
By [TL$_\flat$], $\mathrm{Nie}_\flat \vdash \Box(\flat \to \neg\Box\Box^{n-1} \bot) \vee \Box(\neg\flat \to \Box^{n-1} \bot)$, hence
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}_\flat \vdash \Diamond^n \top \wedge \Box^{n+1} \bot & \to \Box(\flat \to \Diamond^n \top) \wedge \Box^{n+1} \bot \\ & \to \Box\neg\flat \\ &\to \flat \ \text{ by [LL-EL$_\flat$]}. \end{aligned}
\end{equation*}
\notag
$$
For odd $n$,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}_\flat \vdash \Diamond^n \top \wedge \Box^{n+1} \bot &\to \Diamond(\Diamond^{n-1} \top \wedge \Box^n \bot) \\ &\to \Diamond\flat \text{ by induction hypothesis} \\ & \to \neg\flat \ \text{ by [LL-EL$_\flat$]}. \end{aligned}
\end{equation*}
\notag
$$
Corollary 6.10. For all $n\in\omega$, Let us call the formulas of the form $\bot$, $\Diamond^n \top \wedge \mathfrak b(n)$, and $\Diamond^n \top \wedge \Box^{n+1} \bot$, where $n \in \omega$, reduced $\flat$-elementary conjunctions. Corollary 6.11. Each $\flat$-elementary conjunction is equivalent to some reduced $\flat$-elementary conjunction. Proof. The left-to-right implication is by normality and [LL-EL$_\flat$].
Suppose that $n$ is even. By [LL-EL$_\flat$] $\neg\flat \to \Diamond\flat$, whence, by normality,
$$
\begin{equation*}
\mathrm{Nie}_\flat \vdash \Diamond^{n+1} \top \wedge \neg\flat \to \Diamond(\Diamond^n \top \wedge \flat) \vee \Diamond(\Box^n \bot \wedge \flat).
\end{equation*}
\notag
$$
By Lemma 6.9, $\Diamond^{n-1} \top \wedge \Box^n \bot \to \neg\flat$, therefore,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{Nie}_\flat \vdash \Diamond(\Box^n \bot \wedge \flat) &\to \Diamond(\Box^{n-1} \bot \wedge \flat) \\ & \to \Box (\neg b\to \Box^{n-2}\bot) \ \text{ by [TL$_\flat$]} \\ &\to \Box^2(\neg\flat \to \Box^{n-2}\bot) \ \text{ by [Trans$_\flat$]} \\ &\to \Box(\Box\neg\flat \to \Box^{n-1}\bot) \ \text{ by normality} \\ &\to \Box(\flat \to \Box^{n-1}\bot) \ \text{ by [LL-EL$_\flat$]}. \end{aligned}
\end{equation*}
\notag
$$
From $\Box(\neg\flat \to \Box^{n-2}\bot)$ and $\Box(\flat \to \Box^{n-1}\bot)$ follows $\Box^n \bot$, thus
$$
\begin{equation*}
\mathrm{Nie}_\flat \vdash \Diamond^{n+1} \top \wedge \neg\flat \to \Diamond(\Diamond^n \top \wedge \flat).
\end{equation*}
\notag
$$
If $n$ is odd, then, by Lemma 6.9, $\Diamond^n \top \wedge \Box^{n+1} \bot \to \neg\flat$, and, by Lemma 6.3, $\Box$Theorem 6.13. Every variable free modal formula $\varphi \in \mathrm{Fm}(\Box; \flat)$ is equivalent in $\mathrm{Nie}_\flat$ to a disjunction of reduced $\flat$-elementary conjunctions. Proof. The proof is by induction on the construction of $\varphi$. Similarly to Theorem 6.4, we only need to consider the case $\varphi \equiv \Diamond\psi$, where $\psi$ is a reduced $\flat$-elementary conjunction. For $\psi \equiv \bot$, everything is trivial, for $\psi \equiv \Diamond^n \top \wedge \mathfrak b(n)$, it follows from Lemma 6.12, and, for $\psi \equiv \Diamond^n \top \wedge \Box^{n+1} \bot$, from Lemma 6.3. $\Box$ Definition. A normal form is a formula of the form where $r, s \geqslant 0$, $0 \leqslant k_1 < \dots < k_r$, and $0 \leqslant l_1 < \dots < l_s$; $\rho \equiv \bot$ or has one of the following forms: where $k > k_r + 1$, $l > l_s + 1$. If $r = 0$ ($s = 0$), we suppose that the condition $k > k_r + 1$ ($l > l_s + 1$) is satisfied. From Lemma 6.1, since $\mathcal{M}, w \models \flat\iff w \in L^u$, it is obvious that
$$
\begin{equation*}
\begin{gathered} \, D(\Diamond^k \top \wedge \Box^{k+1} \bot) = \{ k \},\qquad D(\Diamond^{2k} \top \wedge \flat) = \{ 2n \mid n \geqslant k \}, \\ D(\Diamond^{2k+1} \top \wedge \neg\flat) = \{ 2n + 1 \mid n \geqslant k \}. \end{gathered}
\end{equation*}
\notag
$$
Applying this equalities, one can easily construct $D(\varphi)$ for each normal form $\varphi$, and show that $D(\varphi) \neq D(\psi)$ for different normal forms $\varphi$ and $\psi$. The following properties are derived as in Proposition 6.5. Proposition 6.14. Every variable free formula $\varphi\in\mathrm{Fm}(\Box; \flat)$ is equivalent in $\mathrm{Nie}_\flat$ to the unique normal form. Corollary 6.15. The model $\mathcal{M}^u$ is universal for the variable free fragment of $\mathrm{Nie}_\flat$, that is, for each variable free formula $\varphi \in \mathrm{Fm}(\Box; \flat)$, 6.3. The variable free fragment of the provability logic of $\mathrm{NA}$ with respect to $\mathrm{NA}$In general, $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ is a bit more complicated to investigate than the previous two logics, since it is not normal and we cannot replace formulas under $\Box$ by equivalent. However, here we can do it much easier using the facts we know about the variable free fragment of $\mathrm{Nie}$. By Theorem 6.4, every variable free formula in $\mathrm{Nie}$ is equivalent to a disjunction of the formulas of the following forms (they are called elementary conjunctions):
$$
\begin{equation*}
\bot,\quad \Diamond^n \top,\quad \Diamond^n \top \wedge \Box^{n+1}\bot,\qquad n \in \omega.
\end{equation*}
\notag
$$
By Corollary 5.11, the same takes place for $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$, but in it we can simplify formulas even more. By a reduced elementary conjunction we will mean a formula of the form
$$
\begin{equation*}
\bot,\quad \Diamond^{2k+1} \top,\quad \Diamond^{2k+1} \top \wedge \Box^{2k+2}\bot,\qquad k \in \omega.
\end{equation*}
\notag
$$
Proof. It is easy to see that in $\mathrm{N}$-models $\Diamond^{2k}\top \to \Diamond^{2k+1}\top$ is false only at leaf nodes of finite depth. Thus, by Theorem 5.10, we are done. $\Box$ Corollary 6.17. Each variable free formula $\varphi \in \mathrm{Fm}(\Box)$ is equivalent in $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ to a disjunction of reduced elementary conjunctions. Definition. A normal form is a formula which has one of the forms where $N \geqslant 0$, $0 \leqslant k_1 < \dots < k_N$, and $k > k_N + 1$. For $N = 0$, the condition $k > k_N + 1$ is considered to be satisfied. Notice that, for different normal forms $\varphi$ and $\psi$,
$$
\begin{equation*}
D(\varphi) \cap \{ 2 n + 1 \mid n \in \omega \} \neq D(\psi) \cap \{ 2 n + 1 \mid n \in \omega \},
\end{equation*}
\notag
$$
whence, arguing as in Proposition 6.5, we obtain the following result. Proposition 6.18. Every variable free formula in $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ is equivalent to the unique normal form. Corollary 6.19. The model $\mathcal{M}^u$ is universal for the variable free fragment of $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ in the following sense: for a variable free formula $\varphi \in \mathrm{Fm}(\Box)$ § 7. Some other properties of the logics under consideration7.1. $\mathrm{Nie}$ is not equal to $\mathrm{Nie}'$In § 3.5, we considered a finitely axiomatizable logic $\mathrm{Nie}'$, whose class of frames coincides with the frames of $\mathrm{Nie}$. At the same time, we will show that these logics are not equal, therefore, $\mathrm{Nie}'$ is not Kripke complete and we do not know if $\mathrm{Nie}$ is finitely axiomatizable. Moreover, at the moment we do not have even infinite explicit axiomatization for it. It is easy to check that the formula
$$
\begin{equation*}
\varphi \equiv \Diamond(\Diamond^2 p \wedge \Box^3 \neg p \wedge \Box\neg p) \to \Box^4 \neg p
\end{equation*}
\notag
$$
is valid in $\mathrm{Nie}$-frames, therefore, is derivable in $\mathrm{Nie}$. But it is not derivable in $\mathrm{Nie}'$. Consider the model $\mathcal{M} = (W, \mathbin{R}, \vartheta)$, where
$$
\begin{equation*}
\begin{gathered} \, W := \{ (n, m) \mid n \leqslant \omega + 1, m \in \{ 0, 1\} \} \cup \{ (\omega + 1, 2) \},\qquad \vartheta(p) := \{ (\omega, 0) \}, \\ \begin{aligned} \, (n, m) \mathbin{R} (n', 1) &\ \Leftrightarrow\ n > n' \vee n = n' = \omega + 1 \wedge m = 2, \\ (n, m) \mathbin{R} (n', 0) &\ \Leftrightarrow n = n' \wedge m \geqslant 1 \end{aligned} \end{gathered}
\end{equation*}
\notag
$$
and the world $(\omega + 1, 2)$ is not accessible from any world. Clearly, $\mathcal{M}, (\omega + 1, 2) \nvDash \varphi$. Let us prove that all substitutional instances of $\mathrm{Nie}'$ axioms are true in $\mathcal{M}$. Notice that $\mathcal{M}' :=(W', R|_{W'}, \vartheta|_{W'})$, where $W' := W \setminus \{(\omega + 1, 2)\}$, is an $\mathrm{N}$-model, therefore, it is sufficient to check that instances of $\mathrm{Nie}'$ axioms are true at $(\omega + 1, 2)$. [Löb]. Suppose that $\mathcal{M}, (\omega + 1, 2) \vDash \Box(\Box(\varphi \vee \Box\varphi) \to \varphi)$ for some $\varphi \in \mathrm{Fm}(\Box)$. Since $\mathbin{R}((\omega + 1, 2)) = \mathbin{R}((\omega + 1, 1)) \cup \{ (\omega + 1, 1) \}$, the same formula is true at $(\omega + 1, 1)$. We know that [Löb] is true at $(\omega + 1, 1)$, therefore, $\mathcal{M}, (\omega + 1, 1) \vDash \Box\varphi$. Since $\Box(\Box(\varphi \vee \Box\varphi) \to \varphi)$ is true at $(\omega + 1, 2)$, $\mathcal{M}, (\omega + 1, 1) \vDash \varphi$. Thus, $\mathcal{M}, (\omega + 1, 2) \vDash \Box\varphi$. [TL]. Let us show that $\mathcal{M}, (\omega + 1, 2) \vDash \Box(\Box\varphi \to \Diamond\Box\varphi)$ for all $\varphi \in \mathrm{Fm}(\Box)$. It is easy to see that the formula $\Box\varphi \to \Diamond\Box\varphi$ is true in all stem nodes $(n, 1), n \leqslant \omega + 1$. So, we need to verify $\mathcal{M}, (\omega + 1, 0) \vDash \Box\varphi \to \Diamond\Box\varphi$. Suppose that $\mathcal{M}, (\omega + 1, 0) \vDash \Box\varphi$. Notice that the submodel of $\mathcal{M}$ containing only the worlds $(n, m), n < \omega, m \in\{0, 1\}$ is $\mathcal{M}^u$. Let $\varphi'$ be a variable free formula, obtained by substituting $\bot$ for $p$ in $\varphi$. Since $p$ is false in $\mathcal{M}^u$, $\mathcal{M}^u \vDash \varphi \leftrightarrow \varphi'$, therefore $\varphi'$ is true at all worlds $(n, 1), n < \omega$. Variable free formula $\varphi'$ is true at infinitely many worlds of $\mathcal{M}^u$, therefore it is true in cofinite subset of $W^u$, so it is also true at all leaves $(n, 0)$, $N \leqslant n < \omega$, for some $N$. Thus, $\mathcal{M}, (N, 1) \vDash \Box\varphi$ and $\mathcal{M}, (\omega + 1, 0) \vDash \Diamond\Box\varphi$. 7.2. Undefinability of $\flat$ and lack of the Craig interpolation property in $\mathrm{Nie}$In § 4, we have considered a conservative extension of $\mathrm{Nie}$ in the language with an additional propositional constant $\flat$ and obtained an explicit axiomatization for it. It would be natural to define $\flat$ by a formula in the language without constant and rewrite the axioms by substituting this formula for $\flat$. However, this is impossible. Proposition 7.1. There is no formula $\eta \in \mathrm{Fm}(\Box)$ such that $\mathrm{Nie}_\flat \vdash \eta \leftrightarrow \flat$. Proof. Suppose that there is such an $\eta$. We replace by $\bot$ all the variables in $\eta$, and denote by $\eta'$ the resulting formula.
Consider the universal model $\mathcal{M}^u$ of the variable free fragment $\mathrm{Nie}$. It is obvious that $\forall\, w \in W^u (\mathcal{M}^u, w \vDash \eta \Leftrightarrow \mathcal{M}^u, w \vDash \eta')$. The variable free formula $\eta'\in\mathrm{Fm}(\Box)$, which does not contain $\flat$, is true at finite or cofinite set of worlds, but the set of the worlds, where $\flat$ is true, does not have this property. A contradiction. $\Box$ However, $\flat$ can be approximated in some sense from above and from below. For a formula $\varphi$ and a valuation $\vartheta$ on a frame $\mathcal{F}$, we denote by $\vartheta(\varphi)$ the set of all worlds in the model $(\mathcal{F}, \vartheta)$ at which $\varphi$ is true. Consider the formulas $\varphi(p) \equiv \Box(p \wedge \neg\Box p)$ and $\psi(q) \equiv \Box\neg\varphi(q)$. It is easy to show that, for every valuation $\vartheta$ on an arbitrary $\mathrm{N}$-frame $\mathcal{F}$,
$$
\begin{equation}
\vartheta(\varphi(p)) \subseteq \vartheta(\flat) = L \subseteq \vartheta(\psi(q)),
\end{equation}
\tag{10}
$$
and, for the valuation $\vartheta(p) = \vartheta(q) = T$, both inclusions turn into equalities. Proof. From inclusions (10) we know that $\mathrm{Nie} \vdash \varphi(p) \to \psi(q)$. Suppose that there is a variable free formula $\eta \in \mathrm{Fm}(\Box)$ such that $\mathrm{Nie} \vdash \varphi(p) \to \eta$ and $\mathrm{Nie} \vdash \eta \to \psi(q)$. Consider the valuation $\vartheta(p) = \vartheta(q) = T^u$ on $\mathcal{F}^u$. We have which is impossible by the above arguments. $\Box$ In $\mathrm{Nie}_\flat$, there is an interpolant $\flat$ for these formulas, and so we can expect that this logic has the Craig interpolation property. However, verification of this claim is beyond the scope of the present paper. 7.3. Embedding of $\mathrm{GL}$ into $\mathrm{Nie}$ and $\mathrm{PSpace}$-completeness of the logics under considerationDefine the operation of duplicating $\Box$ in formulas $b\colon \mathrm{Fm}(\Box) \to \mathrm{Fm}(\Box)$: $b(\Box\psi) := \Box\Box b(\psi)$, variables, constants, and boolean connectives commute with $b$. Proof. Notice that the following formulas are derivable in $\mathrm{Nie}$: The first formula is in $K$. We prove that the second one is derivable by a semantic argument. Suppose that there is an $\mathrm{N}$-model $\mathcal{M} = (W, \succ, \vartheta)$ such that (12) is false at some world $w \in W$. Hence $\mathcal{M}, w \vDash \Box\Box(\Box\Box p \to p)$ and $\mathcal{M}, w \nvDash \Box\Box p$. Therefore, the set is not empty. By (Fund), there is a $\prec$-minimal world $v \in X$. We have $w \succ^2 v$ and $\mathcal{M}, v \nvDash p$. We will show that $\mathcal{M}, v \vDash \Box\Box p$ (this contradicts the fact that $\Box\Box(\Box\Box p \to p)$ is true at $w$). Suppose the converse: there are $u, v' \in W$ such that $v \succ u \succ v'$ and $\mathcal{M}, v' \nvDash p$. If $u \in T$, then by (Trans) $w \succ u$, therefore, $w \succ^2 v'$ and $v' \in X$, contradicting $v$ being minimal. Otherwise, by (LL) $v \in T$ and $v' \in T$, thus, by (Trans) $w \succ v \succ v'$ and $v' \in X$, which also leads us to a contradiction.
Suppose that $\mathrm{GL} \vdash \varphi$. Consider a derivation $d$ of $\varphi$ in $\mathrm{GL}$. This is a sequence of formulas, of which each is either one of the axioms
$$
\begin{equation*}
\Box(p \to q) \to (\Box p \to \Box q),\qquad \Box(\Box p \to p) \to \Box p,
\end{equation*}
\notag
$$
or the product of applying modus ponens, necessitation, or substitution rule to the previous formulas. We apply $b$ to all formulas in $d$, duplicate applications of the necessitation rule and add the derivation of (11), (12) in $\mathrm{Nie}$ at the beginning of the result proof. One can easily see that the sequence of formulas obtained by this method is a correct proof of the formula $b(\varphi)$ in $\mathrm{Nie}$. Thus, $\mathrm{Nie} \vdash b(\varphi)$ and $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash b(\varphi)$.
Conversely. Suppose that $\mathrm{GL} \nvdash \varphi$. Since $\mathrm{GL}$ is complete with respect to finite irreflexive transitive Kripke frames which are trees, there exists a finite irreflexive transitive tree $\mathcal{F}_0 = (T, \succ)$ with root $t_0$ such that, for some valuation $\vartheta$, $\varphi$ is false at $t_0$ in the model $\mathcal{M}_0 = (T, \succ, \vartheta)$. We extend $\mathcal{M}_0$ to the $\mathrm{N}$-model $\mathcal{M} = (W, \succ, \vartheta)$:
$$
\begin{equation*}
\begin{gathered} \, W := T \sqcup L, \quad \text{where }\ \ L := \{ l_t \mid t \in T \}, \\ w \succ l_t \ \Leftrightarrow\ w = t,\qquad l_t \succ w \ \Leftrightarrow\ w \in T \wedge t \succ w, \\ \mathcal{M}, l_t \vDash p \ \Leftrightarrow\ \mathcal{M}_0, t \vDash p \end{gathered}
\end{equation*}
\notag
$$
for all $w \in W$, $t \in T$, $p \in \mathrm{PVar}$.
Let us show that, for every formula $\varphi \in \mathrm{Fm}(\Box)$ and stem node $t \in T$,
$$
\begin{equation*}
\mathcal{M}_0, t \vDash \varphi \ \Leftrightarrow\ \mathcal{M}, t \vDash b(\varphi) \ \Leftrightarrow\ \mathcal{M}, l_t \vDash b(\varphi).
\end{equation*}
\notag
$$
The proof is by induction on the construction of $\varphi$. Consider the case $\varphi \equiv \Box\psi$. If $\mathcal{M}_0, t \nvDash \Box\psi$, then there is a stem node $t'$ accessible from $t$ such that $\mathcal{M}_0, t' \nvDash \psi$. By the induction hypothesis, $\mathcal{M}, l_{t'} \nvDash b(\psi)$. Since $t \succ t' \succ l_{t'}$ and $l_t \succ t' \succ l_{t'}$, $\mathcal{M}, t \nvDash \Box\Box b(\psi)$ and $\mathcal{M}, l_t \nvDash \Box\Box b(\psi)$. Conversely, if $\Box\Box b(\psi)$ is false in $\mathcal{M}$ at $t$ or $l_t$, then there is a stem node $t'$ accessible from $t$ such that $b(\psi)$ is false in $\mathcal{M}$ at $t'$ or $l_{t'}$. By the induction hypothesis, $\mathcal{M}_0, t' \nvDash \psi$, therefore, $\mathcal{M}_0, t \nvDash \Box\psi$.
Thus, $\mathcal{M}, t \nvDash b(\varphi)$. By Theorem 5.10, $b(\varphi)$ is not derivable neither in $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ nor in $\mathrm{Nie}$. $\Box$ Proposition 7.4. The derivability problem for logics $\mathrm{Nie}$, $\mathrm{Nie}S$, $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ and $\mathrm{Nie}_\flat$ is PSpace-complete. Proof. These problems are in $\mathrm{PSpace}$, since by ${}^*$ they can be reduced to derivability problem in $\mathrm{GLB}$ for corresponding bimodal formulas and the last problem is in $\mathrm{PSpace}$ [19]. At the same time, the derivability problem for $\mathrm{GL}$ is $\mathrm{PSpace}$-hard (see [17], Theorem 18.29) and can be reduced by Lemma 7.3 to derivability problem for $\mathrm{Nie}$ and $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$, therefore, the last two problems are $\mathrm{PSpace}$-hard. Moreover, derivability problem for $\mathrm{Nie}$ is trivially reducable to $\mathrm{Nie}_\flat$ and $\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA})$ to $\mathrm{Nie}S$ ($\mathrm{PL}_{\mathrm{NA}}(\mathrm{NA}) \vdash \varphi \Leftrightarrow \mathrm{Nie}S \vdash \Box\varphi$). Thus, these two problems are also $\mathrm{PSpace}$-hard. $\Box$ The author is grateful to his scientific advisor L. D. Beklemishev for assistance in research and useful comments on the manuscript.
Citation in format AMSBIB
\Bibitem{Dvo24} |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|