Abstract
In this chapter we introduce the technique of coding Turing machines in various logics. It is precisely this technique that gave rise to numerous applications of finite model theory in computational complexity. We start by proving the earliest such result, Trakhtenbrot’s theorem, stating that finite satisfiability is not decidable. For the proof of Trakhtenbrot’s theorem, we code Turing machines with no inputs. By a refinement of this technique, we code nondeterministic polynomial time Turing machines in existential second-order logic (∃SO), proving Fagin’s theorem stating that∃SO-definable properties of finite structures are precisely those whose complexity is NP.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Bibliographic Notes
B. A. Trakhtenbrot (B.A. Tpaxren6poT). The impossibilty of an algorithm for the decision problem for finite models (Heso:1MOxcHocTb a.rrropH rxza itna npo6.nembr paspeummocTH Ha xoueuHbrx xsiaccax). Doklady Academii Nauk SSSR Pox•tadbt Axadexmuu Hayx CCCP), 70 (1950), 569 572.
R.. Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation,R. Karp, ed., SIA M-A MS Proceedings,7 (1974), 43–73.
R. Fagin. Monadic generalized spectra. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21 (1975), 89–96.
S. Kleene. Arithmetical predicates and function quantifiers. Transactions of the American Mathematical Society, 79 (1955), 312–340.
S.A. Cook. The complexity of theorem-proving procedures. In Proc. ACM Symp. on Theory of Computing, 1971, ACM Press, pages 151–158.
J. Hoperoft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
L. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3 (1977), 1–22.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Libkin, L. (2004). Turing Machines and Finite Models. In: Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-07003-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-662-07003-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05948-3
Online ISBN: 978-3-662-07003-1
eBook Packages: Springer Book Archive