Geschichten

Es war einmal ein König, der hatte drei Söhne, davon waren zwei klug und gescheit, aber der dritte sprach nicht viel, war einfältig und hieß nur der Dummling …

Nur wenige Worte genügen, uns in eine Gedankenwelt zu entführen, in der wir spannende Abenteuer mit glücklichen oder traurigen Wendungen erwarten. Die dazu benötigte Fähigkeit, sich die handelnden Personen und deren Eigenschaften und Beziehungen zueinander zu merken, besitzen schon kleine Kinder und es stört überhaupt nicht, dass die Personen nur sehr knapp beschrieben sind, ohne Angabe von Größe, Kleidung oder Haarfarbe – im Gegenteil es lässt mehr Freiraum, sie gedanklich durch reale oder fiktive Personen zu ersetzen.

Genau die gleichen Fähigkeiten benötigt man beim Lesen einer Definition oder eines Satzes mit zugehörigem Beweis in der Mathematik, denn auch dabei handelt es sich um Geschichten: Sei K eine Menge und seien A,B,D⊂K. Weiter seien A,B abzählbar und D sei endlich …

In der Metasprache \(\mathbb{M}\)ATh sind mathematische Geschichten (sogenannte settings) wichtige Grundstrukturen. Sie werden beschrieben durch ein oder mehrere Namen für die Hauptdarsteller der Geschichte (die Parameter des setting), eine Liste ihrer angenommenen Eigenschaften und wechselseitigen Beziehungen in Form von mathematischen Aussagen, sowie eine Liste von Folgerungen, die sich für die Parameter und die aus ihnen gebildeten Objekte ergeben. Mit diesen Grundstrukturen lassen sich dann Mengen, Funktionen, Definitionen, Sätze, Modelle und Theorien in einer gemeinsamen Form kodieren.

Für die Struktur des metrischen Raums sieht das setting zum Beispiel so aus:

setting metrischerRaum
  given X:Set
  given d:X^2 --> X
  assume fact Ax1 := [forall x,y:X holds d(x,y)=0 <=> x=y]
  assume fact Ax2 := [forall x,y:X holds d(x,y)=d(x,y)]
  assume fact Ax3 := [forall x,y,z:X holds d(x,y) <= d(x,z) + d(z,y)]
end

Eine Weiterführung der Geschichte besteht dann aus zusätzlichen Definitionen und bewiesenen Aussagen.

develop metrischerRaum
  prove [forall x,y:X holds d(x,y) >= 0] .. (directly)
    // Beweisschritte unterdrückt
  qed
  def B(r:Rpos, x:X) := {y:X with d(y,x) < r}
end