A model-theoretic approach to descriptive general frames: the van Benthem characterization theorem

The celebrated van Benthem characterization theorem states that on Kripke structures modal logic is the bisimulation-invariant fragment of first-order logic. In this paper, we prove an analogue of the van Benthem characterization theorem for models based on descriptive general frames. This is an important class of general frames for which every modal logic is complete. These frames can be represented as Stone spaces equipped with a ‘continuous’ binary relation. The proof of our theorem generalizes Rosen’s proof of the van Benthem theorem for finite frames and uses as an essential technique a new notion of descriptive unravelling. We also develop a basic model theory for descriptive general frames and show that in many ways it behaves like the model theory of finite structures. In particular, we prove the failure of the compactness theorem, of the Beth definability theorem, of the Craig interpolation theorem and of the upward Löwenheim–Skolem theorem.1

SOME MODEL THEORY OF GUARDED NEGATION

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.

INFINITARY PROPOSITIONAL RELEVANT LANGUAGES WITH ABSURDITY

Analogues of Scott’s isomorphism theorem, Karp’s theorem as well as results on lack of compactness and strong completeness are established for infinitary propositional relevant logics. An “interpolation theorem” (of a particular sort introduced by Barwise and van Benthem) for the infinitary quantificational boolean logic L∞ω holds. This yields a preservation result characterizing the expressive power of infinitary relevant languages with absurdity using the model-theoretic relation of relevant directed bisimulation as well as a Beth definability property.

Beth Definability in Expressive Description Logics

The Beth definability property, a well-known property from classical logic, is investigated in the context of description logics: if a general L-TBox implicitly defines an L-concept in terms of a given signature, where L is a description logic, then does there always exist over this signature an explicit definition in L for the concept? This property has been studied before and used to optimize reasoning in description logics. In this paper a complete classification of Beth definability is provided for extensions of the basic description logic ALC with transitive roles, inverse roles, role hierarchies, and/or functionality restrictions, both on arbitrary and on finite structures. Moreover, we present a tableau-based algorithm which computes explicit definitions of at most double exponential size. This algorithm is optimal because it is also shown that the smallest explicit definition of an implicitly defined concept may be double exponentially long in the size of the input TBox. Finally, if explicit definitions are allowed to be expressed in first-order logic, then we show how to compute them in single exponential time.