First-Order Logic: Undecidability and Model Theory *

  • Mordechai Ben-Ari


The chapter surveys several important theoretical results in first-order logic. In Sect. 12.1 we prove that validity in first-order logic is undecidable, a result first proved by Alonzo Church. Validity is decidable for several classes of formulas defined by syntactic restrictions on their form (Sect. 12.2). Next, we introduce model theory (Sect. 12.3): the fact that a semantic tableau has a countable number of nodes leads to some interesting results. Finally, Sect. 12.4 contains an overview of Gödel’s surprising incompleteness result.


Turing Machine Decision Procedure Informal Justification Syntactic Restriction Program Clause 
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.


  1. B. Dreben and W.D. Goldfarb. The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading, MA, 1979. MATHGoogle Scholar
  2. J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages and Computation (Third Edition). Addison-Wesley, 2006. Google Scholar
  3. H.R. Lewis. Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Reading, MA, 1979. MATHGoogle Scholar
  4. Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, NY, 1974. Reprinted by Dover, 2003. MATHGoogle Scholar
  5. E. Mendelson. Introduction to Mathematical Logic (Fifth Edition). Chapman & Hall/CRC, 2009. MATHGoogle Scholar
  6. M.L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ, 1967. MATHGoogle Scholar
  7. J.D. Monk. Mathematical Logic. Springer, 1976. MATHGoogle Scholar
  8. R.M. Smullyan. What Is the Name of This Book?—The Riddle of Dracula and Other Logical Puzzles. Prentice-Hall, 1978. MATHGoogle Scholar

Copyright information

© Springer-Verlag London 2012

Authors and Affiliations

  • Mordechai Ben-Ari
    • 1
  1. 1.Department of Science TeachingWeizmann Institute of ScienceRehovotIsrael

Personalised recommendations