Separating sets by modal formulas

Abstract

Subsequently, we introduce a reasoning formalism which in particular allows to express that certain sets in a system of subsets of a given set are disjoint. The main purpose of considering such a family of subsets is to be able to investigate how knowledge grows as subsets shrink in the course of time. We actually introduce a trimodal logic: we have a system containing operators for knowledge and time, of which the latter corresponds to the effort of measurement and reminds of the nexttime operator of temporal logic; an operator separating sets is added then. So-called subset tree models appear as the relevant semantical structures.We present an axiomatization of the set of valid formulas encompassing the three operators and their interaction. Afterwards the completeness of the given axiomatization is proved. We also give arguments showing that the logic is decidable.