Branching-time logic with quantification over branches: The point of view of modal logic

In Ockhamist branching-time logic [Prior 67], formulas are meant to be evaluated on a specified branch, or history, passing through the moment at hand. The linguistic counterpart of the manifoldness of future is a possibility operator which is read as ‘at some branch, or history (passing through the moment at hand)’. Both the bundled-trees semantics [Burgess 79] and the 〈moment, history〉 semantics [Thomason 84] for the possibility operator involve a quantification over sets of moments. The Ockhamist frames are (3-modal) Kripke structures in which this second-order quantification is represented by a first-order quantification. The aim of the present paper is to investigate the notions of modal definability, validity, and axiomatizability concerning 3-modal frames which can be viewed as generalizations of Ockhamist frames.

A new proof of Sahlqvist's theorem on modal definability and completeness

There are not many global results on modal logics. One of these is the following theorem by Sahlqvist on completeness and correspondence for a wide class of modal formulae (including many well known logics, e.g. D, T, B, S4, K4, S5, …) (see [S]).Sahlqvist's Theorem. Let A be any modal formula which is equivalent to a conjunction of formulae of the form □m(A1 → A2), where m ≥ 0, A2 is positive and A1 is obtained from propositional variables and their negations applying ∧, ∨, ♢, and □ in such a way that no positive occurrence of a variable is in a subformula of the form B1 ∨ B2 or ♢ B1 within the scope of some □. Then A corresponds effectively to a first order formula, and L + A is canonical whenever Lis a canonical logic.A formula A satisfying the above conditions is henceforth called a Sahlqvist formula. Unfortunately, till now, the only complete proof was the original proof of Sahlqvist (a proof of the correspondence half has also been given by van Benthem [vB]). It is so complicated and long that even in an advanced textbook of modal logic [HC] it has not found a place. Here, by considering general frames as topological spaces, an attitude which we developed in [TD], we give a proof of Sahlqvist's theorem simplified to such an extent that one can easily grasp the key idea on which it is based and apply the resulting algorithm to specific modal formulae in a straightforward manner, suitable even for implementation on a personal computer. This key idea also improves on previous preliminary work in the same direction (see [S1], [S2]).