Konstruktivismus
— Geschichte,
Philosophie und
Praxis
Hannes Diener

Das Problem

An Stelle einer "Outline" ein paar Worte als Einleitung.

Das Problem

Satz. Es existieren zwei irrationale Zahlen $a$,$b$, so daß $a^b$ rational ist.

Beweis:

Entweder $\sqrt{2}^\sqrt{2}$ ist rational oder nicht.
$\sqrt{2}^\sqrt{2} \in \mathbb{Q}$:

fertig.
$\sqrt{2}^\sqrt{2} \notin \mathbb{Q}$:

$\left(\sqrt{2}^\sqrt{2}\right)^\sqrt{2}$
$=\sqrt{2}^{\sqrt{2} \cdot \sqrt{2}}$
$= \sqrt{2}^2=2$.

Das Problem

Satz. Es existieren zwei irrationale Zahlen $a$,$b$, so daß $a^b$ rational ist.

Wunderbar, aber ist dieser Beweis befriedigend?

Was ist z.B. wenn wir diese Zahlen $a,b$ in einer Anwendung (sagen wir mal approximiert auf die 7. Dezimalstelle) brauchen?

Das Problem

Zwei Anmerkungen

  1. Es ist mittlerweile bekannt, daß $\sqrt{2}^\sqrt{2}$ irrational ist.
  2. Es gibt ein einfaches Beispiel, welches das Problem umgeht: $e$ und $\ln(2)$

Die Lösung?

Der kritische Schritt im Beweis oben ist ja die Entscheidung ob $\sqrt{2}^\sqrt{2}$ rational ist oder nicht.

Verbieten wir also einfach die Benutzung des Tertium non Daturs: \[P \vee \neg P \ , \] damit alle Beweise konstruktiv sind.

Oder positiver ausgedrückt: verwenden wir intuitionische Logik an Stelle von klassischer Logik.

Die Lösung?

Was ist intuitionistische Logik?

  1. Billige Antwort: klassische Logik ohne das Tertium non Datur.
  2. Bessere Antwort: intuitionistische Logik genügt der BHK-Interpretation. D.h. wir verlagern unser Interesse von wahr zu beweisbar/konstruierbar/berechenbar. Insbesondere gilt also für zusammengesetze Aussagen:
    • $\alpha \wedge \beta$: Wir haben einen Beweis von $\alpha$ und einen von $\beta$
    • $\alpha \vee \beta$: Wir haben einen Beweis von $\alpha$ oder einen von $\beta$
    • $\alpha \rightarrow \beta$: Wir haben einen Algorithmus, der einen Beweis von $\alpha$ in einen von $\beta$ umwandelt.
    • $\neg \alpha$: Wie üblich, definiert als $\alpha \rightarrow \bot$.
    • $\forall x \in S: \alpha(x)$: Ein Algorithmus, der ein Element von $x \in S$ in einen Beweis für $\alpha(x)$ umwandelt
    • $\exists x \in S: \alpha(x)$: Ein Beweis, daß $x \in S$ und $\alpha(x)$ gilt.
  3. Beste Antwort: Standard-Logikbücher.

Logik

Mit der BHK-Interpretation ist auch klar, warum das Tertium non Datur nicht akzeptierbar ist.

Sei zum Beispiel $R$ die Riemann'sche Hypothese. Dann würde \[ R \vee \neg R \] ja bedeuten, daß wir einen Beweis für die Riemann Hypothese haben, oder daß wir einen Beweis haben, daß die Riemann Hypothese zu Widersprüchen führt.

Die Lösung?

Man beachte, daß das Tertium non Datur oft in folgender äquivalenten Form auftritt \[\neg \neg P \rightarrow P \ . \]

Man beachte außerdem, daß zu zeigen, daß $\neg P$ gilt, indem man $P$ annimmt und zum Widerspruch führt nicht dasselbe ist, wie

$P$ zu beweisen, indem man $\neg P$ annimmt und zum Widerspruch führt.

Logik

Wunderbar, aber können wir ohne das Tertium non Datur Mathematik betreiben?

Leben ohne das Tertium non Datur

Dieses Tertium non datur dem Mathematiker zu nehmen, wäre etwa, wie wenn man dem Astronomen das Fernrohr oder dem Boxer den Gebrauch der Fäuste untersagen wollte.

Leben ohne das Tertium non Datur

Brouwers Intuitionismus (INT): alle mathematischen Objekte sind freie Kreationen des menschlichen Geistes.

Brouwer und seine Schüler haben gezeigt, daß man auf dieser Grundlage, formal, Mathematik betreiben kann.

Allerdings ist Brouwers Intuitionismus inkompatibel zur klassischen Mathematik; d.h. es gibt Aussagen $\varphi$ (bzw. Axiome), die für Brouwer beweisbar sind, aber die in der klassischen Mathematik falsch sind: beispielsweise sind alle reellwertigen Funktionen gleichmässig stetig. Obendrein war Brouwer (leider) nicht besonders diplomatisch.

Leben ohne das Tertium non Datur

1950er Jahre: Markovs "russisch-rekursive" Schule der Mathematik (RUSS).

Alle mathematischen Objekte müssen sich durch Algorithmen (Turingmaschinen) konstruieren lassen.

Auch diese Sichtweise ist inkompatibel mit der klassischen Mathematik. (Es gibt z.B. reellwertige, stetige Funktionen auf $[0,1]$, die nicht gleichmässig stetig sind.)

Leben ohne das Tertium non Datur

Nachdem sich INT und RUSS "etablierten" passierte erstmal 20 Jahre nichts...

...bis 1967 Errett Bishop Foundations of constructive Analysis veröffentlichte.

Bishop schaffte, was eigentlich unmöglich schien: Mathematik konstruktiv (also mit intuitionistischer Logik) zu betreiben aber gleichzeitig kompatibel zur klassischen Mathematik, INT, und RUSS zu bleiben.

Bishops Trick war die philosophischen Probleme zu überspringen. (Es ist ja egal, ob alle Funktionen stetig sind oder nicht, wenn wir nur mit den gleichmässig stetigen arbeiten).

Leben ohne das Tertium non Datur

Heute sehen wir die konstruktive Landkarte wie folgt:

CLASS INT RUSS BISH +zusätzliche Annahmen Sorry, your browser does not support inline SVG.

Leben ohne das Tertium non Datur

Wann immer ich von konstruktiv spreche meine ich "Bishop style constructive Mathematics."

Etwas genauer: BISH ist

Leben ohne das Tertium non Datur

Einschub über Vorurteile gegenüber dem Konstruktivismus

Leben ohne das Tertium non Datur

Konstruktive Analysis

Wie gesagt wählen wir eine geeignete mengentheoretische Grundlage. (Alternativ kann man auch mit einer Typtheorie arbeiten: siehe nächsten Vortrag).

Wir können die üblichen Aussagen über natürliche und rationale Zahlen zeigen.

Gleichheit natürlicher Zahlen ist entscheidbar. (Siehe Kronecker.)

Leben ohne das Tertium non Datur

Konstruktive Analysis

Wie können wir jetzt die reellen Zahlen konstruieren?

Dedekind-Schnitte sind ungeignet (nächste Folie).

Am Besten ist die Definition als Cauchy-Folge rationaler Zahlen.

$x \gt 0$ ist definiert als "es gibt $n,m \in \mathbb{N}$ so daß \[ \forall{k \geqslant n} : x_k > 2^{-m} \ . \]

$\geqslant$, $\neq$ und $=$ sind definiert über $\gt$.

Wir können zeigen, daß die reellen Zahlen ein Folgen-vollständiger, archimedisch angeordneter Körper sind.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Doch jetzt fängt es an interessant zu werden.

Wir können nicht zeigen, daß jede beschränkte, nicht-leere Menge reeller Zahlen ein Supremum besitzt: betrachte \[ A= \{ x \in \mathbb{R} \mid x=0 \vee (x=1 \wedge \varphi) \} \ ,\] für eine geschlossene Formel $\varphi$. Würde das Supremum existieren, so können wir uns eine $\frac{1}{4}$-Approximation $s^\prime$ betrachten. Entweder $s^\prime \gt 0$, was bedeutet, daß $1 \in A$ ist, und also $\varphi$, oder $s^\prime \lt 1$, was zu $\neg \varphi$ führt.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Doch jetzt fängt es an interessant zu werden.

In RUSS und INT ist die Aussage, daß für alle Binärfolgen $(a_n)_{n \geqslant 1}$ gilt, daß \[ (LPO) \quad\forall n: a_n =0 \vee \exists n : a_n=1 \ , \] falsch.

Wir können mit Hilfe der Goldbach'schen Vermutung sogar, zumindest intuitiv, ein konkretes Gegenbeispiel geben.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Dies hat zur Folge, daß auch folgende Aussage nicht konstruktiv ist: \[ \forall x \in \mathbb{R} : x \lt 0 \vee x = 0 \vee x \gt 0 \ . \] Ansonsten könnte man die Disjunktion oben auf die Zahl \[ a = \sum_{n=0}^\infty \frac{a_n}{2^n} \ \] anwenden, um zu entscheiden ob $a_n=0$ für alle $n$, oder ob es ein $n$ mit $a_n=1$ gibt.

Wir können aber zeigen, daß für $a \lt b$ gilt, daß entweder $a \lt x$ oder $x \lt b$ ist.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Mit einem ähnlichen Argument (via LLPO) kann man zeigen, daß es keine Hoffnung gibt \[ \forall x \in \mathbb{R} : x \leqslant 0 \vee x \geqslant 0 \ \] zu beweisen.

Leben ohne das Tertium non Datur

Konstruktive Analysis

D.h. aber leider auch, daß wir den Zwischenwertsatz in der üblichen Form nicht beweisen können.

Zwischenwertsatz. Ist $f:[0,1] \to \mathbb{R}$ eine stetige Funktion, $f(0) \lt 0$ und $f(1) \gt 0$, so gibt es $x \in [0,1]$ mit $f(x)=0$.
Wir können allerdings folgende Funktion definieren: Tafel.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Allerdings können wir folgende Version beweisen:

Approximativer Zwischenwertsatz. Ist $f:[0,1] \to \mathbb{R}$ eine stetige Funktion, $f(0) \lt 0$ und $f(1) \gt 0$, so gibt es für $\varepsilon \gt 0$ ein $x \in [0,1]$ mit $|f(x)| \lt \varepsilon$.

Leben ohne das Tertium non Datur

Konstruktive Analysis

Bis auf philosophische Gründe gibt es auch praktische Gründe konstruktiv zu arbeiten. Wir können aus Beweisen Programme extrahieren, die automatisch verifiziert sind.

Das ganze funktioniert sogar, wenn man einen Beweisassistenten verwendet, automatisch