Abstract:

Goedel showed us many things. Among others he showed us the *possibility* of proof (via the Completeness Theorem for First-Order Logic); and then quite soon thereafter he showed us the *impossibility* of proof (via the Incompleteness Theorem for (suitable) Higher- Order Logics). These results are well known and famous, but their impact on the practice of mathematics has perhaps not been very noticeable. To be sure, related recursive unsolvability results have a clear explanatory value in keeping people from searching for algorithms where none can exist. And modern developments in complexity theory show that many easily stated problems have -- in general -- no quick solutions. But again, many commentators agree that there has not been a big shift in main-stream mathematics as a consequence of Goedel's fundamental work. However, the insight into formalization sparked by Goedel's original work is now having major payoffs in mechanized mathematics and proof systems. The lecture will survey some developments, but it will also bring up the questions of what we should now regard as a proof and of how new proof methods develop.