What precisely are fragments of classical first-order logic showing “modal” behaviour? Perhaps the most influential answer is that of Gabbay 1981, which identifies them with so-called “finite-variable fragments”, using only some fixed finite number of variables (free or bound). This view-point has been endorsed by many authors (cf. van Benthem 1991). We will investigate these fragments, and find that, illuminating and interesting though they are, they lack the required nice behaviour in our sense. (Several new negative results support this claim.) (...) As a counterproposal, then, we define a large fragment of predicate logic characterized by its use of only bounded quantification. This so-called guarded fragment enjoys the above nice properties, including decidability, through an effectively bounded finite model property. (These are new results, obtained by generalizing notions and techniques from modal logic.) Moreover, its own internal finite variable hierarchy turns out to work well. Finally, we shall make another move. The above analogy works both ways. Modal operators are like quantifiers, but quantifiers are also like modal operators. This observation inspires a generalized semantics for first-order predicate logic with accessibility constraints on available assignments (cf. N´emeti 1986, 1992) which moves the earlier quantifier restrictions into the semantics. This provides a fresh look at the landscape of possible predicate logics, including candidates sharing various desirable features with basic modal logic – in particular, its decidability. (shrink)

Over the last twenty years, in all of these neighbouring fields, modal systems have been developed that we call multi-dimensional. (Our definition of multi ...

Guarded fragments of first-order logic were recently introduced by Andreka, van Benthem and Nemeti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable (...) fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is EXPTIME-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable. (shrink)

We study several modal languages in which some (sets of) generalized quantifiers can be represented; the main language we consider is suitable for defining any first order definable quantifier, but we also consider a sublanguage thereof, as well as a language for dealing with the modal counterparts of some higher order quantifiers. These languages are studied both from a modal logic perspective and from a quantifier perspective. Thus the issues addressed include normal forms, expressive power, completeness both of modal systems (...) and of systems in the quantifier tradition, complexity as well as syntactic characterizations of special semantic constraints. Throughout the paper several techniques current in the theory of generalized quantifiers are used to obtain results in modal logic, and conversely. (shrink)

Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language ℒ' is the least expressive extension of ℒ with interpolation. For instance, let ℳ be the extension of the basic modal language with a difference operator [7]. First-order logic is the least expressive extension of ℳ with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

We expand first order models with a tolerance relation on thedomain. Intuitively, two elements stand in this relation if they arecognitively close for the agent who holds the model. This simplenotion turns out to be very powerful. It leads to a semanticcharacterization of the guarded fragment of Andréka, van Benthemand Németi, and highlights the strong analogies between modallogic and this fragment. Viewing the resulting logic – tolerance logic– dynamically it is a resource-conscious information processingalternative to classical first order logic. The (...) differences areindicated by several examples. (shrink)

Using a combinatorial theorem of Herwig on extending partial isomorphisms of relational structures, we give a simple proof that certain classes of algebras, including Crs, polyadic Crs, and WA, have the `finite base property' and have decidable universal theories, and that any finite algebra in each class is representable on a finite set.

We study several modal languages in which some (sets of) generalized quantifiers can be represented; the main language we consider is suitable for defining any first order definable quantifier, but we also consider a sublanguage thereof, as well as a language for dealing with the modal counterparts of some higher order quantifiers. These languages are studied both from a modal logic perspective and from a quantifier perspective. Thus the issues addressed include normal forms, expressive power, completeness both of modal systems (...) and of systems in the quantifier tradition, complexity as well as syntactic characterizations of special semantic constraints. Throughout the paper several techniques current in the theory of generalized quantifiers are used to obtain results in modal logic, and conversely. (shrink)

ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

The guarded fragment (GF) was introduced by Andréka, van Benthem and Németi as a fragment of first order logic which combines a great expressive power with nice, modal behavior. It consists of relational first order formulas whose quantifiers are relativized by atoms in a certain way. Slightly generalizing the admissible relativizations yields the packed fragment (PF). In this paper we investigate interpolation and definability in these fragments. We first show that the interpolation property of first order logic fails in restriction (...) to GF and PF. However, each of these fragments turns out to have an alternative interpolation property that closely resembles the interpolation property usually studied in modal logic. These results are strong enough to entail the Beth definability property for GF and PF. Even better, every guarded or packed finite variable fragment has the Beth property. For interpolation, we characterize exactly which finite variable fragments of GF and PF enjoy this property. (shrink)