Turing Machines and Finite Models

  • Leonid Libkin
Part of the Texts in Theoretical Computer Science book series (TTCS)


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.


Linear Order Turing Machine Complexity Class Finite Model Polynomial Hierarchy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliographic Notes

  1. 234.
    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.Google Scholar
  2. 70.
    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.Google Scholar
  3. 71.
    R. Fagin. Monadic generalized spectra. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21 (1975), 89–96.MathSciNetMATHCrossRefGoogle Scholar
  4. 146.
    S. Kleene. Arithmetical predicates and function quantifiers. Transactions of the American Mathematical Society, 79 (1955), 312–340.MathSciNetMATHCrossRefGoogle Scholar
  5. 39.
    S.A. Cook. The complexity of theorem-proving procedures. In Proc. ACM Symp. on Theory of Computing, 1971, ACM Press, pages 151–158.Google Scholar
  6. 126.
    J. Hoperoft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.Google Scholar
  7. 195.
    C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.Google Scholar
  8. 223.
    L. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3 (1977), 1–22.MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Leonid Libkin
    • 1
  1. 1.Department of Computer ScienceUniversity of TorontoTorontoCanada

Personalised recommendations