We determine the strictly positive fragment \(\textsf{QPL}^+(\textsf{HA})\) of the quantified provability logic \(\textsf{QPL}(\textsf{HA})\) of Heyting Arithmetic. We show that \(\textsf{QPL}^+(\textsf{HA})\) is decidable and that it coincides with \(\textsf{QPL}^+(\textsf{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 [ 14 ]. On our way to proving these results, we carve out the strictly positive fragment \(\textsf{PL}^+(\textsf{HA})\) of the provability logic \(\textsf{PL}(\textsf{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 [ 43 ], where an axiomatization for \(\textsf{PL}(\textsf{HA})\) is provided. This axiomatization, although decidable, is of considerable complexity. (shrink)

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)

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)

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^+$$.

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.