# Strictly Positive Fragments of
the Provability Logic of Heyting Arithmetic

Ana de Almeida Borges<EMAIL_ADDRESS>0000-0001-5152-198X Joost J. Joosten
<EMAIL_ADDRESS>0000-0001-9590-5045

(University of Barcelona)

###### Abstract

We determine the strictly positive fragment $\mathsf{QPL}^{+}(\mathsf{HA})$ of
the quantified provability logic $\mathsf{QPL}(\mathsf{HA})$ of Heyting
Arithmetic. We show that $\mathsf{QPL}^{+}(\mathsf{HA})$ is decidable and that
it coincides with $\mathsf{QPL}^{+}(\mathsf{PA})$, which is the strictly
positive fragment of the quantified provability logic of of Peano Arithmetic.
This positively resolves a previous conjecture of the authors described in
[3].

On our way to proving these results, we carve out the strictly positive
fragment $\mathsf{PL}^{+}(\mathsf{HA})$ of the provability logic
$\mathsf{PL}(\mathsf{HA})$ of Heyting Arithmetic, provide a simple
axiomatization, and prove it to be sound and complete for two types of
arithmetical interpretations.

The simple fragments presented in this paper should be contrasted with a
recent result by Mojtahedi [42], where an axiomatization for
$\mathsf{PL}(\mathsf{HA})$ is provided. This axiomatization, although
decidable, is of considerable complexity.

##  1 Introduction

The provability logic of Heyting Arithmetic ($\mathsf{HA}$) has recently been
axiomatized by Mojtahedi [42], solving a fifty-year-old problem. This
axiomatization is decidable but also quite technically complex.

One way of simplifying a logic $L$ without losing all of its expressive power
is to restrict its language to the strictly positive fragment $L^{+}$. This is
the fragment containing only $\top$, propositional or predicate symbols
(depending on whether $L$ is propositional or quantified, respectively),
conjunctions, universal quantifiers (if $L$ is quantified), and diamonds (if
$L$ is modal). Theorems of $L^{+}$ are implications between strictly positive
formulas. For example, $\operatorname{\forall}x\mskip 3.0mu\Diamond
P(x)\vdash_{L^{+}}\Diamond\operatorname{\forall}x\mskip 3.0muP(x)$ is a
grammatical statement that might or not hold depending on $L^{+}$. There are
several examples of pairs $\langle L,L^{+}\rangle$ where $L^{+}$ has lower
complexity than $L$ (see Table 1 in Section 2.3 for a survey), and for at
least some of them $L^{+}$ has been actively studied and used in its own
right.

In [3], we studied the strictly positive fragment of the quantified
provability logic of Peano Arithmetic ($\mathsf{PA}$) and conjectured that it
might coincide with the strictly positive fragment of the quantified
provability logic of $\mathsf{HA}$. In the present paper, we show that this is
indeed the case, by providing a link between a $\mathsf{PA}$-extension and an
$\mathsf{HA}$-extension of a given arithmetical realization.

We further study the strictly positive fragment of the (propositional)
provability logic of $\mathsf{HA}$, and show that it is quite simple and also
coincides with the strictly positive fragment of the provability logic of
$\mathsf{PA}$.

In what follows, we introduce the main concepts related to provability logics,
providing some more context and history, and end this section with a more
detailed plan of the paper.

###  1.1 Provability logics

The arithmetical predicate $\Box_{T}(\cdot)$ has been often used ever since
Gödel. This predicate is a natural and $\Sigma_{1}$-complete formalization of
the concept of provability in the theory $T$, in that
$\mathbb{N}\vDash\Box_{T}(n)$ holds exactly when $n$ is the Gödel number of a
formula that is provable in $T$ (as long as $T$ is a reasonable enough theory,
for example as long as $T$ has a decidable set of axioms).

The provability logic $\mathsf{PL}(T)$ of a theory $T$ describes the
structural behavior of $\Box_{T}(\cdot)$ as can be proven in $T$ itself. This
structural behavior is expressed in a propositional modal logic where, for
example, we have $(\Box(p\land q)\to\Box p)\in\mathsf{PL}(T)$, since, for
every possible arithmetical reading $p^{\star}$ and $q^{\star}$ of $p$ and
$q$, respectively, we have that $T\vdash\Box_{T}(p^{\star}\land
q^{\star})\to\Box_{T}p^{\star}$. In a similar spirit, one defines the set
$\mathsf{TPL}(T)$ to be the set of those propositional logical formulas that
induce corresponding formulas that are always true on the standard model of
arithmetic.

The definition of $\mathsf{PL}(T)$ is of complexity $\Pi_{2}$ (“for all
readings $\cdot^{\star}$, it is provable that $\varphi^{\star}$”), and the
definition of $\mathsf{TPL}(T)$ is not even arithmetical (“for all readings
$\cdot^{\star}$, it is true that $\varphi^{\star}$). However, it turns out
that both $\mathsf{PL}(T)$ and $\mathsf{TPL}(T)$ can be generated by the
decidable modal logics $\mathsf{GL}$ (thus named in reference to Gödel and
Löb) and $\mathsf{GLS}$ (thus named in reference to $\mathsf{GL}$ and Solovay)
respectively, for a large class of classical logical theories $T$, including
Peano Arithmetic. See [13] for a more thorough overview.

###  1.2 Quantified provability logic and its fragments

The quantified provability logic $\mathsf{QPL}(T)$ of a theory $T$ is defined
in an analogous way to $\mathsf{PL}(T)$. We restrict ourselves to the
languages of predicate logic without function symbols or identity.

As an example, the converse Barcan formula is valid:

$(\Box_{T}\operatorname{\forall}x\mskip
3.0mu\varphi(x)\to\operatorname{\forall}x\mskip
3.0mu\Box_{T}\varphi(\dot{x}))\in\mathsf{QPL}(T),$

but the Barcan formula is not:

$(\operatorname{\forall}x\mskip
3.0mu\Box_{T}\varphi(\dot{x})\to\Box_{T}\operatorname{\forall}x\mskip
3.0mu\varphi(x))\notin\mathsf{QPL}(T).$

Recall that, in the classical case, $\mathsf{PL}(T)$ allows for a reduction
from a $\Pi_{2}$-definition to a decidable one. Vardanyan proved in [51] that
this is not the case for $\mathsf{QPL}(\mathsf{PA})$, which is actually
$\Pi_{2}$-complete. George Boolos and Vann McGee [14] proved that
$\mathsf{TQPL}(\mathsf{PA})$ is $\Pi_{1}$-complete in the set of true
arithmetic. Vardanyan’s result allows for various generalizations [52, 12, 55]
and for a few exceptions of very limited range [6, 58, 27].

In [3], the strictly positive fragment $\mathsf{QPL}^{+}(\mathsf{PA})$ of the
quantified provability logic of $\mathsf{PA}$ was presented and proven to be
decidable, axiomatized by a logic called $\mathsf{QRC}_{1}$. The same paper
proved soundness of $\mathsf{QRC}_{1}$ for $\mathsf{HA}$ and conjectured
completeness. The current paper settles that conjecture positively and proves
completeness of $\mathsf{QRC}_{1}$ for $\mathsf{HA}$ for two different
arithmetical readings: the _finitary reading_ and the _infinitary reading_.

The finitary reading translates predicates to arithmetical formulas with the
same arity, as is usual in the case of quantified provability logic. The
infinitary reading falls in the tradition so-called reflection calculi.
Propositional reflection calculus translates propositional variables to
elementary axiomatizations of theories. Generalizing this to predicate logic,
the infinitary reading translates a predicate $S$ to the axiomatization of a
collection of theories parametrized by a number of parameters equal to the
arity of $S$.

###  1.3 Constructive provability logics

For about fifty years, the provability logic of Heyting Arithmetic remained an
open problem. Recently, Mojtahedi presented a solution, with a complete
axiomatization of $\mathsf{PL}(\mathsf{HA})$ described in [42]. Though this
axiomatization is proven to be decidable, it is of considerable complexity. To
give an impression of the nature of $\mathsf{PL}(\mathsf{HA})$, we mention an
incomplete selection of landmark results here and refer the reader to [4] for
a more detailed overview.

De Jongh proved in [16] the non-trivial result that the propositional fragment
of $\mathsf{PL}(\mathsf{HA})$ is exactly $\mathsf{IPC}$, the set of
intuitionistically valid propositional formulas.111The result is not as stable
as in the classical logical case and, for example, the propositional fragment
of the provability logic of $\mathsf{HA}$ together with Markov’s principle and
with Church’s thesis is unknown. It was easy to observe that
$\mathsf{iGL}\subseteq\mathsf{PL}(\mathsf{HA})$, where $\mathsf{iGL}$ is
exactly as $\mathsf{GL}$ except that it is defined over $\mathsf{IPC}$ instead
of over the classical propositional logic $\mathsf{CPC}$.

Since $\mathsf{HA}$ has different meta-mathematical properties than
$\mathsf{PA}$, different provability logical principles were expected to be
found. For example, Markov’s rule is admissible for $\mathsf{HA}$ in that
$\mathsf{HA}\vdash\neg\neg\pi$ implies $\mathsf{HA}\vdash\pi$ whenever
$\pi\in\Pi_{2}$. Then the admissibility of Markov’s rule translates to
$(\Box\neg\neg\Box\varphi\to\Box\Box\varphi)\in\mathsf{PL}(\mathsf{HA})$,
since $\Box_{\mathsf{HA}}\varphi$ is always $\Sigma_{1}$ regardless of
$\varphi$. More generally:

$\left(\Box\neg\neg\left(\Box\varphi\to\bigvee_{i}\Box\varphi_{i}\right)\to\Box\left(\Box\varphi\to\bigvee_{i}\Box\varphi_{i}\right)\right)\in\mathsf{PL}(\mathsf{HA}).$

There is actually a more general relationship between
$\mathsf{PL}(\mathsf{HA})$ and admissible rules. Visser showed that the
admissible rules of $\mathsf{HA}$ and the admissible rules of $\mathsf{IPC}$
are the same so that each admissible rule $\frac{\varphi}{\psi}$ of
$\mathsf{HA}$ gives rise to
$(\Box\varphi\to\Box\psi)\in\mathsf{PL}(\mathsf{HA})$. Although Rybakov showed
in [46] that the collection of admissible rules of $\mathsf{IPC}$ is
decidable, it was only later that concrete characterizations were found. In
particular, Iemhoff showed in [29] how the admissible rules can be defined in
terms of Visser’s rule.

The exact definition of Visser’s rule is not of real importance in the context
of this paper. However, we wish to convey an impression of the complexity of
$\mathsf{PL}(\mathsf{HA})$ and as such we find it instructive to formulate it.
For an arbitrary natural number $n$, using the abbreviation
$(\varphi)(\psi_{1},\ldots,\psi_{n}):=(\varphi\to\psi_{1})\lor\cdots\lor(\varphi\to\psi_{n})$
and letting $\alpha:=\bigwedge_{i=1}^{n}(\epsilon_{i}\to\zeta_{i})$, Visser’s
rule $({\sf V_{n}})$ is defined as:

$\frac{\left(\alpha\to(\beta\lor\gamma)\right)\lor\delta}{(\alpha)(\epsilon_{1},\ldots,\epsilon_{n},\beta,\gamma)\lor\delta},$

leading to:

$\left(\Box\left(\left(\alpha\to(\beta\lor\gamma)\right)\lor\delta\right)\to\Box\left((\alpha)(\epsilon_{1},\ldots,\epsilon_{n},\beta,\gamma)\lor\delta\right)\right)\in\mathsf{PL}(\mathsf{HA}).$

So far we have seen how various meta-mathematical properties led to new
principles of the form $(\Box\varphi\to\Box\psi)$ in
$\mathsf{PL}(\mathsf{HA})$. However, not every meta-mathematical property of
$\mathsf{HA}$ directly translates into a principle in
$\mathsf{PL}(\mathsf{HA})$. For example, Myhill [43] and Friedman [20]
observed that the disjunction property of $\mathsf{HA}$ is not provable in
$\mathsf{HA}$ itself, whence $(\Box(p\lor q)\to\Box p\lor\Box
q)\notin\mathsf{PL}(\mathsf{HA})$. Notwithstanding this negative result,
Leivant could prove in [39, 54] a weak version of the disjunction property to
the extent that $(\Box(p\lor q)\to\Box(p\lor\Box
q))\in\mathsf{PL}(\mathsf{HA})$, whence also $(\Box(p\lor q)\to\Box(\Box
p\lor\Box q))\in\mathsf{PL}(\mathsf{HA})$.

Visser characterized the closed fragment of $\mathsf{PL}(\mathsf{HA})$ in [53]
and the “logic” of $\Sigma_{1}$-substitutions of $\mathsf{HA}$ in [54]. The
latter turned out to be important for Mojtehedi’s result, in a sense,
reflecting that the substitutions in Solovay’s completeness proof are Boolean
combinations of $\Sigma_{1}$-formulas. In [42], Mojtaba Mojtahedi could thus
include and extend all the previous results, culminating in a complete and
decidable axiomatization of $\mathsf{PL}(\mathsf{HA})$. This axiomatization is
$\mathsf{iGL}$ together with axioms of the form $\Box\varphi\to\Box\psi$,
where $\varphi$ and $\psi$ satisfy a complicated yet decidable condition.

The first result of this paper is a simple $\mathsf{PTIME}$-decidable fragment
of $\mathsf{PL}(\mathsf{HA})$: the strictly positive fragment
$\mathsf{PL}(\mathsf{HA})^{+}$. The second result of this paper is that the
first result can be extended to the quantified setting, leading to a decidable
(although to our knowledge not in $\mathsf{PTIME}$) fragment of
$\mathsf{QPL}(\mathsf{HA})$. Since the propositional logic
$\mathsf{PL}(\mathsf{HA})$ was already such a challenge, there has been hardly
any work done on the quantified provability logic $\mathsf{QPL}(\mathsf{HA})$
of $\mathsf{HA}$ before now.

