Welcome to
Joachim Breitner's Homepage

A newly founded Logic Group in Mumbai, which seems to be a private thing but some professors from the IIT Bombay are taking part, has approached me and asked if I can give a talk about Church’s lambda calculus and how he used it to show that Hilbert’s Entscheidungsproblem is not solvable. They are starting a series of talk on logic on the occasion of Turing’s 100th birth year and because I am finally leaving the IIT campus in two days, my talk turned out to be the opening talk for the series. Roughly guessed about fifty people attended, some professors but most of them students from fields other than mathematics and computer science – I hope that they were not too confused by distinguishing truth and provability, expressability and computability, of which I did not give a proper explanation.

I started with a historical exposition of the state of logic in the beginning 20th century, then gave an introduction to lambda calculus, encoding of natural numbers in then, Gödel encoding. Finally I sketched the proof of the unsolvability of the question whether a lambda term has a normal form and then concluded by showing how this implies that the Entscheidungsproblem is not solvable.

I have before hand written out the talk in full, and again I ended up saying completely different things – or at least said things completely different. Nevertheless, I am sharing the (planned) text of my talk, including the timeline that I draw on the whiteboard.