Turing Machines and Finite Models
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.
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 126.J. Hoperoft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.Google Scholar
- 195.C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.Google Scholar