A logics' property is decidable in a class of logics if there exists an algorithm that decides whether a finitely axiomatizable logic in the class has the property. Many properties are undecidable for bimodal logics but decidable for linear tense logics, which leads to a general question on how the interactions of modalities affect the decidability of properties. In this paper, we study the decidability of properties for transitive tense logics and show that most properties are undecidable in the lattice NExt(K4t) of transitive tense logics, including Kripke completeness, the finite model property, and decidability. Our proof method adapts Chagrov's approach of constructing a reduction from an undecidable problem of Minsky machines to the decision problem for logics' properties, yielding a general scheme of proving the undecidability of these properties.
Distributed knowledge is one of the better known group knowledge modalities. While its intuitive idea is relatively clear, there is ample room for interpretation of details. We investigate 12 definitions of distributed knowledge that differ from each other in the kinds of information sharing the agents can perform in order to achieve shared mutual knowledge of a proposition. We then show which kinds of distributed knowledge are equivalent, and which kinds imply each other, i.e., for any two variants $\tau_1$ and $\tau_2$ of distributed knowledge we show whether a proposition $\phi$ being distributed knowledge under definition $\tau_1$ implies that $\phi$ is distributed knowledge under definition $\tau_2$.
Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz. In this paper, we provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.
