Beyond pure axioms: Node creating rules in hybrid tableaux
Patrick Blackburn, Balder ten Cate · UvA-DARE (University of Amsterdam) · 2002
We present a method of extending the tableau calculus for the basic hybrid lan-guage which automatically yields completeness results for many frame classes that cannot be defined by means of pure axioms (for example, Church-Rosser frames). The extended calculus makes use of node-creating rules. These rules trade on the idea of using nominals to perform skolemization on formulas of the strong hybrid language. Alternatively, viewing them from a Hilbert-style perspective, such rules can be viewed as a systematic generalization of Gabbay’s irreflexivity rule. Our completeness result covers all frame classes definable by pure nominal-free univer-sal existential sentences of the strong hybrid language. This properly includes all frame classes definable by universal existential first-order sentences. 1 Basic Hybrid Logic Basic hybrid logic is the result of extending modal logic with nominals and the @-operator. Suppose we are given a set σ of modalities, and two (count-ably infinite) disjoint sets PROP (whose elements are typically written p, q, and r, possibly subscripted, and called proposition letters) and NOM (whose elements are typically written i, j, k, and l, possibly subscripted, and called nominals). Then the basic hybrid language over σ, PROP and NOM is defined as follows: φ:: = p | i | ¬φ | φ ∧ ψ | 4(φ1,... φn) | @iφ. Here p is a proposition letter, i is a nominal, and 4 is an n-ary modality (an element of σ). Thus, except for the clauses for i and @iφ, this is the standard definition of a modal language with arbitrary arity modalities (see, for example, Definition 1.12 in [6]). We follow the usual convention of writing 3φ rather than 4(φ) when working with unary modalities. What do the clauses for i and @iφ give us? Nominals are special proposi-tion letters that are true at precisely one node in any model: they ‘name’, or ‘label’, the unique node they are true at. The @ operator allows us to assert that a formula is true at a named node: