Abstract

In epistemic logic, the beliefs of an agent are modeled in a way very similar to knowledge, except that they are fallible. Thus, the pattern of an agent’s true beliefs is an interesting subject to study. In this paper, we conduct a systematic study on a novel modal logic with the bundled operator ⊡ϕ:=□ϕ∧ϕ as the only primitive modality, where ⊡ captures the notion of true belief. With the help of a novel notion of ⊡-bisimulation, we characterize the expressivity of this new language on relational models, and offer various completeness results. We also discuss some interesting connections between our work and previous works on reflexive-insensitive logics and the so-called boxdot conjecture. Finally, we study two generalizations of the ⊡-operator: one is the iterated true belief operator □nϕ:=ϕ∧□ϕ∧⋯∧□nϕ, the other is the neighborhood semantics for the ⊡-operator.