###  1.4 Plan of the paper

In Section 2 we introduce the most relevant modal logics for this paper, both
propositional and quantified. For each modal logic, we define its
corresponding strictly positive fragment. As the main contribution of this
section, we display some literature findings showing how in general a shift
from the full logic to the strictly positive fragment comes with a drop in
computational complexity of the problem of theoremhood.

In Section 3 we revisit relational and arithmetical semantics for modal
provability logics for both the propositional and the predicate logical case.
We state the main theorems relating the logics and their semantics. All of the
results in this section are known, but they are needed for the sequel. The
only novel detail is the exposition of $\mathsf{QRC}_{1}$ in terms of Kripke
sheaves as in [1].

In Section 4 we prepare for a move to the arithmetical semantics of
provability logics for intuitionistic theories by first analyzing the behavior
of fragments of the arithmetical hierarchy in the constructive setting.

In Section 5 we revisit the main ingredients of the arithmetical completeness
proof for provability logic and observe that the needed substitutions are of
low and constructively well-behaved complexity.

Sections 6 and 7 contain the main results of the paper, providing an
axiomatization of the strictly positive fragment of the provability logic of
Heyting Arithmetic, both in the propositional and in the quantified case.

Finally, Section 8 closes off with some observations on the interpolation and
the fixpoint theorem for these fragments.

##  2 Modal logics and strictly positive fragments

In this section we introduce the most relevant modal logics for this paper.
These are mostly related to the provability logic $\mathsf{GL}$ (see [13]). We
dwell on both propositional logics and on their corresponding predicate
logical versions. For each logic, we define its strictly positive fragment and
display some findings from the literature showing how in general a shift from
the full logic to its strictly positive fragment comes with a drop in the
computational complexity of theoremhood.

###  2.1 Propositional modal logics

The language of propositional modal logic $\mathcal{L}_{\Box}$ is obtained
from the language of propositional logic by extending it with a unary $\Box$
symbol:

$\varphi::=\bot\mid
p\mid(\varphi\to\varphi)\mid(\varphi\land\varphi)\mid(\varphi\lor\varphi)\mid\Box\varphi,$

where $p$ represents a propositional symbol. In classical logic, $\bot$ and
$\to$ suffice to define $\land$ and $\lor$, but not so in constructive logic.
Negation is defined as usual, with $\neg\varphi:=\varphi\to\bot$, and the
diamond operator is defined as the dual of the box:
$\Diamond\varphi:=\neg\Box\neg\varphi$.

The only (non-strictly positive) modal logics that we consider in this paper
are all normal modal logics. Thus, they are an extension of the basic normal
modal logic $\mathsf{K}$. The modal logic $\mathsf{K}$ has as axioms all
propositional logical tautologies in $\mathcal{L}_{\Box}$ and all distribution
axioms of the form $\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi)$. The
rules are _modus ponens_ and necessitation, to wit,
$\mathsf{K}\vdash\varphi\implies\mathsf{K}\vdash\Box\varphi$.

The modal logic $\mathsf{K4}$ is defined from $\mathsf{K}$ by adding all the
transitivity axioms (also called 4), which are of the form
$\Box\varphi\to\Box\Box\varphi$. The modal logic $\mathsf{GL}$ is defined by
adding Löb’s axiom scheme $\Box(\Box\varphi\to\varphi)\to\Box\varphi$ to
$\mathsf{K4}$ (or, equivalently, to $\mathsf{K}$).

For a given ordinal $\Lambda$, the modal logic $\mathsf{GLP}_{\Lambda}$ [30,
7] with language $\mathcal{L}_{[\alpha],\alpha<\Lambda}$ has a modality
$[\alpha]$ for each $\alpha<\Lambda$ (with corresponding dual
$\langle\alpha\rangle$) and is defined such that each modality $[\alpha]$
behaves like the $\Box$ of $\mathsf{GL}$ and furthermore the following two
axiom schemes are available, both with $\beta<\alpha$: monotonicity
$[\beta]\varphi\to[\alpha]\varphi$; and negative introspection
$\langle\beta\rangle\varphi\to[\alpha]\langle\beta\rangle\varphi$.

###  2.2 Quantified modal logics

The language of modal logic can be extended to a quantified (first-order)
setting in the natural way. We describe a simple version with no equality nor
function symbols, $\mathcal{L}_{\Box,\forall}$. Fix a signature $\Sigma$,
which in this case is simply a set of relation symbols
${\textsc{Rel}}_{\Sigma}$ and their respective arities (we mostly omit
specific mentions of $\Sigma$). Then $\mathcal{L}_{\Box,\forall}$ is defined
as follows:

$\varphi::=\bot\mid
S(\bm{x})\mid(\varphi\to\varphi)\mid(\varphi\land\varphi)\mid(\varphi\lor\varphi)\mid\operatorname{\forall}x\mskip
3.0mu\varphi\mid\operatorname{\exists}x\mskip 3.0mu\varphi\mid\Box\varphi,$

where $S\in{\textsc{Rel}}_{\Sigma}$ is a relation symbol with arity $n$,
$\bm{x}$ is an $n$-tuple of variables, and $x$ is a variable. Again,
$\neg\varphi:=\varphi\to\bot$ and $\Diamond\varphi:=\neg\Box\neg\varphi$. In
classical settings, conjunction, disjunction and existential quantification
can be defined from the other connectives.

The free variables of a formula $\varphi$ are defined as usual, and denoted by
${\text{fv}}(\varphi)$. The expression $\varphi[x{\leftarrow}y]$ denotes the
formula $\varphi$ with all free occurrences of the variable $x$ simultaneously
replaced by the variable $y$. We say that $y$ is free for $x$ in $\varphi$ if
no occurrence of $y$ becomes bound in $\varphi[x{\leftarrow}y]$.

Given a propositional modal logic $L$, one can define its quantified version
$\mathsf{Q}L$ as described in [28] by adding the following axiom scheme and
rule to the first order formulation of $L$: $\operatorname{\forall}x\mskip
3.0mu\varphi\to\varphi[x{\leftarrow}y]$ with $y$ free for $x$ in $\varphi$
($\bm{\forall}{\textbf{E}}$); and
$\mathsf{Q}L\vdash\varphi\to\psi\implies\mathsf{Q}L\vdash\varphi\to\operatorname{\forall}x\mskip
3.0mu\psi$ with $x\notin{\text{fv}}(\varphi)$ ($\bm{\forall}{\textbf{I}}$).
This leads to the straightforward definition of logics such as $\mathsf{QK}$,
$\mathsf{QK}4$, and $\mathsf{QGL}$.

As is to be expected, quantified modal logics such as $\mathsf{QK}$ and
$\mathsf{QK}4$ are undecidable (they typically contain plain predicate logic).
Even small fragments of quantified modal logics are undecidable, such as the
fragment with only two variables [32] and the one with only one monadic
predicate symbol and two variables [45]. There are, however, some decidable
fragments of these logics discussed in [57]. Another decidable fragment is
given by the strictly positive quantified modal logic $\mathsf{QRC}_{1}$ [2],
further described below.

###  2.3 Strictly positive logics

Propositional strictly positive formulas (abbreviated p.s.p. formulas) are
built up from $\top$, propositional variables, the binary $\land$ and the
unary $\Diamond$ (or $\langle\alpha\rangle$ in the polymodal setting). Thus,
the strictly positive propositional language $\mathcal{L}^{+}_{\Box}$ is
defined as $\varphi::=\top\mid p\mid(\varphi\land\varphi)\mid\Diamond\varphi$,
and the polymodal version $\mathcal{L}^{+}_{[\alpha],\alpha<\Lambda}$ is
defined as $\varphi::=\top\mid
p\mid(\varphi\land\varphi)\mid\langle\alpha\rangle\varphi$, with
$\alpha<\Lambda$. We extend the definition to strictly positive quantified
modal formulas over some given relational vocabulary $\Sigma$ as
$\varphi::=\top\mid
S(\bm{t})\mid(\varphi\land\varphi)\mid\operatorname{\forall}x\mskip
3.0mu\varphi\mid\Diamond\varphi$, where $S$ is in ${\textsc{Rel}}_{\Sigma}$,
and denote this language by $\mathcal{L}^{+}_{\Box,\forall}$. For practical
reasons related with the study of $\mathsf{QRC}_{1}$, the signature $\Sigma$
may allow for individual constants in the strictly positive case, and so terms
$\bm{t}$ are either variables or constants. We do not work with function
symbols.

Note that the above are the only available connectives. The absence of
implication and negation does not allow us to define any of the other ones.
The statements of a strictly positive logic are implications between two
strictly positive formulas, typically written $\varphi\vdash\psi$ (where
$\varphi,\psi$ are strictly positive) instead of $\varphi\to\psi$ to remind
ourselves that the implication cannot be nested.

An important propositional strictly positive modal logic in the context of
this paper is the Reflection Calculus $\mathsf{RC}_{\Lambda}$, defined as
follows.

######  Definition 2.1 ($\mathsf{RC}_{\Lambda}$ [15, 8, 19]).

For $\varphi,\psi$ and $\chi$ formulas in the language
$\mathcal{L}^{+}_{[\alpha],\alpha<\Lambda}$ and $\alpha,\beta<\Lambda$, the
axioms and rules of the Reflection Calculus (denoted by
$\mathsf{RC}_{\Lambda}$) are the following:

  1. (i)

$\varphi\vdash_{\mathsf{RC}_{\Lambda}}\varphi$ and
$\varphi\vdash_{\mathsf{RC}_{\Lambda}}\top$;

  2. (ii)

$\varphi\land\psi\vdash_{\mathsf{RC}_{\Lambda}}\varphi$ and
$\varphi\land\psi\vdash_{\mathsf{RC}_{\Lambda}}\psi$ (conjunction
elimination);

  3. (iii)

if $\varphi\vdash_{\mathsf{RC}_{\Lambda}}\psi$ and
$\varphi\vdash_{\mathsf{RC}_{\Lambda}}\chi$, then
$\varphi\vdash_{\mathsf{RC}_{\Lambda}}\psi\land\chi$ (conjunction
introduction);

  4. (iv)

if $\varphi\vdash_{\mathsf{RC}_{\Lambda}}\psi$ and
$\psi\vdash_{\mathsf{RC}_{\Lambda}}\chi$, then
$\varphi\vdash_{\mathsf{RC}_{\Lambda}}\chi$ (cut);

  5. (v)

if $\varphi\vdash_{\mathsf{RC}_{\Lambda}}\psi$, then
$\langle\alpha\rangle\varphi\vdash_{\mathsf{RC}_{\Lambda}}\langle\alpha\rangle\psi$
(necessitation);

  6. (vi)

$\langle\alpha\rangle\langle\alpha\rangle\varphi\vdash_{\mathsf{RC}_{\Lambda}}\langle\alpha\rangle\varphi$
(transitivity);

  7. (vii)

$\langle\alpha\rangle\varphi\vdash_{\mathsf{RC}_{\Lambda}}\langle\beta\rangle\varphi$,
for $\alpha>\beta$ (monotonicity);

  8. (viii)

$\langle\alpha\rangle\varphi\land\langle\beta\rangle\psi\vdash_{\mathsf{RC}_{\Lambda}}\langle\alpha\rangle(\varphi\land\langle\beta\rangle\psi)$
for $\alpha>\beta$ (negative introspection).

The logic $\mathsf{RC}_{\Lambda}$ is also called the strictly positive
fragment of $\mathsf{GLP}_{\Lambda}$ since one can prove that for any p.s.p.
formulas $\varphi$ and $\psi$:

$\mathsf{GLP}_{\Lambda}\vdash\varphi\to\psi\iff\varphi\vdash_{\mathsf{RC}_{\Lambda}}\psi.$

See [15, 8, 19, 11] for details.

The logic $\mathsf{RC}_{1}$ has just one modality and is proven in [15] to be
the strictly positive fragment of any modal logic between $\mathsf{K4}$ and
$\mathsf{GL}$, inclusive.

In general, when considering a strictly positive logic $P$, one may ask
whether there is some modal logic $L$ whose strictly positive fragment $L^{+}$
coincides with $P$. In that case we would have:

$\varphi\vdash_{P}\psi\iff L\vdash\varphi\to\psi,$ (2.1)

where $\varphi$ and $\psi$ are strictly positive formulas. In the remainder of
this paper, given a logic $L$ we shall denote its strictly positive fragment
by $L^{+}$.

######  Definition 2.2.

For a modal logic $L$ the _strictly positive fragment_ $L^{+}$ of $L$ is
defined as:

$L^{+}:=\\{\langle\varphi,\psi\rangle\mid L\vdash\varphi\to\psi\text{ and
$\varphi$ and $\psi$ are strictly positive formulas}\\}.$

One can also consider strictly positive fragments for quantified modal logics.
Of principal interest in this paper is the Quantified Reflection Calculus with
one modality $\mathsf{QRC}_{1}$, which is an extension of $\mathsf{RC}_{1}$.

######  Definition 2.3 ($\mathsf{QRC}_{1}$ [2]).

Let $\varphi$, $\psi$, and $\chi$ be strictly positive formulas in
$\mathcal{L}^{+}_{\Box,\forall}$ with signature $\Sigma$. The axioms and rules
of $\mathsf{QRC}_{1}$ are the following:

  1. (i)

$\varphi\vdash\top$ and $\varphi\vdash\varphi$;

  2. (ii)

