https://www.faz.net/-gwz-14est

Mathematik : Gentzens Sequenzen

  • -Aktualisiert am

Tod im Lager

Der Beweis der Widerspruchsfreiheit der Analysis geriet zum Wettlauf mit der Zeit. Als Gefangener erhielt Gentzen nur zu essen, wenn er schwere körperliche Arbeit verrichtete, etwa beim Beseitigen von Barrikaden. Als die Straßen schon geräumt waren und nur noch Pflastersteine auf einen Laster geladen werden mussten, verkürzte eine Verwechslung die Gentzen verbleibende Zeit erheblich. Er war gerade dabei, einen Stein loszurütteln, da schrie plötzlich eine Frau, zeigte wild gestikulierend auf Gentzen, der mit wirrem Haar und Vollbart sich nicht einmal selbst im Spiegel erkannt hätte, und schleuderte einen Pflasterstein nach ihm. Der Stein traf Gentzens Hand und zerquetschte ihm zwei Finger.

Arbeit, die Gentzen gegen Brot und Wasser hätte erledigen können, gab es von nun an kaum noch. Er magerte ab bis auf die Knochen. Vom Hunger getrieben, meldete er sich schließlich zum Teppichklopfen, brach aber unter der Last des nassen Knüpfwerks zusammen; statt Nahrung bekam er Prügel. Gentzen war nun gänzlich arbeitsunfähig. Allein die Arbeit am Widerspruchsfreiheitsbeweis hielt ihn am Leben. Auf die Holzpritsche gekauert, ging er in Gedanken Ansatz für Ansatz durch und berichtete den Zellengenossen von seinen Fortschritten - für die meisten eine willkommene Ablenkung von der täglichen Not. Doch Gentzens Kräfte schwanden. Am 4. August 1945 raffte er sich noch zum Morgenappell auf. Anschließend war er zu schwach, um die Beine auf die Pritsche zu heben. Dann war er tot.

Sequenzen im Computer

Überlebt hat sein Kalkül. Von Gentzens Sequenzen machen die Informatiker heute regen Gebrauch. An der Tafel mag ein Beweis, niedergeschrieben in einer einzigen Sequenz, unanschaulich sein, im Rechner aber verschwinden die Zahlenkolonnen. Dass die Sequenz sehr lang sein kann, ist einem modernen Computer egal. Vielmehr hat eine Sequenz den Vorteil, dass zu einem vollständigen Beweis nicht erst alle Voraussetzungen zusammengeklaubt werden müssen: In einer Sequenz steckt alles drin. Sogenannte Verifizierungsprogramme beweisen mit Hilfe von Sequenzen, dass eine Software keine Fehler macht, indem sie die von der Software erzeugten Sequenzen nach vorgegebenen Regeln verlängern oder verkürzen, bis eine einfache Ja/Nein-Entscheidung möglich ist.

Gentzens eigentliches Ziel, die Widerspruchsfreiheit der Analysis zu beweisen, hat bis heute niemand erreicht, trotz weiterer Anläufe in den 1950er Jahren. Die meisten Mathematiker glauben aber, dass es um die Analysis bestens steht, solange niemand einen Widerspruch nachweist. Es gibt eben noch schlimmere Bedrohungen für die Mathematik als mengentheoretische Paradoxien. Gentzens Leben ist ein Beispiel dafür.

Weitere Themen

Topmeldungen

Der Fall George Floyd : Amerikas Justizwesen ist kaputt

Die amerikanische Politik bleibt in ihrer Übertreibungsspirale gefangen. Deshalb wird es auch nach dem Mordurteil in Minnepolis nicht zu den Reformen kommen, die das Land so dringend braucht.
Juve-Boss Andrea Agnelli: Einer der Initiatoren und Befürworter der Super League

Juve-Präsident Andrea Agnelli : „Verräter, wie Judas“

Juventus-Präsident Agnelli war einer der Initiatoren der Super League. In Italien wird er heftig angefeindet – und hat sogar Ärger mit dem berühmten Taufpaten eines seiner Kinder. Nun wird bekannt: Das Projekt wird verworfen.

Newsletter

Immer auf dem Laufenden Sie haben Post! Abonnieren Sie unsere FAZ.NET-Newsletter und wir liefern die wichtigsten Nachrichten direkt in Ihre Mailbox. Es ist ein Fehler aufgetreten. Bitte versuchen Sie es erneut.
Vielen Dank für Ihr Interesse an den F.A.Z.-Newslettern. Sie erhalten in wenigen Minuten eine E-Mail, um Ihre Newsletterbestellung zu bestätigen.