A zero-one law for logic with a fixed-point operator

The logic obtained by adding the least-fixed-point operator to first-order logic was proposed as a query language by Aho and Ullman (in "Proc. 6th ACM Sympos. on Principles of Programming Languages," 1979, pp. 110-120) and has been studied, particularly in connection with finite models, by numerous authors. We extend to this logic, and to the logic containing the more powerful iterative-fixed-point operator, the zero-one law proved for first-order logic in (Glebskii, Kogan, Liogonki, and Talanov (1969), Kibernetika 2, 31-42; Fagin (1976), J. Symbolic Logic 41, 50-58). For any sentence φ of the extend logic, the proportion of models of φ among all structures with universe {1,2,..., n} approaches 0 or 1 as n tends to infinity. We also show that the problem of deciding, for any φ, whether this proportion approaches 1 is complete for exponential time, if we consider only φ's with a fixed finite vocabulary (or vocabularies of bounded arity) and complete for double-exponential time if φ is unrestricted. In addition, we establish some related results. © 1985 Academic Press, Inc.