$\varphi\land\psi\vdash\varphi$ and $\varphi\land\psi\vdash\psi$ (conjunction
elimination);

  3. (iii)

if $\varphi\vdash\psi$ and $\varphi\vdash\chi$, then
$\varphi\vdash\psi\land\chi$ (conjunction introduction);

  4. (iv)

if $\varphi\vdash\psi$ and $\psi\vdash\chi$, then $\varphi\vdash\chi$ (cut);

  5. (v)

if $\varphi\vdash\psi$, then $\Diamond\varphi\vdash\Diamond\psi$
(necessitation);

  6. (vi)

$\Diamond\Diamond\varphi\vdash\Diamond\varphi$ (transitivity);

  7. (vii)

if $\varphi\vdash\psi$, then $\varphi\vdash\operatorname{\forall}x\mskip
3.0mu\psi$, for $x\notin{\text{fv}}(\varphi)$ (quantifier introduction on the
right);

  8. (viii)

if $\varphi[x{\leftarrow}t]\vdash\psi$, then $\operatorname{\forall}x\mskip
3.0mu\varphi\vdash\psi$, for $t$ free for $x$ in $\varphi$ (quantifier
introduction on the left);

  9. (ix)

if $\varphi\vdash\psi$, then
$\varphi[x{\leftarrow}t]\vdash\psi[x{\leftarrow}t]$, for $t$ free for $x$ in
$\varphi$ and $\psi$ (term instantiation);

  10. (x)

if $\varphi[x{\leftarrow}c]\vdash\psi[x{\leftarrow}c]$, then
$\varphi\vdash\psi$, for $c$ not in $\varphi$ nor $\psi$ (constant
elimination).

Analogously to the propositional case, $\mathsf{QRC}_{1}$ is the strictly
positive fragment of any logic between $\mathsf{QK}4$ and $\mathsf{QGL}$,
inclusive, and also the strictly positive fragment of the quantified
provability logic of Peano Arithmetic [3]. In this paper, we show that
$\mathsf{QRC}_{1}$ is the strictly positive fragment of the quantified
provability logic of Heyting Arithmetic as well.

Moving from a logic to its strictly positive fragment generally leads to a
reduction in the computational complexity of the corresponding decision
procedures. Many such reductions are listed in Table 1, although the
strictness of most reductions depends on complexity theoretical assumptions
such as $\mathsf{PSPACE}\neq\mathsf{PTIME}$. Notably, such assumptions are not
required in the case of $\mathsf{QRC}_{1}$.

Table 1: Complexity of some modal logics and their strictly positive counterparts. Full logic | Strictly positive fragment
---|---
$\mathsf{K}$ |  $\mathsf{PSPACE}$-complete | [38] | $\mathsf{K}^{+}$ | $\mathsf{PTIME}$ | [9, 10]
$\mathsf{K4}$ and $\mathsf{GL}$ |  $\mathsf{PSPACE}$-complete | [23] | $\mathsf{RC}_{1}$ | $\mathsf{PTIME}$ | [15, 8]
$\mathsf{K4.3}$ and $\mathsf{GL.3}$ |  $\mathsf{coNP}$-complete | [40] | $\mathsf{K4.3}^{+}$ | $\mathsf{PTIME}$ | [49]
$\mathsf{GLP}^{0}_{\Lambda}$ $(\Lambda\geq\omega)$ |  $\mathsf{PSPACE}$-complete | [44] | $\mathsf{RC}^{0}_{\Lambda}$ | $\mathsf{PTIME}$ | [15, 8]
$\mathsf{GLP}$ |  $\mathsf{PSPACE}$-complete | [47] | $\mathsf{RC}$ | $\mathsf{PTIME}$ | [15, 8]
$\mathsf{T}$ |  $\mathsf{PSPACE}$-complete | [38] | $\\{\bm{e}_{refl}\\}$ | $\mathsf{PTIME}$ | [31]
$\mathsf{S4}$ |  $\mathsf{PSPACE}$-complete | [38] | $\mathcal{E}_{qo}$ | $\mathsf{PTIME}$ | [31]
$\mathsf{S4.3}$ |  $\mathsf{coNP}$-complete | [23] | $\mathcal{E}_{lin}$ | $\mathsf{PTIME}$ | [31]
$\mathsf{S5}$ |  $\mathsf{coNP}$-complete | [18] | $\mathsf{S5}^{+}$ | $\mathsf{PTIME}$ | [49]
$\mathsf{S5}_{m}$ $(m>1)$ |  $\mathsf{PSPACE}$-complete | [18] | $\mathsf{S5}^{+}_{m}$ | $\mathsf{PTIME}$ | [49]
$\mathsf{QPL}(\mathsf{PA})$ |  $\Pi_{2}$-complete | [51] | $\mathsf{QRC}_{1}$ | decidable | [3]

##  3 Semantics for modal logics

In this section, we revisit relational and arithmetical semantics for modal
provability logics for the propositional and the quantified case and further
state the main theorems relating the logics and their semantics.

###  3.1 Relational semantics

We briefly revisit relational semantics (also known as Kripke semantics) for
classical modal logics and refer to [28] for details. We start with the
propositional case.

######  Definition 3.1 (Kripke frame, Kripke model).

A Kripke frame is a tuple $\langle W,R\rangle$ where $W$ is a non-empty set
(the worlds) and $R\subseteq W\times W$ is a binary relation (we write $wRu$
instead of $\langle w,u\rangle\in R$). A Kripke model is a Kripke frame
together with a valuation function $V:{\textsc{Prop}}\to\wp(W)$, determining
which propositional symbols hold at which worlds.

The truth of a modal formula in a model $\mathcal{M}:=\langle W,R,V\rangle$ at
a world $w$ is defined inductively as follows:

  1. (i)

$\mathcal{M},w\not\Vdash\bot$;

  2. (ii)

$\mathcal{M},w\Vdash p$ if and only if $w\in V(p)$, where
$p\in{\textsc{Prop}}$;

  3. (iii)

$\mathcal{M},w\Vdash\varphi\to\psi$ if and only if either
$\mathcal{M},w\not\Vdash\varphi$ or $\mathcal{M},w\Vdash\psi$;

  4. (iv)

$\mathcal{M},w\Vdash\Box\varphi$ if and only if for every $u$ such that $wRu$
we have $\mathcal{M},u\Vdash\varphi$.

If $\mathcal{M},w\Vdash\varphi$ for every world $w\in W$, we say that
$\varphi$ is valid in $\mathcal{M}$ and write $\mathcal{M}\vDash\varphi$.

We say that a model $\mathcal{M}:=\langle W,R,V\rangle$ is finite if $W$ is
finite, that it is transitive if $R$ is transitive, that it is Noetherian if
every non empty subset of $W$ has an $R$-maximal element, and that it is tree-
like if $R$ is acyclic and there is a root world that is connected to every
other world and is not itself a successor of any world. Both $\mathsf{RC}_{1}$
and $\mathsf{GL}$ are complete with respect to finite transitive Noetherian
tree-like models.

######  Theorem 3.2 ([13, 15]).

Let $\varphi$ be an $\mathcal{L}_{\Box}$ formula and $\psi,\chi$ be
$\mathcal{L}^{+}_{\Box}$ formulas. Let quantifiers over $\mathcal{M}$ range
over finite transitive Noetherian tree-like models with root $r$. Then:

$\displaystyle\mathsf{GL}\vdash\varphi\iff\left(\mathcal{M},r\Vdash\varphi\text{
for any such }\mathcal{M}\right);$
$\displaystyle\psi\vdash_{\mathsf{RC}_{1}}\chi\iff\left(\left(\mathcal{M},r\nVdash\psi\text{
or }\mathcal{M},r\Vdash\chi\right)\text{ for any such }\mathcal{M}\right).$

There have been several proposals for relational semantics for quantified
modal logics, from Kripke [34] to many others. Overviews can be found in [28,
24, 25]. The idea of the semantics we present is to glue together several
first-order models. The precise way in which to do it can vary, due to
different ways to interpret the relationship between quantifiers and modal
symbols, as well as with the first-order domains. In particular, if different
worlds are allowed different domains, there is more than one way of relating
those domains with each other. Here we describe Kripke sheaves [24], which for
any worlds $w$ and $u$ such that $u$ is accessible from $w$ includes a
compatibility function $\eta_{w,u}$ translating the domain of $w$ into the
domain of $u$.

######  Definition 3.3 (Kripke sheaf, first-order Kripke model).

A Kripke sheaf $\mathcal{S}$ is a tuple $\langle
W,R,\allowbreak\\{M_{w}\\}_{w\in W},\\{\eta_{w,u}\\}_{wRu}\rangle$ where:

  1. (i)

$W$ is a non-empty set (the set of worlds, where individual worlds are
referred to as $w,u,v$, etc);

  2. (ii)

$R$ is a binary relation on $W$ (the accessibility relation);

  3. (iii)

each $M_{w}$ is a non-empty set (the domain of the world $w$, whose elements
are referred to as $d,d_{0},d_{1}$, etc);

  4. (iv)

if $wRu$, then $\eta_{w,u}$ is a function from $M_{w}$ to $M_{u}$.

Furthermore, we require two conditions on the compatibility functions:

  1. (v)

if $wRu$, $uRv$, and $wRv$, then for every $d\in M_{w}$ we have
$\eta_{u,v}(\eta_{w,u}(d))=\eta_{w,v}(d)$;

  2. (vi)

if $wRw$ then $\eta_{w,w}$ is the identity function on $M_{w}$.

Given a signature $\Sigma$, a first-order Kripke model $\mathcal{M}$ is a
tuple $\langle\mathcal{S},\\{I_{w}\\}_{w\in W},\\{J_{w}\\}_{w\in W}\rangle$
where $\mathcal{S}:=\langle W,R,\allowbreak\\{M_{w}\\}_{w\in
W},\allowbreak\\{\eta_{w,u}\\}_{wRu}\rangle$ is a Kripke sheaf and:

  * •

for each $w\in W$, the interpretation $I_{w}$ assigns an element of the domain
$M_{w}$ to each constant $c$ of $\Sigma$, written $c^{I_{w}}$;

  * •

$I$ is concordant: if $wRu$, then $c^{I_{u}}=\eta_{w,u}(c^{I_{w}})$ for every
constant $c$ of $\Sigma$.

  * •

for each $w\in W$, the interpretation $J_{w}$ assigns a set of tuples
$S^{J_{w}}\subseteq\wp((M_{w})^{n})$ to each $n$-ary relation symbol $S$ of
$\Sigma$.

In this case, we say that the model $\mathcal{M}$ is based on the sheaf
$\mathcal{S}$.

We say that a Kripke sheaf is finite if both $W$ and the domains $M_{w}$ for
every $w\in W$ are finite, and that it has a constant domain if all the
$M_{w}$ coincide and all the $\eta_{w,u}$ are the identity function. We say
that a model is finite (respectively has a constant domain) if it is based on
a finite (respectively constant domain) sheaf.

In order to define the notion of satisfaction, we need one more ingredient,
namely a way to interpret free variables. For this, we use assignments. Given
a world $w$, a $w$-assignment $g$ is a function form the set of variables to
the domain $M_{w}$. Any $w$-assignment can be seen as a $u$-assignment as long
as $wRu$, by composing it with $\eta_{w,u}$ on the left. We write $g^{u}$ to
shorten $\eta_{w,u}\circ g$ when $w$ is clear from context. A $w$-assignment
$g$ is extended to terms by defining $g(c):=c^{I_{w}}$ for any constant $c$.
Note that this meshes nicely with the concordance restriction of the model:
for any term $t$, if $wRu$ then $g^{u}(t)=\eta_{w,u}(g(t))$. Two
$w$-assignments $g$ and $h$ are $x$-alternative, written $g\sim_{x}h$, if they
coincide on all variables other than $x$.

We are now ready to define the notion of truth.

######  Definition 3.4 (Truth).

Let $\mathcal{M}=\langle W,R,\\{M_{w}\\}_{w\in
W},\allowbreak\\{\eta_{w,u}\\}_{wRu},\allowbreak\\{I_{w}\\}_{w\in
W},\\{J_{w}\\}_{w\in W}\rangle$ be a first-order Kripke model in some
signature $\Sigma$, and let $w\in W$ be a world, $g$ be a $w$-assignment, $S$
be an $n$-ary relation symbol, and $\varphi,\psi$ be
$\mathcal{L}_{\Box,\forall}$-formulas in the language of $\Sigma$.

We define $\mathcal{M},w\Vdash^{g}\varphi$ ($\varphi$ is true at $w$ under
$g$) by induction on $\varphi$ as follows:

  * •

$\mathcal{M},w\not\Vdash^{g}\bot$;

  * •

$\mathcal{M},w\Vdash^{g}S(t_{0},\ldots,t_{n-1})$ if and only if $\langle
g(t_{0}),\ldots,g(t_{n-1})\rangle\in S^{J_{w}}$;

  * •

$\mathcal{M},w\Vdash^{g}\varphi\to\psi$ if and only if either
$\mathcal{M},w\not\Vdash^{g}\varphi$ or $\mathcal{M},w\Vdash^{g}\psi$;

  * •

$\mathcal{M},w\Vdash^{g}\operatorname{\forall}x\mskip 3.0mu\varphi$ if and
only if for all $w$-assignments $h$ such that $h\sim_{x}g$ we have
$\mathcal{M},w\Vdash^{h}\varphi$;

  * •

$\mathcal{M},w\Vdash^{g}\Box\varphi$ if and only if for every $u\in W$ such
that $wRu$ we have $\mathcal{M},u\Vdash^{g^{u}}\varphi$.

