„Logik ist mächtig“ Sie führt an die Grenzen des Denkens und sorgt dafür, dass der Fahrstuhl funktio
„Logik ist mächtig“
Sie führt an die Grenzen des Denkens und sorgt dafür, dass der Fahrstuhl funktioniert. Helmut Veith über eine Wissenschaft, die noch stringenter sein will als die Mathematik
Interview: Christian Weber
Wien war in den 20er-Jahren des vergangenen Jahrhunderts das wichtigste Zentrum für Logik in der Welt. Philosophen und Denker wie Ludwig Wittgenstein, Kurt Gödel, Karl Popper prägten die Wissenschaftsgeschichte jener Zeit. Mittlerweile gehört die Stadt wieder zu den weltweit führenden Standorten der Logikforschung, weshalb derzeit dort der „Vienna Summer of Logic“ stattfindet, mit 2500 Teilnehmern der größte Kongress, seitdem Aristoteles im vierten Jahrhundert v. Chr. die Disziplin der Logik mitbegründete. Helmut Veith von der Technischen Universität Wien ist einer der Hauptorganisatoren.
SZ: Herr Veith, würde Aristoteles auch nur ein Wort verstehen, wenn ihn eine Zeitmaschine in einen Ihrer Konferenzsäle transferieren würde, und da spricht gerade jemand zum Beispiel über bitopologische Dualität?
Helmut Veith: Die Grundfrage unserer Disziplin hat sich seit der Antike nicht geändert: Wie kann ich aus vorliegenden Fakten nur durch formale Schlüsse neue Fakten ableiten? Fachlich müsste auch ein Genie wie Aristoteles sich bestimmt ein halbes Jahr einarbeiten, dann aber hätte er sicher Sympathie und Verständnis für unsere Fragen.
Wenn wir Laien an Logik denken, dann an Sätze wie: „Alle Vögel fliegen. Kurt ist ein Vogel. Also kann Kurt fliegen.“ Mittlerweile ist es ein bisschen komplexer?
Nun ja, es geht in vielen Bereichen unseres Faches schon noch immer um die Frage, wie kann ich Logik einsetzen, um Schlussfolgerungen über die Welt zu ziehen? Vielleicht haben wir über die Jahrhunderte entdeckt, dass die Welt komplizierter ist als anfangs gedacht. Um bei ihrem Beispiel zu bleiben: Klar, Vögel können fliegen, aber was ist mit Ausnahmen wie den Pinguinen? Moderne Logik versucht, eine Sprache auch für solche Probleme der Alltagswelt zu finden.
Aber Paradoxien sind ja nun nicht neu.
Ja, sicher. Bereits im 19. Jahrhundert hatten Leute wie etwa Georg Cantor, Gottlob Frege und Bertrand Russell in der Mathematik zunehmend Paradoxien entdeckt. Bekannt ist etwa Russells Paradox in Freges Mengentheorie. Es entspricht dem berühmten Fall des Barbiers, der genau diejenigen Barbiere rasiert, die sich nicht selbst rasieren. Was macht also dieser Barbier? Falls er sich nicht selbst rasiert, müsste er sich ja rasieren. Falls er sich jedoch rasiert, darf er nicht zu jenen gehören, die sich selbst rasieren. Die Vorstellung eines solchen Barbiers führt also notwendigerweise zu Widersprüchen, und das beunruhigte die Mathematiker. Die Antwort auf solche Probleme war die Entwicklung der mathematischen Logik, die dann auch durch den berühmten deutschen Mathematiker David Hilbert vorangetrieben wurde.
Was war Hilberts Ziel?
Er wollte die gesamte Mathematik logisch fundieren, also auf einfache mechanische Schlussregeln zurückführen, die von wenigen unmittelbar einsichtigen Axiomen ausgehen. Dieses Programm sollte den Weg öffnen für eine Automatisierung der Mathematik, sodass man im Prinzip mit einem Computer mathematische Sätze ableiten kann.
Hätte das Mathematiker arbeitslos gemacht?
So weit ist es nicht gekommen. Hilberts Programm wurde bekanntlich 1931 durch den jungen Kurt Gödel in Wien vernichtet, ohne Zweifel der berühmteste Logiker seit Aristoteles. Er konnte zeigen, dass es in hinreichend komplexen formalen Systemen wie der Arithmetik notwendigerweise Sätze gibt, die sich weder beweisen noch widerlegen lassen.
Der berühmte Unvollständigkeitssatz.
Genau. Er zeigt, dass sich mit keiner logisch-mathematischen Definition die ganze Mathematik erfassen lässt. Es wird also immer Sätze geben, die ich als wahr erkenne, aber nicht beweisen kann. Wahrheit und Beweisbarkeit sind verschiedene Dinge.
Manche Zeitgenossen sehen im Unvollständigkeitssatz deshalb einen Beleg, dass die Welt kausal nicht abgeschlossen ist. Somit entstehe eine Lücke, in der Gott denkbar werde... Sie runzeln die Stirn?
Ich warne davor, dass man ein technisches Resultat nimmt und einfach auf andere Gebiete überträgt. Gödels Satz besagt nur, dass die Mathematik kein abgeschlossenes Projekt ist. Es wird also immer wieder neue Bereiche geben, in die der menschliche Geist mit seinen 1,5 Kilogramm Gehirnmasse vorstoßen kann. Das ist doch eine erfreuliche Nachricht...
...die aber auch ein bisschen unheimlich ist. Das Schöne an der Schulmathematik war ja gerade, dass am Ende immer alles aufging.
Manche Wissenschaftler waren tatsächlich erschüttert. John von Neumann etwa gab wegen des Unvollständigkeitssatzes die Logik auf. Dennoch: Gödels Satz war der Big Bang der modernen Logik, erst aus ihm sind die unterschiedlichen Zweige der modernen mathematischen Logik entstanden, die sich mit prinzipiellen Fragen der Berechenbarkeit, der Beweis- und der Modelltheorie beschäftigen, überhaupt mit den Grundlagen der Mathematik.
Ist das alles wirklich wichtig für die Menschheit?
Natürlich, die moderne logische Forschung hat etwa überhaupt erst die ganze Informatik möglich gemacht. Der britische Mathematiker Alan Turing etwa hat angesichts der neuen logischen Methoden das erste präzise Modell eines Computers entwickelt, die sogenannte Turing-Maschine. Auf ihn gehen auch zentrale Begriffe zurück wie etwa die Unterscheidung zwischen Programm und Speicher.
Kann Logik tatsächlich zur mathematischen Forschung beitragen, wenn doch Gödel - wie Sie eben sagten - das Hilbert’sche Programm der automatisierten Mathematik zerstört hat?
Hilberts Traum war, mit automatisierten Verfahren die gesamte Mathematik zu erfassen. Das geht nicht. Bei engeren, klar umrissenen Fragestellungen ist der Computer aber durchaus hilfreich. Sehr häufig ist man zufrieden, wenn er in praktischen Fällen eine korrekte Antwort liefert und ansonsten sagt: Hier weiß ich die Antwort nicht. Das ist bei menschlichen Experten ja auch nicht anders.
Das ist für einen Logiker ein erstaunlich pragmatischer Ansatz.
Ja, aber dieser Pragmatismus ist verbunden mit mathematischen Untersuchungen, die exakt jene Situationen eingrenzen, wo wir präzise Antworten finden können.
Manche Forscher fühlen sich auch unwohl, weil der Computer ihnen ein Ergebnis ausspuckt, das sie selbst nicht mehr nachprüfen können, manchmal schon aus Zeitgründen: Ein wichtiger Beweis aus der Gruppentheorie war 15 000 Seiten lang.
Es gibt mittlerweile einige Beweise, die mit Computerhilfe erstellt wurden und so groß sind, dass der Mensch alleine sie nicht mehr nachvollziehen kann. So konnte etwa ein Team um Thomas Hales von der University of Pittsburgh nachweisen, dass die berühmte Kepler’sche Vermutung stimmt, wonach zum Beispiel ein Stapel Orangen dann am dichtesten gepackt ist, wenn man sie wie auf dem Markt in Pyramidenform schichtet. Der Beweis war auch mehrere hundert Seiten lang. Doch es gibt eine Lösung: Man verwendet den Computer nicht nur als Rechenknecht für aufwendige Berechnungen, sondern für die Erstellung und Überprüfung des Beweises selbst. Das macht Hales derzeit.
In Beweisen lesen sich ja häufig so Sätze wie „offensichtlich ist zu sehen“. Manche Mathematiker verweisen auf die Schönheit einer Argumentation. Und der berühmte indische Zahlentheoretiker Ramanujan berichtete gelegentlich, die Göttin Namagiri habe ihm in der Nacht wieder eine Formel eingeflüstert.
Im Grunde geht es hier um die geometrische und algebraische Intuition, die in vielen Bereichen der Mathematik tatsächlich eine große Rolle spielt. Als Logiker machen wir einen Schritt zurück: Die Ästhetik einer mathematischen Einsicht kann faszinieren, aber auch irritieren. Deshalb schauen wir genau an, was da gemacht wurde.
Sie sind die Haarspalter?
Die Logik ist halt die Metawissenschaft der Mathematik. Sie verhält sich zur Mathematik wie die Literaturwissenschaft zur Literatur. Im besten Fall ist aber die Literaturkritik selber Literatur. So ist auch die Logik eigentlich metamathematisch, aber in sich auch mathematisch. Das macht die Logik auch so mächtig.
Welche Relevanz hat die Logik denn heute für den Alltag der Menschen?
Sie spielt eine enorm große Rolle in der modernen Informatik. Ich selber suche zum Beispiel mit logischen Methoden nach Fehlern in Hard- und Software. Wenn sie etwa den Programmcode eines üblichen Betriebssystems auf DIN-A4-Papier ausdrucken, dann ergibt das eine Schlange, die von Wien nach München reicht. Es ist vollkommen ausgeschlossen, das händisch zu überprüfen. Deshalb übersetzen wir die Programme in lange logische Formeln und lassen sie von anderen Computern auf Fehler untersuchen.
Woher wissen Sie, dass nicht wiederum Ihre Computer Fehler machen?
Der praktische und auch der philosophische Grund ist, dass wir in der Logik alles auf einige wenige Schlussprinzipien zurückführen. Wenn Sie eine Liste einfacher Regeln auf ein paar Blatt Papier haben, kann man sich recht leicht darauf verständigen, dass diese korrekt sind.
Merkt man etwas von Ihrer Arbeit in der Praxis? Computer stürzen immer noch gerne ab.
In der Industrie werden diese Techniken immer mehr eingesetzt. Mit logischen Verifikationsmethoden sorgen wir für sichere Fahrstühle, Autos, Flugzeuge. Aber auch für die privaten Anwender ist Verifikation zunehmend wichtiger. So hat etwa Microsoft derart die Probleme bei den Gerätetreibern zu einem großen Teil beseitigt. In den nächsten zehn bis zwanzig Jahren wird diese Forschung immer mehr den Alltag der Programmierer prägen.
Was noch können wir von der modernen Logik erwarten?
Immer wichtiger wird ihr Einsatz in der Wissensrepräsentation, in Datenbanken, ganz allgemein in der Künstlichen Intelligenz. Logik ist eine Sprache, die Computer in die Lage versetzt, Schlüsse über die reale Welt zu ziehen. Dafür muss die klassische Logik aber auch erweitert werden. Wir sprachen am Anfang über den Pinguin, der ein Vogel ist, der nicht fliegen kann. Um solche vermeintlichen Widersprüche aufzulösen, brauche ich sogenannte nicht-monotone Logiken. Oder nehmen Sie den Begriff „jung“. Bin ich mit meinen 43 Jahren jetzt noch jung oder nicht? Darüber lässt sich streiten. Für solche Sachverhalte gibt es die Fuzzylogik. Solche Logiken können mit der Vagheit und Ambivalenz der menschlichen Sprache umgehen.
Was bringt das in der Praxis?
Sie können zum Beispiel Suchmaschinen für das Internet verbessern, indem Sie die Inhalte auf Webseiten besser verstehen. Bislang funktioniert die Internet-Suche ja vor allem über Stichwortsuche und Statistik.
Umgekehrt ist man doch etwa bei Übersetzungsprogrammen mit regelgeleiteten Ansätzen noch nicht so richtig vorangekommen. Manche Forscher setzen deshalb auf schiere Rechenkraft und Statistik: Man scannt einfach alle Texte im Internet und sucht nach passenden Übersetzungen für Textteile.
Es gibt beide Ansätze. Wenn ein Computer ein Auto lenken soll, eignen sich maschinelles Lernen und Statistik; für die juristische Analyse eines Unfallhergangs anhand der Gesetze und vorhandenen Informationen, braucht man Logik.
Manche Computerwissenschaftler sagen, dass Roboter auch Emotionen erkennen und vielleicht auch äußern sollten, um effizient mit Menschen zu interagieren.
Ich weiß nicht, ob wir uns humanoide Computer wünschen sollen, die womöglich noch autonom entscheiden und als Chirurgen oder Soldaten agieren. Die Künstliche Intelligenz sollte uns nur Werkzeuge liefern. Die großen Fragen, die ja immer auch moralische Komponenten haben, sollten wir Menschen entscheiden.
Lässt sich nicht auch Moral nach logischen Regeln in Computer und Roboter einbauen? Manche Computerwissenschaftler plädieren für Moralprogramme etwa in Drohnen, weil sie sich an die Regeln besser halten als Menschen, die vielleicht gerade in Todesangst entscheiden müssen.
Schwierige Frage. Ja, eine Drohne läuft nicht Amok. Dennoch wäre es im eigentlichen Sinn des Wortes unmenschlich, Entscheidungen über Leben und Tod dem Computer zu überlassen. Es sei denn, zwei Drohnen erschießen sich gegenseitig, das wäre mir sympathisch - allerdings könnte man den Krieg dann gleich als Computersimulation führen. Aber im Ernst, ich halte es mit Robert Musil, der geschrieben hat, dass Moral die Seele durch Logik ersetzt. Was aber geschieht, wenn der Computer auf Situationen stößt, wo ihm eine logische Regel keine Antwort gibt? Und die Seele fehlt? Ich denke auch an jene berühmten Situationen im Kalten Krieg, wo jemand wie Stanislaw Petrow 1983 dann doch nicht auf den Knopf für die Atomraketen gedrückt hat, weil sein Instinkt nicht an den gegnerischen Angriff geglaubt hat, den ihm die Computer gemeldet hatten.
Brauchen wir also weiterhin so etwas wie Intuition?
Ganz sicher. Für existentielle Extremsituationen ebenso wie für die Schönheit mathematischer Formeln. Aber klar ist auch, dass die Informatik in den nächsten Jahrzehnten eine Schlüsselwissenschaft werden wird, die ganz neue philosophische, juristische und politische Fragen aufwirft. Der öffentliche Diskurs ist da noch nicht weit genug.
Süddeutsche Zeitung, Samstag, den 19. Juli 2014, Seite 22
Sie führt an die Grenzen des Denkens und sorgt dafür, dass der Fahrstuhl funktioniert. Helmut Veith über eine Wissenschaft, die noch stringenter sein will als die Mathematik
Interview: Christian Weber
Wien war in den 20er-Jahren des vergangenen Jahrhunderts das wichtigste Zentrum für Logik in der Welt. Philosophen und Denker wie Ludwig Wittgenstein, Kurt Gödel, Karl Popper prägten die Wissenschaftsgeschichte jener Zeit. Mittlerweile gehört die Stadt wieder zu den weltweit führenden Standorten der Logikforschung, weshalb derzeit dort der „Vienna Summer of Logic“ stattfindet, mit 2500 Teilnehmern der größte Kongress, seitdem Aristoteles im vierten Jahrhundert v. Chr. die Disziplin der Logik mitbegründete. Helmut Veith von der Technischen Universität Wien ist einer der Hauptorganisatoren.
SZ: Herr Veith, würde Aristoteles auch nur ein Wort verstehen, wenn ihn eine Zeitmaschine in einen Ihrer Konferenzsäle transferieren würde, und da spricht gerade jemand zum Beispiel über bitopologische Dualität?
Helmut Veith: Die Grundfrage unserer Disziplin hat sich seit der Antike nicht geändert: Wie kann ich aus vorliegenden Fakten nur durch formale Schlüsse neue Fakten ableiten? Fachlich müsste auch ein Genie wie Aristoteles sich bestimmt ein halbes Jahr einarbeiten, dann aber hätte er sicher Sympathie und Verständnis für unsere Fragen.
Wenn wir Laien an Logik denken, dann an Sätze wie: „Alle Vögel fliegen. Kurt ist ein Vogel. Also kann Kurt fliegen.“ Mittlerweile ist es ein bisschen komplexer?
Nun ja, es geht in vielen Bereichen unseres Faches schon noch immer um die Frage, wie kann ich Logik einsetzen, um Schlussfolgerungen über die Welt zu ziehen? Vielleicht haben wir über die Jahrhunderte entdeckt, dass die Welt komplizierter ist als anfangs gedacht. Um bei ihrem Beispiel zu bleiben: Klar, Vögel können fliegen, aber was ist mit Ausnahmen wie den Pinguinen? Moderne Logik versucht, eine Sprache auch für solche Probleme der Alltagswelt zu finden.
Aber Paradoxien sind ja nun nicht neu.
Ja, sicher. Bereits im 19. Jahrhundert hatten Leute wie etwa Georg Cantor, Gottlob Frege und Bertrand Russell in der Mathematik zunehmend Paradoxien entdeckt. Bekannt ist etwa Russells Paradox in Freges Mengentheorie. Es entspricht dem berühmten Fall des Barbiers, der genau diejenigen Barbiere rasiert, die sich nicht selbst rasieren. Was macht also dieser Barbier? Falls er sich nicht selbst rasiert, müsste er sich ja rasieren. Falls er sich jedoch rasiert, darf er nicht zu jenen gehören, die sich selbst rasieren. Die Vorstellung eines solchen Barbiers führt also notwendigerweise zu Widersprüchen, und das beunruhigte die Mathematiker. Die Antwort auf solche Probleme war die Entwicklung der mathematischen Logik, die dann auch durch den berühmten deutschen Mathematiker David Hilbert vorangetrieben wurde.
Was war Hilberts Ziel?
Er wollte die gesamte Mathematik logisch fundieren, also auf einfache mechanische Schlussregeln zurückführen, die von wenigen unmittelbar einsichtigen Axiomen ausgehen. Dieses Programm sollte den Weg öffnen für eine Automatisierung der Mathematik, sodass man im Prinzip mit einem Computer mathematische Sätze ableiten kann.
Hätte das Mathematiker arbeitslos gemacht?
So weit ist es nicht gekommen. Hilberts Programm wurde bekanntlich 1931 durch den jungen Kurt Gödel in Wien vernichtet, ohne Zweifel der berühmteste Logiker seit Aristoteles. Er konnte zeigen, dass es in hinreichend komplexen formalen Systemen wie der Arithmetik notwendigerweise Sätze gibt, die sich weder beweisen noch widerlegen lassen.
Der berühmte Unvollständigkeitssatz.
Genau. Er zeigt, dass sich mit keiner logisch-mathematischen Definition die ganze Mathematik erfassen lässt. Es wird also immer Sätze geben, die ich als wahr erkenne, aber nicht beweisen kann. Wahrheit und Beweisbarkeit sind verschiedene Dinge.
Manche Zeitgenossen sehen im Unvollständigkeitssatz deshalb einen Beleg, dass die Welt kausal nicht abgeschlossen ist. Somit entstehe eine Lücke, in der Gott denkbar werde... Sie runzeln die Stirn?
Ich warne davor, dass man ein technisches Resultat nimmt und einfach auf andere Gebiete überträgt. Gödels Satz besagt nur, dass die Mathematik kein abgeschlossenes Projekt ist. Es wird also immer wieder neue Bereiche geben, in die der menschliche Geist mit seinen 1,5 Kilogramm Gehirnmasse vorstoßen kann. Das ist doch eine erfreuliche Nachricht...
...die aber auch ein bisschen unheimlich ist. Das Schöne an der Schulmathematik war ja gerade, dass am Ende immer alles aufging.
Manche Wissenschaftler waren tatsächlich erschüttert. John von Neumann etwa gab wegen des Unvollständigkeitssatzes die Logik auf. Dennoch: Gödels Satz war der Big Bang der modernen Logik, erst aus ihm sind die unterschiedlichen Zweige der modernen mathematischen Logik entstanden, die sich mit prinzipiellen Fragen der Berechenbarkeit, der Beweis- und der Modelltheorie beschäftigen, überhaupt mit den Grundlagen der Mathematik.
Ist das alles wirklich wichtig für die Menschheit?
Natürlich, die moderne logische Forschung hat etwa überhaupt erst die ganze Informatik möglich gemacht. Der britische Mathematiker Alan Turing etwa hat angesichts der neuen logischen Methoden das erste präzise Modell eines Computers entwickelt, die sogenannte Turing-Maschine. Auf ihn gehen auch zentrale Begriffe zurück wie etwa die Unterscheidung zwischen Programm und Speicher.
Kann Logik tatsächlich zur mathematischen Forschung beitragen, wenn doch Gödel - wie Sie eben sagten - das Hilbert’sche Programm der automatisierten Mathematik zerstört hat?
Hilberts Traum war, mit automatisierten Verfahren die gesamte Mathematik zu erfassen. Das geht nicht. Bei engeren, klar umrissenen Fragestellungen ist der Computer aber durchaus hilfreich. Sehr häufig ist man zufrieden, wenn er in praktischen Fällen eine korrekte Antwort liefert und ansonsten sagt: Hier weiß ich die Antwort nicht. Das ist bei menschlichen Experten ja auch nicht anders.
Das ist für einen Logiker ein erstaunlich pragmatischer Ansatz.
Ja, aber dieser Pragmatismus ist verbunden mit mathematischen Untersuchungen, die exakt jene Situationen eingrenzen, wo wir präzise Antworten finden können.
Manche Forscher fühlen sich auch unwohl, weil der Computer ihnen ein Ergebnis ausspuckt, das sie selbst nicht mehr nachprüfen können, manchmal schon aus Zeitgründen: Ein wichtiger Beweis aus der Gruppentheorie war 15 000 Seiten lang.
Es gibt mittlerweile einige Beweise, die mit Computerhilfe erstellt wurden und so groß sind, dass der Mensch alleine sie nicht mehr nachvollziehen kann. So konnte etwa ein Team um Thomas Hales von der University of Pittsburgh nachweisen, dass die berühmte Kepler’sche Vermutung stimmt, wonach zum Beispiel ein Stapel Orangen dann am dichtesten gepackt ist, wenn man sie wie auf dem Markt in Pyramidenform schichtet. Der Beweis war auch mehrere hundert Seiten lang. Doch es gibt eine Lösung: Man verwendet den Computer nicht nur als Rechenknecht für aufwendige Berechnungen, sondern für die Erstellung und Überprüfung des Beweises selbst. Das macht Hales derzeit.
In Beweisen lesen sich ja häufig so Sätze wie „offensichtlich ist zu sehen“. Manche Mathematiker verweisen auf die Schönheit einer Argumentation. Und der berühmte indische Zahlentheoretiker Ramanujan berichtete gelegentlich, die Göttin Namagiri habe ihm in der Nacht wieder eine Formel eingeflüstert.
Im Grunde geht es hier um die geometrische und algebraische Intuition, die in vielen Bereichen der Mathematik tatsächlich eine große Rolle spielt. Als Logiker machen wir einen Schritt zurück: Die Ästhetik einer mathematischen Einsicht kann faszinieren, aber auch irritieren. Deshalb schauen wir genau an, was da gemacht wurde.
Sie sind die Haarspalter?
Die Logik ist halt die Metawissenschaft der Mathematik. Sie verhält sich zur Mathematik wie die Literaturwissenschaft zur Literatur. Im besten Fall ist aber die Literaturkritik selber Literatur. So ist auch die Logik eigentlich metamathematisch, aber in sich auch mathematisch. Das macht die Logik auch so mächtig.
Welche Relevanz hat die Logik denn heute für den Alltag der Menschen?
Sie spielt eine enorm große Rolle in der modernen Informatik. Ich selber suche zum Beispiel mit logischen Methoden nach Fehlern in Hard- und Software. Wenn sie etwa den Programmcode eines üblichen Betriebssystems auf DIN-A4-Papier ausdrucken, dann ergibt das eine Schlange, die von Wien nach München reicht. Es ist vollkommen ausgeschlossen, das händisch zu überprüfen. Deshalb übersetzen wir die Programme in lange logische Formeln und lassen sie von anderen Computern auf Fehler untersuchen.
Woher wissen Sie, dass nicht wiederum Ihre Computer Fehler machen?
Der praktische und auch der philosophische Grund ist, dass wir in der Logik alles auf einige wenige Schlussprinzipien zurückführen. Wenn Sie eine Liste einfacher Regeln auf ein paar Blatt Papier haben, kann man sich recht leicht darauf verständigen, dass diese korrekt sind.
Merkt man etwas von Ihrer Arbeit in der Praxis? Computer stürzen immer noch gerne ab.
In der Industrie werden diese Techniken immer mehr eingesetzt. Mit logischen Verifikationsmethoden sorgen wir für sichere Fahrstühle, Autos, Flugzeuge. Aber auch für die privaten Anwender ist Verifikation zunehmend wichtiger. So hat etwa Microsoft derart die Probleme bei den Gerätetreibern zu einem großen Teil beseitigt. In den nächsten zehn bis zwanzig Jahren wird diese Forschung immer mehr den Alltag der Programmierer prägen.
Was noch können wir von der modernen Logik erwarten?
Immer wichtiger wird ihr Einsatz in der Wissensrepräsentation, in Datenbanken, ganz allgemein in der Künstlichen Intelligenz. Logik ist eine Sprache, die Computer in die Lage versetzt, Schlüsse über die reale Welt zu ziehen. Dafür muss die klassische Logik aber auch erweitert werden. Wir sprachen am Anfang über den Pinguin, der ein Vogel ist, der nicht fliegen kann. Um solche vermeintlichen Widersprüche aufzulösen, brauche ich sogenannte nicht-monotone Logiken. Oder nehmen Sie den Begriff „jung“. Bin ich mit meinen 43 Jahren jetzt noch jung oder nicht? Darüber lässt sich streiten. Für solche Sachverhalte gibt es die Fuzzylogik. Solche Logiken können mit der Vagheit und Ambivalenz der menschlichen Sprache umgehen.
Was bringt das in der Praxis?
Sie können zum Beispiel Suchmaschinen für das Internet verbessern, indem Sie die Inhalte auf Webseiten besser verstehen. Bislang funktioniert die Internet-Suche ja vor allem über Stichwortsuche und Statistik.
Umgekehrt ist man doch etwa bei Übersetzungsprogrammen mit regelgeleiteten Ansätzen noch nicht so richtig vorangekommen. Manche Forscher setzen deshalb auf schiere Rechenkraft und Statistik: Man scannt einfach alle Texte im Internet und sucht nach passenden Übersetzungen für Textteile.
Es gibt beide Ansätze. Wenn ein Computer ein Auto lenken soll, eignen sich maschinelles Lernen und Statistik; für die juristische Analyse eines Unfallhergangs anhand der Gesetze und vorhandenen Informationen, braucht man Logik.
Manche Computerwissenschaftler sagen, dass Roboter auch Emotionen erkennen und vielleicht auch äußern sollten, um effizient mit Menschen zu interagieren.
Ich weiß nicht, ob wir uns humanoide Computer wünschen sollen, die womöglich noch autonom entscheiden und als Chirurgen oder Soldaten agieren. Die Künstliche Intelligenz sollte uns nur Werkzeuge liefern. Die großen Fragen, die ja immer auch moralische Komponenten haben, sollten wir Menschen entscheiden.
Lässt sich nicht auch Moral nach logischen Regeln in Computer und Roboter einbauen? Manche Computerwissenschaftler plädieren für Moralprogramme etwa in Drohnen, weil sie sich an die Regeln besser halten als Menschen, die vielleicht gerade in Todesangst entscheiden müssen.
Schwierige Frage. Ja, eine Drohne läuft nicht Amok. Dennoch wäre es im eigentlichen Sinn des Wortes unmenschlich, Entscheidungen über Leben und Tod dem Computer zu überlassen. Es sei denn, zwei Drohnen erschießen sich gegenseitig, das wäre mir sympathisch - allerdings könnte man den Krieg dann gleich als Computersimulation führen. Aber im Ernst, ich halte es mit Robert Musil, der geschrieben hat, dass Moral die Seele durch Logik ersetzt. Was aber geschieht, wenn der Computer auf Situationen stößt, wo ihm eine logische Regel keine Antwort gibt? Und die Seele fehlt? Ich denke auch an jene berühmten Situationen im Kalten Krieg, wo jemand wie Stanislaw Petrow 1983 dann doch nicht auf den Knopf für die Atomraketen gedrückt hat, weil sein Instinkt nicht an den gegnerischen Angriff geglaubt hat, den ihm die Computer gemeldet hatten.
Brauchen wir also weiterhin so etwas wie Intuition?
Ganz sicher. Für existentielle Extremsituationen ebenso wie für die Schönheit mathematischer Formeln. Aber klar ist auch, dass die Informatik in den nächsten Jahrzehnten eine Schlüsselwissenschaft werden wird, die ganz neue philosophische, juristische und politische Fragen aufwirft. Der öffentliche Diskurs ist da noch nicht weit genug.
Süddeutsche Zeitung, Samstag, den 19. Juli 2014, Seite 22