Wie würde Hume computergenerierte mathematische Beweise klassifizieren?

Es ist hilfreich, hier zwei Fragen zu unterscheiden: eine logische und eine erkenntnistheoretische. Wenn Sie fragen, was der logische Status eines angebotenen deduktiven Beweises einer Aussage ist, dann ist er entweder gültig oder nicht. Dabei spielt es keine Rolle, ob der Beweis von einem menschlichen Verstand, einem Computer oder einer Explosion in einer Druckerei erzeugt wurde.

Aber oft interessiert uns die erkenntnistheoretische Frage: Wie können wir sicher sein , dass dieser Beweis richtig ist? Es gibt viele gültige Beweise, die sehr schwer zu verstehen sind: Zum Beispiel wissen nur wenige Menschen genug Mathematik, um den Beweis von Fermats letztem Satz zu verstehen . Außerdem gibt es Beweise für Theoreme, die so lang und komplex sind, dass es wahrscheinlich ist, dass keine einzelne Person sie jemals von Anfang bis Ende gelesen hat: Der Klassifikationssatz in der Gruppentheorie ist einer davon – er umfasst Zehntausende von Arbeitsseiten über Hunderte von veröffentlichten Artikeln von etwa hundert verschiedenen Mathematikern.

Wenn ein Beweis so schwierig ist, ist es sinnvoll, die Hilfe von automatisierten Beweisern in Anspruch zu nehmen. Aber es löst nicht vollständig das Problem, wie man sicher sein kann, weil wir immer noch die Gewissheit brauchen, dass der Beweiser selbst korrekt ist. Da der Beweiser eine physikalische Verkörperung eines formalen Beweissystems ist, gilt für ihn der zweite Unvollständigkeitssatz von Gödel: Er kann seine eigene Konsistenz nicht beweisen. Außerdem ist der Beweiser in Hardware und Software implementiert und wir können nicht beweisen, dass es keine Fehler in der Implementierung gibt (obwohl formale Systeme wie die Z-Notation helfen können).

Um auf Ihre Frage zu Hume zurückzukommen, würde ich sagen, dass jeder Beweis logisch mit dem übereinstimmt, was Hume Beziehungen von Ideen nennt, und dies zumindest im Prinzip a priori ist. Aber es gibt ein nüchtern pragmatisches Element in Humes Denken, das vermuten lässt, dass er die Ausgabe eines Computers nur als eine Art empirischen Beweis ansehen könnte. Vielleicht würde er also einen generierten Beweis als a posteriori betrachten, bis er verinnerlicht und verstanden ist.

Die Frage führt wahrscheinlich leicht zu anachronistischen Antworten. Mein Verständnis ist, dass Hume (und Descartes und Locke) gemäß der aktuellen Wissenschaft Ansichten über Schlussfolgerungen hatten, die der modernen, eher "formalistischen" oder deduktiven Ansicht entgegengesetzt sind.

Descartes, Locke & Hume kannten die formalistische Sichtweise durch das frühere scholastische Verständnis der Deduktion, wonach ein Argument gültig ist, weil die Prämissen und die Konklusion die richtige (Propositions-)Form haben. Diese Idee stammt aus der Syllogistik von Aristoteles und wir haben auch unsere Version davon. Nach dieser Auffassung sind computergenerierte Proofs menschengenerierten Proofs grundsätzlich gleichgestellt.

Hume hingegen erbte seine Ansichten über Schlussfolgerungen von Descartes und Locke. Allen zufolge bewegt sich Ihr "Geist" (oder eine kognitive Fähigkeit) während der Schlussfolgerung von einer Idee zur nächsten. (Mein Verständnis ist, dass sie für Propositionen als spezielle Kategorie keine große Verwendung haben, Propositionen sind Sammlungen von Ideen für sie.)

Zum Beispiel ist eine Demonstration des Satzes des Pythagoras ein Versuch, eine Ideenkette zu finden, die es ermöglicht, zu erkennen (oder zu erahnen), dass die Ideen "Quadrat der Hypotenuse" und "Summe der Quadrate der anderen beiden Seiten" in einer bestimmten Beziehung stehen (in diesem Fall äquivalent sind). (Siehe Owen für weitere Einzelheiten.)

Ich verstehe also nicht, wie man aus dieser Sicht sagen könnte, wie Sie es tun, dass computergenerierte Beweise "Ideenbeziehungen par excellence" sind, weil sie Symbole auf einem Papier sind.

Descartes wandte ausdrücklich ein, dass man bei der formalen Deduktion Wahrheit aus Falschheit und Falschheit aus Falschheit ableiten könne. Für Descartes geht es bei einer Demonstration darum, Wahrheit von Falschheit zu unterscheiden, und dazu muss man den Inhalt des Schlusses im Auge haben.

Für ihn besteht der Schlusspunkt darin, Ihnen neues Wissen zu vermitteln. Formale Deduktion ist also in diesem Sinne nutzlos, weil man erstens durch Deduktion nur dann Erkenntnisse gewinnt, wenn die Wahrheit der Prämissen bereits bekannt ist, und zweitens, weil man keine neuen Erkenntnisse gewinnt, da die Konklusion bereits in den Prämissen enthalten ist.

Zweifellos ist diese Ansicht aus moderner Perspektive sehr problematisch, aber laut Owen war dies die Ansicht von Descartes. (Ian Hacking argumentierte sogar, dass Descartes überhaupt keine Vorstellung von Beweisen hatte!)

Hume hat im Grunde dieselbe Ansicht von Locke geerbt. (Natürlich hatten Descartes und Locke unterschiedliche Ansichten über die Entstehung von Ideen .)

Siehe Hume's Reason von David Owen für weitere Einzelheiten.