Hostname: page-component-66d9dcfd78-cd759 Total loading time: 0 Render date: 2026-08-03T05:47:50.775Z 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: grohe@sunl.mathematik.uni-freiburg.de

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.

Information

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.)

Article purchase

Temporarily unavailable