Gödel Incompleteness and Proof Assistants

by Cristian S. Calude, University of Auckland, New Zealand


Gödel’s first incompleteness theorem states that in every consistent system of axioms which contains a modicum of arithmetic  and its theorems can be listed by an algorithm, there exist true statements about natural numbers that are unprovable in the  system. The second incompleteness theorem states that such a system cannot demonstrate its own consistency. J. von Neumann  called them “a landmark which will remain visible far in space and time.”

The talk will briefly show that both incompleteness results follow from the undecidability of the Halting problem. Then we will discuss theoretically whether the incompleteness results give a “coup de grâce” to Hilbert’s Programme. Finally, we will argue that the current practice of mathematics, which uses extensively proof-assistants, is changing the theoretical views about the impact of incompleteness.