Abstract
Let T be a finitely axiomatized, universal theory in a finite, first-order language L, and suppose T has a model companion T′ with only finitely many countable models. Then by [We1], T is uniformly locally finite, say with generating function g: ℕ → ℕ. We show the existence of a further function am: ℕ → ℕ measuring the extent to which Mod(T) fails to satisfy the amalgamation property. The main result is as follows: There exist explicitly described uniform decision and quantifier elimination procedures for T′, whose asymptotic complexity can be bounded from above by an elementary recursive function in g and am, without any further reference to T or T′. A corresponding result (with g replaced by d) holds, if T is not finitely axiomatized, provided there is a function d: ℕ → ℕ bounding the size of suitable descriptions of n-generated T-models. Our results generalize those in [We2], which deal with the special case that Mod (T) has the amalgamation property, i.e. that am is the zero function. Applications include the following theories T: The theory of trees, the theory of commutative monoids of bounded exponent, universal Horn theories generated by finitely many finite structures, in particular the theory of distributive p-algebras in the finite Lee-classes and the theory of N-colourable graphs. In each of these cases (see [Pa1], [Bu], [Sch], [Wh]), the best previously known upper complexity bounds were primitive recursive.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Burris, Model Companions for finitely generated universal Horn classes, J.Symb.Logic 49 (1984), pp. 68–74.
G. Grätzer, Lattice theory, Freeman, San Francisco 1971.
G. Grätzer, H. Lakser, The structure of pseudocomplemented distributive lattices II: congruence extension and amalgamation, Trans.Amer.Math.Soc. 156 (1971), pp. 343–358.
J. Barwise, Ed., Handbook of mathematical logic, North-Holland, Amsterdam, 1977.
H.J. Keisler, Fundamentals of model theory, in [HML], pp. 47–103.
A. Macintyre, Model completeness, in [HML], pp. 139–180.
M. Parigot, Le modele compagnon de la theorie des arbres, Zeitschrift math. Logik u. Grundl. 29 (1983), pp. 137–150.
M. Parigot, Theories d'arbres, J.Symb.Logic, 47 (1982), pp. 841–853.
M. Rabin, Decidable theories, in [HML], pp. 595–629.
J. Schmid, Model companions of distributive p-algebras, J.Symb.Logic 42 (1982), pp. 680–688.
V. Weispfenning, Model theory of lattice products, Habilitationsschrift, Universität Heidelberg, 1978.
V. Weispfenning, A note on ℵ0-categorical model companions, Archiv. math. Logik 19 (1978), pp. 23–29.
V. Weispfenning, Efficient decision algorithms for locally finite theories, in AECC-3, grenoble, 1985, Springer LNCS. vol. 229, pp. 262–273.
W.H. Wheeler, The first order theory of N-colourable graphs, Trans.Amer.Math.Soc. 250 (1979), pp. 289–310.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weispfenning, V. (1989). Efficient decision procedures for locally finite theories II. In: Gianni, P. (eds) Symbolic and Algebraic Computation. ISSAC 1988. Lecture Notes in Computer Science, vol 358. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51084-2_37
Download citation
DOI: https://doi.org/10.1007/3-540-51084-2_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51084-0
Online ISBN: 978-3-540-46153-1
eBook Packages: Springer Book Archive