Skip to main content

First-Order Logic: Undecidability and Model Theory *

  • Chapter
Mathematical Logic for Computer Science

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  • B. Dreben and W.D. Goldfarb. The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading, MA, 1979.

    MATH  Google Scholar 

  • J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages and Computation (Third Edition). Addison-Wesley, 2006.

    Google Scholar 

  • H.R. Lewis. Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Reading, MA, 1979.

    MATH  Google Scholar 

  • Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, NY, 1974. Reprinted by Dover, 2003.

    MATH  Google Scholar 

  • E. Mendelson. Introduction to Mathematical Logic (Fifth Edition). Chapman & Hall/CRC, 2009.

    MATH  Google Scholar 

  • M.L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ, 1967.

    MATH  Google Scholar 

  • J.D. Monk. Mathematical Logic. Springer, 1976.

    MATH  Google Scholar 

  • R.M. Smullyan. What Is the Name of This Book?—The Riddle of Dracula and Other Logical Puzzles. Prentice-Hall, 1978.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag London

About this chapter

Cite this chapter

Ben-Ari, M. (2012). First-Order Logic: Undecidability and Model Theory *. In: Mathematical Logic for Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-4129-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-4129-7_12

  • Publisher Name: Springer, London

  • Print ISBN: 978-1-4471-4128-0

  • Online ISBN: 978-1-4471-4129-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics