This paper is devoted to the formulation and investigation of a dynamic semantic interpretation of the language of first-order predicate logic. The resulting system, which will be referred to as ‘dynamic predicate logic’, is intended as a first step towards a compositional, non-representational theory of discourse semantics. In the last decade, various theories of discourse semantics have emerged within the paradigm of model-theoretic semantics. A common feature of these theories is a tendency to do away with the principle of compositionality, (...) a principle which, implicitly or explicitly, has dominated semantics since the days of Frege. Therefore the question naturally arises whether non-compositionality is in any way a necessary feature of discourse semantics. Since we subscribe to the interpretation of compositionality as constituting primarily a methodological principle, we consider this to be a methodological rather than an empirical question. As a consequence, the emphasis in the present paper lies on developing an alternative compositional semantics of discourse, which is empirically equivalent to its non-compositional brethren, but which differs from them in a principled methodological way. Hence, no attempts are made to improve on existing theories empirically. Nevertheless, as we indicate in section 5, the development of a compositional alternative may in the end have empirical consequences, too. First of all, it can be argued that the dynamic view on interpretation developed in this paper suggests natural and relatively easy to formulate extensions which enable one to deal with a wider range of phenomena than can be dealt with in existing theories. Moreover, the various approaches to the model-theoretic semantics of discourse that have been developed during the last decade, have constituted a ‘fresh start’ in the sense that much of what had been accomplished before was ignored, at least for a start. Of course, this is a justified strategy if one feels one is trying to develop a radically different approach to recalcitrant problems. However, there comes a time when such new approaches have to be compared with the older one, and when an assessment of the pros and cons of each has to be made. One of the main problems in semantics today, we feel, is that a semantic theory such as Montague grammar, and an approach like Kamp’s discourse representation theory, are hard to compare, let alone that it is possible to unify their insights and results.. (shrink)

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)

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)

In this paper we define computationally well-behaved versions of classical first-order logic and prove that the validity problem is decidable.

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 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 and the loosely guarded fragment 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)

In this paper we show that relativized versions of relation set algebras and cylindric set algebras have undecidable equational theories if we include coordinatewise versions of the counting operations into the similarity type. We apply these results to the guarded fragment of first-order logic.