First-Order Logic: Undecidability and Model Theory *
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.
KeywordsTuring Machine Decision Procedure Informal Justification Syntactic Restriction Program Clause
- J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages and Computation (Third Edition). Addison-Wesley, 2006. Google Scholar