The broad informal question to be addressed is this: Can one "mechanize" significant parts of mathematical reasoning? To answer the question, we carry out a case study for Gvdel's incompleteness theorems and some theorems of set theory. That requires extensive preparatory work in Parts 1 and 2 of the course.We survey in Part 1 problems that led to the search for a notion of mechanical procedure or computability, look at a number of different notions, and give a convincing conceptual analysis that is based on work by Turing, Post and Gandy. The decision problem is one of the problems that were solved, negatively, using such a rigorous notion of computability. The theorem of Church and Turing asserts that there is no mechanical procedure deciding whether or not a sentence in the language of first-order logic is a logical truth. However, Gvdel's completeness theorem guarantees that every logical truth can be proved - in a suitable calculus. A variety of procedures have been developed to search systematically for proofs; Part 2 investigates "proof search procedures" for natural deduction calculi.
