Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-29T02:08:59.435Z Has data issue: false hasContentIssue false

Complete problems for fixed-point logics

Published online by Cambridge University Press:  12 March 2014

Martin Grohe*
Affiliation:
Abteilung für Mathematische Logik und Grundlagen der Mathematik, Universität Freiburg, Albertstr. 23B, 79104 Freiburg, Germany, E-mail: [email protected]

Extract

The notion of logical reducibilities is derived from the idea of interpretations between theories. It was used by Lovász and Gács [LG77] and Immerman [Imm87] to give complete problems for certain complexity classes and hence establish new connections between logical definability and computational complexity.

However, the notion is also interesting in a purely logical context. For example, it is helpful to establish nonexpressibility results.

We say that a class of τ-structures is a >complete problem for a logic under L-reductions if it is definable in [τ] and if every class definable in can be ”translated” into by L-formulae (cf. §4).

We prove the following theorem:

1.1. Theorem. There are complete problemsfor partial fixed-point logic andfor inductive fixed-point logic under quantifier-free reductions.

The main step of the proof is to establish a new normal form for fixed-point formulae (which might be of some interest itself). To obtain this normal form we use theorems of Abiteboul and Vianu [AV91a] that show the equivalence between the fixed-point logics we consider and certain extensions of the database query language Datalog.

In [Dah87] Dahlhaus gave a complete problem for least fixed-point logic. Since least fixed-point logic equals inductive fixed-point logic by a well-known result of Gurevich and Shelah [GS86], this already proves one part of our theorem.

However, our class gives a natural description of the fixed-point process of an inductive fixed-point formula and hence sheds some light on completely different aspects of the logic than Dahlhaus's construction, which is strongly based on the features of least fixed-point formulae.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[AV91a] Abiteboul, S. and Vianu, V., Datalog extensions for database queries and updates, Journal of Computer and System Sciences, vol. 43 (1991), pp. 62124.CrossRefGoogle Scholar
[AV91b] Abiteboul, S. and Vianu, V., Generic computation and its complexity, Proceedings of 23rd ACM symposium on theory of computing (1991), pp. 209219.Google Scholar
[Dah87] Dahlhaus, E., Skolem normal forms concerning the least fixed point, Computation theory and logic (Börger, E., editor), Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1987, pp. 2036.Google Scholar
[Daw93] Dawar, A., Feasible computation through model theory, Ph.D. thesis, University of Pennsylvania, University Park, Pennsylvania, 1993.Google Scholar
[EF] Ebbinghaus, H. D. and Flum, J., Finite model theory (to appear).Google Scholar
[EFT94] Ebbinghaus, H. D., Flum, J., and Thomas, W., Mathematical logic, 2nd ed, Springer-Verlag, Berlin, 1994.CrossRefGoogle Scholar
[GS86] Gurevich, Y. and Shelah, S., Fixed point extensions of first-order logic, Annals of Pure and Applied Logic, vol. 32 (1986), pp. 265280.CrossRefGoogle Scholar
[Hel94] Hella, L., Fixpoint logic vs generalized quantifiers, manuscript (1994).Google Scholar
[Imm87] Immerman, N., Languages that capture complexity classes, SIAM Journal on Computing, vol. 16 (1987), pp. 760778.CrossRefGoogle Scholar
[LG77] Lovász, L. and Gacs, P., Some remarks on generalized spectra, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 23 (1977), pp. 27144.CrossRefGoogle Scholar
[Mos74] Moschovakis, Y. N., Elementary induction on abstract structures, North-Holland, Amsterdam, 1974.Google Scholar
[MP93] Makowsky, J. A. and Pnueli, Y. B., Oracles and quantifiers, Proceedings of the 7th workshop on computer science logic, Lecture Notes in Computer Science, vol. 832, Springer-Verlag, Berlin, 1993, pp. 150164.Google Scholar