If $\mathcal{M},w\Vdash^{g}\varphi$ for every $w$-assignment $g$ we say that
$\varphi$ is satisfied at $w$ and write $\mathcal{M},w\Vdash\varphi$. If
$\varphi$ is satisfied at every world $w$, we say that $\varphi$ is valid in
$\mathcal{M}$ and write $\mathcal{M}\vDash\varphi$. Finally, if $\varphi$ is
valid in every model $\mathcal{M}$ based on a given sheaf $\mathcal{S}$, we
say that $\varphi$ is valid in $\mathcal{S}$ and write
$\mathcal{S}\vDash\varphi$.

The soundness of a propositional modal logic can be leveraged to obtain
soundness with respect to Kripke sheaves for its quantified counterpart.

######  Theorem 3.5 (Soundness for $\mathsf{Q}L$).

Let $\mathcal{F}$ be a Kripke frame for $\mathcal{L}_{\Box}$ as described in
Definition 3.1. If $\mathcal{F}$ satisfies every theorem of a propositional
modal logic $L$, then any sheaf based on $\mathcal{F}$ (i.e., with the same
set of worlds and accessibility relation) satisfies every theorem of
$\mathsf{Q}L$.

###### Proof.

By induction on a $\mathsf{Q}L$ proof of a $\mathcal{L}_{\Box,\forall}$
formula. The proof is analogous to the one for the non-sheaf quantified Kripke
semantics described in [28]. See details in [1, Theorem 2.5.4]. ∎

As always, completeness has to be independently established for each different
logic. Modal completeness for $\mathsf{QRC}_{1}$ is proved in [2], and this
result is strengthened to constant-domain completeness in [3].

######  Theorem 3.6 ([3, Theorem 5.11]).

If $\varphi\nvdash_{\mathsf{QRC}_{1}}\psi$, then there are a finite Kripke
model $\mathcal{M}$ with a constant finite domain where $R$ is irreflexive and
transitive, a world $w\in\mathcal{M}$, and a $w$-assignment $g$ such that
$\mathcal{M},w\Vdash^{g}\varphi$ and $\mathcal{M},w\nVdash^{g}\psi$.

###  3.2 Arithmetical semantics

We refer to [26, 50] for definitions of $\mathsf{PA}$ and $\mathsf{HA}$, which
are Robinson’s arithmetic with full induction over classical or constructive
logic, respectively. As always, $\Delta_{0}$ refers to formulas where all
quantifiers are bounded by some term in our language and we set
$\Pi_{0}:=\Sigma_{0}:=\Delta_{0}$. The class $\Sigma_{n+1}$ arises from
existentially quantifying $\Pi_{n}$ formulas and the class $\Pi_{n+1}$ arises
from universally quantifying $\Sigma_{n}$ formulas. Given a class $\Gamma$
(for example $\Sigma_{1}$) and a theory $T$, we say that a formula $\varphi$
is “$\Gamma$ over $T$” if $T$ proves that $\varphi$ is equivalent to $\psi$,
for some formula $\psi\in\Gamma$.

The theory $\mathsf{EA}$ is as $\mathsf{PA}$ with the induction axiom
restricted to $\Delta_{0}$ formulas. The intuitionistic version of
$\mathsf{EA}$ is denoted by $\mathsf{iEA}$ and it only differs from
$\mathsf{EA}$ in that it is defined over intuitionistic predicate logic
instead of classical predicate logic. A theory is said to be $\Gamma$-sound if
all formulas in $\Gamma$ provable in the theory are valid in the standard
model $\mathbb{N}$.

Modal logics are related to arithmetic via Gödel numbering and via
interpreting the $\Box$ modality as formalized provability. For an
arithmetical formula $\varphi$, we denote its Gödel number by
$\ulcorner\varphi\urcorner$. We suggestively denote the arithmetical
formalized provability predicate by $\Box_{T}$ so that we have
$T\vdash\varphi$ if and only if
$\mathbb{N}\vDash\Box_{T}(\ulcorner\varphi\urcorner)$. Strictly speaking, an
axiomatization $\tau$ of a theory $T$ induces a provability predicate
$\Box_{\tau}$, but we shall often write $\Box_{T}$ when the intended
axiomatization $\tau$ for $T$ is clear from context. We define
$\Diamond_{\tau}\varphi$ as $\neg\Box_{\tau}\neg\varphi$.

Propositional variables in modal logics are taken to represent placeholders
for arbitrary arithmetical formulas. To formalize this idea, we use so-called
realizations.

######  Definition 3.7 (Arithmetical realization for $\mathcal{L}_{\Box}$,
$\cdot^{\star}$, $\cdot^{\star_{T}}$).

An arithmetical realization $\cdot^{\star}$ is a function from Prop to
sentences in the language of arithmetic. Given a c.e. theory $T$ in the
language of arithmetic and an arithmetical realization $\cdot^{\star}$, we
define $\cdot^{\star_{T}}$ on modal formulas as follows:

  * •

$\bot^{\star_{T}}:=(0=1)$;

  * •

$p^{\star_{T}}:=p^{\star}$, where $p\in{\textsc{Prop}}$;

  * •

$(\varphi\to\psi)^{\star_{T}}:=\varphi^{\star_{T}}\to\psi^{\star_{T}}$;

  * •

$(\Box\varphi)^{\star_{T}}:=\Box_{T}\varphi^{\star_{T}}$.

In the case of constructive theories such as $\mathsf{HA}$, the definition is
adapted in the usual way so that $\cdot^{\star_{T}}$ commutes with the
connectives $\land$ and $\lor$.

We can now define the provability logic $\mathsf{PL}(T)$ and the strictly
positive provability logic $\mathsf{PL}^{+}(T)$ of a theory $T$ in the
language as:

$\mathsf{PL}(T):=\\{\varphi\in\mathcal{L}_{\Box}\mid\text{for any
}\cdot^{\star},\text{ we have }T\vdash\varphi^{\star_{T}}\\},$
$\mathsf{PL}^{+}(T):=\\{\langle\varphi,\psi\rangle\in\mathcal{L}^{+}_{\Box}\times\mathcal{L}^{+}_{\Box}\mid\text{for
any }\cdot^{\star},\text{ we have
}T\vdash\varphi^{\star_{T}}\to\psi^{\star_{T}}\\}.$

We observe that, in virtue of their definitions,
$\mathsf{PL}^{+}(T)=(\mathsf{PL}(T))^{+}$.

We can now state that $\mathsf{PL}(T)=\mathsf{GL}$ for a large class of
theories $T$. The version for $\mathsf{PA}$ is known as Solovay’s completeness
theorem.

######  Theorem 3.8 ([48, 17]).

Let $T$ be a c.e. $\Sigma_{1}$-sound extension of $\mathsf{EA}$ and let
$\varphi\in\mathcal{L}_{\Box}$. Then:

$\mathsf{GL}\vdash\varphi\iff\text{for any }\cdot^{\star_{T}},\text{we have
}T\vdash\varphi^{\star_{T}}.$

Strictly positive propositional logics have an alternative arithmetical
interpretation where propositional variables are not mapped to sentences but
rather to formulas axiomatizing a theory.

######  Definition 3.9 (Infinitary arithmetical realization for
$\mathcal{L}^{+}_{\Box}$, $\cdot^{\circ}$, $\cdot^{\circ_{\tau}}$).

Let $\cdot^{\circ}$ be a function from propositional symbols to
axiomatizations of theories of arithmetic. Given a base axiomatization $\tau$,
we extend $\cdot^{\circ}$ to formulas of $\mathcal{L}^{+}_{\Box}$ as follows:

  * •

$\top^{\circ_{\tau}}:=\tau(u)$;

  * •

$p^{\circ_{\tau}}:=p^{\circ}\lor\tau(u)$;

  * •

$(\varphi\land\psi)^{\circ_{\tau}}:=\varphi^{\circ_{\tau}}\lor\psi^{\circ_{\tau}}$;

  * •

$(\Diamond\varphi)^{\circ_{\tau}}:=\tau(u)\lor(u=\ulcorner\Diamond_{\varphi^{\circ_{\tau}}}\top\urcorner)$.

Given these infinitary realizations, we define the reflection logic of a
theory:

$\mathsf{RL}(T):=\\{\langle\varphi,\psi\rangle\in\mathcal{L}^{+}_{\Box}\times\mathcal{L}^{+}_{\Box}\mid\text{for
any }\cdot^{\circ},\text{ we have }T\vdash\operatorname{\forall}\theta\mskip
3.0mu(\Box_{\psi^{\circ_{\tau}}}\theta\to\Box_{\varphi^{\circ_{\tau}}}\theta)\\}.$
(3.1)

Clearly, infinitary realizations extend finitary ones, for given a finitary
realization $\cdot^{\star}$ we can define $p^{\circ}:=(u=\ulcorner
p^{\star}\urcorner)$. Then $p^{\circ_{\tau}}$ axiomatizes the base theory
extended by the single axiom $p^{\star}$. Using this observation it is not
hard to see that $\mathsf{RL}(\mathsf{PA})=\mathsf{RC}_{1}$ and in Section 6
we show that $\mathsf{RL}(\mathsf{HA})=\mathsf{RC}_{1}$ as well.

We extend the notion of (finitary) arithmetical realization to
$\mathcal{L}_{\Box,\forall}$ in the natural way. To simplify matters, in the
sections dealing with both the quantified modal language and the language of
arithmetic, we always use variables named $x_{i}$ (for some $i$) in the modal
setting and variables named $y_{i}$ or $z_{i}$ in the arithmetical setting.

######  Definition 3.10 (Arithmetical realization for
$\mathcal{L}_{\Box,\forall}$ and $\mathcal{L}^{+}_{\Box,\forall}$,
$\cdot^{*}$, $\cdot^{*_{T}}$).

An arithmetical realization $\cdot^{*}$ is a function from relation symbols
applied to a tuple of $n$ variables (corresponding to the symbol’s arity) to
formulas in the language of arithmetic with $n$ free variables. We require
that a variable $x_{i}$ in the modal language be translated to $y_{i}$ in the
arithmetical setting and that a constant $c_{i}$ in the modal language be
translated to $z_{i}$ in the arithmetical setting.

Given a c.e. theory $T$ extending $\mathsf{iEA}$, and an arithmetical
realization $\cdot^{*}$, we define $\cdot^{*_{T}}$ on quantified modal
formulas as follows (extendable to the constructive setting as before):

  * •

$\bot^{*_{T}}:=(0=1)$;

  * •

$S(\bm{t})^{*_{T}}:=S(\bm{t})^{*}$;

  * •

$(\varphi\to\psi)^{*_{T}}:=\varphi^{*_{T}}\to\psi^{*_{T}}$;

  * •

$(\Box\varphi)^{*_{T}}:=\Box_{T}\varphi^{*_{T}}$;

  * •

$(\operatorname{\forall}x_{k}\mskip
3.0mu\varphi)^{*_{T}}:=\operatorname{\forall}y_{k}\mskip
3.0mu\varphi^{*_{T}}$.

This definition can be restricted to $\mathcal{L}^{+}_{\Box,\forall}$ in the
obvious way.

After Solovay’s completeness theorem (Theorem 3.8), it was natural to ask
whether one could find a nice characterization for the counterpart of
$\mathsf{PL}(\mathsf{PA})$ in the quantified modal language, defined as
follows (see Boolos [13]).

######  Definition 3.11 (Quantified provability logic, $\mathsf{QPL}$).

If $T$ is a c.e. extension of $\mathsf{iEA}$, the quantified provability logic
of $T$ is defined as:222Recall that we assume all modal variables are of the
form $x_{i}$ and that these are translated to the arithmetical variables
$y_{i}$. We also assume that all modal constants are translated to some
$z_{i}$, but note that constants are not included in the language
$\mathcal{L}_{\Box,\forall}$, only in $\mathcal{L}^{+}_{\Box,\forall}$. With
$\operatorname{\forall}\bm{y}\mskip 3.0mu\varphi^{*_{T}}$ we mean to quantify
over all the free variables of $\varphi^{*_{T}}$, and similarly in the
$\mathsf{QPL}^{+}(T)$ case.

$\mathsf{QPL}(T):=\\{\varphi\in\mathcal{L}_{\Box,\forall}\mid\text{for any
}\cdot^{*},\text{ we have }T\vdash\operatorname{\forall}\bm{y}\mskip
3.0mu\varphi^{*_{T}}\\},$
$\mathsf{QPL}^{+}(T):=\\{\langle\varphi,\psi\rangle\in\mathcal{L}^{+}_{\Box,\forall}\times\mathcal{L}^{+}_{\Box,\forall}\mid\text{for
any }\cdot^{*},\text{ we have
}T\vdash\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\varphi^{*_{T}}\to\psi^{*_{T}})\\}.$

In general, $\mathsf{QPL}(T)$ can be different depending on the chosen
axiomatization $\tau$ for $T$ (see [5, 35, 36]), but here we assume that an
axiomatization is fixed for each relevant theory for simplicity. It is not
exactly the case that $\mathsf{QPL}^{+}(T)=(\mathsf{QPL}(T))^{+}$ due to the
difference in weather constants are allowed in the language. However, for a
fixed signature $\Sigma$ without constants, we indeed have
$\mathsf{QPL}^{+}(T)=(\mathsf{QPL}(T))^{+}$.

The natural candidate for a quantified provability logic for $\mathsf{PA}$ was
$\mathsf{QGL}$, but although $\mathsf{QGL}\subseteq\mathsf{QPL}(\mathsf{PA})$,
Vardanyan [51] and McGee [41] independently showed that
$\mathsf{QPL}(\mathsf{PA})$ is as complex as it can possibly be:
$\Pi_{2}$-complete. However, in [3] it was proven that the strictly positive
fragment of this $\Pi_{2}$-complete logic is given by $\mathsf{QRC}_{1}$. In
other words, for the corresponding signatures we have the following result.

