Reflection calculus and conservativity spectra

TL;DR

This paper extends the Reflection Calculus with new modalities representing fragments of arithmetical theories, explores their formal properties, and connects them to proof-theoretic ordinals, providing a decidable and complete logical framework.

Contribution

It introduces RC$^ abla$, an extension of Reflection Calculus, with new modalities for arithmetical fragments, and establishes its properties and connections to proof-theoretic ordinals.

Findings

RC$^ abla$ can express reflection principles up to any ordinal less than ε₀.

The variable-free fragment of RC$^ abla$ is decidable and complete with respect to its semantics.

Normal forms of RC$^ abla$ relate to collections of proof-theoretic ordinals for arithmetical theories.

Abstract

Strictly positive logics recently attracted attention both in the description logic and in the provability logic communities for their combination of efficiency and sufficient expressivity. The language of Reflection Calculus RC consists of implications between formulas built up from propositional variables and constant `true' using only conjunction and diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles. We extend the language of RC by another series of modalities representing the operators associating with a given arithmetical theory T its fragment axiomatized by all theorems of T of arithmetical complexity $\Pi^0_n$, for all n>0. We note that such operators, in a precise sense, cannot be represented in the full language of modal logic. We formulate a formal system RC$^\nabla$ extending RC that is sound and, as we conjecture, complete under this interpretation. We show that in this system one is able to express iterations of reflection principles up to any ordinal $<\epsilon_0$. On the other hand, we provide normal forms for its variable-free fragment. Thereby, the variable-free fragment is shown to be decidable and complete w.r.t. its natural arithmetical semantics. Whereas the normal forms for the variable-free formulas of RC correspond in a unique way to ordinals below $\epsilon_0$, the normal forms of RC$^\nabla$ are more general. It turns out that they are related in a canonical way to the collections of proof-theoretic ordinals of (bounded) arithmetical theories for each complexity level $\Pi^0_{n+1}$. Finally, we present an algebraic universal model for the variable-free fragment of RC$^\nabla$ based on Ignatiev's Kripke frame. Our main theorem states the isomorphism of several natural representations of this algebra.

Equations

$$\mathrm{EA}⊢\forall x({\square }_{\tau }(x)\to {\square }_{\sigma }(x)).$$

$$\sigma {\wedge }_{\mathrm{EA}}\tau$$

$$\sigma {\vee }_{\mathrm{EA}}\tau$$

$$\exists y,p⩽x({\mathrm{Prf}}_{\sigma }(y,p)\wedge y\in {\Pi }_n^0\wedge x=\text{disj}(y,┌\bar{p}\ne \bar{p}┐))$$

$$\forall x({\square }_{{\mathrm{\Pi }}_n(\sigma )}(x)\leftrightarrow \exists \pi \in {\Pi }_n^0({\square }_{\sigma }(\pi )\wedge {\square }_{\mathrm{EA}}(\pi \to x)).$$

$$({\overline{\mathfrak{G}}}_T,{\wedge }_T,1_T,\{{\mathrm{R}}_n,{\mathrm{\Pi }}_{n+1}:n<\omega \})$$

$$A::=p\mid \top \mid (A\wedge A)\mid aA,\text{where a∈Σ.}$$

$${◊}_n{◊}_{m}A⊢{◊}_{m}A,{◊}_m{◊}_{n}A⊢{◊}_{m}A,\text{for each m⩽n.}$$

$${◊}_n(A\wedge {◊}_{m}B){=}_{\mathrm{RC}}{◊}_{n}A\wedge {◊}_{m}B.$$

$$A{<}_{n}B\stackrel{\text{def}}{⟺}B{⊢}_{\mathrm{RC}}{◊}_{n}A.$$

$$A{=}_{\mathrm{RC}}B⟺o_n(A)=o_n(B).$$

$$o(A)={\omega }^{o(A_n^{-})}+\cdots +{\omega }^{o(A_1^{-})}.$$

$${\nabla }_{n}A\wedge {\nabla }_{m}B⊢{\nabla }_n(A\wedge {\nabla }_{m}B).$$

$${◊}_{1}A\wedge {\nabla }_{0}B⊢{◊}_1(A\wedge {\nabla }_{0}B)$$

$$A={◊}_n{A}_1\wedge \cdots \wedge {◊}_n{A}_k\wedge {\nabla }_n{B}_1\wedge \dots {\nabla }_n{B}_l\wedge D,$$

$$V\wedge {\nabla }_n{B}_1{◊}_n{B}_2=V\wedge {\nabla }_n(V\wedge {◊}_n{B}_2)=V\wedge {◊}_n{B}_2=V{◊}_n{B}_2.$$

$$B^{\prime }⊢{◊}_{n+1}V\wedge {\nabla }_n{B}^{\prime }⊢{\nabla }_{n+1}V\wedge {\nabla }_n{B}^{\prime }={\nabla }_{n+1}(V\wedge {\nabla }_n{B}^{\prime }).$$

$${\nabla }_n(V\wedge {\nabla }_n{B}^{\prime })⊢{\nabla }_n{\nabla }_n{B}^{\prime }⊢{\nabla }_n{B}^{\prime }.$$

$${\nabla }_n{B}^{\prime }={\nabla }_n(B_1\wedge {◊}_n{B}_2)⊢{\nabla }_n{◊}_n{B}_2={◊}_n{B}_2,$$

$$V\wedge {◊}_n{B}_2=V\wedge {◊}_{n+1}{B}_1\wedge {◊}_n{B}_2=V\wedge {◊}_{n+1}(B_1\wedge {◊}_n{B}_2)=V\wedge {◊}_{n+1}{B}^{\prime }⊢V\wedge {\nabla }_n{B}^{\prime }.$$

$${\nabla }_n{A}_n\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k},$$

$${\nabla }_i{B}_i\wedge {\nabla }_i{C}_i={\nabla }_i{A}_i.$$

$$\begin{gathered} {\nabla }_{i}B={\nabla }_i({\nabla }_n{B}_n\wedge {\nabla }_{n+1}{B}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{B}_{n+k})= \\ ={\nabla }_n{B}_n\wedge \cdots \wedge {\nabla }_{i-1}{B}_{i-1}\wedge {\nabla }_i({\nabla }_i{B}_i\wedge \cdots \wedge {\nabla }_{n+k}{B}_{n+k})= \\ ={\nabla }_n{B}_n\wedge \cdots \wedge {\nabla }_{i-1}{B}_{i-1}\wedge {\nabla }_i{B}_i^{\prime }, \end{gathered}$$

$$\begin{gathered} {◊}_{i}B={◊}_i({\nabla }_n{B}_n\wedge {\nabla }_{n+1}{B}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{B}_{n+k})= \\ ={◊}_n{B}_n\wedge \cdots \wedge {◊}_{i-1}{B}_{i-1}\wedge {◊}_i({\nabla }_i{B}_i\wedge \cdots \wedge {\nabla }_{n+k}{B}_{n+k})= \\ ={\nabla }_n{◊}_n{B}_n\wedge \cdots \wedge {\nabla }_{i-1}{◊}_{i-1}{B}_{i-1}\wedge {\nabla }_i{◊}_i{B}_i^{\prime }, \end{gathered}$$

$$C:={◊}_n{A}_n\wedge \cdots \wedge {◊}_{i-1}{A}_{i-1}\wedge \overline{B_i}.$$

$$C$$

$${\nabla }_i{A}_i\wedge \overline{A_{i+1}}⊬{\nabla }_i{B}_i\wedge \overline{B_{i+1}}.$$

$${\nabla }_i{A}_i⊢{\nabla }_i({\nabla }_i{A}_i\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k}).$$

$$\begin{gathered} {\nabla }_n{A}_n\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k}= \\ ={\nabla }_n({\nabla }_n{A}_n\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k})\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k}= \\ ={\nabla }_n{A}_n^{\prime }\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k}, \end{gathered}$$

$$\begin{gathered} {\nabla }_n{A}_n^{\prime }⊢{\nabla }_n({\nabla }_n{A}_n\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k})⊢ \\ ⊢{\nabla }_n({\nabla }_n{A}_n^{\prime }\wedge {\nabla }_{n+1}{A}_{n+1}\wedge \cdots \wedge {\nabla }_{n+k}{A}_{n+k}), \end{gathered}$$

$$B|A:=A_i{◊}_0\dots {◊}_0{A}_n,$$

Full text

We extend the language of $\mathrm{RC}$ by another series of modalities representing the operators associating with a given arithmetical theory $T$ its fragment axiomatized by all theorems of $T$ of arithmetical complexity $\Pi^{0}_{n}$, for all $n>0$. We note that such operators, in a strong sense, cannot be represented in the full language of modal logic.

We formulate a formal system ${\mathrm{RC}^{\nabla}}$ extending $\mathrm{RC}$ that is sound and, as we conjecture, complete under this interpretation. We show that in this system one is able to express iterations of reflection principles up to any ordinal $<\varepsilon_{0}$. Secondly, we provide normal forms for its variable-free fragment. Thereby, this fragment is shown to be algorithmically decidable and complete w.r.t. its natural arithmetical semantics.

In the last part of the paper we characterize in several natural ways the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$ and its dual Kripke structure. Most importantly, the elements of this algebra correspond to the sequences of proof-theoretic $\Pi^{0}_{n+1}$-ordinals of bounded fragments of Peano arithmetic called conservativity spectra, as well as to the points of the well-known Ignatiev Kripke model.

1 Introduction

A system, called Reflection Calculus and denoted $\mathrm{RC}$, was introduced in [9] and, in a slightly different format, in [19]. From the point of view of modal logic, $\mathrm{RC}$ can be seen as a fragment of Japaridze’s polymodal provability logic $\mathrm{GLP}$ [35, 17] consisting of the implications of the form $A\to B$, where $A$ and $B$ are formulas built-up from $\top$ and propositional variables using just $\land$ and the diamond modalities. We call such formulas $A$ and $B$ strictly positive.

Strictly positive modal logics, earlier and in a different guise, appeared in the work on description logic. They serve as a good compromise between the concerns of efficiency and sufficient expressivity in the knowledge base query answering. In particular, the strictly positive language corresponds to the OWL2EL profile of the OWL web ontology language, and is used in large ontology bases such as SNOMED CT. The papers [37, 38] undertake a general study of strictly positive logics and provide more references, especially in the description logic and in the universal algebraic traditions.

Our concerns in the development of strictly positive provability logic are, in a sense, similar. Reflection calculus $\mathrm{RC}$ is much simpler than its modal companion $\mathrm{GLP}$ yet expressive enough for its main proof-theoretic applications. It has been outlined in [9] that $\mathrm{RC}$ allows to define a natural system of ordinal notations up to $\varepsilon_{0}$ and serves as a convenient basis for a proof-theoretic analysis of Peano Arithmetic in the style of [6, 7]. This includes a consistency proof for Peano arithmetic based on transfinite induction up to $\varepsilon_{0}$, a characterization of its $\Pi_{n}^{0}$-consequences in terms of iterated reflection principles, a slowly terminating term rewriting system [2] and a combinatorial independence result [8].

An axiomatization of $\mathrm{RC}$ (as an equational calculus) has been found by Evgeny Dashkov in his paper [19] which initiated the study of strictly positive provability logics. Dashkov proved two important further facts about $\mathrm{RC}$ which sharply contrast with the corresponding properties of $\mathrm{GLP}$. Firstly, $\mathrm{RC}$ is complete with respect to a natural class of finite Kripke frames. Secondly, $\mathrm{RC}$ is decidable in polynomial time, whereas most of the standard modal logics are PSpace-complete and the same holds for the variable-free fragment of GLP [40].

Another advantage of going to a strictly positive language is exploited in the present paper. Strictly positive modal formulas allow for more general arithmetical interpretations than those of the standard modal logic language. In particular, propositional formulas can now be interpreted as arithmetical theories rather than individual sentences. (Notice that the ‘negation’ of a theory would not be well-defined.) As the first meaningful example for this framework we analysed an extension of $\mathrm{RC}$ by a modality representing the full arithmetical uniform reflection principle [10]. The corresponding strictly positive logic, though arithmetically complete, complete w.r.t. a nice class of finite Kripke models and polytime decidable, turned out not to be equivalent to the fragment of any standard normal modal logic.111This has not been noted in [10], however it follows from Theorem 3 of [14] saying that a s.p. logic is a fragment of a normal modal logic iff it is Kripke frame complete. Modulo some reformulations this result is, in fact, equivalent to Theorem 1 of [37].

More generally, any monotone operator acting on the semilattice of arithmetical theories can be considered as a modality in strictly positive logic. One such operation is particularly attractive from the point of view of proof-theoretic applications, namely the map associating with a theory $T$ its fragment $\mathrm{\Pi}_{n+1}(T)$ axiomatized by all theorems of $T$ of arithmetical complexity $\Pi^{0}_{n+1}$. Since the $\Pi^{0}_{n+1}$-conservativity relation of $T$ over $S$ can be expressed by $S\vdash\mathrm{\Pi}_{n+1}(T)$, we call such operators $\Pi^{0}_{n+1}$-conservativity operators.

This relates our study to the fruitful tradition of research on conservativity and interpretability logics, see e.g. [45, 46, 21, 25, 26, 27, 32]. Our framework happens to be both weaker and stronger than the traditional one: in our system we are able to express the conservativity relations for each class $\Pi^{0}_{n+1}$ and are able to relate not only sentences but theories. However, in this framework the negation is lacking and the conservativity is not a binary modality and cannot be iterated. Yet, we believe that the strictly positive language is both simpler and better tuned to the needs of proof-theoretic analysis of formal systems of arithmetic.

We introduce the system ${\mathrm{RC}^{\nabla}}$ with modalities $\Diamond_{n}$ representing uniform reflection principles of arithmetical complexity $\Sigma_{n}$, and $\nabla_{n}$ representing $\Pi_{n+1}$-conservativity operators. We provide an adequate semantics of ${\mathrm{RC}^{\nabla}}$ in terms of the semilattice $\mathfrak{G}_{\mathrm{EA}}$ of (numerated) arithmetical r.e. theories extending elementary arithmetic $\mathrm{EA}$. Further, we introduce transfinite iterations of monotone semi-idempotent operators along elementary well-orderings, somewhat generalizing the notion of a Turing–Feferman recursive progression of axiomatic systems but mainly following the same development as in [8]. Our first result shows that $\alpha$-iterations of modalities $\Diamond_{n}$, for each $n<\omega$ and ordinals $\alpha<\varepsilon_{0}$, are expressible in the algebra $\mathfrak{G}_{\mathrm{EA}}$. A variable-free strictly positive logic where such iterations are explicitly present in the language has been introduced by Hermo Reyes and Joosten [30] which is, thereby, contained in ${\mathrm{RC}^{\nabla}}$. However, possible generalisations of their system to larger ordinal notation systems would be out of scope of ${\mathrm{RC}^{\nabla}}$.222In the latest version of their paper Hermo Reyes and Joosten did, in fact, exted their setup to arbitrary ordinal notation systems.

Then we turn to a purely syntactic study of the variable-free fragment of the system ${\mathrm{RC}^{\nabla}}$ and provide unique normal forms for its formulas. A corollary is that the variable-free fragment of ${\mathrm{RC}^{\nabla}}$ is decidable and arithmetically complete.

Whereas the normal forms for the variable-free formulas of $\mathrm{RC}$ correspond in a unique way to ordinals below $\varepsilon_{0}$, the normal forms of ${\mathrm{RC}^{\nabla}}$ are more general. It turns out that they are related in a canonical way to the collections of proof-theoretic ordinals of (bounded) arithmetical theories for each complexity level $\Pi_{n+1}$, as defined in [8].

Studying the collections of proof-theoretic ordinals corresponding to several levels of logical complexity as single objects seems to be a rather recent and interesting development. Such collections appeared for the first time in the work of Joost Joosten [36] under the name Turing–Taylor expansions. He established a one-to-one correspondence between such collections (for a certain class of theories) and the points of the Ignatiev universal model for the variable-free fragment of $\mathrm{GLP}$. We call such collections conservativity spectra of arithmetical theories. Our results show that ${\mathrm{RC}^{\nabla}}$ provides a way to syntactically represent and conveniently handle such conservativity spectra.

The third part of our paper provides an algebraic model $\mathfrak{I}$ for the variable-free fragment of ${\mathrm{RC}^{\nabla}}$. This model is obtained in a canonical way on the basis of the Ignatiev model. Our main theorem states the isomorphism of several representations of $\mathfrak{I}$: the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$; a constructive representation in terms of sequences of ordinals below $\varepsilon_{0}$; a representation in terms of the semilattice of bounded $\mathrm{RC}$-theories and as the algebra of cones of the Ignatiev model. In Section 10 we consider its dual relational structure $\mathfrak{I}^{*}$, which is universal for the variable-free fragment of ${\mathrm{RC}^{\nabla}}$. We give a constructive characterization of this large Kripke frame in terms of sequences of ordinals.

Parts of this paper previously appeared in conference proceedings [13, 15] though underwent a thorough revision here. Thanks are due to Albert Visser for suggesting many improvements including Lemma 2.2, as well as to Ilya Shapirovsky, Joost Joosten, and Evgeny Kolmakov for comments and corrections.

2 The lattice of arithmetical theories

We define the intended arithmetical interpretation of the strictly positive modal language. Propositional variables (and strictly positive formulas) will now denote possibly infinite theories rather than individual sentences. We deal with r.e. theories formulated in the language of elementary arithmetic $\mathrm{EA}$ and containing the axioms of $\mathrm{EA}$. The theory $\mathrm{EA}$, aka $I\Delta_{0}(\exp)$ or EFA, is formulated in the language of Peano arithemtic enriched by a symbol for exponentiation ($2^{x}$). In addition to the standard quantifier-free defining axioms for all the symbols of the language, it contains the induction schema for bounded formulas (cf [28, 7]). Bounded formulas in the language of $\mathrm{EA}$ are called elementary formulas, the class of all such formulas is usually denoted $\Delta_{0}(\exp)$.

To avoid well-known problems with the representation of theories in arithmetic, we assume that each theory $S$ comes equipped with an elementary numeration, that is, a bounded formula $\sigma(x)$ in the language of $\mathrm{EA}$ defining the set of axioms of $S$ in the standard model of arithmetic $\mathbb{N}$.

Given such a $\sigma$, we have a standard arithmetical $\Sigma^{0}_{1}$-formula $\Box_{\sigma}(x)$ expressing the provability of $x$ in $S$ (see [22]). We often write $\Box_{\sigma}\varphi$ for $\Box_{\sigma}(\ulcorner\varphi\urcorner)$. The expression $\bar{n}$ denotes the numeral ${0^{\prime}}^{\ldots}{{}^{\prime}}$ ($n$ times). If $\varphi(v)$ contains a parameter $v$, then $\Box_{\sigma}\varphi(\bar{x})$ denotes a formula (with a parameter $x$) expressing the provability of the sentence $\varphi(\bar{x}/v)$ in $S$.

Given two numerations $\sigma$ and $\tau$, we write $\sigma\leqslant_{\mathrm{EA}}\tau$ if

[TABLE]

We will only consider the numerations $\sigma$ such that $\sigma\leqslant_{\mathrm{EA}}\sigma_{\mathrm{EA}},$ where $\sigma_{\mathrm{EA}}$ is some standard numeration of $\mathrm{EA}$. We call such numerated theories Gödelian extensions of $\mathrm{EA}$.

The relation $\leqslant_{\mathrm{EA}}$ defines a natural preorder on the set $\mathfrak{G}_{\mathrm{EA}}$ of Gödelian extensions of $\mathrm{EA}$. Let $\overline{\mathfrak{G}}_{\mathrm{EA}}$ denote the quotient by the associated equivalence relation $=_{\mathrm{EA}}$, where by definition $\sigma=_{\mathrm{EA}}\tau$ iff both $\sigma\leqslant_{\mathrm{EA}}\tau$ and $\tau\leqslant_{\mathrm{EA}}\sigma$. $\overline{\mathfrak{G}}_{\mathrm{EA}}$ is a lattice with $\land_{\mathrm{EA}}$ corresponding to the union of theories and $\lor_{\mathrm{EA}}$ to their intersection. These operations are defined on elementary numerations as follows:

[TABLE]

where $\text{disj}(x_{1},x_{2})$ is an elementary term computing the Gödel number of the disjunction of formulas given by Gödel numbers $x_{1}$ and $x_{2}$.

We will only be concerned with the operation $\land_{\mathrm{EA}}$, that is, with the structure of lower semilattice with top $(\overline{\mathfrak{G}}_{\mathrm{EA}},\land_{\mathrm{EA}},1_{\mathrm{EA}})$. Notice that the top element $1_{\mathrm{EA}}$ corresponds to (the equivalence class of) $\mathrm{EA}$, whereas the bottom $0_{\mathrm{EA}}$ is the class of all inconsistent extensions of $\mathrm{EA}$.

An operator $R:\mathfrak{G}_{\mathrm{EA}}\to\mathfrak{G}_{\mathrm{EA}}$ is called extensional if $\sigma=_{\mathrm{EA}}\tau$ implies $R(\sigma)=_{\mathrm{EA}}R(\tau)$. Similarly, $R$ is called monotone if $\sigma\leqslant_{\mathrm{EA}}\tau$ implies $R(\sigma)\leqslant_{\mathrm{EA}}R(\tau)$. Clearly, each monotone operator is extensional and each extensional operator correctly acts on the quotient lattice $\overline{\mathfrak{G}}_{\mathrm{EA}}$. An operator $R$ is called semi-idempotent if $R(R(\sigma))\leqslant_{\mathrm{EA}}R(\sigma)$. $R$ is a closure operator if it is monotone, semi-idempotent and, in addition, $\sigma\leqslant_{\mathrm{EA}}R(\sigma)$. Operators considered in this paper will usually be at least monotone and semi-idempotent.

Meaningful monotone operators abound in arithmetic. Typical examples are the uniform $\Sigma_{n}$-reflection principles $\mathrm{R}_{n}(\sigma)$ associating with $\sigma$ the extension of $\mathrm{EA}$ by the schema $\{\forall x\>(\Box_{\sigma}\varphi(\bar{x})\to\varphi(x)):\varphi\in\mathrm{\Pi}_{n+1}\}$ taken with its natural elementary numeration that we denote $x\in\mathrm{R}_{n}(\sigma)$. It is known that the theory $\mathrm{R}_{n}(\sigma)$ is finitely axiomatizable. Moreover, $\mathrm{R}_{0}(\sigma)$ is equivalent to Gödel’s consistency assertion $\mathrm{Con}(\sigma)$ for $\sigma$. The following basic lemma will be useful later.

Let $S$ be a Gödelian extension of $\mathrm{EA}$ numerated by $\sigma$, and let $x\in\Pi^{0}_{n}$ denote an elementary formula expressing that $x$ is the Gödel number of a $\Pi^{0}_{n}$-sentence.

Lemma 2.1

1. $\mathrm{(i)}$

If $S$ extends $\mathrm{EA}$ by $\Pi^{0}_{n+1}$-axioms, then $\mathrm{R}_{n}(\sigma)$ contains $S$. 2. $\mathrm{(ii)}$

If $\mathrm{EA}\vdash\forall x\>(\sigma(x)\to x\in\mathrm{\Pi}^{0}_{n+1})$ then $\mathrm{R}_{n}(\sigma)\leqslant_{\mathrm{EA}}\sigma$.

Proof. The second claim is a straightforward formalization of the first one. To prove Claim (i) assume $S\vdash\varphi$. Then there is a $\pi\in\mathrm{\Pi}^{0}_{n+1}$ such that $\mathrm{EA}\vdash\pi\to\varphi$ and $S\vdash\pi$. We have $\mathrm{EA}\vdash\Box_{\sigma}\pi$ by $\Sigma_{1}$-completeness. Then $\mathrm{R}_{n}(\sigma)\vdash\pi\vdash\varphi$. $\Box$

In this paper we will study another series of monotone operators. Given a theory $S$ numerated by $\sigma$, let $\mathrm{\Pi}_{n}(S)$ denote the extension of $\mathrm{EA}$ by all theorems of $S$ of complexity $\Pi^{0}_{n}$. The set $\mathrm{\Pi}_{n}(S)$ is r.e. but in general not elementary recursive. In order to comply with our definitions we apply a form of Craig’s trick that yields an elementary axiomatization of $\mathrm{\Pi}_{n}(S)$.333Over $\mathrm{EA}+\mathrm{B\Sigma}_{1}$ one can work with a natural r.e. axiomatization of $\mathrm{\Pi}_{n}(S)$. Let $\mathrm{\Pi}_{n}(\sigma)$ denote the elementary formula

[TABLE]

and the theory numerated by this formula over $\mathrm{EA}$. Here, $\mathrm{Prf}_{\sigma}(y,p)$ is an elementary formula expressing that $p$ is the Gödel number of a proof of $y$, so that $\exists p\>\mathrm{Prf}_{\sigma}(y,p)$ is $\Box_{\sigma}(y)$. Then it is easy to see that the theory $\mathrm{\Pi}_{n}(\sigma)$ is (externally) deductively equivalent to $\mathrm{\Pi}_{n}(S)$.

We will implicitly rely on the following characterization.

Lemma 2.2

It is provable in $\mathrm{EA}$ that

[TABLE]

Proof. The implication from right to left is easy, we sketch a proof of $(\to)$. Reason within $\mathrm{EA}$. Suppose $p$ is a $\mathrm{\Pi}_{n}(\sigma)$-proof of $x$. It is a $\mathrm{EA}$-proof of $x$ from some assumptions $\pi^{\prime}_{1},\pi^{\prime}_{2},\dots,\pi^{\prime}_{k}$ such that each $\pi^{\prime}_{i}$ has the form $\pi_{i}\lor\overline{p_{i}}\neq\overline{p_{i}}$ where $\pi_{i}\in\Pi^{0}_{n}$ and $\mathrm{Prf}_{\sigma}(\pi_{i},p_{i})$. Since $p$ contains witnesses for all the proofs $p_{i}$, from $p$ one can construct in an elementary way a sentence $\pi\in\Pi^{0}_{n}$ equivalent to $\pi_{1}\land\dots\land\pi_{k}$ together with its $\sigma$-proof and an $\mathrm{EA}$-proof of $\pi\to x$, using a formalization of the deduction theorem in $\mathrm{EA}$. A verification that it is, indeed, the required proof goes by an elementary induction on the length of $p$. $\Box$

Using Lemma 2.2 one can naturally infer that all the operators $\mathrm{R}_{n}$ and $\mathrm{\Pi}_{n}$ are monotone and semi-idempotent, moreover $\mathrm{\Pi}_{n}$ is a closure. It is easy to see that $\mathrm{EA}$ can be replaced in all the previous considerations by any of its Gödelian extensions $T$. The main source of interest for us in this paper will be the structure of semilattice with operators

[TABLE]

and its subsemilattice with operators $\overline{\mathfrak{G}}^{0}_{T}$ generated by $1_{T}$. We call the former the ${\mathrm{RC}^{\nabla}}$-algebra of Gödelian extensions of $T$. The term ${\mathrm{RC}^{\nabla}}$-algebra will be explained below.

3 Strictly positive logics and reflection calculi

We refer the reader to a note [14] for a short introduction to strictly positive logic sufficient for the present paper and to [38] for more information from the general algebraic perspective. For a general background on modal logic and provability logic we refer to the books [18, 43, 17].

3.1 Normal strictly positive logics

Consider a modal language ${\mathcal{L}}_{\Sigma}$ with propositional variables $p,q$,…, a constant $\top$, conjunction $\land$, and a possibly infinite set of symbols $\Sigma=\{a_{i}:i\in J\}$ understood as diamond modalities. The family $\Sigma$ is called the signature of the language ${\mathcal{L}}_{\Sigma}$. Strictly positive formulas (or simply formulas) are built up by the grammar:

[TABLE]

Sequents are expressions of the form $A\vdash B$ where $A,B$ are strictly positive formulas.

Basic sequent-style system, denoted $\mathrm{K}^{+}$, is given by the following axioms and rules:

$A\vdash A;\quad A\vdash\top;\quad$ if $A\vdash B$ and $B\vdash C$ then $A\vdash C$; 2. 2.

$A\land B\vdash A;\quad A\land B\vdash B;\quad$ if $A\vdash B$ and $A\vdash C$ then $A\vdash B\land C$; 3. 3.

if $A\vdash B$ then $aA\vdash aB$, for each $a\in\Sigma$.

It is well-known that $\mathrm{K}^{+}$ axiomatizes the strictly positive fragment of a polymodal version of basic modal logic K (cf [14, 38]). All our systems will also contain the following principle corresponding to the transitivity axiom in modal logic:

$aaA\vdash aA$.

The extension of $\mathrm{K}^{+}$ by this axiom will be denoted $\mathrm{K4}^{+}$ [19].

Let $C[A/p]$ denote the result of replacing in $C$ all occurrences of a variable $p$ by $A$. A set of sequents $L$ is called a normal strictly positive logic if it contains the axioms and is closed under the rules of $\mathrm{K}^{+}$ and under the following substitution rule: if $(A\vdash B)\in L$ then $(A[C/p]\vdash B[C/p])\in L$. We will only consider normal strictly positive logics below. We write $A\vdash_{L}B$ for the statement that $A\vdash B$ is provable in $L$ (or belongs to $L$). $A=_{L}B$ means $A\vdash_{L}B$ and $B\vdash_{L}A$.

Any normal strictly positive logic $L$ satisfies the following simple positive replacement lemma that we leave without proof.

Lemma 3.1

Suppose $A\vdash_{L}B$, then $C[A/p]\vdash_{L}C[B/p]$, for any formula $C$.

3.2 Algebraic semantics

Algebraic semantics for normal strictly positive logics is given by semilattices with monotone operators (SLOs), that is, structures of the form $\mathfrak{M}=(M;\land^{\mathfrak{M}},1^{\mathfrak{M}},\{a^{\mathfrak{M}}:a\in\Sigma\})$ where $(M,\land^{\mathfrak{M}},1^{\mathfrak{M}})$ is a semilattice with top and each $a^{\mathfrak{M}}:M\to M$ is a monotone operator on $\mathfrak{M}$: $x\leqslant y$ implies $a^{\mathfrak{M}}(x)\leqslant a^{\mathfrak{M}}(y)$, for all $x,y\in M$. Every strictly positive formula $A$ of ${\mathcal{L}}_{\Sigma}$ represents a term $A^{\mathfrak{M}}$ of $\mathfrak{M}$. We say that $A\vdash B$ holds in $\mathfrak{M}$ (or $\mathfrak{M}$ satisfies $A\vdash B$) if $\mathfrak{M}\vDash\forall\vec{x}\>A^{\mathfrak{M}}(\vec{x})\leqslant B^{\mathfrak{M}}(\vec{x})$. It is easy to see that $A\vdash_{\mathrm{K}^{+}}B$ if and only if $A\vdash B$ holds in each SLO $\mathfrak{M}$. The SLOs satisfying all the theorems of a normal s.p. logic $L$ are called $L$-algebras.

Given a normal s.p. logic $L$ in a signature $\Sigma$ and an alphabet of variables $V$, its Lindenbaum–Tarski algebra is a SLO $\mathfrak{L}_{L}^{V}$ whose domain consists of the equivalence classes of formulas of the language of $L$ modulo $=_{L}$. Let $[A]_{L}$ denote the equivalence class of $A$. The operations are defined in a standard way as follows: $[A]_{L}\land^{\mathfrak{L}}[B]_{L}:=[A\land B]_{L}$, $a^{\mathfrak{L}}([A]_{L}):=[aA]_{L}$, for each $a\in\Sigma$. It is well-known that $A\vdash_{L}B$ iff $A\vdash B$ holds in $\mathfrak{L}_{L}^{V}$. Hence, any normal s.p. logic $L$ is complete w.r.t. its algebraic semantics, that is, w.r.t. the class of all $L$-algebras.

The algebra $\mathfrak{L}_{L}^{V}$ is also called the free $V$-generated $L$-algebra. In this paper we will be particularly interested in the algebras $\mathfrak{L}_{L}^{V}$ where $V$ is empty. In this case we denote the algebra $\mathfrak{L}_{L}^{V}$ by $\mathfrak{L}_{L}^{0}$.

3.3 The system $\mathrm{RC}$

Reflection calculus $\mathrm{RC}$ is a normal strictly positive logic formulated in the signature $\{\Diamond_{n}:n\in\omega\}$. It is obtained by adjoining to the axioms and rules of $\mathrm{K4}^{+}$ (stated for each $\Diamond_{n}$) the following principles:

$\Diamond_{n}A\vdash\Diamond_{m}A$, for all $n>m$; 2. 6.

$\Diamond_{n}A\land\Diamond_{m}B\vdash\Diamond_{n}(A\land\Diamond_{m}B)$, for all $n>m$.

We notice that $\mathrm{RC}$ proves the following polytransitivity principles:

[TABLE]

Also, the converse of Axiom 6 is provable in $\mathrm{RC}$, so that in fact we have

[TABLE]

The system $\mathrm{RC}$ was introduced in an equational logic format by Dashkov [19], the present formulation is from [9]. Dashkov showed that $\mathrm{RC}$ axiomatizes the set of all sequents $A\vdash B$ such that the implication $A\to B$ is provable in the polymodal logic GLP. Moreover, unlike GLP itself, $\mathrm{RC}$ is polytime decidable (whereas GLP is PSpace-complete [42]) and enjoys the finite frame property (whereas GLP is Kripke incomplete).

We recall a correspondence between variable-free $\mathrm{RC}$-formulas and ordinals [6]. Let $\mathbb{F}$ denote the set of all variable-free $\mathrm{RC}$-formulas, and let $\mathbb{F}_{n}$ denote its restriction to the signature $\{\Diamond_{i}:i\geqslant n\}$, so that $\mathbb{F}=\mathbb{F}_{0}$. For each $n\in\omega$ we define binary relations $<_{n}$ on $\mathbb{F}$ by

[TABLE]

Obviously, $<_{n}$ is a transitive relation invariantly defined on the equivalence classes w.r.t. provable equivalence in $\mathrm{RC}$ (denoted $=_{\mathrm{RC}}$). Since $\mathrm{RC}$ is polytime decidable, so are both $=_{\mathrm{RC}}$ and all of $<_{n}$.

An $\mathrm{RC}$-formula without variables and $\land$ is called a word (or a worm in some treatments). In fact, any such formula syntactically is a finite sequence of letters $\Diamond_{i}$ (followed by $\top$). If $A,B$ are words then $AB$ will denote $A[\top/B]$, that is, the word corresponding to the concatenation of these sequences. $A\circeq B$ denotes the graphical identity of formulas (words).

The set of all words will be denoted $\mathbb{W}$, and $\mathbb{W}_{n}$ will denote its restriction to the signature $\{\Diamond_{i}:i\geqslant n\}$. The following facts are from [6, 9]:

• •

Every $A\in\mathbb{F}_{n}$ is $\mathrm{RC}$-equivalent to a word in $\mathbb{W}_{n}$;

• •

$(\mathbb{W}_{n}/{=_{\mathrm{RC}}},<_{n})$ is isomorphic to $(\varepsilon_{0},<)$.

Here, $\varepsilon_{0}$ is the first ordinal $\alpha$ such that $\omega^{\alpha}=\alpha$. Thus, the set $\mathbb{W}_{n}/{=}_{\mathrm{RC}}$ is well-ordered by the relation $<_{n}$. The isomorphism can be established by an onto and order preserving function $o_{n}:\mathbb{W}_{n}\to\varepsilon_{0}$ such that, for all $A,B\in\mathbb{W}_{n}$,

[TABLE]

Then $o_{n}(A)$ is the order type of $\{B\in\mathbb{W}_{n}:B<_{n}A\}/{=_{\mathrm{RC}}}$.

The function $o(A):=o_{0}(A)$ can be inductively calculated as follows: If $A\circeq\Diamond_{0}^{k}\top$ then $o(A)=k$. If $A\circeq A_{1}\Diamond_{0}A_{2}\Diamond_{0}\cdots\Diamond_{0}A_{n}$, where all $A_{i}\in\mathbb{W}_{1}$ and not all of them are empty, then

[TABLE]

Here, $B^{-}$ is obtained from $B\in\mathbb{W}_{1}$ replacing every $\Diamond_{m+1}$ by $\Diamond_{m}$. For $n>0$ and $A\in\mathbb{W}_{n}$ we let $o_{n}(A)=o_{n-1}(A^{-})$.

3.4 The system ${\mathrm{RC}^{\nabla}}$

Definition 1

The signature of $\mathrm{RC}^{\nabla}$ consists of modalities $\Diamond_{n}$ and $\nabla_{n}$, for each $n<\omega$. The system $\mathrm{RC}^{\nabla}$ is a normal strictly positive logic given by the following axioms and rules, for all $m,n<\omega$:

$\mathrm{RC}$ for $\Diamond_{n}$; $\mathrm{RC}$ for $\nabla_{n}$; 2. 2.

$A\vdash\nabla_{n}A$; 3. 3.

$\Diamond_{n}A\vdash\nabla_{n}A$; 4. 4.

$\Diamond_{m}\nabla_{n}A\vdash\Diamond_{m}A$  if $m\leqslant n$; 5. 5.

$\nabla_{n}\Diamond_{m}A\vdash\Diamond_{m}A$  if $m\leqslant n$.

As a basic syntactic fact about ${\mathrm{RC}^{\nabla}}$ we mention the following useful lemma. For brevity, we often write $=$ for $=_{\mathrm{RC}^{\nabla}}$ and $\vdash$ for $\vdash_{\mathrm{RC}^{\nabla}}$.

Lemma 3.2

The following are theorems of $\mathrm{RC}^{\nabla}$, for all $m<n$:

1. $\mathrm{(i)}$

$\Diamond_{n}(A\land\nabla_{m}B)=\Diamond_{n}A\land\Diamond_{m}B$; 2. $\mathrm{(ii)}$

$\nabla_{n}(A\land\Diamond_{m}B)=\nabla_{n}A\land\Diamond_{m}B$.

Proof. (i) Part $(\,\vdash\,)$ follows from $\Diamond_{n}\nabla_{m}B\vdash\Diamond_{m}B$. Part $(\,\dashv\,)$ follows from $\Diamond_{n}A\land\Diamond_{m}B\vdash\Diamond_{n}(A\land\Diamond_{m}B)\vdash\Diamond_{n}(A\land\nabla_{m}B)$ using positive replacement.

(ii) Part $(\,\vdash\,)$ follows from $\nabla_{n}\Diamond_{m}B\vdash\Diamond_{m}B$. Part $(\,\dashv\,)$ follows from $\nabla_{n}A\land\Diamond_{m}B\vdash\nabla_{n}A\land\nabla_{m}\Diamond_{m}B\vdash\nabla_{n}(A\land\nabla_{m}\Diamond_{m}B)\vdash\nabla_{n}(A\land\Diamond_{m}B)$ using Axiom 6 for $\nabla$ modalities, the fact that $\Diamond_{m}B=\nabla_{m}\Diamond_{m}B$ and positive replacement. $\Box$

A formula $A$ is called ordered if no modality with a smaller index $i$ (be it $\Diamond_{i}$ or $\nabla_{i}$) occurs in $A$ within the scope of a modality with a larger index $j>i$.

Lemma 3.3

Every formula $A$ of ${\mathrm{RC}^{\nabla}}$ is equivalent to an ordered one.

Proof. Apply equation (1) of $\mathrm{RC}$ for $\Diamond$ and for $\nabla$ modalities, and the identities of Lemma 3.2 from left to right, until the rules are not applicable to any of the subformulas of $A$. $\Box$

The intended arithmetical interpretation of ${\mathrm{RC}^{\nabla}}$ maps strictly positive formulas to Gödelian theories in $\mathfrak{G}_{T}$ in such a way that $\top$ corresponds to $T$, $\land$ corresponds to the union of theories, $\Diamond_{n}$ corresponds to $\mathrm{R}_{n}$ and $\nabla_{n}$ corresponds to $\mathrm{\Pi}_{n+1}$, for each $n\in\omega$.

Definition 2

An arithmetical interpretation in $\mathfrak{G}_{T}$ is a map $*$ from strictly positive modal formulas to $\mathfrak{G}_{T}$ satisfying the following conditions for all $n\in\omega$:

• •

$\top^{*}=T$;  $(A\land B)^{*}=(A^{*}\land_{T}B^{*})$;

• •

$(\Diamond_{n}A)^{*}=\mathrm{R}_{n}(A^{*})$;  $(\nabla_{n}A)^{*}=\mathrm{\Pi}_{n+1}(A^{*})$.

The following result shows, as expected, that every theorem of ${\mathrm{RC}^{\nabla}}$ represents an identity of the structure $(\overline{\mathfrak{G}}_{T},\land_{T},1_{T},\{\mathrm{R}_{n},\mathrm{\Pi}_{n+1}:n<\omega\})$.

Theorem 1

For any formulas $A,B$ of $\mathrm{RC}^{\nabla}$, if $A\vdash_{{\mathrm{RC}^{\nabla}}}B$ then $A^{*}\leqslant_{T}B^{*}$, for all arithmetical interpretations $*$ in $\mathfrak{G}_{T}$.

Proof. A proof of Theorem 1 is routine by induction on the length of the derivation. For the axioms and rules of $\mathrm{RC}$ for the $\Diamond$-fragment the claim has been carefully verified in [10]. The RC-axioms for the $\nabla$-fragment are obvious except for Axiom 6, that is, the principle

[TABLE]

Consider any arithmetical interpretation $*$, and let $S=A^{*}$ and $U=B^{*}$ be the corresponding Gödelian theories (with the associated numerations $\sigma$ and $\tau$, respectively). We rely on Lemma 2.2. The principle (2) is the formalization in $\mathrm{EA}$ of the following assertion: For any sentence $\pi\in\Pi^{0}_{n+1}$, if $S\cup\mathrm{\Pi}_{m+1}(U)\vdash\pi$ then $\mathrm{\Pi}_{n+1}(S)\cup\mathrm{\Pi}_{m+1}(U)\vdash\pi$. Reasoning in $\mathrm{EA}$, consider a sentence $\varphi\in\mathrm{\Pi}_{m+1}(U)$ such that $S,\varphi\vdash\pi$. Then $S\vdash\varphi\to\pi$ and, since $\varphi\to\pi$ is logically equivalent to a $\Pi^{0}_{n+1}$-sentence, conclude $\mathrm{\Pi}_{n+1}(S)\vdash\varphi\to\pi$. Thus, $\mathrm{\Pi}_{n+1}(S)\cup\mathrm{\Pi}_{m+1}(U)\vdash\pi$.

Concerning the remaining axioms of ${\mathrm{RC}^{\nabla}}$ we remark that Axiom 2 holds since the theory $\mathrm{\Pi}_{n+1}(S)$ is (provably) contained in $S$. Axiom 3 is Lemma 2.1 (ii).

Axiom 4: Assume $\mathrm{R}_{m}(\mathrm{\Pi}_{n+1}(\sigma))$. In order to prove $\mathrm{R}_{m}(\sigma)$ let $\varphi\in\mathrm{\Pi}_{m+1}$ and $\Box_{\sigma}\varphi$. Then clearly $\Box_{\mathrm{\Pi}_{n+1}(\sigma)}\varphi$, since $m\leqslant n$, and hence $\varphi$, by $\mathrm{R}_{m}(\mathrm{\Pi}_{n+1}(\sigma))$.

Axiom 5 formalizes the fact that $\mathrm{R}_{m}(\sigma)$ is an extension of $T$ by a $\Pi_{m+1}$-sentence. $\Box$

Theorem 1, together with Gödel’s second incompleteness theorem, has as its corollary the following property of the logic ${\mathrm{RC}^{\nabla}}$.

Corollary 3.4

For all ${\mathrm{RC}^{\nabla}}$ formulas $A$, $A\nvdash_{{\mathrm{RC}^{\nabla}}}\Diamond_{n}A$.

Proof. Assume otherwise, then interpreting ${\mathrm{RC}^{\nabla}}$ in $\mathfrak{G}_{\mathrm{EA}}$ yields $A^{*}\leqslant_{\mathrm{EA}}\mathrm{R}_{n}(A^{*})$ by Theorem 1. Hence, by Gödel’s theorem the theory $A^{*}$ is inconsistent. This contradicts the soundness of $\mathrm{EA}$. $\Box$

A similar fact is known for $\mathrm{GLP}$ and can also be proved by purely modal logic means [16, 1]. An elementary argument for $\mathrm{RC}$ is given in Appendix A. David Fernández-Duque gives another proof for a generalization of $\mathrm{RC}$ with transfinitely many modalities. We will make use of Corollary 3.4 (for $\mathrm{RC}$) in the normal form theorems below. Whereas a reference to the given proof of Corollary 3.4 presupposes at least the soundness of $\mathrm{EA}$, the elementary Kripke model argument for $\mathrm{RC}$ is formalizable in $\mathrm{EA}$.

Conjecture 1

${\mathrm{RC}^{\nabla}}$* is arithmetically complete, that is, the converse of Theorem 1 also holds, provided $T$ is arihmetically sound.*

3.5 Kripke incompleteness of $\mathrm{RC}^{\nabla}$

Kripke frames and models are understood in this paper in the usual sense. A Kripke frame ${\mathcal{W}}$ for the language of $\mathrm{RC}^{\nabla}$ consists of a non-empty set $W$ equipped with a family of binary relations $\{R_{n},S_{n}:n\in\omega\}$.

A Kripke model is a Kripke frame ${\mathcal{W}}$ together with a valuation $v:W\times\mathrm{Var}\to\{0,1\}$ assigning a truth value to each propositional variable at every node of ${\mathcal{W}}$. As usual, we write ${\mathcal{W}},x\Vdash A$ to denote that a formula $A$ is true at a node $x$ of a model ${\mathcal{W}}$. This relation is inductively defined as follows:

• •

${\mathcal{W}},x\Vdash p\iff v(x,p)=1$, for each $p\in\mathrm{Var}$;

• •

${\mathcal{W}},x\Vdash\top$;  ${\mathcal{W}},x\Vdash A\land B\iff({\mathcal{W}},x\Vdash A\text{ and }{\mathcal{W}},x\Vdash B)$;

• •

${\mathcal{W}},x\Vdash\Diamond_{n}A\iff\exists y\>(xR_{n}y\text{ and }{\mathcal{W}},y\Vdash A)$;

• •

${\mathcal{W}},x\Vdash\nabla_{n}A\iff\exists y\>(xS_{n}y\text{ and }{\mathcal{W}},y\Vdash A)$.

A formula $A$ is valid in a Kripke frame ${\mathcal{W}}$ if ${\mathcal{W}},x\Vdash A$, for each $x\in W$ and each valuation $v$ on ${\mathcal{W}}$. The following lemma is standard and easy.

Lemma 3.5

A Kripke frame ${\mathcal{W}}$ validates all theorems of ${\mathrm{RC}^{\nabla}}$ iff the following conditions hold, for all $m,n<\omega$:

1. $\mathrm{(i)}$

$R_{n}$* is transitive; $R_{n}\subseteq R_{m}$ if $m<n$; $R_{n}^{-1}R_{m}\subseteq R_{m}$ if $m<n$;* 2. $\mathrm{(ii)}$

$S_{n}$* is transitive, reflexive; $S_{n}\subseteq S_{m}$ if $m<n$; $S_{n}^{-1}S_{m}\subseteq S_{m}$ if $m<n$;* 3. $\mathrm{(iii)}$

$R_{n}\subseteq S_{n}$; $S_{n}R_{m}\subseteq R_{m}$, $R_{m}S_{n}\subseteq R_{m}$ if $m\leqslant n$.

By the following proposition ${\mathrm{RC}^{\nabla}}$ turns out to be incomplete w.r.t. its Kripke frames.

Proposition 3.6

The sequent

[TABLE]

is valid in every Kripke frame satisfying ${\mathrm{RC}^{\nabla}}$. However, it is unprovable in ${\mathrm{RC}^{\nabla}}$ (and arithmetically invalid).

Proof. Firstly, it is easy to see that conditions $R_{1}\subseteq S_{1}$ and $S_{1}^{-1}S_{0}\subseteq S_{0}$ imply $R_{1}^{-1}S_{0}\subseteq S_{0}$. Therefore, $(*)$ holds in each Kripke frame of ${\mathrm{RC}^{\nabla}}$.

Secondly, take $\top$ for $A$ and $\Diamond_{1}\top$ for $B$. The left hand side is ${\mathrm{RC}^{\nabla}}$-equivalent to $\Diamond_{1}\top$. The right hand side is equivalent to $\Diamond_{1}(\top\land\nabla_{0}\Diamond_{1}\top)=_{\mathrm{RC}^{\nabla}}\Diamond_{1}\top\land\Diamond_{0}\Diamond_{1}\top$, by Lemma 3.2(i). By Corollary 3.4, $\Diamond_{1}\top\nvdash_{{\mathrm{RC}^{\nabla}}}\Diamond_{0}\Diamond_{1}\top$. Hence, $(*)$ is unprovable in ${\mathrm{RC}^{\nabla}}$. $\Box$

By Theorem 3 of [14], a normal strictly positive logic is a fragment of some normal modal logic if and only if it is Kripke complete. Hence, we obtain

Corollary 3.7

${\mathrm{RC}^{\nabla}}$* is not a strictly positive fragment of any normal modal logic.*

4 The variable-free fragment of ${\mathrm{RC}^{\nabla}}$

Let $\mathbb{F}_{n}^{\nabla}$ denote the set of all variable-free strictly positive formulas in the language of ${\mathrm{RC}^{\nabla}}$ with the modalities $\{\Diamond_{i},\nabla_{i}:i\geqslant n\}$ only, and let $\mathbb{F}^{\nabla}$ denote $\mathbb{F}_{0}^{\nabla}$. We abbreviate $F\vdash_{{\mathrm{RC}^{\nabla}}}\nabla_{n}G$ by $F\vdash_{n}G$ and $\nabla_{n}F=_{\mathrm{RC}^{\nabla}}\nabla_{n}G$ by $F\equiv_{n}G$. First, we are going to establish a crucial result that every formula in $\mathbb{F}_{n}^{\nabla}$ is equivalent to a word in $\mathbb{W}_{n}$ modulo $\equiv_{n}$. From this fact we will infer a weak normal form theorem for the variable-free fragment of ${\mathrm{RC}^{\nabla}}$. Second, we will obtain two different unique normal form theorems for the variable-free fragment by sharpening the weak normal forms.

4.1 Weak normal forms

We begin with a few auxiliary lemmas.

Lemma 4.1

1. $\mathrm{(i)}$

If $A\vdash_{n}B$ and $m<n$, then $A\land\Diamond_{m}C\vdash_{n}B\land\Diamond_{m}C$; 2. $\mathrm{(ii)}$

If $A\vdash_{n}B$ and $B\vdash\nabla_{n}C$, then $A\vdash\nabla_{n}C$; 3. $\mathrm{(iii)}$

If $A\vdash_{n}B$ and $B\vdash\Diamond_{n}C$, then $A\vdash\Diamond_{n}C$.

Proof. (i) $A\land\Diamond_{m}C\vdash\nabla_{n}B\land\Diamond_{m}C\vdash\nabla_{n}(B\land\Diamond_{m}C)$.

(ii) $A\vdash\nabla_{n}B\vdash\nabla_{n}\nabla_{n}C\vdash\nabla_{n}C$;

(iii) $A\vdash\nabla_{n}B\vdash\nabla_{n}\Diamond_{n}C\vdash\Diamond_{n}C$. $\Box$

Lemma 4.2

1. $\mathrm{(i)}$

$\Diamond_{i}A\land B=\nabla_{i}(\Diamond_{i}A\land B)\land B$; 2. $\mathrm{(ii)}$

$\nabla_{i}A\land B=\nabla_{i}(\nabla_{i}A\land B)\land B$.

Proof. In both (i) and (ii) the implication $(\vdash)$ follows from the axiom $C\vdash\nabla_{i}C$. For $(\dashv)$ we obtain $\nabla_{i}(\Diamond_{i}A\land B)\vdash\nabla_{i}\Diamond_{i}A=\Diamond_{i}A$ for (i) and simlarly $\nabla_{i}(\nabla_{i}A\land B)\vdash\nabla_{i}\nabla_{i}A=\nabla_{i}A$ for (ii). $\Box$

Lemma 4.3

The set of all formulas $\{\Diamond_{n}F,\nabla_{n}G:F,G\in\mathbb{W}_{n}\}$ is linearly ordered by $\vdash_{\mathrm{RC}^{\nabla}}$.

Proof. For any $F,G\in\mathbb{W}_{n}$ we know that either $F\vdash_{\mathrm{RC}}\Diamond_{n}G$ or $G\vdash_{\mathrm{RC}}\Diamond_{n}F$ or $F=_{\mathrm{RC}}G$. In the first case we obtain provably in ${\mathrm{RC}^{\nabla}}$: $\Diamond_{n}F\vdash\nabla_{n}F\vdash\Diamond_{n}G\vdash\nabla_{n}G$. The second case is symmetrical. In the third case we obtain $\Diamond_{n}F=\Diamond_{n}G\vdash\nabla_{n}F=\nabla_{n}G$. $\Box$

Theorem 2

For each $A\in\mathbb{F}_{n}^{\nabla}$ there is a word $W\in\mathbb{W}_{n}$ such that $A\equiv_{n}W$.

Proof. By Lemma 3.3 it is sufficient to prove the theorem for ordered formulas $A$. The proof goes by induction on the length of ordered $A$. We can also assume that the minimal modality occurring in $A$ is $\Diamond_{n}$ or $\nabla_{n}$. (Otherwise, prove it for the minimum $m>n$ and infer $A\equiv_{n}W$ from $A\equiv_{m}W$.) The basis of induction is trivial, we consider the induction step.

Assume that the induction hypothesis holds for all formulas shorter than $A$. Since $A$ is ordered, $A$ can be written in the form

[TABLE]

where $D\in\mathbb{F}_{n+1}^{\nabla}$ and $A_{i},B_{j}\in\mathbb{F}_{n}^{\nabla}$. Since $\Diamond_{n}$ or $\nabla_{n}$ must occur in $A$, we know that $D$ and each $A_{i},B_{j}$ are strictly shorter than $A$. By the induction hypothesis and Lemma 4.3 we can delete from the conjunction all but one members of the form $\Diamond_{n}A_{i}$, $\nabla_{n}B_{j}$. Thus, $A=D\land\Diamond_{n}A^{\prime}$ or $A=D\land\nabla_{n}B^{\prime}$, for some words $A^{\prime},B^{\prime}\in\mathbb{W}_{n}$.

Now we apply the induction hypothesis to $D$ and obtain a word $V\in\mathbb{W}_{n+1}$ such that $V\equiv_{n+1}D$. It follows that $D\land\Diamond_{n}A^{\prime}\equiv_{n+1}V\land\Diamond_{n}A^{\prime}$ and $D\land\nabla_{n}B^{\prime}\equiv_{n+1}V\land\nabla_{n}B^{\prime}$, by Lemma 4.1. Hence, it is sufficient to prove that, for some $W\in\mathbb{W}_{n}$, $V\land\Diamond_{n}A^{\prime}\equiv_{n}W$ and similarly, for some $W\in\mathbb{W}_{n}$, $V\land\nabla_{n}B^{\prime}\equiv_{n}W$.

In the first case we actually have $V\land\Diamond_{n}A^{\prime}=_{\mathrm{RC}}W$, for some word $W$, which immediately yields the claim.

In the second case we write $B^{\prime}=B_{1}\Diamond_{n}B_{2}$ where $B_{1}\in\mathbb{W}_{n+1}$. There are three cases to consider: (a) $B_{1}\vdash\Diamond_{n+1}V$, (b) $V\vdash\Diamond_{n+1}B_{1}$, (c) $V=B_{1}$.

In case (c) by Lemma 4.2 we obtain:

[TABLE]

In case (a) we show $\nabla_{n}(V\land\nabla_{n}B^{\prime})=\nabla_{n}B^{\prime}$. Firstly,

[TABLE]

Hence, $\nabla_{n}B^{\prime}\vdash\nabla_{n}\nabla_{n+1}(V\land\nabla_{n}B^{\prime})=\nabla_{n}(V\land\nabla_{n}B^{\prime}).$ On the other hand,

[TABLE]

In case (b) we show $\nabla_{n}(V\land\nabla_{n}B^{\prime})=\nabla_{n}(V\land\Diamond_{n}B_{2})$ so that one can infer $\nabla_{n}(V\land\nabla_{n}B^{\prime})=\nabla_{n}V\Diamond_{n}B_{2}$. On the one hand, we have

[TABLE]

which implies $\nabla_{n}(V\land\nabla_{n}B^{\prime})\vdash\nabla_{n}(V\land\Diamond_{n}B_{2})$. On the other hand,

[TABLE]

Hence, $\nabla_{n}(V\land\Diamond_{n}B_{2})\vdash\nabla_{n}(V\land\nabla_{n}B^{\prime})$. $\Box$

From Theorem 2 we obtain the following strengthening of Lemma 4.3.

Corollary 4.4

The set of all formulas $\{\Diamond_{n}F,\nabla_{n}G:F,G\in\mathbb{F}_{n}^{\nabla}\}$ is linearly ordered by $\vdash_{\mathrm{RC}^{\nabla}}$.

Corollary 4.5

For all formulas $A,B\in\mathbb{F}_{n}^{\nabla}$, either $A\vdash\Diamond_{n}B$, or $B\vdash\Diamond_{n}A$, or $A\equiv_{n}B$.

Proof. Consider the words $A_{1}\equiv_{n}A$ and $B_{1}\equiv_{n}B$. By the linearity property for words either $A_{1}\vdash\Diamond_{n}B_{1}$ or $B_{1}\vdash\Diamond_{n}A_{1}$ or $A_{1}=B_{1}$. In the first case we obtain $A\vdash\nabla_{n}A_{1}\vdash\nabla_{n}\Diamond_{n}B_{1}\vdash\Diamond_{n}B_{1}\vdash\Diamond_{n}\nabla_{n}B\vdash\Diamond_{n}B$. The second case is symmetrical, the third one implies $A\equiv_{n}B$ immediately. $\Box$

Corollary 4.6

For all $A,B\in\mathbb{F}_{n}^{\nabla}$, $\Diamond_{n}A\vdash\Diamond_{n}B$ iff $A\vdash\nabla_{n}B$.

Proof. Assume $\Diamond_{n}A\vdash\Diamond_{n}B$. By Corollary 4.5, either $A\vdash\Diamond_{n}B$, or $B\vdash\Diamond_{n}A$, or $A\equiv_{n}B$. In the first and the third cases we immediately have $A\vdash\nabla_{n}B$. In the second case we obtain $\Diamond_{n}A\vdash\Diamond_{n}B\vdash\Diamond_{n}\Diamond_{n}A$ contradicting Corollary 3.4.

In the opposite direction, if $A\vdash\nabla_{n}B$ then $\Diamond_{n}A\vdash\Diamond_{n}\nabla_{n}B\vdash\Diamond_{n}B$. $\Box$

Theorem 3** (weak normal forms)**

Every formula $A\in\mathbb{F}_{n}^{\nabla}$ is equivalent in ${\mathrm{RC}^{\nabla}}$ to a formula of the form

[TABLE]

for some $k$, where $A_{i}\in\mathbb{W}_{i}$ for all $i=n,\dots,n+k$.

Proof. Induction on the build-up of $A\in\mathbb{F}_{n}^{\nabla}$. We consider the following cases.

1. $A=B\land C$. The induction hypothesis is applicable to $B$ and $C$, so it is sufficient to prove: for any $B_{i},C_{i}\in\mathbb{W}_{i}$ there is a word $A_{i}\in\mathbb{W}_{i}$ such that

[TABLE]

By Lemma 4.3 we can take one of $B_{i},C_{i}$ as $A_{i}$.

2. $A=\nabla_{i}B$, for some $i\geqslant n$. Then we obtain

[TABLE]

for some $B^{\prime}_{i}\in\mathbb{W}_{i}$, by Theorem 2.

3. $A=\Diamond_{i}B$, for some $i\geqslant n$. Then we obtain, using Lemma 3.2,

[TABLE]

for some $B^{\prime}_{i}\in\mathbb{W}_{i}$, by Theorem 2. $\Box$

Weak normal forms are, in general, not unique. However, the following lemma and its corollary show that the “tails” of the weak normal forms are invariant (up to equivalence in ${\mathrm{RC}^{\nabla}}$).

Lemma 4.7

Let $A\circeq\nabla_{n}A_{n}\land\nabla_{n+1}A_{n+1}\land\dots\land\nabla_{k}A_{k}$ and $B\circeq\nabla_{n}B_{n}\land\nabla_{n+1}B_{n+1}\land\dots\land\nabla_{m}B_{m}$ be weak normal forms, $B_{m}\not\circeq\top$ and $A\vdash B$. Then $k\geqslant m$ and for all $i$ such that $n\leqslant i\leqslant k$ there holds

1. $\mathrm{(i)}$

$\nabla_{i}A_{i}\land\dots\land\nabla_{k}A_{k}\vdash_{i}\nabla_{i}B_{i}\land\dots\land\nabla_{m}B_{m};$** 2. $\mathrm{(ii)}$

$\nabla_{i}A_{i}\land\dots\land\nabla_{k}A_{k}\vdash\nabla_{i}B_{i}\land\dots\land\nabla_{m}B_{m}.$**

Proof. By definition, Claim (ii) implies Claim (i), but we first prove (i) and then strengthen it to (ii). For $i=n$ both claims are vacuous, so we assume $i>n$.

Denote $\overline{A_{i}}:=\nabla_{i}A_{i}\land\dots\land\nabla_{k}A_{k}$ and $\overline{B_{i}}:=\nabla_{i}B_{i}\land\dots\land\nabla_{m}B_{m}$. By Lemma 4.5 we have either $\overline{A_{i}}\vdash\Diamond_{i}\overline{B_{i}}$ or $\overline{B_{i}}\vdash\Diamond_{i}\overline{A_{i}}$ or $\overline{A_{i}}\equiv_{i}\overline{B_{i}}$. In the first and in the third case we obviously have $\overline{A_{i}}\vdash_{i}\overline{B_{i}}$ as required.

Assume $\overline{B_{i}}\vdash\Diamond_{i}\overline{A_{i}}$. Consider the formula

[TABLE]

We show that $C\vdash\Diamond_{i}C$ contradicting Corollary 3.4.

Using our assumption and Lemma 3.2 (i) we obtain

[TABLE]

This proves Claim (i).

To prove (ii) assume the contrary and consider the maximal number $i$ such that $\overline{A_{i}}\nvdash\overline{B_{i}}$. Such an $i$ exists, since both $A$ and $B$ have finitely many terms. Thus, we have $\overline{A_{i+1}}\vdash\overline{B_{i+1}}$ and

[TABLE]

It follows that $\nabla_{i}A_{i}\land\overline{A_{i+1}}\nvdash\nabla_{i}B_{i}=\nabla_{i}\nabla_{i}B_{i}$, hence $\overline{A_{i}}\nvdash_{i}\nabla_{i}B_{i}$. Since $\overline{B_{i}}\vdash\nabla_{i}B_{i}$, we obtain $\overline{A_{i}}\nvdash_{i}\overline{B_{i}}$ contradicting Claim (i). $\Box$

Corollary 4.8

Let $\nabla_{n}A_{n}\land\nabla_{n+1}A_{n+1}\land\dots\land\nabla_{k}A_{k}$ be any weak normal form of a formula $A\in\mathbb{F}_{n}^{\nabla}$ with $A_{k}\not\circeq\top$. Then $k$ and each tail $\nabla_{i}A_{i}\land\dots\land\nabla_{k}A_{k}$ is defined uniquely up to equivalence in ${\mathrm{RC}^{\nabla}}$.

There are two formats for graphically unique normal forms. We call them ‘fat’ and ‘thin’, because the former consist of larger expressions, whereas the latter are obtained by pruning certain parts of a given formula. Fat normal forms, presented below, have a natural proof-theoretic meaning and are tightly related to collections of proof-theoretic ordinals called conservativity spectra or Turing–Taylor expansions [36].

4.2 Fat normal forms

Definition 3

A formula $A\in\mathbb{F}_{n}^{\nabla}$ is in the fat normal form for $\mathbb{F}_{n}^{\nabla}$ if either $A\circeq\top$ or it has the form $\nabla_{n}A_{n}\land\nabla_{n+1}A_{n+1}\land\dots\land\nabla_{n+k}A_{n+k}$, where for all $i=n,\dots,n+k$, $A_{i}\in\mathbb{W}_{i}$, $A_{n+k}\not\circeq\top$ and

[TABLE]

A variable-free formula $A$ is in the fat normal form if $A$ is in the fat normal form for $\mathbb{F}_{0}^{\nabla}$.

Remark 4.9

In a fat normal form, for each $i$ such that $n\leqslant i\leqslant n+k$, there holds $\nabla_{i}A_{i}=_{{\mathrm{RC}^{\nabla}}}\nabla_{i}(\nabla_{i}A_{i}\land\dots\land\nabla_{n+k}A_{n+k}).$

Theorem 4

1. $\mathrm{(i)}$

Every $A\in\mathbb{F}_{n}^{\nabla}$ is equivalent to a formula in the fat normal form for $\mathbb{F}_{n}^{\nabla}$. 2. $\mathrm{(ii)}$

For any $A\in\mathbb{F}_{n}^{\nabla}$, the words $A_{i}$ in the fat normal form of $A$ for $\mathbb{F}_{n}^{\nabla}$ are unique modulo equivalence in $\mathrm{RC}$.

Proof. (i) First, we apply Theorem 2. Then, by induction on $k$ we show that any formula $\nabla_{n}A_{n}\land\dots\land\nabla_{n+k}A_{n+k}$ can be transformed into one satisfying $(*)$.

For $k=0$ the claim is trivial. Otherwise, by the induction hypothesis we can assume that $(*)$ holds for $i=n+1,\dots,n+k$. Then we argue using Lemma 4.2 as follows:

[TABLE]

where $A^{\prime}\in\mathbb{W}_{n}$ is obtained from Theorem 2. Notice that

[TABLE]

hence $(*)$ holds for $i=n$. This proves Claim (i).

To prove Claim (ii) we apply Lemma 4.7. Assume $A\vdash B$, $A=\nabla_{n}A_{n}\land\dots\land\nabla_{n+k}A_{n+k}$ is in the fat normal form and $B=\nabla_{n}B_{n}\land\dots\land\nabla_{n+m}B_{n+m}$ is in a weak normal form. Then $k\geqslant m$ and, for all $i=n,\dots,n+m$, $\nabla_{i}A_{i}\vdash\nabla_{i}B_{i}$.

It follows that, if $A,B\in\mathbb{F}_{n}^{\nabla}$ are both in the fat normal form and $A=B$ in ${\mathrm{RC}^{\nabla}}$, then $m=k$ and $\nabla_{i}A_{i}=\nabla_{i}B_{i}$, for $i=n,\dots,n+k$. Since $\mathbb{W}_{i}$ is linearly preordered by $<_{i}$ in $\mathrm{RC}$, the latter is only possible if $A_{i}=_{\mathrm{RC}}B_{i}$. $\Box$

Remark 4.10

As stated in Theorem 4, fat normal forms are only unique modulo equivalence of the constituent words $A_{i}$ in $\mathrm{RC}$. However, we know that words have graphically unique $\mathrm{RC}$-normal forms [6]. Combining the two notions together yields graphically unique normal forms for ${\mathrm{RC}^{\nabla}}$.

Thus, we can test the equality of two variable-free formulas in ${\mathrm{RC}^{\nabla}}$ by graphically comparing their unique normal forms. Alternatively, we observe the following property.

Lemma 4.11

Let $A\circeq\nabla_{n}A_{n}\land\nabla_{n+1}A_{n+1}\land\dots\land\nabla_{k}A_{k}$ and $B\circeq\nabla_{n}B_{n}\land\nabla_{n+1}B_{n+1}\land\dots\land\nabla_{m}B_{m}$ be any fat normal forms. Then $A\vdash_{\mathrm{RC}^{\nabla}}B$ holds iff $k\geqslant m$ and, for all $i$ such that $n\leqslant i\leqslant m$, one has $\Diamond_{i}A_{i}\vdash_{\mathrm{RC}}\Diamond_{i}B_{i}$.

Proof. By Lemma 4.7 and Remark 4.9, $A\vdash_{\mathrm{RC}^{\nabla}}B$ holds iff, for all $i$ such that $n\leqslant i\leqslant m$, one has $\nabla_{i}A_{i}\vdash_{\mathrm{RC}^{\nabla}}\nabla_{i}B_{i}$. However, the latter is equivalent to $A_{i}\vdash_{\mathrm{RC}^{\nabla}}\nabla_{i}B_{i}$ and to $\Diamond_{i}A_{i}\vdash_{\mathrm{RC}^{\nabla}}\Diamond_{i}B_{i}$ by Corollary 4.6. Since words are linearly preordered in $\mathrm{RC}$, the latter is also equivalent to $\Diamond_{i}A_{i}\vdash_{\mathrm{RC}}\Diamond_{i}B_{i}$. $\Box$

The transformation of a variable-free formula to its fat normal form is computable. Hence, we obtain

Corollary 4.12

The set of variable-free sequents $A\vdash B$ provable in ${\mathrm{RC}^{\nabla}}$ is decidable.

From the uniqueness of normal forms we also obtain arithmetical completeness of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$ in the standard way.

Corollary 4.13

Suppose $A,B$ are variable-free and $T$ is a sound Gödelian extension of $\mathrm{EA}$. Then $A\vdash_{\mathrm{RC}^{\nabla}}B$ iff $A^{*}\leqslant_{T}B^{*}$, for all arithmetical interpretations $*$ in $\mathfrak{G}_{T}$.

Corollary 4.14

Suppose $T$ is a sound Gödelian extension of $\mathrm{EA}$. Then the algebra $\overline{\mathfrak{G}}_{T}^{0}$ is isomorphic to the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$.

4.3 Thin normal forms

Let $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$ be in a weak normal form. As before, we denote $\overline{A_{i}}\circeq\nabla_{i}A_{i}\land\dots\land\nabla_{k}A_{k}$.

Definition 4

$A$ is in a thin normal form if either $A\circeq\top$ or $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$ where $A_{k}\not\circeq\top$, for all $i<k$ $A_{i}\in\mathbb{W}_{i}$, and there is no $B_{i}\in\mathbb{W}_{i}$ such that $B_{i}<_{i}A_{i}$ and $\overline{A_{i}}=_{{\mathrm{RC}^{\nabla}}}\nabla_{i}B_{i}\land\overline{A_{i+1}}$.

This definition allows one to easily prove the existence and uniqueness of normal forms using the fact that words in $\mathbb{W}_{i}$ are pre-wellordered by $<_{i}$.

Theorem 5

For each $A\in\mathbb{F}^{\nabla}$ there is a thin normal form equivalent to $A$ in ${\mathrm{RC}^{\nabla}}$. The thin normal form is unique modulo equivalence of the constitutent words $A_{i}$ in $\mathrm{RC}$.

Proof. We recursively define the words $A_{k},A_{k-1},\dots,A_{0}$. To determine $k$ and $A_{k}$ one takes any weak normal form for $A$ (observe that $\top$ is the $<_{i}$-minimum for each $i$). Once one has defined $A_{k},\dots,A_{i+1}$ one can define $A_{i}$ by considering all the weak normal forms with the given $\nabla_{i+1}A_{i+1}$, …, $\nabla_{k}A_{k}$ and selecting the one with the $<_{i}$-minimal $A_{i}$. By induction on $k-i$ it is also easy to see that all the words $A_{k},\dots,A_{0}$ are thus uniquely determined modulo $\mathrm{RC}$. $\Box$

The given proof, though short, is non-constructive. Now we will show that the thin normal form can be effectively computed. First, we consider a particular case when the given weak normal form is $\nabla_{0}A\land\nabla_{1}B$. Then we will reduce the general case to this one.

Let $A\in\mathbb{W}_{0},B\in\mathbb{W}_{1},B\not\circeq\top$ and $A\circeq A_{0}\Diamond_{0}A_{1}\Diamond_{0}\dots\Diamond_{0}A_{n}$ with $A_{i}\in\mathbb{W}_{1}$. If $B\vdash\nabla_{0}A$ then $\nabla_{0}A\land\nabla_{1}B=\nabla_{0}\top\land\nabla_{1}B$ which is its thin normal form. So we assume $B\nvdash\nabla_{0}A$. We define

[TABLE]

where $i$ is the least such that $B\leqslant_{1}A_{i}$. Such an $i$ exists, for otherwise $B\vdash\Diamond_{0}A\vdash\nabla_{0}A$. Clearly, $B|A$ can be found effectively from $A$ and $B$ by deleting the appropriate initial segment of $A$. Also notice that $B\land A=_{\mathrm{RC}}B\land(B|A)$. We consider three cases.

Case 1: $A_{0}>_{1}B$. We claim that $\nabla_{0}A\land\nabla_{1}B$ is in a thin normal form.

Assume $A^{\prime}<_{0}A$, then $A\vdash\Diamond_{1}B\land\Diamond_{0}A^{\prime}=\Diamond_{1}(B\land\Diamond_{0}A^{\prime})\vdash\Diamond_{1}(\nabla_{0}A^{\prime}\land\nabla_{1}B)$. Hence, if $\nabla_{0}A^{\prime}\land\nabla_{1}B\vdash\nabla_{0}A$, then $A\vdash\Diamond_{1}(\nabla_{0}A\land\nabla_{1}B)\vdash\Diamond_{1}A$ contradicting Corollary 3.4 .

Case 2: $A_{0}<_{1}B$. We claim that $\nabla_{0}\Diamond_{0}(B|A)\land\nabla_{1}B$ is the thin normal form of $\nabla_{0}A\land\nabla_{1}B$. Firstly, we show that $\Diamond_{0}(B|A)\land\nabla_{1}B\vdash\nabla_{0}A$. By downwards induction on $j:=i$ to [math] we show that

[TABLE]

Basis of induction holds since $B|A=A_{i}\Diamond_{0}\dots\Diamond_{0}A_{n}$. Assume the claim holds for $j$. Since $\nabla_{1}B\vdash\nabla_{1}\Diamond_{1}A_{j-1}=\Diamond_{1}A_{j-1}$, we obtain:

[TABLE]

Hence, the claim holds for $j-1$ and by induction we conclude that

[TABLE]

Now we need to show that for all $A^{\prime}<_{0}\Diamond_{0}(B|A)$ one has $\nabla_{0}A^{\prime}\land\nabla_{1}B\nvdash\nabla_{0}A$. If $\Diamond_{0}(B|A)\vdash\Diamond_{0}A^{\prime}$ then by Lemma 4.6 $B|A\vdash\nabla_{0}A^{\prime}$. Also $B|A\vdash A_{i}\vdash\nabla_{1}B$, since we assume $B\leqslant_{1}A_{i}$. It follows that $B|A\vdash\nabla_{0}A^{\prime}\land\nabla_{1}B$. On the other hand, $A\vdash\Diamond_{0}(B|A)$ and $\nabla_{0}A\vdash\Diamond_{0}(B|A)$ whence $\nabla_{0}A^{\prime}\land\nabla_{1}B\nvdash\nabla_{0}A$ by Corollary 3.4.

Case 3: $A_{0}=B$. Let $C:=A_{1}\Diamond_{0}\dots\Diamond_{0}A_{n}$, thus $A\circeq B\Diamond_{0}C$.We claim that $\nabla_{0}\Diamond_{0}C\land\nabla_{1}B$ is the thin normal form of $\nabla_{0}A\land\nabla_{1}B$.

First, $\nabla_{1}B\land\Diamond_{0}C\vdash\nabla_{1}(B\land\Diamond_{0}C)\vdash\nabla_{0}(B\Diamond_{0}C)=\nabla_{0}A.$ Hence, $\nabla_{0}\Diamond_{0}C\land\nabla_{1}B=\nabla_{0}A\land\nabla_{1}B$.

Second, we show that if $A^{\prime}<_{0}\Diamond_{0}C$ then $\nabla_{0}A^{\prime}\land\nabla_{1}B\nvdash\nabla_{0}A$. Assume $A^{\prime}<_{0}\Diamond_{0}C$. By Lemma 4.6 we have $C\vdash\nabla_{0}A^{\prime}$. Also, since $A_{1}\geqslant_{1}B$, we have $C\vdash A_{1}\vdash\nabla_{1}B$ by Lemma 4.6. It follows that $C\vdash\nabla_{0}A^{\prime}\land\nabla_{1}B$. On the other hand, $A=B\land\Diamond_{0}C\vdash\Diamond_{0}C$, hence $\nabla_{0}A\vdash\nabla_{0}\Diamond_{0}C\vdash\Diamond_{0}C$. Therefore, by Corollary 3.4 $\nabla_{0}A^{\prime}\land\nabla_{1}B\nvdash\nabla_{0}A$.

In all three cases we have explicitly constructed the thin normal form. Hence, we obtain the following theorem.

Theorem 6

For any variable-free formula of ${\mathrm{RC}^{\nabla}}$, its unique thin normal form can be effectively constructed.

Proof. Let a formula $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$ in a weak normal form be given. We argue by induction on $k$. For $k=0$ the claim is obvious. Consider $k>0$, by IH we may assume that $\overline{A_{1}}:=\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$ is in a thin normal form. (To formally apply the IH one should consider the formula obtained from $\overline{A_{1}}$ by decreasing all indices of modalities by $1$.) By Theorem 2 there is a word $B\in S_{1}$ such that $\nabla_{1}B\equiv_{1}\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$.

Consider the formula $\nabla_{0}A_{0}\land\nabla_{1}B$ and bring it to a thin normal form, that is, find a $<_{0}$-minimal $A_{0}^{\prime}\in S_{0}$ such that $\nabla_{0}A_{0}^{\prime}\land\nabla_{1}B=\nabla_{0}A_{0}\land\nabla_{1}B$. We claim that $A^{\prime}:=\nabla_{0}A_{0}^{\prime}\land\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k}$ is equivalent to $A$ and is in a thin normal form.

Firstly, $A^{\prime}\vdash\nabla_{0}A_{0}^{\prime}\land\nabla_{1}B\vdash\nabla_{0}A_{0}$, hence $A^{\prime}\vdash A$. On the other hand, $A\vdash\nabla_{0}A_{0}\land\nabla_{1}B=\nabla_{0}A_{0}^{\prime}$, hence $A\vdash A^{\prime}$.

Secondly, assume there is an $A^{\prime\prime}<_{0}A^{\prime}_{0}$ such that $\nabla_{0}A^{\prime\prime}\land\overline{A_{1}}\vdash\nabla_{0}A^{\prime}_{0}$. By Lemma 4.1, $\nabla_{0}A^{\prime\prime}\land\overline{A_{1}}\equiv_{1}\nabla_{0}A^{\prime\prime}\land\nabla_{1}B$. Hence, $\nabla_{0}A^{\prime\prime}\land\nabla_{1}B\vdash\nabla_{0}A^{\prime}_{0}$ contradicting the $<_{0}$-minimality of $A^{\prime}_{0}$. $\Box$

5 Iterating monotone operators on $\mathfrak{G}_{\mathrm{EA}}$

Transfinite iterations of reflection principles play an important role in proof theory starting from the works of A. Turing [44] and S. Feferman [23] on recursive progressions. Here we present a general result on defining iterations of monotone semi-idempotent operators in $\mathfrak{G}_{\mathrm{EA}}$.

An operator $R:\mathfrak{G}_{\mathrm{EA}}\to\mathfrak{G}_{\mathrm{EA}}$ is called computable if so is the function $\ulcorner\sigma\urcorner\mapsto\ulcorner R(\sigma)\urcorner$. By extension of terminology we also call computable any operator $R^{\prime}$ such that $\forall\sigma\in\mathfrak{G}_{\mathrm{EA}}\>R^{\prime}(\sigma)=_{\mathrm{EA}}R(\sigma)$, for some computable $R$.

Bounded formulas in the language of $\mathrm{EA}$ will henceforth be called elementary. An operator $R:\mathfrak{G}_{\mathrm{EA}}\to\mathfrak{G}_{\mathrm{EA}}$ is called uniformly definable if there is an elementary formula $\mathrm{Ax}_{R}(x,y)$ such that

1. $\mathrm{(i)}$

For each $\sigma\in\mathfrak{G}_{\mathrm{EA}}$ one has $R(\sigma)=_{\mathrm{EA}}\mathrm{Ax}_{R}(x,\overline{\ulcorner\sigma\urcorner})$, 2. $\mathrm{(ii)}$

$\mathrm{EA}\vdash\forall x,y\>(\mathrm{Ax}_{R}(x,y)\to x\geqslant y).$

The operators $\mathrm{R}_{n}$ and $\mathrm{\Pi}_{n+1}$ are uniformly definable in a very special way. For example, the formula $\mathrm{R}_{n}(\sigma)$ is obtained by substituting $\sigma(x)$ for $X(x)$ into a fixed elementary formula containing a single positive occurrence of a predicate variable $X$. More generally, it can be shown that an operator $R:\mathfrak{G}_{\mathrm{EA}}\to\mathfrak{G}_{\mathrm{EA}}$ is uniformly definable iff $R$ is computable. A proof of this fact is given in Appendix B.

Definition 5

A uniformly definable $R$ is called

• •

provably monotone if $\mathrm{EA}\vdash\forall\sigma,\tau\>(\mbox{``}\tau\leqslant_{\mathrm{EA}}\sigma\mbox{''}\to\mbox{``}R(\tau)\leqslant_{\mathrm{EA}}R(\sigma)\mbox{''}),$

• •

reflexively monotone if $\mathrm{EA}\vdash\forall\sigma,\tau\>(\mbox{``}\tau\leqslant_{\mathrm{EA}}\sigma\mbox{''}\to\mbox{``}R(\tau)\leqslant R(\sigma)\mbox{''}).$

Here, $\sigma,\tau$ range over Gödel numbers of elementary formulas in one free variable, $\mbox{``}\tau\leqslant_{\mathrm{EA}}\sigma\mbox{''}$ abbreviates $\Box_{\mathrm{EA}}\forall x\>(\Box_{\sigma}(x)\to\Box_{\tau}(x))$ and $\mbox{``}R(\tau)\leqslant R(\sigma)\mbox{''}$ stands for $\forall x\>(\Box_{\mathrm{Ax}_{R}(\cdot,\bar{\sigma})}(x)\to\Box_{\mathrm{Ax}_{R}(\cdot,\bar{\tau})}(x)).$ Reflexive monotonicity here refers to the fact that $\mbox{``}R(\tau)\leqslant R(\sigma)\mbox{''}$ is the statement of inclusion of theories rather than provable inclusion. Since the formula $\mbox{``}\tau\leqslant_{\mathrm{EA}}\sigma\mbox{''}$ implies its own provability in $\mathrm{EA}$, reflexively monotone operators are (provably) monotone but not necessarily vice versa.

It is also easy to see that the operators $\mathrm{R}_{n}$ (along with all the usual reflection principles) are reflexively monotone.

Next we turn to iterations of operators along ordinal notation systems. In this paper, ordinal notation systems will be pre-wellorderings, that is, reflexive, transitive binary relations whose quotient order is a well-ordering. An elementary pre-wellordering is a pair of bounded formulas $D(x)$ and $x\preccurlyeq y$ and a constant [math] such that the relation $\preccurlyeq$ provably in $\mathrm{EA}$ is a linear preorder on $D$ with the least element [math], and is a pre-wellorder of $D$ in the standard model of arithmetic. Given an elementary well-ordering $(D,\preccurlyeq,0)$, we will denote its elements by Greek letters and will identify them with an initial segment of the ordinals. We denote

[TABLE]

Let $R$ be an uniformly definable monotone operator. The $\alpha$-th iterate of $R$ along $(D,\preccurlyeq,0)$ is a map associating with any numeration $\sigma$ the Gödelian extension of $\mathrm{EA}$ numerated by an elementary formula $\rho(\overline{\alpha},x)$ such that provably in $\mathrm{EA}$:

[TABLE]

A natural Gödel numbering of formulas and terms should satisfy the inequalities $\ulcorner\rho(\bar{\beta},x)\urcorner\geqslant\ulcorner\bar{\beta}\urcorner\geqslant\beta$. Hence, the quantifier on $\beta$ in equation (3) can be bounded by $x$. Thus, some elementary formula $\rho(\alpha,x)$ satisfying (3) can be constructed by the fixed point lemma.

The parametrized family of theories numerated by $\rho(\alpha,x)$ will be denoted $R^{\alpha}(\sigma)$ and the formula $\rho(\alpha,x)$ will be more suggestively written as $x\in R^{\alpha}(\sigma)$. Then, equation (3) can be interpreted as saying that $R^{0}(\sigma)=_{\mathrm{EA}}\sigma$ and, if $\alpha\succ 0$,

[TABLE]

Lemma 5.1

Suppose $R$ is uniformly definable.

1. $\mathrm{(i)}$

If $0\prec\alpha\preccurlyeq\beta$ then $R^{\beta}(\sigma)\leqslant_{\mathrm{EA}}R^{\alpha}(\sigma)$; 2. $\mathrm{(ii)}$

$\mathrm{EA}\vdash\forall\alpha,\beta\>(0\prec\alpha\prec\beta\to\mbox{``}R^{\beta}(\sigma)\leqslant R^{\alpha}(\sigma)\mbox{''}).$**

Proof. Obviously, Claim (i) follows from Claim (ii). For the latter we unwind the definition of $\rho(\alpha,x)$ and prove within $\mathrm{EA}$

[TABLE]

This is sufficient to obtain from the same premise $\forall x\>(\Box_{\rho(\alpha,\cdot)}(x)\to\Box_{\rho(\beta,\cdot)}(x)).$

For a proof of (4) we reason within $\mathrm{EA}$: If $\rho(\alpha,x)$ and $\alpha\not\approx 0$ then there is a $\gamma\prec\alpha$ such that $\mathrm{Ax}_{R}(x,\ulcorner\rho(\overline{\gamma},x)\urcorner)$. By the provable transitivity of $\prec$ from $\alpha\prec\beta$ we obtain $\gamma\prec\beta$, hence $\rho(\beta,x)$, q.e.d. $\Box$

Lemma 5.2

Suppose $R$ is reflexively monotone. If $\tau\leqslant_{\mathrm{EA}}\sigma$ then $R^{\alpha}(\tau)\leqslant_{\mathrm{EA}}R^{\alpha}(\sigma)$ and, moreover, $\mathrm{EA}\vdash\forall\alpha\>\mbox{``}R^{\alpha}(\tau)\leqslant R^{\alpha}(\sigma)\mbox{''}.$

Proof. We argue by reflexive induction similarly to [5], that is, we prove in $\mathrm{EA}$ that

[TABLE]

and then apply Löb’s theorem in $\mathrm{EA}$. Assume $\tau\leqslant_{\mathrm{EA}}\sigma$.

Reason within $\mathrm{EA}$: If $\Box_{R^{\alpha}(\sigma)}(x)$ then either $\alpha\approx 0\land\Box_{\sigma}(x)$, or there is a $\beta\prec\alpha$ such that $\Box_{R(R^{\overline{\beta}}(\sigma))}(x)$. In the first case we obtain $\Box_{\tau}(x)$ by the external assumption $\tau\leqslant_{\mathrm{EA}}\sigma$ and are done. In the second case, by the premise and the reflexive monotonicity of $R$ we obtain $\Box_{R(R^{\overline{\beta}}(\tau))}(x)$ which yields $\Box_{R^{\alpha}(\tau)}(x)$. $\Box$

Corollary 5.3

The iteration of $R$ along $(D,\prec)$ is uniquely defined, that is, equation (3) has a unique solution modulo $=_{\mathrm{EA}}$.

Lemma 5.4

Suppose $R$ is reflexively monotone and semi-idempotent. Then

1. $\mathrm{(i)}$

If $0\prec\alpha$ then $R(R^{\alpha}(\sigma))\leqslant_{\mathrm{EA}}R^{\alpha}(\sigma)$; 2. $\mathrm{(ii)}$

$\mathrm{EA}\vdash\forall\alpha\>(0\prec\alpha\to\mbox{``}R(R^{\alpha}(\sigma))\leqslant R^{\alpha}(\sigma)\mbox{''}).$**

Proof. Claim (i) follows from (ii). For the latter, it is sufficient to prove the claim within $\mathrm{EA}+\mathrm{B\Sigma}_{1}$ and refer to the $\Pi_{2}^{0}$-conservativity of $\mathrm{B\Sigma}_{1}$ over $\mathrm{EA}$ (cf [28]).

Reason in $\mathrm{EA}+\mathrm{B\Sigma}_{1}$: If $0\prec\alpha$ and $x\in R^{\alpha}(\sigma)$, then there is a $\beta\prec\alpha$ such that $x\in R(R^{\beta}(\sigma))$. We consider two cases. If $0\prec\beta$ then, since (provably) $\beta\prec\alpha$, by Lemma 5.1 we have $R^{\alpha}(\sigma)\leqslant_{\mathrm{EA}}R^{\beta}(\sigma)$. By the reflexive monotonicity of $R$ we obtain $R(R^{\alpha}(\sigma))\leqslant R(R^{\beta}(\sigma))$. Hence, $\Box_{R(R^{\alpha}(\sigma))}(x)$ and we are done.

If $\beta\approx 0$ then by the definition $R^{\beta}(\sigma)=_{\mathrm{EA}}\sigma$. Hence, by the reflexive monotonicity of $R$, $R(\sigma)\leqslant R(R^{\beta}(\sigma))$. Since $0\prec\alpha$, by the definition $R^{\alpha}(\sigma)\leqslant_{\mathrm{EA}}R(R^{0}(\sigma))\leqslant_{\mathrm{EA}}R(\sigma)$. It follows that $R(R^{\alpha}(\sigma))\leqslant R(R(\sigma))\leqslant R(\sigma)$ and therefore $\Box_{R(R^{\alpha}(\sigma))}(x)$.

Thus, using $\mathrm{B\Sigma}_{1}$ we may conclude that $0\prec\alpha$ implies

[TABLE]

as required. $\Box$

The following lemma is most naturally stated for elementary pre-wellorderings equipped with elementary formulas $\mathrm{Suc}(\alpha,\beta)$ expressing “$\beta$ is a successor of $\alpha$” and $\mathrm{Lim}(\alpha)$ expressing “$\alpha$ is a limit” that provably in $\mathrm{EA}$ satisfy their defining properties:

[TABLE]

Lemma 5.5

Suppose $R$ is reflexively monotone and semi-idempotent. Then

1. $\mathrm{(i)}$

$R^{\alpha}(\sigma)=_{\mathrm{EA}}\sigma$* if $\alpha\approx 0$,* 2. $\mathrm{(ii)}$

$R^{\beta}(\sigma)=_{\mathrm{EA}}R(R^{\alpha}(\sigma))$* if $\mathrm{Suc}(\alpha,\beta)$,* 3. $\mathrm{(iii)}$

$R^{\lambda}(\sigma)=_{\mathrm{EA}}\bigwedge\{R^{\alpha}(\sigma):0\prec\alpha\prec\lambda\}$* if $\mathrm{Lim}(\lambda)$.*

Here $\bigwedge\{R^{\alpha}(\sigma):0\prec\alpha\prec\lambda\}$ denotes the Gödelian theory numerated by

[TABLE]

Proof. Claim (i) is easy. For Claim (ii) assume $\mathrm{Suc}(\alpha,\beta)$. The implication $R^{\beta}(\sigma)\leqslant_{\mathrm{EA}}R(R^{\alpha}(\sigma))$ is easy, since $\alpha\prec\beta$ and this fact is provable in $\mathrm{EA}$. For the opposite implication it is sufficient to prove in $\mathrm{EA}+\mathrm{B\Sigma}_{1}$:

[TABLE]

Then one will be able to conclude using $\mathrm{B\Sigma}_{1}$ that $\forall x\>(\Box_{R^{\beta}(\sigma)}(x)\to\Box_{R(R^{\alpha}(\sigma))}(x))$ and then appeal to the $\Pi_{2}^{0}$-conservativity of $\mathrm{B\Sigma}_{1}$ over $\mathrm{EA}$.

Reason in $\mathrm{EA}+\mathrm{B\Sigma}_{1}$: Assume $x\in R^{\beta}(\sigma)$ then (since $\beta\not\approx 0$) there is a $\gamma\prec\beta$ such that $x\in R(R^{\gamma}(\sigma))$. If $\gamma\approx\alpha$ then $x\in R(R^{\alpha}(\sigma))$ and we are done. Otherwise, $\gamma\prec\alpha$ and one has $R^{\alpha}(\sigma)\leqslant R(R^{\gamma}(\sigma))$. On the other hand, by Lemma 5.4, $R(R^{\alpha}(\sigma))\leqslant R^{\alpha}(\sigma)$. Hence, $R(R^{\alpha}(\sigma))\leqslant R(R^{\gamma}(\sigma))$, therefore $\Box_{R(R^{\alpha}(\sigma))}(x)$ as required.

To prove Claim (iii) we argue in a similar manner. Assume $\mathrm{Lim}(\lambda)$, then this fact is also provable in $\mathrm{EA}$. To prove the implication from left to right we reason in $\mathrm{EA}+\mathrm{B\Sigma}_{1}$:

Assume $x\in R^{\lambda}(\sigma)$. Since $\lambda\not\approx 0$ there is a $\beta\prec\lambda$ such that $x\in R(R^{\beta}(\sigma))$. Since $\mathrm{Lim}(\lambda)$ there is an $\alpha$ such that $\beta\prec\alpha\prec\lambda$. Then $R^{\alpha}(\sigma)\leqslant_{\mathrm{EA}}R(R^{\beta}(\sigma))$ and hence $\Box_{R^{\alpha}(\sigma)}(x)$.

From right to left we reason in $\mathrm{EA}+\mathrm{B\Sigma}_{1}$: Assume $0\prec\alpha\prec\lambda$ and $x\in R^{\alpha}(\sigma)$. Since $\alpha\prec\lambda$ we have by definition $R^{\lambda}(\sigma)\leqslant R(R^{\alpha}(\sigma))$. On the other hand, since $\alpha\succ 0$, by Lemma 5.4 we have $R(R^{\alpha}(\sigma))\leqslant R^{\alpha}(\sigma)$. Then $R^{\lambda}(\sigma)\leqslant R^{\alpha}(\sigma)$ and $\Box_{R^{\lambda}(\sigma)}(x)$, as required. $\Box$

6 Expressibility of iterated reflection

In this section we confuse the arithmetical and reflection calculus notation. We write $\Diamond_{n}$ for $\mathrm{R}_{n}$ and $\nabla_{n}$ for $\mathrm{\Pi}_{n+1}$. Our goal is to show that iterated operators $\Diamond_{n}^{\alpha}$, for natural ordinal notations $\alpha<\varepsilon_{0}$, are expressible in the language of ${\mathrm{RC}^{\nabla}}$. We will rely on the so-called reduction property (cf. [6], the present version is somewhat more general and follows from [5, Theorem 2], see also [12]).

Let $\mathrm{EA}^{+}$ denote the theory $\mathrm{R}_{1}(\mathrm{EA})$ which is known to be equivalent to $\mathrm{EA}+\text{Supexp}$. Theories in this and the following section will be Gödelian extensions of $\mathrm{EA}^{+}$. We could have worked more generally over $\mathrm{EA}$ at the cost of replacing the reflection and conservativity operators of $\mathfrak{G}_{\mathrm{EA}}$ by their analogs stated for cut-free provability (see [5, Appendix C]). Taking cut-free version of $\mathrm{EA}$ as our base Gödelian theory seems to be a better choice for proof-theoretic applications. However, for simplicity we prefer to strengthen our base theory to $\mathrm{EA}^{+}$ as it was done in some previous papers we would like to refer to.

Working in $\mathfrak{G}_{\mathrm{EA}^{+}}$ we write $\Diamond_{n,\sigma}(\tau)$ for $\Diamond_{n}(\sigma\land\tau)$. Obviously, $\Diamond_{n,\sigma}$ is a monotone semi-idempotent operator, for each $\sigma$. Also, $1$ will stand for $1_{\mathrm{EA}^{+}}$.

Theorem 7** (reduction property)**

For all $\sigma\in\mathfrak{G}_{\mathrm{EA}^{+}}$, $n\in\omega$,

[TABLE]

We also remark that the theory $\Diamond_{n,\sigma}^{\omega}(1)$ is equivalent to the one axiomatized over $\mathrm{EA}$ by the union of theories $\{\mathrm{Q}_{n}^{k}(\sigma):k<\omega\}$, where $\mathrm{Q}_{n}^{0}(\sigma):=\Diamond_{n}\sigma$ and $\mathrm{Q}_{n}^{k+1}(\sigma):=\Diamond_{n}(\sigma\land\mathrm{Q}_{n}^{k}(\sigma))$ are defined by formulas in one variable of $\mathrm{RC}$. The corresponding Gödelian theory taken with its natural numeration will be denoted $\bigwedge_{k<\omega}\mathrm{Q}_{n}^{k}(\sigma)$.

Concerning these formulas we note three well-known facts.

Lemma 6.1

Provably in $\mathrm{EA}$,

$\forall B\in\mathbb{W}_{n}\>\forall k\>\mathrm{Q}_{n}^{k+1}(B)\vdash_{\mathrm{RC}}\mathrm{Q}_{n}^{k}(B)\land\Diamond_{n}\mathrm{Q}_{n}^{k}(B)$; 2. 2.

$\forall B\in\mathbb{W}_{n}\>\forall k\>\mathrm{Q}_{n}^{k}(B)<_{n}\Diamond_{n+1}B$; 3. 3.

$\forall B\in\mathbb{W}_{n}\>\forall k\>\exists A\in\mathbb{W}_{n}\>\mathrm{Q}_{n}^{k}(B)=_{\mathrm{RC}}A$.

The first two of these claims are proved by an easy induction on $k$. The third one is a consequence of a more general theorem that any variable-free formula of $\mathrm{RC}$ is equivalent to a word. An explicit rule for calculating such an $A$ is also well-known and related to the so-called Worm sequence, see [7, Lemma 5.9].

We consider the set of words $(\mathbb{W}_{n},<_{n})$ modulo equivalence in $\mathrm{RC}$, together with its natural representation in $\mathrm{EA}$, as an elementary pre-wellordering. Recall that, for each $A\in\mathbb{W}_{n}$, $o_{n}(A)$ denotes the order type of $\{B<_{n}A:B\in\mathbb{W}_{n}\}$ modulo $=_{\mathrm{RC}}$. In a formalized context, the ordinal $o_{n}(A)$ is represented by its notation, the word $A$, however we still write $o_{n}(A)$, as it reminds us that $A$ must be viewed as an ordinal and indicates which system of ordinal notation is considered. From the reduction property we obtain the following theorem that was stated as Theorem 6 in [6] in a somewhat different way. We provide a proof for the reader’s convenience, though it is nearly the same as in [6].

For a word $A$ and a Gödelian theory $\sigma\in\mathfrak{G}_{\mathrm{EA}^{+}}$, let $A^{*}(\sigma)$ denote the interpretation of the formula $A[p/\top]$ in $\mathfrak{G}_{\mathrm{EA}^{+}}$ sending $p$ to $\sigma$.

Theorem 8

For all words $A\in\mathbb{W}_{n}\setminus\{\top\}$, in $\mathfrak{G}_{\mathrm{EA}^{+}}$ there holds

[TABLE]

Proof. We argue by reflexive induction in $\mathrm{EA}^{+}$ and prove that, for all $\sigma\in\mathfrak{G}_{\mathrm{EA}^{+}}$ and all $n<\omega$,

[TABLE]

Arguing inside $\mathrm{EA}^{+}$, we will omit the quotation marks and read the expressions $\tau\leqslant\nu$ as $\forall x\>(\Box_{\nu}(x)\to\Box_{\tau}(x))$ and $\tau=\nu$ as $\forall x\>(\Box_{\tau}(x)\leftrightarrow\Box_{\nu}(x))$.

If $A\circeq\Diamond_{n}B$ then $o_{n}(A)=o_{n}(B)+1$. If $B\circeq\top$ the claim follows since $\nabla_{n}A^{*}(\sigma)=\nabla_{n}\Diamond_{n}\sigma=\Diamond_{n}(\sigma).$ If $B\not\circeq\top$ we have by the reflexive induction hypothesis $\nabla_{n}B^{*}(\sigma)=_{\mathrm{EA}^{+}}\Diamond_{n}^{o_{n}(B)}(\sigma)$. It follows that $\Diamond_{n}(\Diamond_{n}^{o_{n}(B)}(\sigma))=\Diamond_{n}\nabla_{n}B^{*}(\sigma)=\Diamond_{n}B^{*}(\sigma).$ Therefore, we obtain

[TABLE]

If $A\circeq\Diamond_{m+1}B$ with $m\geqslant n$ then $\nabla_{n}A^{*}(\sigma)=\nabla_{n}\nabla_{m}\Diamond_{m+1}B^{*}(\sigma)$. By the reduction property $\nabla_{m}\Diamond_{m+1}B^{*}(\sigma)=\bigwedge_{k<\omega}\mathrm{Q}_{m}^{k}(B^{*}(\sigma))$. Moreover, by Lemma 6.1 (i), if a sentence is provable in $\bigwedge_{k<\omega}\mathrm{Q}_{m}^{k}(B^{*}(\sigma))$, it must be provable in $\mathrm{Q}_{m}^{k}(B^{*}(\sigma))$, for some $k<\omega$. Hence, we can infer

[TABLE]

By Lemma 6.1(ii) and (iii), each of $\mathrm{Q}_{m}^{k}(B)$ is $<_{n}$-below $A\circeq\Diamond_{m+1}B$ and is equivalent to a word in $\mathbb{W}_{n}$. Hence,

[TABLE]

By the reflexive induction hypothesis, for each $C<_{n}A$ we have

[TABLE]

(If $C=\top$ the claim holds trivially.) It follows that

[TABLE]

On the other hand, if $C<_{n}A$ then $A^{*}(\sigma)\leqslant\Diamond_{n}C^{*}(\sigma)$ and $\nabla_{n}A^{*}(\sigma)\leqslant\nabla_{n}\Diamond_{n}C^{*}(\sigma)\leqslant\Diamond_{n}C^{*}(\sigma)$. Hence,

[TABLE]

Thus, we have proved $\nabla_{n}A^{*}(\sigma)=\Diamond_{n}^{o_{n}(A)}(\sigma)$, as required. $\Box$

For ordinals $\alpha<\varepsilon_{0}$, let $\mathrm{A}^{n}_{\alpha}\in\mathbb{W}_{n}$ denote a canonical notation for $\alpha$ in the system $(\mathbb{W}_{n},<_{n})$. Thus, $o_{n}(\mathrm{A}^{n}_{\alpha})=\alpha$. We are going to show that the operations $\Diamond_{n}^{\alpha}$ are expressible in ${\mathrm{RC}^{\nabla}}$ in the following sense.

Theorem 9

For each $n<\omega$ and $0<\alpha<\varepsilon_{0}$ there is an $\mathrm{RC}$-formula $A(p)$ such that $\forall\sigma\in\mathfrak{G}_{\mathrm{EA}^{+}}\>\Diamond_{n}^{\alpha}(\sigma)=_{\mathrm{EA}^{+}}\nabla_{n}A^{*}(\sigma)$.

Proof. Take $A(p):=\mathrm{A}^{n}_{\alpha}[p/\top]$ and apply Theorem 8. $\Box$

7 Proof-theoretic $\Pi_{n+1}^{0}$-ordinals and conservativity spectra

Let $S$ be a Gödelian extension of $\mathrm{EA}^{+}$ and $(\Omega,<)$ a fixed elementary recursive well-ordering. In this section we additionally assume that $\Omega$ is an epsilon number and is equipped with elementary terms representing the ordinal constants and functions $0,1,+,\cdot,\omega^{x}$. These functions should provably in $\mathrm{EA}$ satisfy some minimal natural axioms NWO listed in [4]. We call such well-orderings nice. Recall the following definitions from [6] (writing $1$ for $1_{\mathrm{EA}^{+}}$):

• •

$\Pi_{n+1}^{0}$-ordinal of $S$, denoted $\mathrm{ord}_{n}(S)$, is the supremum of all $\alpha\in\Omega$ such that $S\vdash\mathrm{R}_{n}^{\alpha}(1)$;

• •

$S$ is $\Pi_{n+1}^{0}$-regular if $S$ is $\Pi_{n+1}^{0}$-conservative over $\mathrm{R}_{n}^{\alpha}(1)$, for some $\alpha\in\Omega$.

The following basic proposition states that $\Pi^{0}_{n+1}$-ordinals are insensitive to $\Pi^{0}_{n+1}$-conservative extensions and to extensions by consistent $\Sigma^{0}_{n+1}$-axioms.

Proposition 7.1

For any $S,T$ and a nice well-ordering $\Omega$, for all $n\in\omega$,

1. $\mathrm{(i)}$

If $S\vdash\Pi_{n+1}(T)$ then $\mathrm{ord}_{n}(S)\geqslant\mathrm{ord}_{n}(T)$; 2. $\mathrm{(ii)}$

*If $T$ is axiomatized by $\Sigma_{n+1}^{0}$-sentences and $S\cup T$ is consistent, then *

$\mathrm{ord}_{n}(S\cup T)=\mathrm{ord}_{n}(S)$.

Proof. The first claim follows from the fact that $\mathrm{R}_{n}^{\alpha}(1)$ is a $\Pi_{n+1}^{0}$-axiomatized theory. The second claim follows from the well-known result by Kreisel and Lévy [39] that $\mathrm{R}_{n}(U)$ is not contained in any consistent $\Sigma_{n+1}^{0}$-axiomatized extension of $U$. $\Box$

We refer the readers to [6] or [11] for an extended discussion of proof-theoretic $\Pi_{n+1}^{0}$-ordinals. In this paper we consider the sequences of $\Pi_{n+1}^{0}$-ordinals associated with a given system. Such sequences as objects of study first appeared in the work of Joost Joosten [36]. He showed for theories between $\mathrm{EA}^{+}$ and $\mathsf{PA}$ that their conservativity spectra correspond to decreasing sequences of ordinals below $\varepsilon_{0}$ of a certain kind, that is, to the points in the so-called Ignatiev frame. We reproduce this interesting characterization here in a slightly more general and streamlined way and also show its tight relationship with the fat normal forms for ${\mathrm{RC}^{\nabla}}$.

Definition 6

Conservativity spectrum of $S$ is the sequence $(\alpha_{0},\alpha_{1},\alpha_{2},\dots)$ such that $\alpha_{i}=\mathrm{ord}_{i}(S)$.

Here are some examples of theories and their spectra (the results are either well-known and/or can be found in [5]):

$I\Sigma_{1}:\ (\omega^{\omega},\omega,1,0,0,\dots)$;  $\mathsf{PRA}:\ (\omega^{\omega},\omega,0,0,0,\dots)$; 2. 2.

$\mathsf{PA}:\ (\varepsilon_{0},\varepsilon_{0},\varepsilon_{0},\dots)$;   $\mathsf{PA}+\mathrm{Con}(\mathsf{PA}):\ (\varepsilon_{0}\cdot 2,\varepsilon_{0},\varepsilon_{0},\dots)$ 3. 3.

$\mathsf{PA}+\mathrm{R}_{1}(\mathsf{PA}):\quad(\varepsilon_{0}^{2},\varepsilon_{0}\cdot 2,\varepsilon_{0},\varepsilon_{0},\dots)$.

We will need the following auxiliary lemma concerning the iterations of the reflection operators $\mathrm{R}_{n}$ on $\mathfrak{G}_{T}$, for any Gödelian extension $T$ of $\mathrm{EA}$.

Lemma 7.2

Let $(D,\preccurlyeq,0)$ be an elementary pre-wellordering, then for all $\sigma_{1},\sigma_{2}\in\mathfrak{G}_{T}$ there holds

[TABLE]

Proof. The proof is routine by reflexive induction on $\alpha$ using the $\mathrm{RC}$-identity

[TABLE]

$\Box$

The following proposition provides a necessary condition for a sequence of ordinals to be a conservativity spectrum.

Proposition 7.3

For any $S$ and a nice well-ordering $\Omega$, for all $n\in\omega$,

1. $\mathrm{(i)}$

$\mathrm{ord}_{n+1}(S)\leqslant\ell(\mathrm{ord}_{n}(S))$; 2. $\mathrm{(ii)}$

If $S$ is $\Pi_{n+1}^{0}$-regular and $n>0$, then $\forall i<n\>\mathrm{ord}_{i}(S)=\omega^{\mathrm{ord}_{i+1}(S)}$.

Proof. For (i) let $\vec{\alpha}$ denote the conservativity spectrum of $S$ and assume $\alpha_{n+1}>\ell(\alpha_{n})$. Select a $\gamma$ such that $\alpha_{n}=\gamma+\omega^{\ell(\alpha_{n})}$. Notice that

[TABLE]

Then by Lemma 7.2 we obtain

[TABLE]

By Theorem 3 of [6] we have:

[TABLE]

for all $\Pi_{n+1}$-axiomatized extensions $\sigma$ of $\mathrm{EA}^{+}$. Hence,

[TABLE]

It follows that $\alpha_{n}=\mathrm{ord}_{n}(S)\geqslant\gamma+\omega^{\alpha_{n+1}}$. On the other hand, by our assumption $\gamma+\omega^{\alpha_{n+1}}>\gamma+\omega^{\ell(\alpha_{n})}=\alpha_{n}$, a contradiction.

Since a $\Pi_{m}$-regular theory is $\Pi_{i}$-regular, for all $i<m$, it is sufficient to prove the claim for $i=n-1$. If $S$ is $\Pi_{n+1}^{0}$-regular, then $\mathrm{\Pi}_{n+1}(S)=\mathrm{R}_{n}^{\alpha}(1)$ where $\alpha=\mathrm{ord}_{n}(S)$. It follows that $\mathrm{\Pi}_{n}(S)=\mathrm{\Pi}_{n}(\mathrm{\Pi}_{n+1}(S))=\mathrm{\Pi}_{n}(\mathrm{R}_{n}^{\alpha}(1))=\mathrm{R}_{n-1}^{\omega^{\alpha}}(1)$. $\Box$

We consider the ordering of words $(\mathbb{W}_{i},<_{i})$ modulo equivalence in $\mathrm{RC}$ as a nice well-ordering of length $\varepsilon_{0}$. As before, the order type of a word $A_{i}$ within $(\mathbb{W}_{i},<_{i})$ is denoted $o_{i}(A_{i})$. A direct correspondence between fat normal forms and conservativity spectra is expressed by the following theorem.

Theorem 10

Let $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{k}A_{k},$ for some $k$, where $A_{n}\in\mathbb{W}_{n}$ for all $n\leqslant k$, be in the fat normal form. Let $A^{*}$ denote the interpretation of $A$ in $\mathfrak{G}_{\mathrm{EA}^{+}}$. Then, $A_{n}$ represents the $\Pi_{n+1}^{0}$-ordinal of $A^{*}$: $o_{n}(A_{n})=\mathrm{ord}_{n}(A^{*}).$ Moreover, $A^{*}$ is equivalent to the union of progressions, that is, in $\mathfrak{G}_{\mathrm{EA}^{+}}$

[TABLE]

Proof. Firstly, by applying Proposition 7.1 we observe that

[TABLE]

The first equality holds, because the deleted part of the normal form of $A$ is interpreted as a true $\Pi^{0}_{n}$-theory. The second equality holds, since the remaining part of the fat normal form of $A$ is $\Pi_{n+1}^{0}$-conservative over $A_{n}^{*}$:

[TABLE]

Then, by Theorem 8,

[TABLE]

hence $A_{n}^{*}$ is $\Pi_{n+1}^{0}$-regular and $\mathrm{ord}_{n}(A_{n}^{*})=o_{n}(A_{n})$. Moreover, equation (6) also yields representation (5) of $A^{*}$ as a union of progressions. $\Box$

Joosten [36] calls the representations of theories as the unions of Turing progressions Turing–Taylor expansions. Thus, the fat normal form of $A$ represents the Turing–Taylor expansion of $A^{*}$ by way of (5).

Notice that Theorem 10 also yields another way of showing that the fat normal form of $A$ is unique. We will come back to the topic of conservativity spectra after we discuss the Ignatiev frame and its associated ${\mathrm{RC}^{\nabla}}$-algebra.

8 Ignatiev frame and Ignatiev ${\mathrm{RC}^{\nabla}}$-algebra

In this and the following section we characterize in several ways the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$. It turns out that this structure is tightly related to the so-called Ignatiev’s Kripke frame. This frame, denoted here $\mathcal{I}$, has been introduced by Konstantin Ignatiev [33] as a universal frame for the variable-free fragment of Japaridze’s logic GLP. Later this frame has been slightly modified and studied in more detail in [16, 31]. In particular, Thomas Icard established a detailed relationship between $\mathcal{I}$ and the canonical frame for the variable-free fragment of $\mathrm{GLP}$ and used it to define a complete topological semantics for this fragment. David Fernández and Joost Joosten [24] generalized $\mathcal{I}$ to a version of GLP with transfinitely many modalities. Ignatiev’s frame is defined constructively (‘coordinatewise’) as follows.

Let $\bar{\mathrm{I}}$ denote the set of all $\omega$-sequences of ordinals $\vec{\alpha}=(\alpha_{0},\alpha_{1},\dots)$ such that $\alpha_{i}\leqslant\varepsilon_{0}$ and $\alpha_{i+1}\leqslant\ell(\alpha_{i})$, for all $i\in\omega$. Here, the function $\ell$ is defined by: $\ell(\beta)=0$ if $\beta=0$, and $\ell(\beta)=\gamma$ if $\beta=\delta+\omega^{\gamma}$, for some $\delta,\gamma$. Thus, all sequences of $\bar{\mathrm{I}}$, with the exception of identically $\varepsilon_{0}$, are eventually zero. Elements of $\bar{\mathrm{I}}$ will also be called $\ell$-sequences.

Relations $R_{n}$ on $\bar{\mathrm{I}}$ are defined by:

[TABLE]

The structure $\overline{\mathcal{I}}=(\bar{\mathrm{I}},(R_{n})_{n\in\omega})$ is called the extended Ignatiev frame (see [31]). The Ignatiev frame is its restriction to the subset $\mathrm{I}$ of all sequences $\vec{\alpha}\in\bar{\mathrm{I}}$ such that $\forall i\in\omega\>\alpha_{i}<\varepsilon_{0}$. This subset is upwards closed w.r.t. all relations $R_{n}$, hence the evaluation of the variable-free $\mathrm{RC}$-formulas (and $\mathrm{GLP}$-formulas) in $\mathcal{I}$ and in $\overline{\mathcal{I}}$ coincide. We denote by $\mathcal{I},\vec{\alpha}\Vdash\varphi$ the truth of a $\mathrm{GLP}$-formula $\varphi$ at a node $\vec{\alpha}$ of $\mathcal{I}$. If $\varphi$ is variable-free, the set $\{\vec{\alpha}\in\mathrm{I}:\mathcal{I},\vec{\alpha}\Vdash\varphi\}$ will be denoted $v(\varphi)$.

The following important theorem is a corollary of the results of Ignatiev but, in fact, has an easier direct proof (which we omit for the reasons of brevity).

Proposition 8.1

For any variable-free formulas $A,B$ of $\mathrm{RC}$, $A\vdash_{\mathrm{RC}}B$ iff $\mathcal{I},\vec{\alpha}\Vdash A\to B$, for all $\vec{\alpha}\in\mathrm{I}$.

The set of sequences $\vec{\alpha}\in\mathrm{I}$ such that $\forall i<\omega\>\alpha_{i+1}=\ell(\alpha_{i})$ is called the main axis of $\mathcal{I}$ and is denoted $\mathrm{O}$. Obviously, a sequence in $\mathrm{O}$ is uniquely determined by its initial element $\alpha_{0}$, hence $\mathrm{O}$ naturally corresponds to the ordinals up to $\varepsilon_{0}$. We can also associate with every word $A\in\mathbb{W}$ an element $\iota(A)\in\mathrm{O}$ by letting

[TABLE]

The following lemma, explicitly stated by Thomas Icard [31, Lemma 3.8] (see also another argument in [20, Lemma 10.2]), describes all the subsets of $\overline{\mathcal{I}}$ definable by words (and hence by all variable-free s.p. formulas of $\mathrm{RC}$).

Lemma 8.2

Suppose $A\in\mathbb{W}$ and $\vec{\alpha}=\iota(A)$. Then, for all $\vec{\beta}\in\overline{\mathcal{I}}$,  $\overline{\mathcal{I}},\vec{\beta}\Vdash A$ iff $\forall i\in\omega\>\alpha_{i}\leqslant\beta_{i}$.

Our goal is to transform $\mathcal{I}$ into an ${\mathrm{RC}^{\nabla}}$-algebra $\mathfrak{I}$ with the same domain $\mathrm{I}$, that is, into an SLO satisfying ${\mathrm{RC}^{\nabla}}$. We consider the set $\bar{\mathrm{I}}$ equipped with the ordering

[TABLE]

The structure $(\bar{\mathrm{I}},\leqslant_{\mathfrak{I}})$ can be seen as a subordering of the product ordering on the set of all $\omega$-sequences of ordinals $\leqslant\varepsilon_{0}$, which we denote ${\mathcal{E}}$.

A cone in ${\mathcal{E}}$ is the set of points $E_{\vec{\alpha}}:=\{\vec{\beta}\in{\mathcal{E}}:\vec{\beta}\leqslant_{\mathfrak{I}}\vec{\alpha}\}$, for some $\vec{\alpha}\in{\mathcal{E}}$. A sequence $\vec{\alpha}\in{\mathcal{E}}$ is called bounded if $\forall i\in\omega\>\alpha_{i}<\varepsilon_{0}$ and $\alpha_{i}\neq 0$ for only finitely many $i\in\omega$. Obviously, each $\vec{\alpha}\in\mathrm{I}$ is bounded.

Lemma 8.3

Suppose $\vec{\alpha}\in{\mathcal{E}}$ is bounded. Then $E_{\vec{\alpha}}\cap\mathrm{I}$ is not empty and has a greatest point $\vec{\beta}$ w.r.t. $\leqslant_{\mathfrak{I}}$.

Proof. Let $n\in\omega$ be the largest number such that $\alpha_{n}\neq 0$. Consider the sequence $\vec{\beta}$ such that $\beta_{i}=0$ for all $i>n$, $\beta_{n}:=\alpha_{n}$, and, for all $i<n$:

[TABLE]

It is easy to see that $\vec{\beta}$ is the greatest point of $E_{\vec{\alpha}}\cap\mathrm{I}$. Also notice that $\vec{\beta}$ can be effectively computed from $\vec{\alpha}$. $\Box$

Corollary 8.4

$(\mathrm{I},\leqslant_{\mathfrak{I}})$* is a meet-semilattice with top.*

Proof. Let $\vec{\alpha},\vec{\beta}\in\mathrm{I}$. The sequence $\vec{\gamma}:=(\max(\alpha_{i},\beta_{i}))_{i<\omega}$ is the g.l.b. of $\vec{\alpha}$ and $\vec{\beta}$ in ${\mathcal{E}}$ and is bounded. By Lemma 8.3, $E_{\vec{\gamma}}\cap\mathrm{I}$ has a greatest point, which has to be the g.l.b. of $\vec{\alpha}$ and $\vec{\beta}$ in $\mathrm{I}$. $\Box$

We denote by $\land_{\mathfrak{I}}$ the meet operation of this semilattice. A nonempty set $C_{\alpha}:=E_{\vec{\alpha}}\cap\mathrm{I}$ is called a cone in $\mathcal{I}$. The set of all cones in $\mathcal{I}$ ordered by inclusion is denoted $\mathrm{C}(\mathcal{I})$. The orderings $(\mathrm{C}(\mathcal{I}),\subseteq)$ and $(\mathrm{I},\leqslant_{\mathfrak{I}})$ are isomorphic by the map $\vec{\alpha}\mapsto C_{\vec{\alpha}}$. So, we have

Corollary 8.5

For all $\vec{\alpha},\vec{\beta}\in\mathrm{I}$, $C_{\vec{\alpha}\land_{\mathfrak{I}}\vec{\beta}}=C_{\vec{\alpha}}\cap C_{\vec{\beta}}$.

Let $\mathrm{C}(\mathrm{O})$ denote the set $\{C_{\vec{\alpha}}:\vec{\alpha}\in\mathrm{O}\}$ of all cones in $\mathcal{I}$ generated by the points of the main axis. For all $X\subseteq\bar{\mathrm{I}}$ define $R_{n}^{-1}(X):=\{y\in X:\exists x\in X\>yR_{n}x\}$. We claim that the operations $\cap$ and $R_{n}^{-1}$ map cones of $\mathrm{C}(\mathrm{O})$ to cones of $\mathrm{C}(\mathrm{O})$. Moreover, the following proposition holds.444We do not distinguish notationally an operation on a set and its restriction to a subset.

Proposition 8.6

The algebra $\mathfrak{C}(\mathrm{O})=(\mathrm{C}(\mathrm{O});\cap,\{R_{n}^{-1}:n\in\omega\})$ is isomorphic to the Lindenbaum–Tarski algebra $\mathfrak{L}^{0}_{\mathrm{RC}}$.

Proof. Let $v:\mathbb{F}\to{\mathcal{P}}(\mathrm{I})$ denote the map associating with every variable-free formula $A$ of $\mathrm{RC}$ the set $v(A)$ of all points where this formula is true. By the soundness and completeness of $\mathrm{RC}$ w.r.t. the Ignatiev model we have $v(A)=v(B)$ iff $A=_{\mathrm{RC}}B$. Moreover, by Lemma 8.2 the range of $v$ consists of all the cones of $\mathrm{C}(\mathrm{O})$. So, $v$ factors to a bijective map $\bar{v}:\mathfrak{L}^{0}_{\mathrm{RC}}\to\mathrm{C}(\mathrm{O})$. The operations $\cap$ and $R_{n}^{-1}$ correspond to the definition of truth in a Kripke model, hence $\mathrm{C}(\mathrm{O})$ is closed under these operations and $\bar{v}$ is an isomorphism of the respective algebras. $\Box$

We remark that the work of Pakhomov [41] shows that the elementary theory of the algebra $\mathfrak{L}^{0}_{\mathrm{RC}}$ is undecidable. We now define the structure of an ${\mathrm{RC}^{\nabla}}$-algebra on $\mathrm{I}$.

Definition 7

For all $n\in\omega$ we define the functions $\nabla_{n}^{\mathfrak{I}},\Diamond_{n}^{\mathfrak{I}}:\mathrm{I}\to\mathrm{I}$. For each element $\vec{\alpha}=(\alpha_{0},\alpha_{1},\dots,\alpha_{n},\dots)\in\mathrm{I}$ let:

$\nabla_{n}^{\mathfrak{I}}(\vec{\alpha}):=(\alpha_{0},\alpha_{1},\dots,\alpha_{n},0,\dots)$;

$\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha}):=(\beta_{0},\beta_{1},\dots,\beta_{n},0,\dots)$, where $\beta_{n+1}:=0$ and $\beta_{i}:=\alpha_{i}+\omega^{\beta_{i+1}}$, for all $i\leqslant n$.

The algebra $\mathfrak{I}=(\mathrm{I},\land_{\mathfrak{I}},\{\Diamond_{n}^{\mathfrak{I}},\nabla_{n}^{\mathfrak{I}}:n\in\omega\})$ is called the Ignatiev ${\mathrm{RC}^{\nabla}}$-algebra.

The definition of the operations $\Diamond_{n}^{\mathfrak{I}}$ is motivated by the following lemma and its corollary.

Lemma 8.7

Suppose $\vec{\alpha}\in\mathrm{I}$ and $\vec{\beta}=\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha})$. Then $\vec{\beta}\in\mathrm{O}$ and

1. $\mathrm{(i)}$

$C_{\vec{\beta}}=\bigcap_{i\leqslant n}R_{i}^{-1}(C_{\vec{\alpha}})$; 2. $\mathrm{(ii)}$

If $\vec{\alpha}\in\mathrm{O}$ then $C_{\vec{\beta}}=R_{n}^{-1}(C_{\vec{\alpha}}).$

Proof. (i) It is easy to see that each of the sets $R_{i}^{-1}(C_{\vec{\alpha}})$, for $i\leqslant n$, is a cone in $\mathcal{I}$ generated by the bounded sequence $(\alpha_{0},\dots,\alpha_{i-1},\alpha_{i}+1,0,\dots)$ from ${\mathcal{E}}$. Hence, the intersection of these cones is a cone generated by $(\alpha_{0}+1,\dots,\alpha_{n-1}+1,\alpha_{n}+1,0,\dots)$. Its greatest element in $\mathrm{I}$ obviously coincides with $\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha})$.

(ii) Clearly, $\vec{\beta}\in R_{n}^{-1}(C_{\vec{\alpha}})$, since $\vec{\beta}^{\prime}:=(\beta_{0},\beta_{1},\dots,\beta_{n-1},\alpha_{n},\alpha_{n+1},\dots)$ satisfies $\vec{\beta}R_{n}\vec{\beta}^{\prime}$ and $\vec{\beta}^{\prime}\leqslant_{\mathfrak{I}}\vec{\alpha}$. In the opposite direction, show by downward induction on $i\leqslant n$ that if $\vec{\gamma}\in R_{n}^{-1}(C_{\vec{\alpha}})$ then $\gamma_{i}\geqslant\beta_{i}$. For $i=n$ the claim is obvious. Assume $i<n$, then $\gamma_{i}\geqslant\alpha_{i}$. Since $\ell(\gamma_{i})\geqslant\gamma_{i+1}\geqslant\beta_{i+1}$ and $\ell(\alpha_{i})=\alpha_{i+1}<\beta_{i+1}$, we must also have $\gamma_{i}\geqslant\alpha_{i}+\omega^{\beta_{i+1}}=\beta_{i}$. $\Box$

Corollary 8.8

$\mathfrak{C}(\mathrm{O})$* is isomorphic to the algebra $\mathfrak{O}=(\mathrm{O},\land_{\mathfrak{I}},\{\Diamond_{n}^{\mathfrak{I}}:n\in\omega\})$.*

Proof. Consider the bijection $c:\vec{\alpha}\longmapsto C_{\vec{\alpha}}$ from $\mathrm{O}$ to $\mathrm{C}(\mathrm{O})$. By Corollary 8.5 this map preserves the meet, and by Lemma 8.7 it preserves the diamond modalities. $\Box$

We summarize the previous results in the following theorem characterizing the Lindenbaum–Tarski algebra of the variable-free fragment of $\mathrm{RC}$.

Theorem 11

The algebras $\mathfrak{L}_{\mathrm{RC}}^{0}$, $\mathfrak{C}(\mathrm{O})$, $\mathfrak{O}$ are naturally isomorphic by the following maps:

1. $\mathrm{(i)}$

$\bar{v}:\mathfrak{L}_{\mathrm{RC}}^{0}\to\mathfrak{C}(\mathrm{O})$; 2. $\mathrm{(ii)}$

$c:\mathfrak{O}\to\mathfrak{C}(\mathrm{O})$; 3. $\mathrm{(iii)}$

$\bar{\iota}:\mathfrak{L}_{\mathrm{RC}}^{0}\to\mathfrak{O}$.

Here, for any $A\in\mathbb{F}$, $\bar{\iota}([A]_{\mathrm{RC}}):=\iota(A^{\prime})$, where $A^{\prime}\in\mathbb{W}$ is a word such that $A=_{\mathrm{RC}}A^{\prime}$. This definition is invariant, since, for any words $A^{\prime},A^{\prime\prime}$, if $A^{\prime}=_{\mathrm{RC}}A^{\prime\prime}$ then $o(A^{\prime})=o(A^{\prime\prime})$ and hence $\iota(A^{\prime})=\iota(A^{\prime\prime})$. For a proof that (iii) is an isomorphism it is sufficient to remark that $v(A)=c(\iota(A))$, for each $A\in\mathbb{W}$, by Lemma 8.2.

Our next goal is to show that $\mathfrak{I}$ is isomorphic to the Lindenbaum–Tarski algebra of ${\mathrm{RC}^{\nabla}}$. First, we need an auxiliary lemma.

Lemma 8.9

For every $\vec{\alpha}\in\mathrm{I}$ and $n\in\omega$, there is an $\vec{\alpha}^{\prime}\in\mathrm{O}$ such that $\vec{\alpha}^{\prime}\leqslant_{\mathfrak{I}}\vec{\alpha}$ and $\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha})=\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha}^{\prime})$.

Proof. Let $\alpha_{n}^{\prime}:=\alpha_{n}$, $\forall i\geqslant n\>\alpha^{\prime}_{i+1}:=\ell(\alpha^{\prime}_{i})$, and $\forall i<n\>\alpha^{\prime}_{i}:=\alpha_{i}+\omega^{\alpha^{\prime}_{i+1}}$. It is easy to check that $\vec{\alpha}^{\prime}$ is as required. $\Box$

Let $A^{\mathfrak{I}}$ denote the value of a variable-free ${\mathrm{RC}^{\nabla}}$-formula $A$ in $\mathfrak{I}$. The following lemma shows that $\mathfrak{I}$ satisfies the variable-free fragment of ${\mathrm{RC}^{\nabla}}$.

Lemma 8.10

For any $A,B\in\mathbb{F}^{\nabla}$, $A\vdash_{{\mathrm{RC}^{\nabla}}}B$ implies $A^{\mathfrak{I}}\leqslant_{\mathfrak{I}}B^{\mathfrak{I}}$.

Proof. We argue by induction on the length of ${\mathrm{RC}^{\nabla}}$-derivation. In almost all the cases the proof is routine. We consider the nontrivial case of the axiom $\Diamond_{n}A\land\Diamond_{m}B\vdash\Diamond_{n}(A\land\Diamond_{m}B)$ for $m<n$. Let $\vec{\alpha}=A^{\mathfrak{I}}$ and $\vec{\beta}=B^{\mathfrak{I}}$. Using Lemma 8.9 we obtain $\vec{\alpha}^{\prime},\vec{\beta}^{\prime}\in\mathrm{O}$ such that $\vec{\alpha}^{\prime}\leqslant_{\mathfrak{I}}\vec{\alpha}$, $\vec{\beta}^{\prime}\leqslant_{\mathfrak{I}}\vec{\beta}$ and $\Diamond^{\mathfrak{I}}_{n}\vec{\alpha}=\Diamond^{\mathfrak{I}}_{n}\vec{\alpha}^{\prime}$, $\Diamond^{\mathfrak{I}}_{m}\vec{\beta}=\Diamond^{\mathfrak{I}}_{m}\vec{\beta}^{\prime}$. By Theorem 11 the algebra $\mathfrak{O}$ satisfies $\mathrm{RC}$, hence

[TABLE]

Therefore, $\Diamond^{\mathfrak{I}}_{n}\vec{\alpha}\land_{\mathfrak{I}}\Diamond^{\mathfrak{I}}_{m}\vec{\beta}\leqslant_{\mathfrak{I}}\Diamond^{\mathfrak{I}}_{n}(\vec{\alpha}^{\prime}\land_{\mathfrak{I}}\Diamond^{\mathfrak{I}}_{m}\vec{\beta})\leqslant_{\mathfrak{I}}\Diamond^{\mathfrak{I}}_{n}(\vec{\alpha}\land_{\mathfrak{I}}\Diamond^{\mathfrak{I}}_{m}\vec{\beta}).$ The second inequality holds by the monotonicity of $\land_{\mathfrak{I}}$ and $\Diamond^{\mathfrak{I}}_{n}$. $\Box$

Lemma 8.11

Suppose $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{n}A_{n}$ is in the fat normal form. Then $A^{\mathfrak{I}}=(o_{0}(A_{0}),o_{1}(A_{1}),\dots,o_{n}(A_{n}),0,\dots)$.

Proof. Firstly, since each $A_{i}\in\mathbb{W}_{i}$ we obtain from Theorem 11 that

[TABLE]

where by definition $\omega_{0}(\alpha)=\alpha$ and $\omega_{k+1}(\alpha)=\omega^{\omega_{k}(\alpha)}$. Hence,

[TABLE]

Denote $\overline{A_{i}}:=\nabla_{i}A_{i}\land\nabla_{i+1}A_{i+1}\land\dots\land\nabla_{n}A_{n}$. By downwards induction on $i\leqslant n$ we show that $(\overline{A_{i}})^{\mathfrak{I}}$ equals

[TABLE]

For $i=n$ the claim follows from the above. Assume $i<n$ and that the claim holds for $i+1$. Since in a fat normal form

[TABLE]

by Lemma 8.10 we obtain that the sequence $(\nabla_{i}A_{i})^{\mathfrak{I}}$ coordinatewise majorizes the sequence $(\nabla_{i}(\nabla_{i}A_{i}\land\nabla_{i+1}A_{i+1}))^{\mathfrak{I}}$. The former has the ordinal $o_{i}(A_{i})$ at $i$-th position, and the latter has at the same place the least ordinal $\alpha$ such that $\alpha\geqslant o_{i}(A_{i}),\omega^{o_{i+1}(A_{i+1})}$ and $\ell(\alpha)\geqslant o_{i+1}(A_{i+1})$. Therefore, $o_{i}(A_{i})=\alpha$ and $\ell(o_{i}(A_{i}))\geqslant o_{i+1}(A_{i+1})$.

Now consider the sequence $(\overline{A_{i}})^{\mathfrak{I}}=(\nabla_{i}A_{i}\land\overline{A_{i+1}})^{\mathfrak{I}}$. By the induction hypothesis its tail coincides with that of (7) starting from position $i+1$. Since $\ell(o_{i}(A_{i}))\geqslant o_{i+1}(A_{i+1})$, the ordinal $o_{i}(A_{i})$ occurs in it on $i$-th position. Also, for each $k<i$ we have $\omega_{k}(o_{i}(A_{i}))\geqslant\omega_{k}(\omega^{o_{i+1}(A_{i+1})})$. It follows that the sequence $(\overline{A_{i}})^{\mathfrak{I}}$ coincides with (7). $\Box$

The following corollary will be useful later on.

Corollary 8.12

For any $A,B\in\mathbb{W}$ and $n\in\omega$, if $\mathfrak{I}\vDash\nabla_{n}A=\nabla_{n}B$ then $A=_{\mathrm{RC}}B$.

Proof. Firstly, we infer: $\mathfrak{I}\vDash\nabla_{0}A=\nabla_{0}\nabla_{n}A=\nabla_{0}\nabla_{n}B=\nabla_{0}B$. By Lemma 8.11 we conclude $o(A)=o(B)$, therefore $A=_{\mathrm{RC}}B$. $\Box$

Theorem 12

For all $A,B\in\mathbb{F}^{\nabla}$, $A\vdash_{\mathrm{RC}^{\nabla}}B$ iff $A^{\mathfrak{I}}\leqslant_{\mathfrak{I}}B^{\mathfrak{I}}$.

Proof. We must only prove the ‘only if’ part. Moreover, it is sufficient to prove it for fat normal forms $A\circeq\nabla_{0}A_{0}\land\nabla_{1}A_{1}\land\dots\land\nabla_{n}A_{n}$ and $B\circeq\nabla_{0}B_{0}\land\nabla_{1}B_{1}\land\dots\land\nabla_{m}B_{m}$. If $A^{\mathfrak{I}}\leqslant_{\mathfrak{I}}B^{\mathfrak{I}}$ then by Lemma 8.11 we have $n\geqslant m$ and $o_{i}(A_{i})\geqslant o_{i}(B_{i})$, for each $i\leqslant m$. Since $A_{i},B_{i}\in\mathbb{W}_{i}$, this means that $A_{i}\vdash_{\mathrm{RC}}\Diamond_{i}B_{i}$ or $A_{i}=_{\mathrm{RC}}B_{i}$. In either case we can infer $\nabla_{i}A_{i}\vdash_{\mathrm{RC}^{\nabla}}\nabla_{i}B_{i}$ for each $i\leqslant m$. It follows that $A\vdash_{\mathrm{RC}^{\nabla}}B$. $\Box$

Theorem 12 essentially means the following.

Corollary 8.13

The Ignatiev ${\mathrm{RC}^{\nabla}}$-algebra $\mathfrak{I}$ is isomorphic to the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$.

9 $\mathfrak{I}$ as the algebra of variable-free $\mathrm{RC}$-theories

Another, perhaps even more natural, view of the Ignatiev ${\mathrm{RC}^{\nabla}}$-algebra is via an interpretation of the points of $\mathcal{I}$ as variable-free $\mathrm{RC}$-theories. It nicely agrees with the arithmetical interpretation in that we can also view such a theory as an arithmetical theory (every variable-free $\mathrm{RC}$-formula corresponds to an arithmetical sentence). In this section we will presuppose that the language is variable-free and will only consider variable-free formulas and theories.

A set of strictly positive formulas $T$ is called an $\mathrm{RC}$-theory if $B\in T$ whenever there are $A_{1},\dots,A_{n}\in T$ such that $A_{1}\land\dots\land A_{n}\vdash_{\mathrm{RC}}B$. A theory $T$ is called improper if $T$ coincides with the set of all strictly positive formulas, otherwise it is called proper.555We avoid the term ‘consistent’, for even the improper theory corresponds to a consistent set of arithmetical sentences. A theory is called bounded if there is a strictly positive formula $A$ such that $T\subseteq\{B:A\vdash_{\mathrm{RC}}B\}$. We will use the following basic fact.

The set $\bar{\mathrm{I}}$ bears a natural topology generated as a subbase by the set of all cones in $\overline{\mathcal{I}}$ and their complements. By [31, Theorem 3.12], this topology coincides with the product topology of the space ${\mathcal{E}}$ induced on $\bar{\mathrm{I}}$. Obviously, for each $\mathrm{RC}$-formula $A$, the set $v(A)$ is clopen. Moreover, this topology is compact and totally disconnected on $\bar{\mathrm{I}}$, since $\bar{\mathrm{I}}$ is closed in ${\mathcal{E}}$ and ${\mathcal{E}}$ is compact by Tychonoff theorem. As a corollary we obtain the following strong completeness result. For each $\mathrm{RC}$-theory $T$ define $v(T):=\{\vec{\alpha}\in\mathrm{I}:\mathcal{I},\vec{\alpha}\Vdash T\}$.

Proposition 9.1

Let $T$ be an $\mathrm{RC}$-theory and $A$ an $\mathrm{RC}$-formula.

1. $\mathrm{(i)}$

$T\nvdash_{\mathrm{RC}}A$* iff there is an $\vec{\alpha}\in\overline{\mathcal{I}}$ such that $\overline{\mathcal{I}},\vec{\alpha}\Vdash T$ and $\overline{\mathcal{I}},\vec{\alpha}\nVdash A$;* 2. $\mathrm{(ii)}$

If $T$ is bounded then $T\nvdash_{\mathrm{RC}}A$ iff there is an $\vec{\alpha}\in\mathcal{I}$ such that $\mathcal{I},\vec{\alpha}\Vdash T$ and $\mathcal{I},\vec{\alpha}\nVdash A$.

Proof. (i) The nontrivial implication is from left to right. Assume $T\nvdash_{\mathrm{RC}}A$. There is an increasing sequence of finite theories $(T_{n})_{n\in\omega}$ such that $T=\bigcup_{n\in\omega}T_{n}$. By the completeness of the variable-free fragment of $\mathrm{RC}$ w.r.t. $\mathcal{I}$ each of the sets $v(T_{n})\setminus v(A)$ is nonempty and clopen. By the compactness of $\bar{\mathrm{I}}$ there is a point $\vec{\alpha}\in\bigcap_{n\in\omega}v(T_{n})\setminus v(A)=v(T)\setminus v(A)$.

(ii) In case $T$ is bounded we have $v(T)\supseteq v(B)$, for some word $B$. There is a bounded sequence $\vec{\beta}\in{\mathcal{E}}$ such that $v(T)=E_{\vec{\beta}}\cap\bar{\mathrm{I}}$: consider the pointwise supremum of the generating points of the cones $v(T_{n})$ in $\overline{\mathcal{I}}$, each of which is pointwise majorized by the greatest element $B^{\mathfrak{I}}$ of $v(B)$. By Lemma 8.3, the set $v(T)$ has a greatest point, say $\vec{\gamma}\in\mathrm{I}$. Since $\vec{\alpha}\in v(T)$ we have $\vec{\alpha}\leqslant_{\mathfrak{I}}\vec{\gamma}$, hence $\mathcal{I},\vec{\gamma}\nVdash A$. $\Box$

For any $\mathrm{RC}$-theories $T,S$ define $T\leqslant_{\mathrm{RC}}S$ iff $T\supseteq S$. The g.l.b. of $T$ and $S$ in this ordering, denoted $T\land_{\mathrm{RC}}S$, is the theory generated by the union $T\cup S$. Thus, the set $\mathfrak{T}^{0}_{\mathrm{RC}}$ of all bounded variable-free $\mathrm{RC}$-theories is a semilattice (it is, in fact, a lattice with $T\cap S$ the l.u.b. of $T$ and $S$). The set $\{A\in\mathbb{F}:\top\vdash_{\mathrm{RC}}A\}$ corresponds to the top of this lattice and is denoted $\top_{\mathrm{RC}}$.

For each $\vec{\alpha}\in\overline{\mathcal{I}}$ define an $\mathrm{RC}$-theory $[\vec{\alpha}]:=\{A:\overline{\mathcal{I}},\vec{\alpha}\Vdash A\}$. It is easy to see that $[\vec{\alpha}]$ is bounded if $\vec{\alpha}\in\mathrm{I}$ (consider the point $\vec{\beta}$ on the main axis of $\mathcal{I}$ such that $\vec{\beta}\leqslant_{\mathfrak{I}}\vec{\alpha}$ and a word $B$ such that $\iota(B)=\vec{\beta}$).

Proposition 9.2

1. $\mathrm{(i)}$

The map $\vec{\alpha}\mapsto[\vec{\alpha}]$ is an isomorphism between $(\mathcal{I},\leqslant_{\mathfrak{I}})$ and the ordered set $\mathfrak{T}^{0}_{\mathrm{RC}}$ of bounded $\mathrm{RC}$-theories. 2. $\mathrm{(ii)}$

The map $v$ is an isomorphism between $\mathfrak{T}^{0}_{\mathrm{RC}}$ and the ordered set $(\mathrm{C}(\mathcal{I}),\subseteq)$ of cones in $\mathcal{I}$.

Proof. It is sufficient to prove that

1. (a)

The maps $\vec{\alpha}\mapsto[\vec{\alpha}]$ and $T\mapsto v(T)$ are order-preserving; 2. (b)

$\forall\vec{\alpha}\in\mathrm{I}\>v([\vec{\alpha}])=C_{\vec{\alpha}}$; 3. (c)

If $v(T)=C_{\vec{\alpha}}$ then $T=[\vec{\alpha}]$.

Item (a) is obvious. For (b) we observe:

[TABLE]

The right hand side is equivalent to $\vec{\beta}\leqslant_{\mathfrak{I}}\vec{\alpha}$: If $\vec{\beta}\leqslant_{\mathfrak{I}}\vec{\alpha}$ and $\mathcal{I},\vec{\alpha}\Vdash A$ then $\mathcal{I},\vec{\beta}\Vdash A$ by Proposition 8.2. If $\vec{\beta}\nleqslant_{\mathfrak{I}}\vec{\alpha}$ then there is a word $A$ such that $\mathcal{I},\vec{\alpha}\Vdash A$ and $\mathcal{I},\vec{\beta}\nVdash A$, by [31, Corollary 3.9]. Hence, $\vec{\beta}\in v([\vec{\alpha}])$ iff $\vec{\beta}\in C_{\vec{\alpha}}$.

For (c) we use Proposition 9.1. Suppose $\vec{\alpha}\in\mathrm{I}$ and $v(T)=C_{\vec{\alpha}}$. Then $\mathcal{I},\vec{\alpha}\Vdash T$ and thus $T\subseteq[\vec{\alpha}]$. For the opposite inclusion assume $A\in[\vec{\alpha}]$ and $A\notin T$. By Proposition 9.1 there is a node $\vec{\beta}\in\mathrm{I}$ such that $\mathcal{I},\vec{\beta}\Vdash T$ and $\mathcal{I},\vec{\beta}\nVdash A$. Thus, $\vec{\beta}\in v(T)$ and, since $v(A)$ is downwards closed, $\vec{\beta}\nleqslant_{\mathfrak{I}}\vec{\alpha}$. It follows that $v(T)\nsubseteq C_{\vec{\alpha}}$. $\Box$

The operations of the Ignatiev ${\mathrm{RC}^{\nabla}}$-algebra can be interpreted in terms of the semilattice of bounded theories as follows. For each $T\in\mathfrak{T}^{0}_{\mathrm{RC}}$ let $\nabla_{n}^{\mathrm{RC}}T$ denote the $\mathrm{RC}$-theory axiomatized by $\{\Diamond_{m}A:\Diamond_{m}A\in T\text{ and }m\leqslant n\}.$

Lemma 9.3

For all $\vec{\alpha}\in\mathfrak{I}$, $\nabla^{\mathrm{RC}}_{n}([\vec{\alpha}])=[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$.

Proof. For the inclusion $(\subseteq)$ we need to show: if $m\leqslant n$ and $\Diamond_{m}A\in[\vec{\alpha}]$ then $\Diamond_{m}A\in[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$. If $\Diamond_{m}A\in[\vec{\alpha}]$ then $\mathcal{I},\vec{\alpha}\Vdash\Diamond_{m}A$, hence there is a $\vec{\beta}$ such that $\vec{\alpha}R_{m}\vec{\beta}$ and $\mathcal{I},\vec{\beta}\Vdash A$. So, we have $\forall i<m\>\,\alpha_{i}=\beta_{i}$ and $\alpha_{m}>\beta_{m}$. Since $m\leqslant n$, the node $\nabla^{\mathfrak{I}}_{n}\vec{\alpha}$ has the same coordinates as $\vec{\alpha}$ for all $i\leqslant m$. Therefore, $(\nabla^{\mathfrak{I}}_{n}\vec{\alpha})R_{m}\vec{\beta}$ and $\mathcal{I},(\nabla^{\mathfrak{I}}_{n}\vec{\alpha})\Vdash\Diamond_{m}A$.

For the inclusion $(\supseteq)$ we consider any node $\vec{\gamma}\in\mathrm{I}$ such that $\mathcal{I},\vec{\gamma}\Vdash\nabla^{\mathrm{RC}}_{n}[\vec{\alpha}]$ and show that $\mathcal{I},\vec{\gamma}\Vdash[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$. This means that $v(\nabla^{\mathrm{RC}}_{n}[\vec{\alpha}])\subseteq v([\nabla^{\mathfrak{I}}_{n}\vec{\alpha}])$ and hence $\nabla^{\mathrm{RC}}_{n}([\vec{\alpha}])\supseteq[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$ by Proposition 9.2.

Assume $\mathcal{I},\vec{\gamma}\nVdash[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$. Since $v(\nabla_{n}^{\mathfrak{I}}\vec{\alpha})=C_{\nabla_{n}^{\mathfrak{I}}\vec{\alpha}}$ we have $\vec{\gamma}\notin C_{\nabla_{n}^{\mathfrak{I}}\vec{\alpha}}$, hence there is an $m\leqslant n$ such that $\gamma_{m}<\alpha_{m}$. Consider a word $A\in\mathbb{W}_{m}$ such that $o_{m}(A)=\gamma_{m}$. Recall that the point on the main axis corresponding to $A$ is $\iota(A)=(\omega_{m}(\gamma_{m}),\dots,\omega^{\gamma_{m}},\gamma_{m},\ell(\gamma_{m}),\dots)$.

We claim that $\mathcal{I},\vec{\gamma}\nVdash\Diamond_{m}A$, whereas $\mathcal{I},\vec{\alpha}\Vdash\Diamond_{m}A$. The former holds, since for all $\vec{\delta}$ such that $\vec{\gamma}R_{m}\vec{\delta}$ one has $\delta_{m}<\gamma_{m}$, hence $\vec{\delta}\nleqslant_{\mathfrak{I}}\iota(A)$ and $\mathcal{I},\vec{\delta}\nVdash A$. On the other hand, $\mathcal{I},\vec{\alpha}\Vdash\Diamond_{m}A$ holds, since there is a sequence $\vec{\alpha}^{\prime}:=(\alpha_{0},\ldots,\alpha_{m-1},\gamma_{m},\gamma_{m+1},\dots)$ such that $\vec{\alpha}R_{m}\vec{\alpha}^{\prime}$ and $\mathcal{I},\vec{\alpha}^{\prime}\Vdash A$.

To show that $\vec{\alpha}^{\prime}\leqslant_{\mathfrak{I}}\iota(A)$ we prove that $\forall i\leqslant m\>\omega_{m-i}(\gamma_{m})\leqslant\alpha_{i}$ by downward induction on $i\leqslant m$. Assume the claim holds for some $i$ such that $0<i\leqslant m$. Then $\alpha_{i-1}\geqslant\omega^{\ell(\alpha_{i-1})}\geqslant\omega^{\alpha_{i}}\geqslant\omega^{\gamma_{i}}=\gamma_{i-1}$. $\Box$

In order to define the operations $\Diamond^{\mathrm{RC}}_{n}$ on the set of bounded $\mathrm{RC}$-theories we need a few definitions. An $\mathrm{RC}$-theory $T$ is of level $n$ if $T$ is generated by a (nonempty) set of formulas $\Diamond_{n}A$ such that $A\in\mathbb{W}_{n}$. A theory $T$ is of level at least $n$ if it is generated by a (nonempty) subset of $\mathbb{W}_{n}\setminus\{\top\}$.

Lemma 9.4

Every bounded $\mathrm{RC}$-theory $T$ is representable in the form $T=T_{0}\land_{\mathrm{RC}}T_{1}\land_{\mathrm{RC}}\dots\land_{\mathrm{RC}}T_{n}$ where each $T_{i}$ is of level $i$ or $T_{i}=\top_{\mathrm{RC}}$.

Proof. Recall that every $\mathrm{RC}$-formula is $\mathrm{RC}$-equivalent to an ordered formula. Moreover, every variable-free $\mathrm{RC}$-formula in which only the modalities $\Diamond_{i}$ with $i\geqslant m$ occur is equivalent to a word in $\mathbb{W}_{m}$. Hence, every formula is equivalent to a conjunction of formulas of the form $\Diamond_{i}A$ with $A\in\mathbb{W}_{i}$. Since $T$ is bounded, the set of indices of modalities occurring in the axioms of $T$ is bounded, say by $n$. Hence, each axiom of $T$ can be replaced by a finite set of formulas of various levels below $n$ and one can partition the union of all these axioms into the disjoint subsets of the same level. $\Box$

Lemma 9.5

For each $\vec{\alpha}\in\mathrm{I}$ such that $\alpha_{n}>0$, the theory generated by $[\vec{\alpha}]\cap\mathbb{W}_{n}$ corresponds to the sequence $\vec{\alpha}^{\prime}:=(\omega_{n}(\alpha_{n}),\dots,\omega^{\alpha_{n}},\alpha_{n},\alpha_{n+1},\dots)$.

We remark that if $\alpha_{n}=0$ then the theory generated by $[\vec{\alpha}]\cap\mathbb{W}_{n}$ is $\top_{\mathrm{RC}}$.

Proof. Let $T$ be the theory generated by $[\vec{\alpha}]\cap\mathbb{W}_{n}$. We consider a $\vec{\beta}\in\mathrm{I}$ such that $[\vec{\beta}]=T$ and show that $\vec{\beta}=\vec{\alpha}^{\prime}$. It is easy to see that $\vec{\alpha}\leqslant_{\mathfrak{I}}\vec{\alpha}^{\prime}$ and that the submodel of $\mathcal{I}$ generated from $\vec{\alpha}$ by the relations $R_{k}$, for all $k\geqslant n$, is isomorphic to the submodel generated by these relations from $\vec{\alpha}^{\prime}$. Hence, if $B$ is a formula in which only the modalities $\Diamond_{k}$ with $k\geqslant n$ occur, then $\mathcal{I},\vec{\alpha}\Vdash B$ holds iff $\mathcal{I},\vec{\alpha}^{\prime}\Vdash B$. It follows that $[\vec{\alpha}]\cap\mathbb{W}_{n}\subseteq[\vec{\alpha}^{\prime}]$, that is, $\vec{\alpha}^{\prime}\leqslant_{\mathfrak{I}}\vec{\beta}$.

Now assume $\vec{\alpha}^{\prime}<_{\mathfrak{I}}\vec{\beta}$, so there is a $k\in\omega$ such that $\beta_{k}<\alpha^{\prime}_{k}$. If $k<n$ then $\beta_{k}<\omega_{n-k}(\alpha_{n})$. For all ordinals $\gamma,\delta$, if $\gamma<\omega^{\delta}$ then $\ell(\gamma)<\delta$. Then, by induction, for all $i=k,\dots,n$ we obtain $\beta_{i}<\omega_{n-i}(\alpha_{n})$. Ergo $\beta_{n}<\alpha_{n}$.

So, we may assume that $k\geqslant n$. In this case consider a word $B\in\mathbb{W}_{k}$ such that $o_{k}(B)=\beta_{k}+1$. Then,

[TABLE]

We have $\mathcal{I},\vec{\beta}\nVdash B$, since $\beta_{k}+1>\beta_{k}$. On the other hand,

[TABLE]

which is easy to see by induction on $i$. It follows that $\mathcal{I},\vec{\alpha}\Vdash B$, therefore $[\vec{\beta}]\neq T$, a contradiction.$\Box$

Corollary 9.6

For each $\vec{\alpha}\in\mathrm{I}$, $[\vec{\alpha}]$ is of level at least $n$ iff $\alpha_{n}>0$ and

[TABLE]

Lemma 9.7

For each bounded $\mathrm{RC}$-theory $T$ of level at least $n$, there is an $\mathrm{RC}$-formula $A\in\mathbb{W}_{n}$ such that $\nabla^{\mathrm{RC}}_{n}A=\nabla^{\mathrm{RC}}_{n}T$ holds in $\mathfrak{T}^{0}_{\mathrm{RC}}$.

Proof. Suppose $T=[\vec{\alpha}]$ is of level at least $n$. Let $A\in\mathbb{W}_{n}$ be such that $o_{n}(A)=\alpha_{n}>0$. Then, by Lemma 9.3, $\nabla^{\mathrm{RC}}_{n}(T)=\nabla^{\mathrm{RC}}_{n}([\vec{\alpha}])=[\nabla^{\mathfrak{I}}_{n}\vec{\alpha}]$. By (8) we have

[TABLE]

On the other hand, $\iota(A)=(\omega_{n}(\alpha_{n}),\omega_{n-1}(\alpha_{n}),\dots,\alpha_{n},\ell(\alpha_{n}),\dots),$ and we obtain $\nabla^{\mathrm{RC}}_{n}A=[\nabla^{\mathfrak{I}}_{n}(\iota(A))]=[(\omega_{n}(\alpha_{n}),\omega_{n-1}(\alpha_{n}),\dots,\alpha_{n},0,\dots)]$. Proposition 9.2 yields the result. $\Box$

Now we can give the following definition of the theory $\Diamond^{\mathrm{RC}}_{n}T$, for each bounded $\mathrm{RC}$-theory $T$.

If $T$ is of level at least $n$ or $T=\top_{\mathrm{RC}}$, we let $\Diamond^{\mathrm{RC}}_{n}T$ be the theory generated by the formula $\Diamond_{n}A$, where $A\in\mathbb{W}_{n}$ is such that $\nabla^{\mathrm{RC}}_{n}A=\nabla^{\mathrm{RC}}_{n}T$ in $\mathfrak{T}_{\mathrm{RC}}^{0}$. (Notice that this definition is correct, since any two words $A_{1},A_{2}$ satisfying $\nabla^{\mathrm{RC}}_{n}A_{1}=\nabla^{\mathrm{RC}}_{n}A_{2}$ in $\mathfrak{T}_{\mathrm{RC}}^{0}$ also satisfy $\Diamond_{n}A_{1}=_{\mathrm{RC}}\Diamond_{n}A_{2}$ by Corollary 8.12.)

For each $i\leqslant n$, let $T_{i}$ denote the theory generated by $T\cap\mathbb{W}_{i}$. We define

[TABLE]

The following lemma shows that this definition agrees with the operations on the Ignatiev algebra.

Lemma 9.8

For all $\vec{\alpha}\in\mathfrak{I}$, $\Diamond^{\mathrm{RC}}_{n}([\vec{\alpha}])=[\Diamond^{\mathfrak{I}}_{n}(\vec{\alpha})]$.

Proof. If $T=[\vec{\alpha}]$ then by Lemma 9.5, for each $i\leqslant n$, either the theory $T_{i}:=T\cap\mathbb{W}_{i}$ is $\top_{\mathrm{RC}}$ or corresponds to the sequence $\vec{\alpha}^{\prime}:=(\omega_{i}(\alpha_{i}),\dots,\omega^{\alpha_{i}},\alpha_{i},\alpha_{i+1},\dots)$ with $\alpha_{i}>0$. If $T_{i}=\top_{\mathrm{RC}}$ we have $\Diamond_{i}^{\mathrm{RC}}T_{i}=\Diamond_{i}\top$. Otherwise, $\Diamond^{\mathrm{RC}}_{i}T_{i}=\Diamond_{i}A_{i}$ where $A_{i}$ corresponds to $(\omega_{i}(\alpha_{i}),\dots,\omega^{\alpha_{i}},\alpha_{i},\ell(\alpha_{i}),\dots)$. In both cases

[TABLE]

Then we observe that $\Diamond^{\mathrm{RC}}_{n}(T)=\Diamond^{\mathrm{RC}}_{0}(T_{0})\land_{\mathrm{RC}}\Diamond^{\mathrm{RC}}_{1}(T_{1})\land_{\mathrm{RC}}\dots\land_{\mathrm{RC}}\Diamond^{\mathrm{RC}}_{n}(T_{n})$ corresponds to the cone generated by $(\alpha_{0}+1,\alpha_{1}+1,\dots,\alpha_{n}+1,0,\dots)$ in ${\mathcal{E}}$ which coincides with the cone of $\Diamond_{n}^{\mathfrak{I}}(\vec{\alpha})$ (cf. Lemma 8.7). $\Box$

Using Lemma 8.7 we can also isomorphically represent $\mathfrak{I}$ as an algebra of cones in $\mathcal{I}$. Given a cone $C\in\mathrm{C}(\mathcal{I})$ let $\Diamond^{\mathfrak{C}}_{n}(C):=\bigcap_{i\leqslant n}R_{i}^{-1}(C)$. We also define

[TABLE]

We summarize the main results of this paper in the following theorem.

Theorem 13

The following structures are isomorphic:

1. $\mathrm{(i)}$

$\overline{\mathfrak{G}}^{0}_{T}$, for any sound Gödelian extension $T$ of $\mathrm{EA}$; 2. $\mathrm{(ii)}$

$\mathfrak{L}^{0}_{{\mathrm{RC}^{\nabla}}}$, the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$; 3. $\mathrm{(iii)}$

$\mathfrak{I}=(\mathrm{I},\land_{\mathfrak{I}},\{\Diamond^{\mathfrak{I}}_{n},\nabla^{\mathfrak{I}}_{n}:n\in\omega\})$; 4. $\mathrm{(iv)}$

$(\mathfrak{T}^{0}_{\mathrm{RC}},\land_{\mathrm{RC}},\{\Diamond^{\mathrm{RC}}_{n},\nabla^{\mathrm{RC}}_{n}:n\in\omega\})$; 5. $\mathrm{(v)}$

$\mathfrak{C}(\mathcal{I})=(\mathrm{C}(\mathcal{I}),\cap,\{\Diamond^{\mathfrak{C}}_{n},\nabla_{n}^{\mathfrak{C}}:n\in\omega\})$.

Proof. We only need to prove the isomorphism of (v) with either (iii) or (iv). Proposition 9.2 provides the isomorphisms of the semilattice reducts. Further, for all $\vec{\alpha}\in\mathrm{I}$, $\Diamond^{\mathfrak{C}}_{n}(C_{\vec{\alpha}})=C_{\Diamond^{\mathfrak{I}}_{n}(\vec{\alpha})}$ by Lemma 8.7 (i). Hence, $\Diamond^{\mathfrak{C}}_{n}$ corresponds to $\Diamond_{n}^{\mathfrak{I}}$ of (iii). On the other hand, $\nabla_{n}^{\mathfrak{C}}(C_{\vec{\alpha}})=v(\nabla_{n}^{\mathrm{RC}}([\vec{\alpha}]))$. Hence, $\nabla_{n}^{\mathfrak{C}}$ corresponds to $\nabla_{n}^{\mathrm{RC}}$ of (iv). $\Box$

We remark that the algebra $\mathfrak{C}(\mathcal{I})$ has rather simple definitions of meet and diamonds, but somewhat convoluted nablas. In contrast, $\mathfrak{T}^{0}_{\mathrm{RC}}$ has simple meet and nablas but somewhat convoluted diamonds. The algebra $\mathfrak{I}$, perhaps the most elegant of all three, has a more complicated meet operation (though the order relation $\leqslant_{\mathfrak{I}}$ is simple).

Finally, we briefly return to the subject of conservativity spectra and look at it from the point of view of established isomorphisms.

Let us call a theory $S$ in the language of $\mathsf{PA}$ bounded if $S$ is contained in a consistent finitely axiomatizable theory. The unboundedness theorem by Kreisel and Lévy [39] yields that $\mathrm{ord}_{n}(S)=0$, for all sufficiently large $n\in\omega$, whenever $S$ is bounded. We need to restrict ourselves to bounded subtheories of $\mathsf{PA}$ if we want to establish a bijection between their conservativity spectra and the Ignatiev algebra.

Theorem 14

1. $\mathrm{(i)}$

Let $T$ be a Gödelian extension of $\mathrm{EA}^{+}$ and let $\vec{\alpha}$ be the conservativity spectrum of $T$. If $\mathsf{PA}\vdash T$ then $\vec{\alpha}\in\bar{\mathrm{I}}$. If, in addition, $T$ is bounded, then $\vec{\alpha}\in I$. 2. $\mathrm{(ii)}$

Let $\vec{\alpha}\in\mathfrak{I}$, $A$ be a variable-free ${\mathrm{RC}^{\nabla}}$-formula corresponding to $\vec{\alpha}$ via the isomorphism, and $A^{*}\in\mathfrak{G}^{0}_{\mathrm{EA}^{+}}$ its arithmetical interpretation. Then $A^{*}$ is a bounded subtheory of $\mathsf{PA}$ and $\vec{\alpha}$ is the conservativity spectrum of $A^{*}$. 3. $\mathrm{(iii)}$

Under the same assumptions, $A^{*}$ is the weakest theory with the given conservativity spectrum $\vec{\alpha}$.

Proof. (i) In view of Lemma 7.3, for the first claim it is sufficient to prove that $\forall n\in\omega\>\alpha_{n}\leqslant\varepsilon_{0}$. Since $\mathsf{PA}$ contains $T$, this follows from Proposition 7.1 (i).

Since $\mathsf{PA}$ is equivalent to the union of theories $\{\mathrm{R}_{n}(1):n\in\omega\}$, any finite subtheory of $\mathsf{PA}$ is contained in a theory of the form $\mathrm{R}_{n}(1)$, for some $n\in\omega$ (we write $1$ for $1_{\mathrm{EA}^{+}}$). Hence, its conservativity spectrum is $\leqslant_{\mathfrak{I}}$ above that of $\mathrm{R}_{n}(1)$, that is, belongs to $\mathfrak{I}$.

(ii) That $A^{*}$ is a bounded subtheory of $\mathsf{PA}$ easily follows by induction on the build-up of $A$. The equality $\mathrm{sp}(A^{*})=\vec{\alpha}$ is a part of Theorem 10.

(iii) This follows from the fact that any theory $T$ such that $\mathrm{sp}(T)\leqslant_{\mathfrak{I}}\vec{\alpha}$ must contain the union of progressions

[TABLE]

which is equivalent to $A^{*}$ by Theorem 10. $\Box$

Let $\mathrm{sp}(T)$ denote the conservativity spectrum of $T$ and let $\mathrm{th}:\mathfrak{I}\to\overline{\mathfrak{G}}_{\mathrm{EA}^{+}}$ denote the natural isomorphic embedding of ${\mathrm{RC}^{\nabla}}$-algebras. As we already noted, $\mathrm{th}(\vec{\alpha})$ is a bounded subtheory of $\mathsf{PA}$, for each $\vec{\alpha}$.

Corollary 9.9

The maps $\mathrm{th}$ and $\mathrm{sp}$ form a Galois connection: for each bounded subtheory $S$ of $\mathsf{PA}$,

[TABLE]

We remark that the map $\mathrm{sp}$ is order-preserving, however it is not a semilattice homomorphism, even when restricted to bounded subtheories of $\mathsf{PA}$. For example, it is well known that $\mathrm{ord}_{1}(I\Sigma_{1})=\omega=\mathrm{ord}_{1}(I\Pi_{2}^{-})$ and both theories are $\Pi_{2}^{0}$-regular:

[TABLE]

On the other hand, $\mathrm{ord}_{1}(I\Sigma_{1}\land_{\mathrm{EA}}I\Pi_{2}^{-})=\omega^{2}>\omega$ and

[TABLE]

10 A universal Kripke frame for the variable-free fragment of ${\mathrm{RC}^{\nabla}}$

In view of Theorem 13 it is natural to ask if one can describe a convenient universal Kripke frame for the variable-free fragment of ${\mathrm{RC}^{\nabla}}$. There are two known general constructions associating with an SLO $\mathfrak{B}=(B,\land^{\mathfrak{B}},\{a^{\mathfrak{B}}:a\in\Sigma\})$ its ‘dual’ Kripke frame, so that $\mathfrak{B}$ is embeddable into the algebra of subsets of that frame (see [37, Section 4.1]). One construction is similar to the way the canonical model of a strictly positive logic $L$ is obtained from its Lindenbaum–Tarski algebra and goes from $\mathfrak{B}$ to the set of all filters of $\mathfrak{B}$ equipped with binary relations $\{R_{a}:a\in\Sigma\}$ such that, for all filters $F,G$,

[TABLE]

The corresponding frame for the ${\mathrm{RC}^{\nabla}}$-algebra $\mathfrak{I}$ is constructively described in [3] in terms of appropriate sequences of ordinals. However, the relations of the frame look sufficiently complicated, so that one would really want a simpler construction for practical use.

Another approach (see [34, 37]) is to consider the set $B$ itself as a dual space, and to specify binary relations on $B$ by

[TABLE]

Let $\mathfrak{B}^{*}$ denote the Kripke frame $(B,\{R_{a}:a\in\Sigma\})$ together with the canonical valuation $v:\mathfrak{B}\to{\mathcal{P}}(B)$, where $v(x):=\{y\in B:y\leqslant_{\mathfrak{B}}x\}$.

Lemma 10.1

For all $x,y\in\mathfrak{B}$ and $a\in\Sigma$, the following relations hold in $\mathfrak{B}^{*}$:

1. $\mathrm{(i)}$

$v(x\land_{\mathfrak{B}}y)=v(x)\cap v(y)$; 2. $\mathrm{(ii)}$

$R_{a}^{-1}(v(x))=v(a^{\mathfrak{B}}(x))$.

Proof. Claim (i) is just the fact that $x\land_{\mathfrak{B}}y$ is the g.l.b. of $x$ and $y$. To prove Claim (ii) we argue as follows: $z\in R_{a}^{-1}(v(x))$ means there is a $u\leqslant_{\mathfrak{B}}x$ such that $zR_{a}u$, that is, $z\leqslant_{\mathfrak{B}}a^{\mathfrak{B}}(u)$. Thus, if $z\in R_{a}^{-1}(v(x))$ we have by monotonicity $a^{\mathfrak{B}}(u)\leqslant_{\mathfrak{B}}a^{\mathfrak{B}}(x)$ and therefore $z\leqslant_{\mathfrak{B}}a^{\mathfrak{B}}(x)$.

If $z\leqslant_{\mathfrak{B}}a^{\mathfrak{B}}(x)$ then we take $x$ for $u$ and observe that $u\leqslant_{\mathfrak{B}}x$ and $z\leqslant_{\mathfrak{B}}a^{\mathfrak{B}}(u)$, hence $z\in R_{a}^{-1}(v(x))$. $\Box$

We obtain the following corollaries.

Proposition 10.2

1. $\mathrm{(i)}$

The map $v:\mathfrak{B}\to{\mathcal{P}}(B)$ is an embedding of $\mathfrak{B}$ into the algebra $({\mathcal{P}}(B),\cap,\{R^{-1}_{a}:a\in\Sigma\})$. 2. $\mathrm{(ii)}$

If $A,B$ in ${\mathcal{L}}_{\Sigma}$ are variable-free, then $A\vdash B$ holds in $\mathfrak{B}$ iff $\mathfrak{B}^{*},x\Vdash A\to B$ for all $x\in B$.

Corollary 10.3

The variable-free fragment of ${\mathrm{RC}^{\nabla}}$ is complete w.r.t. $\mathfrak{I}^{*}$.

The Kripke frame $\mathfrak{I}^{*}$ has a simple constructive characterization. We know that its domain is the set $I$ of all sequences of ordinals $\vec{\alpha}=(\alpha_{0},\alpha_{1},\dots)$ such that, for all $n\in\omega$, $\alpha_{n}<\varepsilon_{0}$ and $\alpha_{n+1}\leqslant\ell(\alpha_{n})$. Our task is to characterize the relations $R^{*}_{n}$ and $S^{*}_{n}$ on $I$ corresponding to, respectively, $\Diamond_{n}$ and $\nabla_{n}$, for all $n\in\omega$, where

[TABLE]

The answer is given by the following proposition.

Proposition 10.4

For all $\vec{\alpha},\vec{\beta}\in I$,

1. $\mathrm{(i)}$

$\vec{\alpha}R^{*}_{n}\vec{\beta}\iff\forall i\leqslant n\>\alpha_{i}>\beta_{i};$** 2. $\mathrm{(ii)}$

$\vec{\alpha}S^{*}_{n}\vec{\beta}\iff\forall i\leqslant n\>\alpha_{i}\geqslant\beta_{i}.$**

Proof. Claim (ii) is obvious, since $\nabla^{\mathfrak{I}}_{n}\vec{\beta}=(\beta_{0},\beta_{1},\dots,\beta_{n},0,\dots)$. To prove Claim (i) we recall that $\Diamond^{\mathfrak{I}}_{n}\vec{\beta}=(\beta^{\prime}_{0},\beta^{\prime}_{1},\dots,\beta^{\prime}_{n},0,\dots)$ where $\beta^{\prime}_{i}=0$ for $i>n$ and $\beta^{\prime}_{i}=\beta_{i}+\omega^{\beta^{\prime}_{i+1}}$ for $i\leqslant n$. Clearly, for all $i\leqslant n$ $\beta^{\prime}_{i}>\beta_{i}$. Hence, the ‘only if’ part of the claim is obvious.

To prove the ‘if’ part, we assume $\forall i\geqslant n\>\alpha_{i}>\beta_{i}$ and prove by downwards induction on $i\leqslant n$ that $\forall i\geqslant n\>\alpha_{i}\geqslant\beta^{\prime}_{i}$. If $i=n$ then $\beta^{\prime}_{i}=\beta_{i}+1$ and the claim is clear. If $i<n$ then $\alpha_{i}>\beta_{i}$ and by the induction hypothesis $\alpha_{i+1}\geqslant\beta^{\prime}_{i+1}$. Since $\vec{\alpha}\in I$ we have $\ell(\alpha_{i})\geqslant\alpha_{i+1}\geqslant\beta^{\prime}_{i+1}$. At this point we need an auxiliary lemma.

Lemma 10.5

For any ordinals $\alpha,\beta,\gamma$, if $\alpha>\beta$ and $\ell(\alpha)\geqslant\gamma$ then $\alpha\geqslant\beta+\omega^{\gamma}$.

Proof. We can write $\alpha=\beta+\nu$ with $\nu>0$. Then $\ell(\nu)=\ell(\alpha)\geqslant\gamma$, hence $\nu\geqslant\omega^{\gamma}$ and $\alpha=\beta+\nu\geqslant\beta+\omega^{\gamma}$. $\Box$

By this lemma we conclude that $\alpha_{i}\geqslant\beta_{i}+\omega^{\beta^{\prime}_{i+1}}=\beta^{\prime}_{i}$ and the induction step is complete. $\Box$

Looking at the frame $\mathfrak{I}^{*}$ as a dual of the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$ we observe that, for any $A,B\in\mathbb{F}^{\nabla}$, $AR^{*}_{n}B$ holds iff $A\vdash_{\mathrm{RC}^{\nabla}}\Diamond_{n}B$. Hence, $R_{n}^{*}$ is the same as the previously considered relation $<_{n}$ on words (now extended to all variable-free formulas of ${\mathrm{RC}^{\nabla}}$).

On the other hand, $AS^{*}_{n}B$ holds iff $A\vdash_{\mathrm{RC}^{\nabla}}\nabla_{n}B$. Hence, $S^{*}_{n}$ is the same as the $\Pi^{0}_{n+1}$-conservativity relation previously denoted $\vdash_{n}$ (cf Section 4).

Instead of the Lindenbaum–Tarski algebra of the variable-free fragment of ${\mathrm{RC}^{\nabla}}$ we can also work directly with its isomorphic arithmetical counterpart, the SLO $\overline{\mathfrak{G}}_{T}^{0}$ for a sound extension $T$ of $\mathrm{EA}$. Then, $\sigma R_{n}^{*}\nu$ means that the Gödelian theory $\sigma$ proves $\mathrm{R}_{n}(\nu)$, and $\sigma S_{n}^{*}\nu$ means that $\nu$ is $\Pi_{n+1}^{0}$-conservative over $\sigma$.

Remark 10.6

The same definitions also apply to a much larger Kripke frame $\overline{\mathfrak{G}}^{*}_{T}$ that is dual to the ${\mathrm{RC}^{\nabla}}$-algebra of all Gödelian extensions of $T$, $\overline{\mathfrak{G}}_{T}$.

Remark 10.7

A recent paper by Hermo Reyes and Joosten [29] introduces a universal Kripke frame for the so-called Turing–Schmerl Calculus. This model turns out to be very similar to $\mathfrak{I}^{*}$. The differences amount to the following two aspects. Firstly, their relations $R_{n}$ can be defined as $R^{*}_{n}\cap\leqslant_{\mathfrak{I}}$. This reflects the fact that all their modalities satisfy the principle $\Diamond A\vdash A$. Secondly, their models lack the $S_{i}$ relations, but allow the $\alpha$-iterations of relations $R_{n}$.

Appendix A Irreflexivity of $<_{0}$ in $\mathrm{RC}$

We work in (the variable-free fragment of) the reflection calculus $\mathrm{RC}$. We will use the techniques of Kripke models for $\mathrm{RC}$. The notions of the canonical tree for a formula $A$, its RC-closure $\mathrm{RC}[A]$ and that of an RC-model are defined in [10]. We recall that $\mathrm{RC}[A]$ is an RC-model satisfying $A$ at the root. Its valuation will be empty if $A$ is variable-free.

The following lemma is easily obtained from Lemma 3.3 taking into account that words in $\mathbb{W}_{n}$ are linearly pre-ordered by $<_{n}$.

Lemma A.1

Any variable-free formula of $\mathrm{RC}$ is equivalent to $\top$ or to a formula of the form $A\circeq\bigwedge_{i\leqslant k}\Diamond_{m_{i}}A_{i}$ where

1. $\mathrm{(i)}$

$A_{i}\in\mathbb{F}_{m_{i}}$, for each $i$; 2. $\mathrm{(ii)}$

$m_{0}>m_{1}>\dots>m_{k}$; 3. $\mathrm{(iii)}$

$\Diamond_{m_{i}}A_{i}\nvdash_{\mathrm{RC}}\Diamond_{m_{j}}A_{j}$, for all $j>i$.

Such formulas are called properly ordered. If $A$ is properly ordered, then $\mathrm{RC}[A]$ can be characterized as follows.

If $A\circeq\top$ then $\mathrm{RC}[A]$ is the irreflexive singleton frame. If $A\circeq\bigwedge_{i\leqslant k}\Diamond_{m_{i}}A_{i}$ then $\mathrm{RC}[A]$ consists of the disjoint union of the frames $\mathrm{RC}[A_{i}]$, for all $i\leqslant k$, augmented by a new root $a$. In addition to all the relations inherited from the frames $\mathrm{RC}[A_{i}]$, the following relations are postulated:

$aR_{n}x$, for each $i\leqslant k$, $n\leqslant m_{i}$ and $x\in\mathrm{RC}[A_{i}]$; 2. 2.

$xR_{n}y$, for each $i\leqslant k$, $n<m_{i}$, and $x,y\in\bigcup_{j\leqslant i}\mathrm{RC}[A_{j}]$; 3. 3.

$xR_{n}y$, for each $i\leqslant k$, $n\leqslant m_{i}$, $y\in\mathrm{RC}[A_{i}]$ and $x\in\bigcup_{j<i}\mathrm{RC}[A_{j}]$.

The following lemma is routine.

Lemma A.2

$\mathrm{RC}[A]$* thus described is an RC-frame.*

Theorem 15

For any formula $A$ of $\mathrm{RC}$, $A\nvdash_{\mathrm{RC}}\Diamond_{0}A$.

Proof. It is sufficient to prove the claim for variable-free and properly ordered $A$. For such an $A$, we argue by induction on the length of $A$. Basis is trivial. Suppose $A=\bigwedge_{i\leqslant k}\Diamond_{m_{i}}A_{i}$. If $A\vdash\Diamond_{0}A$ then there is a homomorphism $f$ of $\mathrm{RC}[A]$ into itself such that $aR_{0}f(a)$. Then there is an $i\leqslant k$ such that $f(a)\in\mathrm{RC}[A_{i}]$.

Let $X$ denote the subset of $\mathrm{RC}[A]$ corresponding to $\mathrm{RC}[A_{i}]$. Consider any $n\geqslant m_{i}$ and an $R_{n}$-arrow whose source is in $X$. By the construction of $\mathrm{RC}[A]$, this arrow can only be an old arrow from the frame $\mathrm{RC}[A_{i}]$. Hence, the target of this arrow will also be in $X$. Since $A_{i}\in\mathbb{F}_{m_{i}}$, it follows that $f(X\cup\{a\})\subseteq X$. The subset $X\cup\{a\}$ together with all the inherited relations can be considered as a submodel of $\mathrm{RC}[A]$ isomorphic to $\mathrm{RC}[\Diamond_{m_{i}}A_{i}]$. Hence, $f$ induces a homomorphism $f:\mathrm{RC}[\Diamond_{m_{i}}A_{i}]\to\mathrm{RC}[A_{i}]$. This implies that either $A_{i}\vdash_{\mathrm{RC}}\Diamond_{m_{i}}A_{i}$ (if $f(a)$ is the root of $\mathrm{RC}[A_{i}]$), or $A_{i}\vdash_{\mathrm{RC}}\Diamond_{m_{i}}\Diamond_{m_{i}}A_{i}\vdash_{\mathrm{RC}}\Diamond_{m_{i}}A_{i}$ (if $f(a)$ is strictly above the root). In any case $A_{i}\vdash_{\mathrm{RC}}\Diamond_{m_{i}}A_{i}\vdash_{\mathrm{RC}}\Diamond_{0}A_{i}$ contradicting the induction hypothesis. $\Box$

Appendix B Uniform definability of computable operators

Theorem 16

An operator $R:\mathfrak{G}_{\mathrm{EA}}\to\mathfrak{G}_{\mathrm{EA}}$ is uniformly definable iff $R$ is computable.

Proof. The main point is to show that computable $R$ are uniformly definable. Let $R$ be computable, hence there is a $\Sigma_{1}^{0}$-formula $\mathrm{Ax}_{R}(x,y)$ such that $\mathrm{Ax}_{R}(x,\overline{\ulcorner\sigma\urcorner})$ numerates the theory $R(\sigma)$ for each $\sigma$. Notice that $R(\sigma)$ is an elementary formula, for each $\sigma$. We claim that one can select $\mathrm{Ax}_{R}$ in such a way that for each $\sigma$ there is an elementary numeration $\delta$ such that

[TABLE]

Let $\mathrm{Sat}_{\Delta_{0}}(e,x)$ be a $\Sigma_{1}^{0}$-truthdefinition for elementary formulas that can be represented in the form

[TABLE]

where $T(e,x,q)$ is an elementary formula expressing that $q$ is a protocol of a computation verifying that an elementary formula $e$ holds on assignment $x$. For each specific formula $e$, the size of $q$ is bounded by a $d$-fold iterate of exponential function in $x$ where $d$ elementarily depends on $e$. Whereas in $\mathrm{EA}$ one cannot prove that $2_{d(e)}^{x}$ is defined for all $e$ and $x$, it is known that for each specific $n$ there is an $\mathrm{EA}$-proof of $\forall x\>\exists y\>\>2_{\bar{n}}^{x}=y$. So, for each specific formula $\sigma$ there is a number $n=d(\ulcorner\sigma\urcorner)$ such that provably in $\mathrm{EA}$

[TABLE]

Now, if $F_{R}(x,y)$ is a $\Sigma_{1}^{0}$-formula strongly representing the map $R:\ulcorner\sigma\urcorner\mapsto\ulcorner R(\sigma)\urcorner$, we can define

[TABLE]

Then, for each $\sigma$ there is a provably unique $\tau=R(\sigma)$ such that $\mathrm{EA}\vdash F_{R}(\overline{\ulcorner\sigma\urcorner},\overline{\ulcorner\tau\urcorner})$. Hence, $\mathrm{Ax}_{R}(x,\overline{\ulcorner\sigma\urcorner})$ is provably equivalent to $\mathrm{Sat}_{\Delta_{0}}(\overline{\ulcorner\tau\urcorner},x)$ which is equivalent to an elementary formula by (10). This proves (9).

To provide a uniform definition of $R$ we apply a version of Craig’s trick and let

[TABLE]

where $W_{R}(z,y,p)$ is an elementary formula expressing that $p$ witnesses $\mathrm{Ax}_{R}(z,y)$. Here, we may assume that $\mathrm{EA}\vdash W_{R}(z,y,p)\to z\leqslant p$. Clearly, $\mathrm{Ax}_{R^{\prime}}(x,y)$ is elementary and condition (ii) is satisfied. Externally, it numerates the same family of theories as $\mathrm{Ax}_{R}(x,y)$. We show that, for each $\sigma$,

[TABLE]

First, we obtain an elementary numeration $\delta$ such that $\mathrm{EA}\vdash\forall x\>(\mathrm{Ax}_{R}(x,\overline{\ulcorner\sigma\urcorner})\leftrightarrow\delta(x)).$ It follows that $\mathrm{EA}\vdash\forall x\>(\Box_{R(\sigma)}(x)\leftrightarrow\Box_{\delta}(x)).$ Thus, using $\Pi_{2}^{0}$-conservativity of $\mathrm{B\Sigma}_{1}$ over $\mathrm{EA}$ it is sufficient to prove

[TABLE]

Using $\mathrm{B\Sigma}_{1}$ it is sufficient to prove that $\mathrm{EA}\vdash\forall x\>(\delta(x)\to\Box_{R^{\prime}(\sigma)}(x)).$ Reason in $\mathrm{EA}$: Assume $\delta(x)$ then $\mathrm{Ax}_{R}(x,\overline{\ulcorner\sigma\urcorner})$. Hence, there is a witness $p$ such that $W_{R}(x,\overline{\ulcorner\sigma\urcorner},p)$. Then for $u:=\text{disj}(x,\ulcorner\overline{p}\neq\overline{p}\urcorner)$ we have $\mathrm{Ax}_{R^{\prime}}(u,\overline{\ulcorner\sigma\urcorner})$ and from $p$ we obtain a proof of $\overline{p}\neq\overline{p}$ and hence a proof of $x$ from hypothesis $u$ in an elementary way. Therefore, $\Box_{R^{\prime}(\sigma)}(x)$. $\Box$