In these lectures we cover the following topics: Computability and Recursive Functions, Proof that exactly the partial recursive functions are computable, Gödel’s Incompleteness Theorems, Löb's Theorem.These very deep and very powerful results in metalogic from the 1930s were unexpected. They arose in a context in which it was expected that a finitary proof of consistency of arithmetic would shortly be forthcoming. This followed the proposal by the mathematician David Hilbert (1862-1943) for the complete axiomatisation and formalisation of all mathematical knowledge and proofs. Although committed to formal methods, many of Hilbert’s proofs were existential in nature, which ran counter to the finitistic, constructivist methods of mathematics. To deal with this criticism, Hilbert proposed that the formal methods program should establish that all of the “Ideal” existential arguments could in principle be replaced by “Real” constructive arguments, by showing some sort of conservation result. However, the incompleteness results showed that this ‘program’ could not be carried out in a simple way.