######  Theorem 3.12 ([3, Theorem 9.1]).

$\mathsf{QPL}^{+}(\mathsf{PA})=\mathsf{QRC}_{1}$.

In Section 7 we prove that likewise
$\mathsf{QPL}^{+}(\mathsf{HA})=\mathsf{QRC}_{1}$.

The strictly positive fragment $\mathcal{L}^{+}_{\Box,\forall}$ again allows
for an infinitary arithmetical interpretation. In that case, a predicate
$S(\bm{x},\bm{c})$ in the signature $\Sigma$ is mapped to a formula
$S^{\circ}(\bm{y},\bm{z})$ that axiomatizes a collection of theories
parametrized by $\bm{y},\bm{z}$.

######  Definition 3.13 (Infinitary arithmetical realization for
$\mathcal{L}^{+}_{\Box,\forall}$, $\cdot^{\circ}$, $\cdot^{\circ_{\tau}}$).

Let $\cdot^{\circ}$ be a realization such that, for a given $n$-ary predicate
$S$ and terms $\bm{t}$, $S(\bm{t})^{\circ}$ is an $(n+1)$-ary $\Sigma_{1}$
arithmetical formula where modal variables $x_{k}$ are interpreted as $y_{k}$
and modal constants $c_{k}$ are interpreted as $z_{k}$. Let $\tau$ be a
$\Sigma_{1}$ axiomatization of some base theory $T$. We extend this
realization to $\mathsf{QRC}_{1}$ formulas as follows:

  * •

$\top^{\circ_{\tau}}:=\tau(u)$;

  * •

$S(\bm{x},\bm{c})^{\circ_{\tau}}:=S(\bm{x},\bm{c})^{\circ}\lor\tau(u)$;

  * •

$(\psi\land\delta)^{\circ_{\tau}}:=\psi^{\circ_{\tau}}\lor\delta^{\circ_{\tau}}$;

  * •

$(\lozenge\psi)^{\circ_{\tau}}:=\tau(u)\lor(u=\ulcorner\Diamond_{\psi^{\circ_{\tau}}}\top\urcorner)$;

  * •

$(\operatorname{\forall}x_{i}\mskip
3.0mu\psi)^{\circ_{\tau}}:=\operatorname{\exists}y_{i}\mskip
3.0mu\psi^{\circ_{\tau}}$.

Using the infinitary semantics, we can define the quantified reflection logic
$\mathsf{QRL}(T)$ of a theory $T$ in analogy with (3.1) as:

$\mathsf{QRL}(T):=\\{\langle\varphi,\psi\rangle\in\mathcal{L}^{+}_{\Box,\forall}\times\mathcal{L}^{+}_{\Box,\forall}\mid\text{for
any }\cdot^{\circ},\ T\vdash\operatorname{\forall}\theta\mskip
3.0mu\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\Box_{\psi^{\circ_{\tau}}}\theta\to\Box_{\varphi^{\circ_{\tau}}}\theta)\\}.$

In [3, Theorems 7.2 and 8.9] it is shown that
$\mathsf{QRL}(\mathsf{PA})=\mathsf{QRC}_{1}$ and in Section 7 we prove that
furthermore $\mathsf{QRL}(\mathsf{HA})=\mathsf{QRC}_{1}$.

##  4 The arithmetical hierarchy in $\mathsf{HA}$

Heyting Arithmetic does not permit a simple treatment of the arithmetical
hierarchy (see e.g. [22]). In this section we collect some basic observations
on approximations to classical reasoning regarding formula complexity, which
we use later in the paper.

###  4.1 Closure and semi-closure under double negations

Using standard coding techniques, it is possible to see that $\mathsf{HA}$
proves that $\Sigma_{1}$ sentences are closed under conjunction, and this fact
is formalizable in $\mathsf{HA}$. We furthermore recall that for any
arithmetical formula $\varphi$ we have:

$\mathsf{HA}\vdash\operatorname{\forall}x\mskip
3.0mu\neg\varphi\leftrightarrow\neg\operatorname{\exists}x\mskip
3.0mu\varphi.$ (4.1)

This equivalence can be contrasted with
$\mathsf{HA}\nvdash\operatorname{\exists}x\mskip
3.0mu\neg\varphi\leftrightarrow\neg\operatorname{\forall}x\mskip
3.0mu\varphi$.

Additionally, $\mathsf{HA}$ proves excluded middle for decidable formulas.
Consequently, if $\delta$ is a decidable formula, then:

$\mathsf{HA}\vdash\neg\neg\delta\leftrightarrow\delta.$ (4.2)

In fact, this holds for arithmetical formulas $\delta$ of complexity
$\Delta_{1}$. However, excluded middle fails to hold for genuine $\Pi_{1}$
sentences $\pi$, but double negation elimination is still possible:

$\mathsf{HA}\vdash\neg\neg\pi\leftrightarrow\pi.$

The same equivalence does not hold for genuine $\Sigma_{1}$ sentences
$\sigma$:

$\mathsf{HA}\nvdash\neg\neg\sigma\leftrightarrow\sigma.$

Even though double negation elimination fails in general for $\Sigma_{1}$
sentences, we do have a certain formalized version. In Lemma 4.2 we will see
that
$\mathsf{HA}\vdash\Box_{\mathsf{HA}}\sigma\leftrightarrow\Box_{\mathsf{HA}}\neg\neg\sigma$
for $\Sigma_{1}$ sentences $\sigma$. This is due to a certain amount of
conservatism between $\mathsf{HA}$ and $\mathsf{PA}$ that shall be discussed
in the next subsection.

The class of $\Sigma_{2}$ formulas is particularly important for our study. In
pure constructive predicate logic, $\Sigma_{2}$ formulas are provably closed
under conjunctions but not under disjunctions. However, in $\mathsf{HA}$ we do
have the latter.

######  Lemma 4.1.

For each $\varphi_{0},\varphi_{1}\in\Sigma_{2}$, there is
$\varphi\in\Sigma_{2}$ such that:

$\mathsf{HA}\vdash\varphi_{0}\lor\varphi_{1}\leftrightarrow\varphi.$

###### Proof.

Let $\varphi_{0}=\exists s\,\forall t\,\tilde{\varphi}_{0}(s,t)$ and
$\varphi_{1}=\exists u\,\forall v\,\tilde{\varphi}_{1}(u,v)$, with
$\tilde{\varphi}_{1}(u,v),\tilde{\varphi}_{0}(s,t)\in\Delta_{0}$. We can take:

$\varphi:=\operatorname{\exists}x\mskip 3.0mu\operatorname{\forall}y\mskip
3.0mu(((x)_{0}=0\land\tilde{\varphi}_{0}((x)_{1},y))\lor((x)_{0}=1\land\tilde{\varphi}_{1}((x)_{1},y))),$

where $x$ is being interpreted as a pair, of which $(x)_{0}$ and $(x)_{1}$ are
the first and second projections, respectively. ∎

###  4.2 Equi-consistency results in $\mathsf{HA}$

When moving between $\mathsf{PA}$ and $\mathsf{HA}$, one conservativity
direction is trivial and formalizable in $\mathsf{HA}$:

$\mathsf{HA}\vdash\operatorname{\forall}\varphi\mskip
3.0mu(\Box_{\mathsf{HA}}\varphi\to\Box_{\mathsf{PA}}\varphi).$ (4.3)

The other direction is known to hold provably in $\mathsf{HA}$ for $\Pi_{2}$
sentences (see [21]), both in the non-formalized setting and in the formalized
setting, so we have an equivalence:

$\mathsf{HA}\vdash\operatorname{\forall}\pi\in\Pi_{2}\mskip
3.0mu(\Box_{\mathsf{PA}}\pi\leftrightarrow\Box_{\mathsf{HA}}\pi).$ (4.4)

With this conservativity result, we obtain a certain amount of classical
behavior for $\Pi_{2}$ sentences in a formalized setting. In particular,
combining the above we have a $\mathsf{HA}$ provable semi-closure of a certain
kind of double negation.

######  Lemma 4.2.

  1. 1.

$\mathsf{HA}\vdash\operatorname{\forall}\sigma\in\Sigma_{1}\mskip
3.0mu(\Box_{\mathsf{HA}}\neg\neg\sigma\leftrightarrow\Box_{\mathsf{HA}}\sigma)$;

  2. 2.

$\mathsf{HA}\vdash\operatorname{\forall}\sigma\in\Sigma_{1}\mskip
3.0mu(\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\neg\neg\sigma\leftrightarrow\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\sigma)$.

###### Proof.

Clearly, the first statement follows from the second, and so we only focus on
the latter. Reason in $\mathsf{HA}$ and fix an arbitrary
$\sigma\in\Sigma_{1}$. Since clearly $\sigma\to\neg\neg\sigma$, we focus on
the other implication. Consider:

$\displaystyle\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\neg\neg\sigma$
$\displaystyle\to\Box_{\mathsf{PA}}\operatorname{\forall}x\mskip
3.0mu\neg\neg\sigma$ by (4.3)
$\displaystyle\to\Box_{\mathsf{PA}}\operatorname{\forall}x\mskip 3.0mu\sigma$
$\displaystyle\to\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip 3.0mu\sigma$
by (4.4).

∎

Combining some of the above observations, it is easy to see that the negation
of a $\Pi_{1}$ sentence is equivalent to the double negation of a $\Sigma_{1}$
sentence over $\mathsf{HA}$.

######  Lemma 4.3.

Given a $\Pi_{1}$ sentence $\pi$, there is a $\Sigma_{1}$ sentence $\sigma$
such that:

$\mathsf{HA}\vdash\neg\pi\leftrightarrow\neg\neg\sigma.$

###### Proof.

Let $\pi:=\operatorname{\forall}x\mskip 3.0mu\delta$ where
$\delta\in\Delta_{0}$. Consider:

$\displaystyle\mathsf{HA}\vdash\neg\operatorname{\forall}x\mskip 3.0mu\delta$
$\displaystyle\leftrightarrow\neg\operatorname{\forall}x\mskip
3.0mu\neg\neg\delta$
$\displaystyle\leftrightarrow\neg\neg\operatorname{\exists}x\mskip
3.0mu\neg\delta$ by (4.1).

Then $\sigma:=\operatorname{\exists}x\mskip 3.0mu\neg\delta$ is the required
$\Sigma_{1}$ sentence. ∎

We can now prove a dual version of (4.4).

######  Lemma 4.4.

  1. 1.

$\mathsf{HA}\vdash\operatorname{\forall}\varphi\in\Sigma_{2}\mskip
3.0mu(\Box_{\mathsf{HA}}\neg\varphi\leftrightarrow\Box_{\mathsf{PA}}\neg\varphi)$;

  2. 2.

$\mathsf{HA}\vdash\operatorname{\forall}\varphi\in\Sigma_{2}\mskip
3.0mu(\Diamond_{\mathsf{HA}}\varphi\leftrightarrow\Diamond_{\mathsf{PA}}\varphi)$.

###### Proof.

The second statement easily follows from the first. Reason in $\mathsf{HA}$
and fix an arbitrary $\varphi\in\Sigma_{2}$. We can write $\varphi$ as
$\operatorname{\exists}x\mskip 3.0mu\pi$ for some $\pi\in\Pi_{1}$. Let
$\sigma$ be the $\Sigma_{1}$ sentence given by Lemma (4.3) for our fixed $\pi$
such that:

$\Box_{\mathsf{HA}}(\neg\pi\leftrightarrow\neg\neg\sigma).$ (4.5)

Now consider:

$\displaystyle\Box_{\mathsf{HA}}\neg\varphi$
$\displaystyle\leftrightarrow\Box_{\mathsf{HA}}\neg\operatorname{\exists}x\mskip
3.0mu\pi$
$\displaystyle\leftrightarrow\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\neg\pi$ by (4.1)
$\displaystyle\leftrightarrow\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\neg\neg\sigma$ by (4.5)
$\displaystyle\leftrightarrow\Box_{\mathsf{HA}}\operatorname{\forall}x\mskip
3.0mu\sigma$ by Lemma 4.2
$\displaystyle\leftrightarrow\Box_{\mathsf{PA}}\operatorname{\forall}x\mskip
3.0mu\sigma$ by (4.4)
$\displaystyle\leftrightarrow\Box_{\mathsf{PA}}\neg\neg\operatorname{\forall}x\mskip
3.0mu\sigma$
$\displaystyle\leftrightarrow\Box_{\mathsf{PA}}\neg\operatorname{\exists}x\mskip
3.0mu\neg\sigma$
$\displaystyle\leftrightarrow\Box_{\mathsf{PA}}\neg\operatorname{\exists}x\mskip
3.0mu\pi$ by (4.5)
$\displaystyle\leftrightarrow\Box_{\mathsf{PA}}\neg\varphi.$

∎

The above lemma is reminiscent of the following result by Kreisel.

######  Theorem 4.5 (Kreisel [33]).

For every formula $\varphi$ in prenex normal form we have:

$\mathsf{HA}\vdash\Box_{\mathsf{PA}}\neg\varphi\leftrightarrow\Box_{\mathsf{HA}}\neg\varphi.$

###### Proof.

The right to left implication is is clear, so we focus on the other direction.
Reason in $\mathsf{HA}$ and assume:

$\Box_{\mathsf{PA}}\neg\forall x_{1}\exists y_{1}\forall x_{2}\exists
y_{2}\cdots\delta,$

taking $\varphi$ as $\forall x_{1}\exists y_{1}\forall x_{2}\exists
y_{2}\cdots\delta$ for some $\Delta_{0}$-formula $\delta$, where the first
universal quantification may be vacuous. By the Kuroda translation [37], we
deduce:

