Proofs, Computability, Undecidability, Complexity, And the Lambda Calculus: An Introduction

The main goal of this book is to present a mix of material dealing with: Proof systems. Computability and undecidability. The Lambda Calculus. Some aspects of complexity theory. Historically, the theory of computability and undecidability arose from Hilbert’s efforts to completely formalize mathematics and from Godel’s first incompleteness theorem that showed that such a program was doomed to fail. People realized that to carry out both Hilbert’s program and Godel’s work it was necessary to define precisely what is the notion of a computable function and the notion of a mechanically checkable proof. The first definition given around 1934 was that of the class of computable function in the sense of Herbrand–Godel–Kleene. The second definition given by Church in 1935-1936 was the notion of a function definable in the λ-calculus. The equivalence of these two definitions was shown by Kleene in 1936. Shortly after in 1936, Turing introduced a third definition, that of a Turing-computable function. Turing proved the equivalence of his definition with the Herbrand–Godel–Kleene definition in 1937 (his proofs are rather sketchy compared to Kleene’s proofs).