Including Separation in the Modal Logic of Subset Spaces
Subsequently, we present 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. This corresponds to the intuitive notion that more and more precise measurements imply that the measured quantity lies within bounds of possibility which accordingly become smaller and smaller. Now, separating sets of knowledge states enables one to determine the future behaviour of these sets more rigorously. In fact, it may be controlled by formulas how they decompose, leading to more precise assertions about the measured quantity. In this way the expressive power of the underlying logical language is strengthened so that it becomes better suited to the reasoning about knowledge. - We introduce and study a trimodal logic representing the reasoning formalism just sketched. Besides a knowledge operator and a time operator, which corresponds to the effort of measurement and reminds of the nexttime operator of usual temporal logic, a separation operator is present in our system. So-called subset tree models appear as the relevant semantical structures. We presend and discuss an axiomatization of the set of valid formulas encompassing the three operators and their interaction. Afterwards the completeness of given axiomatization is proved; this goes to make up the technical part of the paper. Concerning the decidability of the system we only sketch the correctness proof of a corresponding procedure.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten