Vor Jahren hörte ich mal einen Kolloquiumsvortrag, in dem ein australischer Professor über eine Theorie referierte, in der aus der Verneinung der Verneinung nicht die Richtigkeit einer Aussage folgt. Zum Abschluß meinte er noch geheimnisvoll, seine Theorie sei “not without applications” und war sich der Komik dieses Statements – aus dem in seiner Logik ja eben nicht das Vorhandensein von Anwendungen folgt – offenkundig gar nicht bewußt.
Konstruktive Mathematik nimmt nicht von vornherein an, dass für jede Aussage entweder P oder nicht-P richtig ist, sondern sie muss das in jedem Einzelfall beweisen. Zum Beispiel muss sie erst aus den Peano-Axiomen der natürlichen Zahlen herleiten, dass zwei Zahlen entweder gleich oder ungleich sind. Man weiß in der konstruktiven Mahematik, dass nicht gleichzeitig P und nicht-P gelten können, aber man weiss im Allgemeinen nicht, dass eines von beiden richtig ist.
Die heute gebräuchliche Mathematik benutzt die Zermelo-Frenkel-Mengenlehre und das Auswahlaxiom. Man kann aus dem Auswahlaxiom herleiten, dass für jede Aussage entweder P oder nicht-P richtig ist. Konstruktive Mathematik muss also auf das Auswahlaxiom verzichten.
Im Oktober-Heft des Bulletin of the American Mathematical Society versucht Andrej Bauer zu begründen, dass auch konstruktive Mathematik interessant sei: Five stages of accepting constructive mathematics
Bauer zeigt zunächst, dass man auch in der konstruktiven Mathematik viele Sätze beweisen kann, deren klassische Beweise eigentlich Widerspruchsbeweise sind, und dass sogar viele üblicherweise als Widerspruchsbeweise geführte Beweise eigentlich keine sind, sondern einfach nur eine Negation beweisen (also nicht benutzen, dass entweder P oder nicht-P gilt, sondern nur dass nicht P und nicht-P gelten können): zum Beispiel die Irrationalität der Wurzel aus 2, die Überabzählbarkeit der reellen Zahlen oder dass es keine Menge aller Mengen gibt. Außerdem zeigt er auch, dass man Teile der Mathematik retten kann, wenn man statt des Auswahlaxioms nur die Existenz einer Auswahlfunktion auf abzählbaren Mengenfamilien annimmt. Mit dieser Variante kann man zum Beispiel immer noch den Lebesgueschen Überdeckungssatz beweisen.
Konstruktive Mathematik war zur Zeit ihrer Entstehung in den 20er Jahren sehr umstritten. Bauer führt dies darau zurück, dass mit dem konstruktivistischen Ansatz beim damaligen Stand weite Teile der Mathematik nicht mehr funktioniert hätten und Hilbert deshalb dagegen war. (Und, was Bauer nicht schreibt, man aber versucht ist zu vermuten, Brouwer wohl aus genau diesem Grund dafür.) Laut Bauer ist konstruktive Mathematik erst seit 1967, dem Jahr des Erscheinens von Bishops Buch über konstruktive Analysis, in der Lage grundlegende mathematische Fragen anzugehen. Er zitiert aus einer Besprechung von Bishops Buch:
The thrust of Bishop’s work was that both Hilbert and Brouwer had been wrong about an important point on which they had agreed. Namely both of them thought that if one took constructive mathematics seriously, it would be necessary to “give up” the most important parts of modern mathematics (such as, for example, measure theory or complex analysis). Bishop showed that this was simply false …
Bauer diskutiert dann verschiedene konstruktivistische Modelle, darunter eines das Grothendiecks Theorie der Topoi von Garben verwendet:
In the topos the truth values are the open subsets of X. The truth value of a
statement is the largest open set on which it holds, and the logic is dictated by the topology of X:
• falsehood and truth are ∅ and X, the least and greatest open sets, respec- tively;
• conjunction U ∧V is U ∩V, the largest open set contained in U and V;
• disjunction U ∨V is U ∪V, the least open set containing U and V;
• negation ¬U is the topological exterior ext(U), the largest open set disjoint
from U;
• implication U ⇒ V is ext(U \ V ), the largest open set whose intersection
with U is contained in V .
Excluded middle amounts to saying that U ∪ ext(U) = X for all open U ⊆ X, a condition equivalent to open and closed sets coinciding. Only a very special kind of space X satisfies this condition, for as soon as it is a T0-space (points are uniquely determined by their neighborhoods), it has to be discrete.
Kommentare (27)