The expressive power of fixed-point logic with counting

Journal of Symbolic Logic 61 (1):147-176 (1996)
  Copy   BIBTEX

Abstract

We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. To this end an isomorphism preserving (`generic') model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved. In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics L r ∞ω (∃ ≥ m ) m∈ω and the corresponding pebble games. The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants (J r ) r≥ 1 with the following properties: $\bullet$ The invariants themselves can be evaluated in polynomial time. $\bullet$ A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants. $\bullet$ The invariant J r classifies all finite relational structures exactly up to equivalence with respect to the logic L r ∞ω (∃ ≥ m ) m∈ω . We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the L r ωω (∃ ≥ m ) m∈ω : It corresponds exactly to the polynomial time computable families (φ n ) n∈ω in these logics. Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindstrom quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Yet another hierarchy theorem.Max Kubierschky - 2000 - Journal of Symbolic Logic 65 (2):627-640.
Guarded quantification in least fixed point logic.Gregory McColm - 2004 - Journal of Logic, Language and Information 13 (1):61-110.
On fixed-point logic with counting.Jörg Flum & Martin Grohe - 2000 - Journal of Symbolic Logic 65 (2):777-787.
Iterative and fixed point common belief.Aviad Heifetz - 1999 - Journal of Philosophical Logic 28 (1):61-79.
On the weak Kleene scheme in Kripke's theory of truth.James Cain & Zlatan Damnjanovic - 1991 - Journal of Symbolic Logic 56 (4):1452-1468.
Minimal Predicates. Fixed-Points, and Definability.Johan Van Benthem - 2005 - Journal of Symbolic Logic 70 (3):696 - 712.
Fixed point logics.Anuj Dawar & Yuri Gurevich - 2002 - Bulletin of Symbolic Logic 8 (1):65-88.

Analytics

Added to PP
2009-01-28

Downloads
201 (#91,639)

6 months
8 (#158,054)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

How to define a linear order on finite models.Lauri Hella, Phokion G. Kolaitis & Kerkko Luosto - 1997 - Annals of Pure and Applied Logic 87 (3):241-267.
Canonization for two variables and puzzles on the square.Martin Otto - 1997 - Annals of Pure and Applied Logic 85 (3):243-282.
Finite variable logics in descriptive complexity theory.Martin Grohe - 1998 - Bulletin of Symbolic Logic 4 (4):345-398.

Add more citations

References found in this work

Fixed-point extensions of first-order logic.Yuri Gurevich & Saharon Shelah - 1986 - Annals of Pure and Applied Logic 32:265-280.

Add more references