$\Box_{\mathsf{HA}}\neg\forall x_{1}\neg\neg\exists y_{1}\forall
x_{2}\neg\neg\exists y_{2}\cdots\delta.$

Since $\mathsf{HA}\vdash\forall x_{1}\exists y_{1}\forall x_{2}\exists
y_{2}\cdots\delta\to\forall x_{1}\neg\neg\exists y_{1}\forall
x_{2}\neg\neg\exists y_{2}\cdots\delta$, we obtain:

$\Box_{\mathsf{HA}}\neg\forall x_{1}\exists y_{1}\forall x_{2}\exists
y_{2}\cdots\delta,$

that is, $\Box_{\mathsf{HA}}\neg\varphi$, as desired. ∎

From Kreisel’s observation we directly obtain the following corollary.

######  Corollary 4.6.

For every formula $\varphi$ in prenex normal form we have:

$\mathsf{HA}\vdash\Diamond_{\mathsf{PA}}\varphi\leftrightarrow\Diamond_{\mathsf{HA}}\varphi.$

##  5 Reflections on arithmetical completeness

In this section we briefly revisit the ingredients of Solovay’s arithmetical
completeness proof for $\mathsf{GL}$. We have a particular interest in the
complexity of the formulas occurring in that proof so that we can invoke
conservativity of $\mathsf{PA}$ over $\mathsf{HA}$. We first observe that the
complexity of the arithmetical realizations of propositional strictly positive
formulas can be kept low.

######  Lemma 5.1.

For every realization $\cdot^{\star}:{\textsc{Prop}}\to\Sigma_{2}$, every c.e.
theory $T$ and every p.s.p. formula $\varphi$ we have that
$\varphi^{\star_{T}}$ is $\Sigma_{2}$ over $\mathsf{HA}$, and this is provable
in $\mathsf{HA}$.

###### Proof.

By an easy induction on the complexity of $\varphi$. The only interesting case
is the complexity of $\Diamond\psi$, which is taken care of by (4.1) since the
negation of a $\Sigma_{1}$ sentence is $\Pi_{1}$, whence also $\Sigma_{2}$. ∎

This simple observation can be used to see that extending a realization using
$\mathsf{HA}$ provability or $\mathsf{PA}$ provability yields
$\mathsf{HA}$-equivalent formulas, provably in $\mathsf{HA}$.

######  Lemma 5.2.

For every realization $\cdot^{\star}:{\textsc{Prop}}\to\Sigma_{2}$ and every
p.s.p. formula $\varphi$ we have:

$\mathsf{HA}\vdash\varphi^{\star_{\mathsf{HA}}}\leftrightarrow\varphi^{\star_{\mathsf{PA}}}.$

###### Proof.

By an easy induction on $\varphi$ where the $\Diamond$ case is taken care of
by Lemma 4.4. ∎

Solovay proved the arithmetical completeness theorem for $\mathsf{GL}$ by
embedding Kripke frames into arithmetic. Given a Kripke frame with worlds
$1,\ldots,N$, a new world $0$ is added such that it can see all the other
worlds. Then, each $i\in\\{0,1,\ldots,N\\}$ is assigned an arithmetical
sentence $\lambda_{i}$ such that each $\lambda_{i}$ is independent from
$\mathsf{PA}$ and that these $\lambda_{i}$ sentences mimic the accessibility
relations between their respective worlds as described by the following lemma.
Then the realization $\cdot^{\star}$ of Solovay’s proof is defined as
$p^{\star}:=\bigvee_{i\Vdash p}\lambda_{i}$.

######  Lemma 5.3 (Embedding [13]).

  1. 5.3.1.

$\mathsf{PA}\vdash\bigvee_{i\leq N}\lambda_{i}$;

  2. 5.3.2.

$\mathsf{PA}\vdash\lambda_{i}\to\bigwedge_{j\leq N,j\neq i}\neg\lambda_{j}$,
for $i\leq N$;

  3. 5.3.3.

$\mathsf{PA}\vdash\lambda_{i}\to\bigwedge_{j\leq
N,iRj}\Diamond_{\mathsf{PA}}\lambda_{j}$, for $i\leq N$;

  4. 5.3.4.

$\mathsf{PA}\vdash\lambda_{i}\to\Box_{\mathsf{PA}}\bigvee_{j\leq
N,iRj}\lambda_{j}$, for $0<i\leq N$;

  5. 5.3.5.

$\mathbb{N}\vDash\lambda_{0}$.

The sentence $\lambda_{i}$ states that the limit of a so-called Solovay
function $f:\mathbb{N}\to\\{0,1,\ldots,N\\}$ is $i$. Each sentence is thus _a
priori_ of complexity $\Sigma_{2}$. However, by definition, the Solovay
function can only move along $R$-transitions in the frame, so we can write
$\lambda_{i}$ as a conjunction of $\Pi_{1}$ and $\Sigma_{1}$ sentences as
follows:

$\lambda_{i}=(\operatorname{\exists}x\mskip
3.0muf(x)=i)\land\operatorname{\forall}x,y\mskip 3.0mu(x\leq y\to(f(x)=i\to
f(y)=i)).$ (5.1)

We denote the class of formulas built of conjunctions and disjunctions of
$\Pi_{1}$ and $\Sigma_{1}$ formulas by $\mathcal{DC}(\Pi_{1},\Sigma_{1})$.
Since in Solovay’s proof $p^{\star}:=\bigvee_{i\Vdash p}\lambda_{i}$, it is
clear that the realization satisfies
$\cdot^{\star}:{\textsc{Prop}}\to\mathcal{DC}(\Pi_{1},\Sigma_{1})$. In fact,
$\varphi^{\star_{T}}$ still has complexity $\mathcal{DC}(\Pi_{1},\Sigma_{1})$,
which can be proved by a simple induction on $\varphi$.

######  Remark 5.4.

For any p.s.p. formula $\varphi$ we have
$\varphi^{\star_{T}}\in\mathcal{DC}(\Pi_{1},\Sigma_{1})$.

Note that $\mathcal{DC}(\Pi_{1},\Sigma_{1})\subseteq\Sigma_{2}$ over
$\mathsf{HA}$ by Lemma 4.1. As a direct consequence of the previous
observations we obtain the following result.

######  Corollary 5.5.

Let $\cdot^{\star}$ be a realization obtained via Solovay’s embedding of a
finite transitive Noetherian tree-like model. Then for any p.s.p. formula
$\varphi$:

$\mathsf{HA}\vdash\neg\varphi^{\star_{\mathsf{HA}}}\iff\mathsf{PA}\vdash\neg\varphi^{\star_{\mathsf{PA}}}.$

Moreover, this is formalizable in $\mathsf{HA}$.

###### Proof.

By Remark 5.4, Lemma 5.2, and Lemma 4.4. ∎

Note that we cannot prove a version of Corollary 5.5 without the negation: if
$\mathsf{PA}\vdash p^{\star_{\mathsf{PA}}}$ implied $\mathsf{HA}\vdash
p^{\star_{\mathsf{HA}}}$, then by the disjunction property we would have
$\mathsf{HA}\vdash\lambda_{i}$ for some $i$, which would contradict the
independence of $\lambda_{i}$ from $\mathsf{PA}$.

##  6 The strictly positive fragment of $\mathsf{PL}(\mathsf{HA})$

In this section we show that the strictly positive provability logic of
$\mathsf{HA}$ and the reflection logic of $\mathsf{HA}$ both coincide with
$\mathsf{RC}_{1}$.

######  Theorem 6.1.

Let $\varphi$ and $\psi$ be p.s.p. formulas. We have
$\varphi\vdash_{\mathsf{RC}_{1}}\psi$ if and only if for all realizations
$\cdot^{\star}$ we have
$\mathsf{HA}\vdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}$.

###### Proof.

Soundness is easy given the derivability conditions of $\Box_{\mathsf{HA}}$
(see [56]) and it was already incidentally observed in [1, Theorem 5.4.3]. For
completeness, reason as follows:

$\displaystyle\varphi\nvdash_{\mathsf{RC}_{1}}\psi$
$\displaystyle\implies\text{ there is }\cdot^{\star}\text{ s.t.
}\mathsf{PA}\nvdash\varphi^{\star_{\mathsf{PA}}}\to\psi^{\star_{\mathsf{PA}}}$
by Theorem 3.8 $\displaystyle\implies\text{ there is }\cdot^{\star}\text{ s.t.
}\mathsf{PA}\nvdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}$
by Lemma 5.2 $\displaystyle\implies\text{ there is }\cdot^{\star}\text{ s.t.
}\mathsf{HA}\nvdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}$
by (4.3).

∎

We note that there is some room for improvement and generalization,
arithmetically speaking. Can this be exploited to get a slightly larger
fragment (disjunctions seem to come for free, and boxes with a bit of extra
work)?

Recall that infinitary realizations extend finitary ones in the following
sense. Given a finitary realization $\cdot^{\star}$, we can define
$p^{\circ}:=(u=\ulcorner p^{\star}\urcorner)$. Then $p^{\circ_{\tau}}$
axiomatizes the base theory extended by the single axiom $p^{\star}$. This
infinitary realization behaves exactly like its finitary counterpart, as the
following lemma illustrates.

######  Lemma 6.2.

Let $\varphi$ be a p.s.p. formula, $\cdot^{\star}$ be a finitary realization
and $\cdot^{\circ}$ be its finitary counterpart as described above. Then:

$\mathsf{HA}\vdash\operatorname{\forall}\theta\mskip
3.0mu(\Box_{\varphi^{\circ_{\eta}}}\theta\leftrightarrow\Box_{\mathsf{HA}}(\varphi^{\star_{\mathsf{HA}}}\to\theta)).$

###### Proof.

By an easy external induction on $\varphi$. ∎

Using this the reflection logic of $\mathsf{HA}$ can be obtained as follows
(recall (3.1)).

######  Theorem 6.3.

$\mathsf{RL}(\mathsf{HA})=\mathsf{RC}_{1}$.

###### Proof.

The soundness, that $\mathsf{RC}_{1}\subseteq\mathsf{RL}(\mathsf{HA})$,
follows from a straightforward induction and was already incidentally observed
in [3, Theorem 10.3]. For the other direction, assume that
$\varphi\nvdash_{\mathsf{RC}_{1}}\psi$. With Theorem 6.1 we find
$\cdot^{\star}$ such that
$\mathsf{HA}\nvdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}$.
We now set $p^{\circ}:=(u=\ulcorner p^{\star}\urcorner)$. We have
$\mathsf{HA}\vdash\Box_{\psi^{\circ_{\eta}}}\psi^{\star_{\mathsf{HA}}}$ by
Lemma 6.2. We now check that
$\mathsf{HA}\nvdash\Box_{\varphi^{\circ_{\eta}}}\psi^{\star_{\mathsf{HA}}}$
with the following reasoning:

$\displaystyle\mathsf{HA}\vdash\Box_{\varphi^{\circ_{\eta}}}\psi^{\star_{\mathsf{HA}}}$
$\displaystyle\implies\mathsf{HA}\vdash\Box_{\mathsf{HA}}(\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}})$
by Lemma 6.2
$\displaystyle\implies\mathbb{N}\vDash\Box_{\mathsf{HA}}(\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}})$
by $\Sigma_{1}$-soundness
$\displaystyle\implies\mathsf{HA}\vdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}.$

Since
$\mathsf{HA}\nvdash\varphi^{\star_{\mathsf{HA}}}\to\psi^{\star_{\mathsf{HA}}}$
by the choice of $\cdot^{\star}$, we conclude that
$\mathsf{HA}\nvdash\Box_{\varphi^{\circ_{\eta}}}\psi^{\star_{\mathsf{HA}}}$.
Consequently, $\mathsf{HA}\nvdash\operatorname{\forall}\theta\mskip
3.0mu(\Box_{\psi^{\circ_{\eta}}}\theta\to\Box_{\varphi^{\circ_{\eta}}}\theta)$,
as was to be shown. ∎

##  7 The strictly positive fragment of $\mathsf{QPL}(\mathsf{HA})$

In this section we prove that
$\mathsf{QPL}^{+}(\mathsf{HA})=\mathsf{QRL}(\mathsf{HA})=\mathsf{QRC}_{1}$.
The proofs are essentially the same as the ones in the propositional case as
stated in Theorems 6.1 and 6.3, because we can reduce the quantified case to
the propositional case. In [3] this reduction was done in $\mathsf{PA}$ but it
can actually be obtained in $\mathsf{HA}$.

The reduction boils down to the finite model property of $\mathsf{QRC}_{1}$
(Theorem 3.6), which implies that a seemingly unrestricted universal
quantification is equivalent to a finite conjunction. This is observed in
Lemma 7.2 below. As such, the complexity of the arithmetical interpretations
of our quantified modal formulas can be restricted, as observed in Lemma 7.3.

To obtain these results, we first recall the arithmetical interpretations used
in the arithmetical completeness proof presented in [3], where finite first-
order Kripke models are embedded in arithmetic.

For the remainder of this section, we fix a certain finite constant domain
model $\mathcal{M}$. Let the domain of every world of $\mathcal{M}$ be denoted
by $M$. Let $m$ be the size of $M$, and $\lcorners\cdot\rcorners$ be a
bijection between $M$ and the set of numerals
$\\{\overline{0},\ldots,\overline{m-1}\\}$.

For a given $n$-ary predicate symbol $S$ and terms
$\bm{t}:=t_{0},\ldots,t_{n-1}$, the $\cdot^{\circledast}$ interpretation of
$S$ is defined as follows:

