Was sind die philosophischen Konsequenzen des Einsatzes von Computern für Wissenschaft und Mathematik?

Da die erkenntnistheoretischen und methodischen Probleme mit Simulationen, die computererweiterte Analoga von Gedankenexperimenten sind, und computergestützten Beweisen ähnlich sind, werde ich mich nur auf letztere konzentrieren. Computerunterstützte Beweise gewannen mit dem (angeblichen) Beweis des Vierfarbensatzes von Appel-Haken-Koch an Bedeutung. Tymoczko schrieb 1980 in seiner Arbeit Computers, Proofs and Mathematicians : „ Computergestützte Beweise veranschaulichen die Notwendigkeit einer realistischeren Philosophie der Mathematik, die Fehlbarkeit und empirische Elemente zulässt “. Dies bedeutete jedoch, den Umfang der Mathematik nur zu erweitern und den "rigorosen", computerfreien abzugrenzen:

"Das Lemma behauptet, dass jede Konfiguration in einer bestimmten Menge D-reduzierbar (oder C-reduzierbar) ist. Der Grund für dieses Lemma ist, dass geeignet programmierte Computer eine bestimmte Ausgabe liefern, wenn sie eine bestimmte Eingabe erhalten. Solche Gründe sind jedoch grundsätzlich fehlbar. Die Ausgabe könnte falsch gelesen worden sein, die Computer hätten eine Fehlfunktion gehabt, die Computer könnten falsch programmiert worden sein, die Programme könnten die mathematische Absicht nicht erfasst haben. Wenn eine dieser Möglichkeiten zutrifft, dann könnte nach allem, was wir wissen, der Vier-Farben-Satz falsch sein ... Natürlich ist die Möglichkeit eines Irrtums ziemlich gering. Es hindert Mathematiker nicht mehr daran, den Vierfarbensatz zu kennen, als die Möglichkeit eines Irrtums Wissenschaftler daran hindert, Tatsachen über das physikalische Universum zu kennen. Aber diese kleine Fehlermöglichkeit hindert Mathematiker daran, den Vierfarbensatz mit absoluter Sicherheit zu kennen. Der Beweis ist nicht streng."

Seitdem wurde darauf hingewiesen, dass "absolute Gewissheit" niemals absolut sei und Probleme mit der gesellschaftlichen Akzeptanz von Beweisen nicht von Computern herrührten. Zum Beispiel wurde Kempes 1879er Beweis des Vier-Farben-Theorems elf Jahre lang als solcher akzeptiert, bis Heawood einen Fehler darin fand. Eine heftige Debatte über die Rolle von Strenge und Experimenten/Simulationen begann, als Jaffe und Quinn 1993 vorschlugen, Tymoczkos Idee umzusetzen, indem sie „theoretische“ (nach dem Vorbild der theoretischen Physik) und „rigorose“ Mathematik institutionell, in Veröffentlichungen usw. voneinander abgrenzen. Siehe Diskussion und Referenzen unter Was macht etwas zu Mathematik?Die Institutionalisierungsidee hat sich nicht durchgesetzt (einige sahen den Jaffe-Quinn-Vorschlag als einen Versuch an, „theoretische Mathematik“ abzuwerten), aber eine klare Abgrenzung von mutmaßlichem/heuristischem Material bleibt eine informelle Norm. Es wird auch erwartet, dass jede substantielle Verwendung von Computerwerkzeugen, selbst bei Berechnungen, geschweige denn Beweisen, explizit erwähnt und ausreichend beschrieben wird, um reproduzierbar zu sein (ähnlich wie bei der Berichterstattung über Experimente in der Wissenschaft).

Aber das Händeringen um „absolute“ Strenge ist nicht die einzige Sorge. Hamming , dessen Mathematik informatikorientiert war, ist bekannt dafür, dass er witzelte: „ Tippen ist kein Ersatz für Denken “ und „ der Zweck des Rechnens ist Einsicht, nicht Zahlen “. Man kann es pragmatisch nehmen, oder man kann es grundsätzlicher nehmen. Selbst pragmatisch können uns beispielsweise Simulationen der Hurrikanbewegungen Vorhersagen liefern, aber nicht warumsie sind so und so. Wenn Modelle nicht übereinstimmen, werden wir im Dunkeln gelassen, weil das entscheidende Element der Einsicht fehlt. Und nach der kantianisch/intuitionistischen Auffassung von Mathematik und mathematischer Gültigkeit ist die Kluft zwischen menschlichen und computergestützten Beweisen mehr als eine Frage des Grades. Dass eine Deduktion einen Beweis darstellt, solange sie in jedem Schritt den „Regeln“ entspricht, ist eine formalistische Vorstellung. Aber nicht alle Wissenschaftler oder Mathematiker sind Formalisten. Für einige gibt es diesen schwer fassbaren Aspekt intuitiver Einsicht, ohne den ein Beweis bestenfalls eine blinde Berechnung ist, mit dem Stigma der Minderwertigkeit. „Verstehen“ findet einfach nicht außerhalb eines Verstehenden statt, und ein Beweis ist kein Beweis, bis er verstanden wird. Ähnliche Empfindlichkeiten beeinträchtigen die Rezeption der Quantenmechanik, Beschwerden über "sind keine Seltenheit.

