Search

Given a class of linear order types C, we identify and study several different classes of trees, naturally associated with C in terms of how the paths in those trees are related to the order types belonging to C. We investigate and completely determine the set-theoretic relationships between these classes of trees and between their corresponding first-order theories. We then obtain some general results about the axiomatization of the first-order theories of some of these classes of trees in terms of the first-order theory of the generating class C, and indicate the problems obstructing such general results for the other classes. These problems arise from the possible existence of nondefinable paths in trees, that need not satisfy the first-order theory of C, so we have started analysing first-order definable and undefinable paths in trees.

In Conradie, Goranko, and Vakarelov (2006, Logical Methods in Computer Science, 2) we introduced a new algorithm, , for computing first-order equivalents and proving the canonicity of modal formulae of the basic modal language. Here we extend , first to arbitrary and reversive polyadic modal languages, and then to hybrid polyadic languages too. We present the algorithm, illustrate it with some examples, and prove its correctness with respect to local equivalence of the input and output formulae, its completeness with respect to the polyadic inductive formulae introduced in Goranko and Vakarelov (2001, J. Logic. Comput., 11, 737–754) and Goranko and Vakarelov (2006, Ann. Pure. Appl. Logic, 141, 180–217), and the d-persistence (with respect to descriptive frames) of the formulae on which the algorithm succeeds. These results readily expand to completeness with respect to hybrid inductive polyadic formulae and di-persistence (with respect to discrete frames) in hybrid reversive polyadic languages.

This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. We then consider a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees.

Building on a new approach to polyadic modal languages and Sahlqvist formulas introduced in [10] we define Sahlqvist formulas in hybrid polyadic modal languages containing nominals and universal modality or satisfaction operators. Particularly interesting is the case of reversive polyadic languages, closed under all ‘inverses’ of polyadic modalities because the minimal valuations arising in the computation of the first-order equivalents of polyadic Sahlqvist formulae are definable in such languages and that makes the proof of first-order definability and canonicity of these formulas a simple syntactic exercise. Furthermore, the first-order definability of Sahlqvist formulas immediately transfers to arbitrary polyadic languages, while the direct transfer of canonicity requires a more involved proof-theoretic analysis.

The paper investigates a simple and natural enrichment of the usual modal language !£ = !£