$\displaystyle S(\bm{t})^{\circledast}:=\bigvee_{i\leq
N}\left(\lambda_{i}\land\Phi^{S(\bm{t})}_{i}\right)\text{, where:}$
$\displaystyle\Phi_{i}^{S(\bm{t})}:=\bigvee_{\langle
a_{0},\ldots,a_{n-1}\rangle\in S^{J_{i}}}\bigwedge_{l<n}\left(\lcorners
a_{l}\rcorners=\begin{cases}y_{k}\operatorname{mod}\overline{m}&\text{if
}t_{l}=x_{k}\\\ z_{k}\operatorname{mod}\overline{m}&\text{if
}t_{l}=c_{k}\end{cases}\right).$

Here $x_{k}$ is any $\mathsf{QRC}_{1}$ variable, $y_{k}$ is the corresponding
arithmetical variable, $c_{k}$ is any $\mathsf{QRC}_{1}$ constant, $z_{k}$ is
the corresponding arithmetical variable, and $\cdot^{J_{i}}$ is the denotation
of a predicate symbol at world $i$. It is clear that $\cdot^{\circledast}$
depends on the particular choice of $\mathcal{M}$, but this dependency is
omitted in the notation for simplicity. We keep $\mathcal{M}$ fixed throughout
this section, so this should not lead to confusion.

######  Remark 7.1.

For any given finite and constant domain model $\mathcal{M}$, we have that
$S(\bm{t})^{\circledast}\in\mathcal{DC}(\Pi_{1},\Sigma_{1})$.

The $\cdot^{\circledast}$ interpretation is extended to all strictly positive
formulas as described in Definition 3.10. The interpretation
$S(\bm{t})^{\circledast}$ depends only on the values of its free variables
modulo $m$. This modular dependence propagates over all formulas, as shown by
the following lemma.

######  Lemma 7.2.

For any c.e. theory $T$, any $\mathsf{QRC}_{1}$ formula $\varphi$, and any
arithmetical variable $u$:

  1. 1.

$\mathsf{HA}\vdash\varphi^{\circledast_{T}}\leftrightarrow\varphi^{\circledast_{T}}[u{\leftarrow}(u\operatorname{mod}\overline{m})]$;

  2. 2.

$\mathsf{HA}\vdash\operatorname{\forall}u\mskip
3.0mu\varphi^{\circledast_{T}}\leftrightarrow\bigwedge_{u\in\\{\overline{0},\ldots,\overline{m-1}\\}}\varphi^{\circledast_{T}}$.

###### Proof.

The second item is a straightforward consequence of the first, which is proved
by an external induction on the complexity of $\varphi$, noting that
$\mathsf{HA}$ proves:

$(u\operatorname{mod}\overline{m})\operatorname{mod}\overline{m}=u\operatorname{mod}\overline{m}$

for any $u$. ∎

Since quantification does not essentially increase complexity, we see that the
arithmetical interpretations of $\mathcal{L}^{+}_{\Box,\forall}$ are all of
low complexity.

######  Lemma 7.3.

For any c.e. theory $T$ and any s.p. formula
$\varphi\in\mathcal{L}^{+}_{\Box,\forall}$, we have that
$\varphi^{{}^{\circledast_{T}}}\in\mathcal{DC}(\Pi_{1},\Sigma_{1})$.

###### Proof.

By an easy induction using Remark 7.1 for the base case and Lemma 7.2 for the
only non-trivial inductive step. ∎

We can now obtain the analogous of Lemma 5.2 in the quantified case. Note
however that this does not hold in general for all realizations; the claim
here is only for the specific realization $\cdot^{\circledast}$.

######  Lemma 7.4.

For any formula $\varphi\in\mathcal{L}^{+}_{\Box,\forall}$, we have
$\mathsf{HA}\vdash\varphi^{\circledast_{\mathsf{HA}}}\leftrightarrow\varphi^{\circledast_{\mathsf{PA}}}$.

###### Proof.

By an easy external induction using Lemma 4.4 for the diamond case and Lemma
7.2 for the quantifier case. ∎

Finally, we can be more specific in the statement of the completeness theorem
$\mathsf{QPL}^{+}(\mathsf{PA})\subseteq\mathsf{QRC}_{1}$.

######  Theorem 7.5 ([3, Theorem 8.7]).

Let $\varphi$ and $\psi$ be $\mathsf{QRC}_{1}$ formulas and let
$\bm{y},\bm{z}$ represent all the free variables of
$\varphi^{\circledast_{\mathsf{PA}}}\land\psi^{\circledast_{\mathsf{PA}}}$. If
$\varphi\nvdash_{\mathsf{QRC}_{1}}\psi$, then there are standard numbers
$\bm{y_{0}},\bm{z_{0}}$ such that
$\mathsf{PA}\nvdash(\varphi^{\circledast_{\mathsf{PA}}}\to\psi^{\circledast_{\mathsf{PA}}})[\bm{y}{\leftarrow}\bm{y_{0}}][\bm{z}{\leftarrow}\bm{z_{0}}]$.

With these preparations, we repeat our propositional completeness proof and
obtain a quantified completeness proof.

######  Theorem 7.6.

Let $\varphi$ and $\psi$ be formulas in $\mathcal{L}^{+}_{\Box,\forall}$. We
have $\varphi\vdash_{\mathsf{QRC}_{1}}\psi$ if and only if for all
realizations $\cdot^{*}$ we have
$\mathsf{HA}\vdash\varphi^{*_{\mathsf{HA}}}\to\psi^{*_{\mathsf{HA}}}$.

###### Proof.

Soundness is proven by a straightforward induction on
$\varphi\vdash_{\mathsf{QRC}_{1}}\psi$ and was already observed in [1, Theorem
5.4.3]. For completeness we reason as follows:

$\displaystyle\varphi\nvdash_{\mathsf{QRC}_{1}}\psi$
$\displaystyle\implies\mathsf{PA}\nvdash(\varphi^{\circledast_{\mathsf{PA}}}\to\psi^{\circledast_{\mathsf{PA}}})[\bm{y}{\leftarrow}\bm{y_{0}}][\bm{z}{\leftarrow}\bm{z_{0}}]$
by Theorem 7.5
$\displaystyle\implies\mathsf{PA}\nvdash(\varphi^{\circledast_{\mathsf{HA}}}\to\psi^{\circledast_{\mathsf{HA}}})[\bm{y}{\leftarrow}\bm{y_{0}}][\bm{z}{\leftarrow}\bm{z_{0}}]$
by Lemma 7.4
$\displaystyle\implies\mathsf{HA}\nvdash(\varphi^{\circledast_{\mathsf{HA}}}\to\psi^{\circledast_{\mathsf{HA}}})[\bm{y}{\leftarrow}\bm{y_{0}}][\bm{z}{\leftarrow}\bm{z_{0}}]$
by (4.3),

where $\bm{y},\bm{z}$ are the free variables of
$\varphi^{\circledast_{\mathsf{PA}}}$ and $\psi^{\circledast_{\mathsf{PA}}}$
(which are the same as the free variables of
$\varphi^{\circledast_{\mathsf{HA}}}$ and $\psi^{\circledast_{\mathsf{HA}}}$)
and $\bm{y_{0}},\bm{z_{0}}$ are as given by Theorem 7.5. Thus there is a
realization $\cdot^{\circledast}$ such that
$\mathsf{HA}\nvdash\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\varphi^{\circledast_{\mathsf{HA}}}\to\psi^{\circledast_{\mathsf{HA}}})$,
as we wanted to show. ∎

We now determine $\mathsf{QRL}(\mathsf{HA})$, the quantified reflection logic
of $\mathsf{HA}$. Just as in the propositional case, we can interpret a
finitary realization $\cdot^{*}$ as an infinitary one by taking
$S(\bm{t})^{\circ}:=(u=\ulcorner S(\bm{t})^{*}\urcorner)$. However, unlike in
the propositional case, the realizations $\varphi^{\circ_{\tau}}$ and
$\tau\lor(u=\ulcorner\varphi^{*}\urcorner)$ are not necessarily equivalent
(contrast with Lemma 6.2). In general, one can only prove
$T\vdash\operatorname{\forall}\theta\mskip
3.0mu\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\Box_{\varphi^{\circ_{\tau}}}\theta\to\Box_{\tau}(\varphi^{*_{T}}\to\theta))$
(see [1, Lemma 5.2.8] and the following discussion), but in the specific case
of the realization ⊛ above we can indeed prove the equivalence.

Let $\cdot^{\circledcirc}$ be the infinitary counterpart to
$\cdot^{\circledast}$, i.e., $S(\bm{t})^{\circledcirc}:=(u=\ulcorner
S(\bm{t})^{\circledast}\urcorner)$. Note that $\varphi^{\circledcirc_{\tau}}$
has same free variables as $\varphi^{\circledast_{T}}$ for any $\varphi$.

######  Lemma 7.7.

Let $\eta$ denote a standard axiomatization of $\mathsf{HA}$ and let $\varphi$
be a $\mathsf{QRC}_{1}$ formula with free variables $\bm{x}$ and constants
$\bm{c}$. Then:

$\mathsf{HA}\vdash\operatorname{\forall}\theta\mskip
3.0mu\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\Box_{\varphi^{\circledcirc_{\eta}}}\theta\leftrightarrow\Box_{\mathsf{HA}}(\varphi^{\circledast_{\mathsf{HA}}}\to\theta)),$

where $\theta$ is (the Gödel number of) a closed formula.

###### Proof.

By external induction on $\varphi$. The proof is presented for $\mathsf{PA}$
in [3, Lemma 8.8] and adapts without any problem to $\mathsf{HA}$. ∎

With this reduction from quantified to propositional we can now determine the
quantified reflection logic of $\mathsf{HA}$.

######  Theorem 7.8.

$\mathsf{QRL}(\mathsf{HA})=\mathsf{QRC}_{1}$.

###### Proof.

The inclusion $\mathsf{QRC}_{1}\subseteq\mathsf{QRL}(\mathsf{HA})$ is a
straightforward induction and is proved in [3, Theorem 10.3]. For the other
direction, we reason as in the proof of Theorem 6.3 and assume that
$\varphi\nvdash_{\mathsf{QRC}_{1}}\psi$.

By Theorem 7.6 we find $\cdot^{\circledast}$ and $\bm{y_{0}},\bm{z_{0}}$ such
that:

$\mathsf{HA}\nvdash(\varphi^{\circledast_{\mathsf{HA}}}\to\psi^{\circledast_{\mathsf{HA}}})[\bm{y}{\leftarrow}\bm{y_{0}}][\bm{z}{\leftarrow}\bm{z_{0}}].$
(7.1)

By Lemma 7.7 we get for the corresponding $\cdot^{\circledcirc_{\eta}}$ that
for arbitrary $\bm{y},\bm{z}$ we have
$\mathsf{HA}\vdash\Box_{\psi^{\circledcirc_{\eta}}}\psi^{\circledast_{\mathsf{HA}}}$.
Again by Lemma 7.7 and using (7.1), in complete analogy with the proof of
Theorem 6.3, we see that
$\mathsf{HA}\nvdash\Box_{\varphi^{\circledcirc_{\eta}}}\psi^{\circledast_{\mathsf{HA}}}$,
so $\mathsf{HA}\nvdash\operatorname{\forall}\theta\mskip
3.0mu\operatorname{\forall}\bm{y},\bm{z}\mskip
3.0mu(\Box_{\psi^{\circledcirc_{\eta}}}\theta\to\Box_{\varphi^{\circledcirc_{\eta}}}\theta)$
as was to be shown. ∎

##  8 On interpolation and the fixpoint theorem

The interpolation and fixpoint theorems are important properties of theories
and logics. In this section we consider them in the setting of
$\mathsf{QRC}_{1}$.

###  8.1 Interpolation

The predicate provability logic of Peano Arithmetic does not have the
interpolation property (due to Vardanyan, see [13]). Since
$\mathsf{QPL}(\mathsf{PA})$ fails interpolation, it is important to ask
whether our fragment does satisfy interpolation. It turns out that indeed,
both $\mathsf{RC}_{1}$ and $\mathsf{QRC}_{1}$ have interpolation, and the
proof is rather trivial.

######  Theorem 8.1.

Let $T$ be either $\mathsf{RC}$ or $\mathsf{QRC}_{1}$. If
$\varphi\vdash_{T}\psi$, then there is a formula $\chi$ in the common language
of $\varphi$ and $\psi$ such that both $\varphi\vdash_{T}\chi$ and
$\chi\vdash_{T}\psi$.

###### Proof.

By an easy induction on a proof of $\varphi\vdash_{T}\psi$ we observe that all
symbols occurring in $\psi$ already occur in $\varphi$. Consequently, we can
take $\chi:=\psi$, that is, $\psi$ is the required interpolant. ∎

###  8.2 Fixpoint theorem

The fixpoint theorem for $\mathsf{GL}$ states that for each formula $\varphi$
where all appearances of $p$ occur under the scope of a modality, we can find
a fixpoint $\chi$ of $\varphi$ where $p$ does not occur such that
$\mathsf{GL}\vdash\boxdot(p\leftrightarrow\varphi)\to(p\leftrightarrow\chi)$
(where $\boxdot\delta:=\delta\land\Box\delta$).

We observe that the fixpoint theorem cannot really be formulated in our
framework. The best we could do is to demand both $p\vdash\varphi(p,\bm{q})$
and $\varphi(p,\bm{q})\vdash p$ as antecedents (with $p$ occurring modalized
in $\varphi$) of our version of the fixpoint theorem. Note, however, that
$p\nvdash\varphi(p,\bm{q})$ for any $\varphi$ where $p$ occurs modalized. This
is due to the following elementary observation.

