16 problems

Let ${\bf GL}$ be Gödel–Löb provability logic, let … and define Solovay's logic by … Let ${\bf S5}$ denote the modal logic of equivalence frames, and let $\rightthreetimes$ denote…

Expanding commutator conjecture. Setting $\mathsf{L}_v\in\{\mathsf{K4},\mathsf{K4.3}\}$ should lead to incompleteness, whereas setting…

Linearization generality conjecture. This technique should be usable in other settings to extract linear nested sequent systems from tree sequent or nested sequent systems.

Let ${\sf iPH}_{\Sigma}$ be the logic introduced in the subsection for $\Sigma_1$-preservativity, and let a $\Sigma_1$-substitution $\sigma$ assign $\Sigma_1$ arithmetical formulas…

Let ${\sf iPH}$ be the logic over the language with binary modal operator $\rhd$ introduced for arithmetical interpretations in Heyting arithmetic ${\rm HA}$. An arithmetical inter…

Let $\mathbf{GL} \otimes \mathbf{K}$ and $\mathbf{GL} \otimes \mathbf{GL}$ be the bimodal logics obtained from the provability logic $\mathbf{GL}$ paired respectively with…

Cieśliński–Urbaniak's conjecture. Any two distinct instances $Y^R(\overline{m})$ and $Y^R(\overline{n})$ are not provably equivalent.

Let $\widetilde{\mathfrak{G}_1^{\bullet}}$ be the frame whose validity on the closed fragment $\mathcal{F}_1$ characterizes provability in ${\mathrm{PRA}}$, and let…

Characterizations and reductions conjecture. The following characterizations and reductions hold:

Let $A$ be a finitely axiomatized sequential theory and let $N_0:{\sf S}^1_2\lhd A$. For an interpretation $M:A\rhd A$, let $\rho(M)$ denote its complexity, and let $\mathcal I_n$…

Let ${\sf HA}^*$ be the arithmetic theory considered in the paper, and let $\Box A$ denote the provability modality for modal propositions. Let $\iH^*$ be the intuitionistic modal…

Let $\mathsf{Con}^\alpha$ denote the transfinite iterate of the consistency operator along a recursive well-ordering $\alpha$ on true sentences, and let $1\mathsf{Con}$ be the cons…

Let $T$ be a theory, and let ${\mathrm{RC}^\nabla\hspace{-0.7pt}}$ be the reflection calculus with modalities $\Diamond_n$ and $\nabla_n$. An arithmetical interpretation $*$ in…

Let $A$ and $B$ be formulas, and let ${\textup{\textbf{IL}}{\sf{W^*P_0}}}$ and ${\textup{\textbf{IL}}({\rm All})}$ denote the corresponding interpretability logics, with…

Boxdot conjecture. Every normal modal logic $L$ satisfying

Uniform-exponent conjecture. There is no uniform $N$ such that, for every $n$, there is a decision algorithm for $GLP^n_0$ with running time $\mathcal{O}(|\varphi|^N)$.