Assuming the existence of suitable large cardinals, we show it is consistent that the Provability logic $\mathbf {GL}$ is complete with respect to the filter sequence of normal measures. This result answers a question of Andreas Blass from 1990 and a related question of Beklemishev and Joosten.

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$—the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$.

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal {M}$ , or an axiomatization S thereof, we find a modal logic M such that a modal sentence $\varphi $ is a theorem of M if and only if the sentence $\varphi ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal {M}$ or a theorem of S under all such translations. To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and establish the completeness of a family of noncongruent modal logics whose internal logic is nonclassical with respect to this semantics.

We consider Hilbert-style non–well-founded derivations in the Gödel-Löb provability logic GL and establish that GL with the obtained derivability relation is globally complete for algebraic and neighbourhood semantics.

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A (Definition 2.4). We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $ (Definition 3.17).

In this article, we tell a story about incompleteness in modal logic. The story weaves together an article of van Benthem (1979), “Syntactic aspects of modal incompleteness theorems,” and a longstanding open question: whether every normal modal logic can be characterized by a class of completely additive modal algebras, or as we call them, ${\cal V}$-baos. Using a first-order reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem’s article resolves the open question in the negative. In addition, for the case of bimodal logic, we show that there is a naturally occurring logic that is incomplete with respect to ${\cal V}$-baos, namely the provability logic $GLB$ (Japaridze, 1988; Boolos, 1993). We also show that even logics that are unsound with respect to such algebras do not have to be more complex than the classical propositional calculus. On the other hand, we observe that it is undecidable whether a syntactically defined logic is ${\cal V}$-complete. After these results, we generalize the Blok Dichotomy (Blok, 1978) to degrees of ${\cal V}$-incompleteness. In the end, we return to van Benthem’s theme of syntactic aspects of modal incompleteness.

Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.

For a set of formulas Γ, define predicative oracle reflection for T over Γ (Pred–O–RFNΓ(T)) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then

$$\forall \,\lambda < {\rm{\Lambda }}\,([\lambda |X]_T^{\rm{\Lambda }}\varphi \to \varphi ).$$

In particular, define predicative oracle consistency (Pred–O–Cons(T)) as Pred–O–RFN{0=1}(T).

Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then,

$${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left( {{\rm{ACA}}} \right).$$

We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic.

Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles.

Given a scattered space $\mathfrak{X} = \left( {X,\tau } \right)$ and an ordinal λ, we define a topology $\tau _{ + \lambda } $ in such a way that τ +0 = τ and, when $\mathfrak{X}$ is an ordinal with the initial segment topology, the resulting sequence {τ +λ}λ∈Ord coincides with the family of topologies $\left\{ {\mathcal{I}_\lambda } \right\}_{\lambda \in Ord} $ used by Icard, Joosten, and the second author to provide semantics for polymodal provability logics.

We prove that given any scattered space $\mathfrak{X}$ of large-enough rank and any ordinal λ > 0, GL is strongly complete for τ + λ. The special case where $\mathfrak{X} = \omega ^\omega + 1$ and λ = 1 yields a strengthening of a theorem of Abashidze and Blass.

In this paper we give a new proof of the characterization of the closed fragment of the provability logic of Heyting's Arithmetic. We also provide a characterization of the closed fragment of the provability logic of Heyting's Arithmetic plus Markov's Principle and Heyting's Arithmetic plus Primitive Recursive Markov's Principle.