######  Lemma 8.2 ([2, Lemma 2.4]).

Let ${\text{d}}_{\Diamond}(\varphi)$ be the modal depth (maximum number of
nested diamonds) of $\varphi$. If $\varphi\vdash_{\mathsf{RC}_{1}}\psi$ or
$\varphi\vdash_{\mathsf{QRC}_{1}}\psi$, then
${\text{d}}_{\Diamond}(\varphi)\geq{\text{d}}_{\Diamond}(\psi)$.

###### Proof.

By an easy induction on the length of a $\mathsf{RC}_{1}$ or
$\mathsf{QRC}_{1}$ proof. ∎

Thus, $p$ cannot prove any formula $\varphi$ that is modalized in $p$ (since
the only available modality is the diamond). Our framework is hence not
expressive enough to formulate a sensible version of the fixpoint theorem.
Alternatively, we could state that the fixpoint theorem holds vacuously true.

## Acknowledgments

We are very grateful to Dick de Jongh, Mojtaba Mojtahedi, and Albert Visser,
who helped with the intuitionistic mathematics involved in this work. Their
reading, comments, suggestions and discussions substantially helped the
presentation of this paper.

## References

  * de Almeida Borges [2023] de Almeida Borges, A. (2023).  Suitable logics: provability, temporal laws, and formalization.  Ph.D. thesis, University of Barcelona.
URL https://mat.ub.edu/pop/doctorat/tesis/Thesis_Ana_Almeida.pdf

  * de Almeida Borges & Joosten [2020] de Almeida Borges, A., & Joosten, J. J. (2020).  Quantified Reflection Calculus with one modality.  In N. Olivetti, R. Verbrugge, S. Negri, & G. Sandu (Eds.) Advances in Modal Logic 13, (pp. 13–32). College Publications.
URL http://www.aiml.net/volumes/volume13/deAlmeidaBorges-Joosten.pdf

  * de Almeida Borges & Joosten [2023] de Almeida Borges, A., & Joosten, J. J. (2023).  An escape from Vardanyan’s Theorem.  The Journal of Symbolic Logic, 88(4), 1613–1638.
URL https://www.cambridge.org/core/journals/journal-of-symbolic-
logic/article/an-escape-from-vardanyans-
theorem/03E13D4C282563F918AF77CF6E2830DA

  * Artemov & Beklemishev [2004] Artemov, S., & Beklemishev, L. (2004).  Provability logic.  In D. Gabbay, & F. Guenthner (Eds.) Handbook of Philosophical Logic, 2nd ed., vol. 13, (pp. 229–403). Dordrecht: Springer.
  * Artemov [1986] Artemov, S. N. (1986).  Numerically correct logics of provability.  Doklady Akademii Nauk SSSR, 290(6), 1289–1292.  In Russian.
  * Artemov & Japaridze [1990] Artemov, S. N., & Japaridze, G. K. (1990).  Finite Kripke models and predicate logics of provability.  Journal of Symbolic Logic, 55(3), 1090–1098.
  * Beklemishev [2005] Beklemishev, L. D. (2005).  Veblen hierarchy in the context of provability algebras.  In P. Hájek, L. Valdés-Villanueva, & D. Westerståhl (Eds.) Logic, Methodology and Philosophy of Science, Proceedings of the Twelfth International Congress, (pp. 65–78). Kings College Publications.
  * Beklemishev [2012] Beklemishev, L. D. (2012).  Calibrating provability logic: From modal logic to Reflection Calculus.  In T. Bolander, T. Braüner, T. S. Ghilardi, & L. Moss (Eds.) Advances in Modal Logic 9, (pp. 89–94). London: College Publications.
  * Beklemishev [2018] Beklemishev, L. D. (2018).  A note on strictly positive logics and word rewriting systems.  In S. Odintsov (Ed.) Larisa Maximova on Implication, Interpolation, and Definability, vol. 15, (pp. 61–70). Berlin, Heidelberg: Springer.
  * Beklemishev [2021] Beklemishev, L. D. (2021).  Strictly positive provability logics: Recent progress and open questions.
URL http://yongcheng.whu.edu.cn/webPageContent/Goedel2021/Goedel-Lev.pdf

  * Beklemishev et al. [2014] Beklemishev, L. D., Fernández-Duque, D., & Joosten, J. J. (2014).  On provability logics with linearly ordered modalities.  Studia Logica, 102, 541–566.
  * Berarducci [1989] Berarducci, A. (1989).  ${\Sigma}^{0}_{n}$-interpretations of modal logic.  Bollettino dell’Unione Matematica Italiana, 7(3-A), 177–184.
  * Boolos [1993] Boolos, G. S. (1993).  The logic of provability.  Cambridge: Cambridge University Press.
  * Boolos & McGee [1987] Boolos, G. S., & McGee, V. R. (1987).  The degree of the set of sentences of predicate provability logic that are true under every interpretation.  The Journal of Symbolic Logic, 52, 165–171.
  * Dashkov [2012] Dashkov, E. V. (2012).  On the positive fragment of the polymodal provability logic GLP.  Mathematical Notes, 91(3–4), 318–333.
  * de Jongh [1970] de Jongh, D. (1970).  The maximality of the intuitionistic predicate calculus with respect to Heyting’s Arithmetic.  The Journal of Symbolic Logic, 36, 606.
  * de Jongh et al. [1991] de Jongh, D., Jumelet, M., & Montagna, F. (1991).  On the proof of Solovay’s theorem.  Studia Logica, 50, 51–69.
  * Fagin et al. [1995] Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995).  Reasoning About Knowledge.  Cambridge, MA: MIT Press.
  * Fernández-Duque & Joosten [2014] Fernández-Duque, D., & Joosten, J. J. (2014).  Well-orders in the transfinite Japaridze algebra.  Logic Journal of the IGPL, 22(6), 933–963.
  * Friedman [1975] Friedman, H. (1975).  The disjunction property implies the numerical existence property.  Proceedings of the National Academy of Sciences, 72(8), 2877–2878.
  * Friedman [1978] Friedman, H. (1978).  Classically and intuitionistically provably recursive functions.  In D. S. Scott, & G. H. Muller (Eds.) Higher Set Theory, vol. 699, (pp. 21–28). Springer Verlag.
  * Fujiwara & Kurahashi [2023] Fujiwara, M., & Kurahashi, T. (2023).  Prenex normalization and the hierarchical classification of formulas.  arXiv:2302.11808 [math.LO].
  * Gabbay et al. [2003] Gabbay, D. M., Kurucz, A., Wolter, F., & Zakharyaschev, M. (2003).  Many-dimensional modal logics: Theory and applications.  Elsevier.
  * Gabbay et al. [2009] Gabbay, D. M., Shehtman, V. B., & Skvortsov, D. P. (2009).  Quantification in Nonclassical Logic, Volume 1.  Amsterdam: Elsevier.
  * Goldblatt [2011] Goldblatt, R. (2011).  Quantifiers, propositions and identity, admissible semantics for quantified modal and substructural logics.  Cambridge University Press.
  * Hájek & Pudlák [1993] Hájek, P., & Pudlák, P. (1993).  Metamathematics of First Order Arithmetic.  Berlin, Heidelberg, New York: Springer-Verlag.
  * Hao & Tourlakis [2021] Hao, Y., & Tourlakis, G. (2021).  An arithmetically complete predicate modal logic.  Bulletin of the Section of Logic.
URL https://czasopisma.uni.lodz.pl/bulletin/article/view/8441

  * Hughes & Cresswell [1996] Hughes, G. E., & Cresswell, M. J. (1996).  A New Introduction to Modal Logic.  Routledge.
  * Iemhoff [2001] Iemhoff, R. (2001).  On the admissible rules of intuitionistic propositional logic.  Journal of Symbolic Logic, (pp. 281–294).
  * Japaridze [1988] Japaridze, G. K. (1988).  The polymodal provability logic.  In Intensional logics and logical structure of theories: material from the fourth Soviet-Finnish symposium on logic, Telavi, May 20–24, 1985, (pp. 16–48). Metsniereba.  In Russian.
  * Kikot et al. [2019] Kikot, S., Kurucz, A., Tanaka, Y., Wolter, F., & Zakharyaschev, M. (2019).  Kripke completeness of strictly positive modal logics over meet-semilattices with operators.  The Journal of Symbolic Logic, 84(2), 533–588.
  * Kontchakov et al. [2005] Kontchakov, R., Kurucz, A., & Zakharyaschev, M. (2005).  Undecidability of first-order intuitionistic and modal logics with two variables.  Bulletin of Symbolic Logic, 11(3), 428–438.
  * Kreisel [1951] Kreisel, G. (1951).  On the interpretation of non-finitist proofs — Part I.  The Journal of Symbolic Logic, 16(4), 241–267.
  * Kripke [1963] Kripke, S. A. (1963).  Semantical considerations on modal logic.  Acta Philosophica Fennica, 16, 83–94.
  * Kurahashi [2013] Kurahashi, T. (2013).  On predicate provability logics and binumerations of fragments of Peano Arithmetic.  Archive for Mathematical Logic, 52, 871–880.
  * Kurahashi [2022] Kurahashi, T. (2022).  On inclusions between quantified provability logics.  Studia Logica, 110, 165–188.
  * Kuroda [1951] Kuroda, S. (1951).  Intuitionistische Untersuchungen der formalistischen Logik.  Nagoya Mathematical Journal, 2, 35–47.
  * Ladner [1977] Ladner, R. E. (1977).  The computational complexity of provability in systems of modal propositional logic.  SIAM journal on computing, 6(3), 467–480.
  * Leivant [1979] Leivant, D. (1979).  Absoluteness in intuitionistic logic, vol. 73.  Amsterdam: Mathematical Centre Tract.  The Thesis was originally published in 1975.
  * Litak & Wolter [2005] Litak, T., & Wolter, F. (2005).  All finitely axiomatizable tense logics of linear time flows are coNP-complete.  Studia Logica, 81, 153–165.
  * McGee [1985] McGee, V. R. (1985).  Truth and Necessity in Partially Interpreted Languages.  Ph.D. thesis, University of California, Berkeley.
  * Mojtahedi [2022] Mojtahedi, M. (2022).  On provability logic of HA.  arXiv:2206.00445 [math.LO].
  * Myhill [1973] Myhill, J. (1973).  A note on indicator functions.  Proceedings of the AMS, 39, 181–183.
  * Pakhomov [2014] Pakhomov, F. (2014).  On the complexity of the closed fragment of Japaridze’s provability logic.  Archive for Mathematical Logic, 53(7–8), 949–967.
  * Rybakov & Shkatov [2019] Rybakov, M., & Shkatov, D. (2019).  Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter.  Studia Logica, 107(4), 695–717.
  * Rybakov [1997] Rybakov, V. V. (1997).  Admissibility of logical inference rules.  Studies in Logic. Amsterdam: Elsevier.
  * Shapirovsky [2008] Shapirovsky, I. (2008).  PSPACE-decidability of Japaridze’s polymodal logic.  In C. Areces, & R. Goldblatt (Eds.) Advances in Modal Logic 7, (pp. 289–304). College Publications.
  * Solovay [1976] Solovay, R. M. (1976).  Provability interpretations of modal logic.  Israel Journal of Mathematics, 28, 33–71.
  * Svyatlovskiy [2018] Svyatlovskiy, M. V. (2018).  Axiomatization and polynomial solvability of strictly positive fragments of certain modal logics.  Mathematical Notes, 103, 952–967.
  * Troelstra [1973] Troelstra, A. S. (1973).  Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, vol. 344 of Lecture Notes in Mathematics.  Berlin: Springer.
  * Vardanyan [1986] Vardanyan, V. A. (1986).  Arithmetic complexity of predicate logics of provability and their fragments.  Doklady Akad. Nauk SSSR, 288(1), 11–14.  In Russian. English translation in Soviet Mathematics Doklady 33, 569–572 (1986).
  * Vardanyan [1988] Vardanyan, V. A. (1988).  Bounds on the arithmetical complexity of predicate logics of provability.  In S. N. Adyan (Ed.) Questions of Cybernetics: Complexity of Computation and Applied Mathematical Logic, vol. 134 of Scientific Council of the USSR Academy of Sciences on the complex problem “Cybernetics”, (pp. 46–72). Academy of Sciences of the USSR.  In Russian.
  * Visser [1985] Visser, A. (1985).  Evaluation, provably deductive equivalence in Heyting’s Arithmetic of substitution instances of propositional formulas.  Logic Group Preprint Series 4, Faculty of Humanities, Philosophy, Utrecht University, Janskerkhof 13, 3512 BL Utrecht.
  * Visser [2002] Visser, A. (2002).  Substitutions of ${\Sigma}^{0}_{1}$-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic.  Annals of Pure and Applied Logic, 114, 227–271.
  * Visser & de Jonge [2006] Visser, A., & de Jonge, M. (2006).  No escape from Vardanyan’s theorem.  Archive for Mathematical Logic, 45(5), 539–554.
  * Visser & Zoethout [2019] Visser, A., & Zoethout, J. (2019).  Provability logic and the completeness principle.  Annals of Pure and Applied Logic, 170(6), 718–753.
  * Wolter & Zakharyaschev [2001] Wolter, F., & Zakharyaschev, M. (2001).  Decidable fragments of first-order modal logics.  The Journal of Symbolic Logic, 66(3), 1415–1438.
  * Yavorsky [2002] Yavorsky, R. E. (2002).  On arithmetical completeness of first-order logics of provability.  In F. Wolter, H. Wansing, M. de Rijke, & M. Zakharyaschev (Eds.) Advances in Modal Logic 3, (pp. 1–16). World Scientific Publishing Co. Pte. Ltd.