In seinen Bemerkungen zu den Grundlagen der Mathematik hat Wittgenstein bereits vor dem Aufkommen der Computer ein allgemeines Phänomen identifiziert, das solche Sorgen nährt. Um einen Computer in die Lage zu versetzen, einen Beweis zu unterstützen, sind viele sprachliche Konvertierungen erforderlich. Wir gehen normalerweise von der „Transparenz der Sprache“ aus und betrachten sie als Umwandlung der „gleichen“ Berechnungen in unterschiedliche Formalismen, aber angenommene „Umwandlungen“ können die Vorstellung dessen, was getan wird, verändern. Das „ Gefährliche, Trügerische “ daran ist, dass „ es die Begriffsbestimmung – die Begriffsbildung – wie eine Naturtatsache erscheinen lässt “:

„ Ein mathematischer Beweis muss klar sein … Der Beweis muss eine Konfiguration sein, deren exakte Reproduktion sicher sein kann … Was uns überzeugt – das ist der Beweis: eine Konfiguration, die uns nicht überzeugt, ist nicht der Beweis, selbst wenn sie es ist exemplarisch für den bewiesenen Satz gezeigt werden kann, das heißt: Es muss nicht notwendig sein, eine physikalische Untersuchung der Beweiskonfiguration vorzunehmen, um uns das Bewiesene zu zeigen.

[...] Ich will sagen: man braucht die Russellsche Rechentechnik gar nicht anzuerkennen -- und kann mit einer anderen Rechentechnik beweisen, daß es einen Russellschen Beweis des Satzes geben muß. Aber dann basiert der Satz natürlich nicht mehr auf dem Russellschen Beweis.

[...] Es ist keine Logik - möchte ich sagen - die mich dazu zwingt, einen Satz anzunehmen ... wenn es eine Million Variablen in den ersten beiden Klammerpaaren und zwei Millionen in der dritten gibt. Ich will sagen: Die Logik würde mich in diesem Fall überhaupt nicht zwingen, irgendeinen Satz anzunehmen. Etwas anderes zwingt mich, einen solchen Satz als logisch anzunehmen ... Ich will sagen: mit der Logik der Principia Mathematica wäre es möglich, eine Arithmetik zu rechtfertigen, in der 1000 + 1 = 1000 ist; und dazu bräuchte es nur, an der vernünftigen Richtigkeit der Berechnungen zu zweifeln. Aber wenn wir nicht daran zweifeln, dann ist nicht unsere Überzeugung von der Wahrheit der Logik verantwortlich. "

Mit anderen Worten, Wittgenstein lehnt die Unterscheidung zwischen Formalismus und Implementierung ab (die sich implizit auf sprachtranszendente platonische Entitäten bezieht, die in verschiedenen Implementierungen „ausgedrückt“ werden) und weist darauf hin, dass „Konversion“ einen neuen Formalismus schafft. Da bei Computern der eine "einsichtig" ist und der andere nicht, haben wir einen qualitativen Unterschied zwischen beiden, nicht nur einen pragmatischen. Natürlich hätte er nichts gegen die Hinwendung zu neuen Beweisen (" Philosophie lässt alles, wie es ist "), sondern eher gegen die philosophische Selbsttäuschung, dass der hier gemachte Sprung nur eine kosmetische Überarbeitung sei.

Solch ein heimlicher Wechsel von konstruktiven zu platonistischen Beweisen motivierte den intuitionistischen Pushback, aber wie Wittgenstein betont, ist die damit verbundene Selbsttäuschung weitaus allgegenwärtiger. Dieser Punkt betrifft sogar Formalisten, da solche Verschiebungen große Änderungen in den Regeln der "formalen Spiele" der Mathematik mit sich bringen können. Andererseits wäre es selbst für Intuitionisten dumm, computergestützte Beweise nicht pragmatisch einzusetzen. Schließlich bieten sie, wenn sie von kompetenten und vertrauenswürdigen Fachleuten durchgeführt werden, einen weitaus größeren Grad an Sicherheit als die numerische Überprüfung von Vermutungen, die eine ehrwürdige Geschichte mit Euler und Gauß haben.