Unendlich viele Zahlen, unendlich große Mengen, unendlich viele Rechenschritte: In der Mathematik hat man es oft mit Unendlichkeiten zu tun. Trotzdem haben mathematische Bücher eine endliche Seitenanzahl. Wie kann man mit endlichen Ausdrücken über Unendliches reden? Damit beschäftigt sich die Beweistheorie, ein Teilgebiet der Logik, das der Mathematiker Stefan Hetzl von der TU Wien (Institut für Diskrete Mathematik und Geometrie) mit der Theorie formaler Sprachen verbinden will. Aus dieser Verknüpfung sollen wichtige neue Ergebnisse für die Informatik gewonnen werden – denn auch dort lauert die Unendlichkeit, etwa wenn man feststellen will, ob ein Computerprogramm mit jedem beliebigen Input aus unendlich vielen Möglichkeiten zurechtkommt.

Der Wiener Wissenschafts-, Forschungs- und Technologiefonds (WWTF) fördert das Forschungsprojekt von Stefan Hetzl nun im Rahmen des Programms „Vienna Research Groups for Young Investigators“ mit 1.5 Millionen Euro. Hetzl wird mit diesem Geld in den nächsten Jahren seine eigene Forschungsgruppe an der TU Wien aufbauen.

Unendlich viele Schaltjahre
Auch im Alltag haben wir mit endlichen Beschreibungen für Unendliches zu tun: „Es gibt unendlich viele Schaltjahre“, erklärt Stefan Hetzl, „doch sie lassen sich mit endlichen Regeln definieren.“ Die erste, grobe Regel lautet: Jedes Jahr, das durch vier teilbar ist, gilt als Schaltjahr. Ist das Jahr zusätzlich durch hundert teilbar, ist es kein Schaltjahr – alle vierhundert Jahre aber doch. Mit unterschiedlich komplizierten Beschreibungen kann man also unterschiedliche Klassen von Jahren beschreiben, mit ausreichend vielen Regeln lässt sich die unendliche Menge der Schaltjahre vollständig definieren.

Die Mathematik bleibt immer unvollständig
„Ähnlich ist das in der Beweistheorie“, sagt Stefan Hetzl. „Je mächtiger die Theorie aus logischen Regeln ist, umso mehr mathematisch wahre Aussagen lassen sich aus ihr ableiten.“ An ein Ende kommt man dabei freilich nie, wie der große Wiener Logiker Kurt Gödel Anfang der Dreißigerjahre bewies: Kein logisches System kann gleichzeitig ausnahmslos alle logischen Wahrheiten beinhalten und gleichzeitig in sich widerspruchsfrei sein. „Theorien sind immer Approximationen an die Wahrheit, die vollständige Wahrheit erreicht man nie“, meint Stefan Hetzl.

Ähnlich wie sich die Beweistheorie damit beschäftigt, wie mathematischen Aussagen miteinander zusammenhängen und woraus sie abgeleitet werden können, beschäftigt sich die Sprachtheorie mit dem Regelwerk von Grammatik, Sprache und Aussagen. „Den Begriff ‚Sprache‘ fasst man dabei sehr weit“, erklärt Stefan Hetzl. „Das kann eine natürliche Sprache wie englisch oder deutsch sein, das kann eine Computersprache sein, auch die Menge aller mathematischen Ausdrücke, die nach bestimmten Regeln gebildet werden, kann man als Sprache interpretieren.“ In der Logik arbeitet man mit unterschiedlich mächtigen Regelsystemen, die unterschiedliche Aussagen zulassen, in der Sprachtheorie kann man unterschiedliche Typen von Grammatiken beschreiben, die unterschiedliche Sprachen hervorbringen.

Vollständige Induktion: Beweise mit Domino-Effekt
Ein besonders mächtiges Instrument der mathematischen Beweisführung ist die „vollständige Induktion“. Mit ihr kann man Aussagen über unendliche Mengen von Zahlen beweisen: Das Aufaddieren aller ungerader Zahlen  bis zu einer beliebigen höchsten Zahl ergibt eine Quadratzahl, zum Beispiel: 1+3+5=9, und das ist drei zum Quadrat. Man beweist das, indem man zuerst überprüft ob es für den allerersten Schritt zutrifft. Danach hat man zu zeigen, dass sich die Aussage – wenn sie für einen beliebigen Schritt gültig ist - immer auf den nächsten Schritt übertragen lässt (siehe Kasten unten). Gelingt das, hat man die Aussage für alle unendlich vielen möglichen Schritte bewiesen, so wie man eine unendlich Kette von Domino-Steinen zu Fall bringen kann, wenn man nur den ersten anstößt und sicherstellt, dass jeder den nächsten umwirft.

„Diese Methode der vollständigen Induktion ist gerade in der Informatik sehr wichtig“, sagt Stefan Hetzl. „Wenn Computerprogramme Schleifen durchlaufen, wenn Größen rekursiv definiert sind, dann ist die vollständige Induktion das Beweis-Werkzeug der Wahl.“ Doch ist sie wirklich immer nützlich und zielführend? Hetzl hofft, durch die Verknüpfung der Beweistheorie mit Sprachen-Theorie neue Einblicke in die theoretischen Grundlagen solcher Beweisführungen zu gewinnen.

Bewiesenermaßen richtige Computerprogramme
Ein Arbeitsfeld, in dem solche Forschungen große Bedeutung haben, ist die Softwareverifikation: „Man will Computerprogramme haben, die möglichst stabil laufen, die sich also richtig verhalten, egal welche Eingabe sie bekommen“, sagt Hetzl. Typischerweise gibt es aber unendlich viele verschiedene denkbare Eingaben – mit bloßem Durchprobieren wird man ein Programm also nie vollständig austesten können. Um zu zeigen, dass ein Computerprogramm vollständig richtig ist, muss man daher beweistheoretisch klug vorgehen, um in einer endlichen Anzahl von Schritten unendlich viele Möglichkeiten abdecken zu können.

Stefan Hetzl sieht sich zwar als Mathematiker, hat aber auch Informatik studiert – es fällt ihm daher nicht schwer, in diesen Fachbereich Brücken zu schlagen. Seit 2012 gibt es an der Fakultät für Informatik der TU Wien das „Vienna Center for Logic and Algorithms“, das sich auf ähnliche Weise mit Logik-Forschung beschäftigt. „Meine Gruppe wird in den nächsten Jahren wohl hauptsächlich mit Papier und Bleistift arbeiten. Mit den Ergebnissen daraus werden wir uns dann auch in Richtung Anwendung bewegen“, kündigt Hetzl an.

<link http: www.tuwien.ac.at dle pr aktuelles downloads unendlich link_extern> Fotodownload

Rückfragehinweis:
Dr. Stefan Hetzl
Institut für Diskrete Mathematik und Geometrie
Technische Universität Wien
Wiedner Hauptstraße 8-10
T: +43-1-58801-104262
<link>stefan.hetzl@tuwien.ac.at