Vortrag von nomeata auf der GPN11.
Hilbert hatte einen Traum: Er wünschte sich eine formale Sprache, in der
alle Mathematik formuliert werden kann, die widerspruchsfrei und
vollständig ist und eine Maschine, die jede Aussage als wahr oder falsch
identifiziert. Dann kam Church und weckte Hilbert aus seinem Traum: So
eine Maschine kann es nicht geben, wir brauchen also weiter Mathematiker
um Beweise zu finden.
Nach einer logikgeschichtlichen Einordnung werden wir sehen wie Church sein junges Lambda-Kalkül, die Mutter aller funktionalen Programmiersprachen, verwendet um das Entscheidungsproblem negativ zu lösen – wenige Monate bevor dies auch von Turing mit seiner bekannteren Arbeit zum Halteproblem gezeigt wurde.
