A finite axiomatization of the set of strongly valid Ockhamist formulas (Q1066884)

Ockhamist (propositional) logic is a normal 3-modal logic in which one operator, \(\diamond\), expresses S5-possibility and the others, P and F, are tense operators for linear time. The usual interpretations for this logic are trees and the propositional variables are assumed to range over a set \({\mathcal B}\) of branches. The ''accessibility'' relation connected with the tense operators is the set-theoretical inclusion between branches, while two branches are related with respect to \(\diamond\) iff they have the same initial point. Ockhamist strong validity is defined by requiring that (1) \({\mathcal B}\) is closed under inclusions and extensions and (2) for every point x in the tree, there is a branch in \({\mathcal B}\) which passes through x. In the paper a finite axiomatization is provided for this concept of validity. The main result is a sort of diagram-completion in \(<{\mathcal M},{\mathcal R},\prec >\), where \({\mathcal M}\) is the set of maximal consistent sets, \({\mathcal R}\) is the relation (on \({\mathcal M})\) corresponding to \(\diamond\), and \(\prec\) is the relation corresponding to P and F. There exists an equivalence relation \({\mathcal R}^*\subseteq {\mathcal R}\) satisfying the following conditions: (1) \({\mathcal R}^*\) has all the properties which are needed for a Kripke-Lemmon construction; (2) for all maximal consistent sets \(\Delta\), \(\Sigma\), \(\Gamma\), \(\Delta\) ', \(\Gamma\) ' if \(\Delta\) \(\prec \Sigma \prec \Gamma\), \(\Delta\) \({\mathcal R}^*\Delta '\), and \(\Gamma\) \({\mathcal R}^*\Gamma '\), then (at least in the relevant cases) \(\Sigma\) \({\mathcal R}^*\Sigma '\) and \(\Delta\) '\(\prec \Sigma '\prec \Gamma '\) hold for a suitable maximal consistent set \(\Sigma\) '.