What is a mathematical proof? How can proofs be justified? Are there
limitations to provability? To what extent can machines carry out mathe-
matical proofs? Only in this century has there been success in obtaining
substantial and satisfactory answers. The present book contains a
systematic discussion of these results. The investigations are centered
around first-order logic. Our first goal is Godel's completeness
theorem, which shows that the con- sequence relation coincides with
formal provability: By means of a calcu- lus consisting of simple formal
inference rules, one can obtain all conse- quences of a given axiom
system (and in particular, imitate all mathemat- ical proofs). A short
digression into model theory will help us to analyze the expres- sive
power of the first-order language, and it will turn out that there are
certain deficiencies. For example, the first-order language does not
allow the formulation of an adequate axiom system for arithmetic or
analysis. On the other hand, this difficulty can be overcome--even in
the framework of first-order logic-by developing mathematics in
set-theoretic terms. We explain the prerequisites from set theory
necessary for this purpose and then treat the subtle relation between
logic and set theory in a thorough manner.