Abstract

existence of undecidable statements in any consistent axiomatic theory for mathematics,

unsolvability of the halting problem,

nonexistence of a decision algorithm for elementary arithmetic,

nonexistence of a decision algorithm for predicate calculus.
These are easily proved using an elegant line of argument due to Gregory Chaitin. Then the somewhat more delicate line of argument leading to Gödel’s two incompleteness theorems is considered: this more detailed discussion continues to emphasize the basic role of set theory.
The chapter ends with a discussion on the axioms of reflections, whose addition to the axioms of set theory has direct practical interest: these in fact make the collection of proof mechanisms available to the verifier indefinitely extensible.
Keywords
Free Variable Function Symbol Logical System Atomic Formula Predicate SymbolReferences
 [AW80]Aiello, L., Weyhrauch, R.W.: Using metatheoretic reasoning to do algebra. In: Bibel, W., Kowalski, R. (eds.) Proc. of the 5th Conference on Automated Deduction, Les Arcs, France. LNCS, vol. 87, pp. 1–13. Springer, Berlin (1980) Google Scholar
 [SDDS86]Schwartz, J.T., Dewar, R.K.B., Dubinsky, E., Schonberg, E.: Programming with Sets: An Introduction to SETL. Texts and Monographs in Computer Science. Springer, Berlin (1986) MATHGoogle Scholar