We study modal companions of $$K4^+$$, the strictly positive fragment of K4. We partially find the boundary between all normal extensions of K4 and modal companions of $$K4^+$$ among them. We also show that there is no greatest modal companion of $$K4^+$$.

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})$. (shrink)

We study modal companions of \(K4^+\), the strictly positive fragment of _K_4. We partially find the boundary between all normal extensions of _K_4 and modal companions of \(K4^+\) among them. We also show that there is no greatest modal companion of \(K4^+\).

Positive modal algebras are the$$\left\langle { \wedge, \vee,\diamondsuit,\square,0,1} \right\rangle $$-subreducts of modal algebras. We prove that the variety of positive S4-algebras is not locally finite. On the other hand, the free one-generated positive S4-algebra is shown to be finite. Moreover, we describe the bottom part of the lattice of varieties of positive S4-algebras. Building on this, we characterize structurally complete varieties of positive K4-algebras.

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same (...) consequence relations for a given spi-logic. (shrink)