Non-definability of the class of complete bundled trees

Abstract
In several semantics for branching-time logic, the evaluation rules involve a quantification over the set of all histories (that is, maximal linearly ordered sets) in a given tree-like structure T. These semantics are often generalized by replacing these quantifications by quantifications over a bundle in T, that is, over a set of histories fulfilling suitable closure properties. According to this generalization, the basic semantical structures are pairs 〈T, B〉 (bundled trees) in which B is a bundle in T. The problem of the definability of the class of complete bundled trees, in a given class G, concerns the existence of a set Γ of formulas such that, for every bundled tree 〈T, B〉 in G, Γ is true in 〈T, B〉 if and only if B is the set of all histories in T. In Ockhamist branching-time logic, (singleton) sets Γ corresponding to particular classes G have been found. It will be proved that Γ does not exist if G is the class of all bundled trees. Keywords:Temporal Logic, Branching-Time, Bundled Trees, Definability

This publication has 0 references indexed in Scilit: