Introducing reactive modal tableaux (Q1935590)

The paper shows how to build reactive Beth tableaux for modal logics characterized by means of reactive Kripke frames. The idea of reactivity is based on the observation that we can change the logic of a relational frame, making it more dynamic, if we make the possible moves from some state dependent on the path which leads to this state. Formally it deserves to treat paths as additional states of the structure. This solution was already applied by Gabbay and his cooperators to characterize contrary-to-duty obligations, hierarchical conditionals, nonmonotonic consequence, and other things. The paper starts with the case study of a simple logic of one-point reflexive frame and shows how to make it reactive. First, the simplest case of so-called switch reactive models is discussed, where the notion of \(k\)-level arrow is inductively defined. The set of these arrows generalizes the ordinary accessibility relation (the set of 1-level arrows). In the rest of the paper, more general and involved constructions are introduced and Beth tableaux for them are considered. Among other things, some axiomatic systems are presented with a sketch of the completeness result, and it is shown that reactive frames are stronger than ordinary Kripke frames. In general, it is shown in a semantical way how to turn tableaux reactive by addition of higher-level arrows and allows the model to change accordingly. The last section presents a syntactical approach with definitions of reactive tableaux complexity, feasibility and validity algorithm.