Reactive intuitionistic tableaux (Q542126)

Every ordinary Kripke model \({\mathfrak m}\) for intuitionistic propositional logic turns into a so-called pre-reactive Kripke model \({\mathfrak n}\) whose worlds are the finite increasing (relative to the immediate accessibility) sequences of worlds in \({\mathfrak m}\), where the accessibility relation \(\alpha\preceq\beta\) means that \(\alpha\) is an initial subsequence of \(\beta\), and for every atom \(A\), \((*)\) \([\alpha\models A\text{ in }{\mathfrak n}\Leftrightarrow|\alpha|\models A\text{ in }{\mathfrak m}]\), where \(|\alpha|\) is the end element in \(\alpha\). In fact, these models are equivalent in the sense that \((*)\) holds for every formula \(A\). A reactive intuitionistic Kripke frame is obtained from a pre-reactive one by forbidding some sequences. Pre-reactive Beth tableaux are defined too. It is proved that the logic defined by the reactive frames is intuitionistic logic. There exists a reactive frame whose logic is not complete for any class of ordinary intuitionistic Kripke frames. This means that reactive semantics is stronger than the ordinary Kripke semantics.