Die Sprache der Mathematik

Eine Lesehilfe für Laien: was Zeichen wie ∀, ∣, ⇔ und Σ bedeuten, wie ein mathematischer Artikel aufgebaut ist, und wie man einen Beweis in Lean Zeile für Zeile liest.

Die Kapitel dieser Rubrik schreiben ihre Sätze und Beweise so, wie es in mathematischen Fachartikeln üblich ist. Das sieht zuerst fremd aus, ist aber nur eine Kurzschrift. Dieses Kapitel erklärt sie. Man muss es nicht auswendig lernen, sondern kann hier nachschlagen, wenn einem ein Zeichen begegnet.

Warum eine eigene Schrift?

Derselbe Satz einmal in Worten:

Für jede natürliche Zahl n ist die Summe aller Zahlen von 1 bis n gleich dem Produkt aus n und n plus eins, geteilt durch zwei.

Und einmal in der Schreibweise der Mathematik:

\forall n \in \mathbb{N}: \quad \sum_{i=1}^{n} i = \frac{n(n+1)}{2}

Beides sagt genau dasselbe. Die zweite Fassung ist kürzer, man erfasst sie mit einem Blick, und sie lässt keinen Spielraum für Missverständnisse. Darum haben Mathematiker über Jahrhunderte diese Zeichen erfunden. Gelesen wird die Zeile so: „Für alle n aus den natürlichen Zahlen gilt: Die Summe der i von i gleich 1 bis n ist n mal n plus 1, durch 2.“

Zahlen und Mengen

Zeichen	gelesen	Beispiel
$\mathbb{N}$	die natürlichen Zahlen 1, 2, 3 …	$10 \in \mathbb{N}$
$\mathbb{N}_0$	die natürlichen Zahlen mit der Null	$0 \in \mathbb{N}_0$
$\in$	ist Element von, gehört zu	$7 \in \mathbb{N}$
$\notin$	gehört nicht zu	$\tfrac{1}{2} \notin \mathbb{N}$
$\{\, \dots \,\}$	die Menge aus …	$\{1, 2, 5, 10\}$
$\{x : \dots\}$	die Menge aller x, für die … gilt	$\{d \in \mathbb{N} : d \mid 10\} = \{1,2,5,10\}$

Rechnen und Teilen

Zeichen	gelesen	Beispiel
$a \cdot b$ , $ab$	a mal b	$4 \cdot 5 = 20$
$\frac{a}{b}$	a geteilt durch b	$\frac{20}{2} = 10$
$\sum_{i=1}^{n} i$	Summe der i von 1 bis `n`	$\sum_{i=1}^{4} i = 1+2+3+4$
$\prod_{i=1}^{n} i$ , $n!$	Produkt der i von 1 bis `n`, „`n` Fakultät“	$4! = 1 \cdot 2 \cdot 3 \cdot 4 = 24$
$a \mid b$	a teilt b	$5 \mid 10$
$a \nmid b$	a teilt b nicht	$4 \nmid 10$
$\gcd(a, b)$	größter gemeinsamer Teiler, deutsch ggT	$\gcd(10, 4) = 2$
$a \equiv b \pmod{m}$	a und b lassen bei Teilung durch m denselben Rest	$25 \equiv 1 \pmod{6}$
$\lfloor x \rfloor$	x abgerundet	$\lfloor 2{,}5 \rfloor = 2$

Ein Wort zum senkrechten Strich: $a \mid b$ ist eine Aussage („5 teilt 10“, das ist wahr oder falsch), keine Rechnung. $\frac{b}{a}$ dagegen ist eine Zahl. Das Zeichen ist ein Strich, kein Bruchstrich, gerade damit man beides nicht verwechselt.

Logik

Zeichen	gelesen	Beispiel
$\forall$	für alle	$\forall n \in \mathbb{N}: n + 1 > n$
$\exists$	es gibt	$\exists d: 1 < d < 10 \text{ und } d \mid 10$
$\land$ , $\lor$	und, oder	$2 \mid 10 \land 5 \mid 10$
$\lnot$	nicht	$\lnot\, (3 \mid 10)$
$A \Rightarrow B$	aus A folgt B, wenn A, dann B	$4 \mid n \Rightarrow 2 \mid n$
$A \Leftrightarrow B$	A genau dann, wenn B	$2 \mid n \Leftrightarrow n \text{ gerade}$
$:=$	ist definiert als	$T(n) := \sum_{i=1}^n i$

Das „oder“ der Mathematik ist immer einschließend: $A \lor B$ ist auch wahr, wenn beides gilt. Und $A \Rightarrow B$ sagt nichts darüber, was passiert, wenn A falsch ist. Aus „Wenn es regnet, ist die Straße nass“ folgt nicht, dass die Straße trocken ist, wenn es nicht regnet.

Wie ein Artikel aufgebaut ist

Mathematische Texte bestehen aus wenigen Bausteinen, die immer gleich heißen:

Definition: Ein Begriff wird festgelegt. Ab dann bedeutet das Wort genau das und nichts anderes.
Satz (englisch Theorem): eine wichtige bewiesene Aussage.
Lemma: ein Hilfssatz, der vor allem gebraucht wird, um einen anderen Satz zu beweisen.
Folgerung (englisch Corollary): ein Satz, der sich mit wenigen Zeilen aus einem vorigen ergibt.
Beweis: die Begründung. Sein Ende markiert das Zeichen ∎ oder die Abkürzung q. e. d., lateinisch quod erat demonstrandum, „was zu beweisen war“.

Auch innerhalb eines Beweises gibt es feste Wendungen:

„Sei n ∈ ℕ“ heißt: Wir nehmen irgendeine natürliche Zahl, ohne zu sagen, welche. Was dann folgt, gilt für jede.
„O. B. d. A.“, ohne Beschränkung der Allgemeinheit: Wir betrachten nur einen Fall, weil die anderen genauso gehen.
„Angenommen, …“ leitet oft einen Widerspruchsbeweis ein: Man nimmt das Gegenteil an und zeigt, dass daraus Unsinn folgt.
Induktionsanfang und Induktionsschritt sind die beiden Teile eines Induktionsbeweises, der erste und der jeweils nächste Dominostein (siehe Was ist ein Beweis?).

Ein kleines vollständiges Beispiel in dieser Form:

Satz

Für alle $n \in \mathbb{N}$ ist $n(n+1)$ gerade.

Beweis

Sei $n \in \mathbb{N}$ . Von den beiden aufeinanderfolgenden Zahlen $n$ und $n+1$ ist genau eine gerade. Ein Produkt mit einem geraden Faktor ist gerade. Also gilt $2 \mid n(n+1)$ .

∎

Zeile für Zeile gelesen: Der Satz behauptet etwas über alle natürlichen Zahlen. „Sei n ∈ ℕ“ greift eine beliebige heraus. Die nächsten zwei Sätze sind die Begründung, der letzte schreibt das Ergebnis in Zeichen, und ∎ sagt: fertig. Genau so sind alle Beweise dieser Rubrik gebaut.

Wie man Lean liest

Unter wichtigen Sätzen steht ein aufklappbarer Kasten mit demselben Beweis in Lean, einer Programmiersprache für Beweise, die seit 2013 entwickelt wird. Lean ist strenger als jeder menschliche Leser: Es nimmt einen Beweis nur an, wenn jeder Schritt aus den Regeln der Logik folgt. Hier ist der Beweis der Dreieckszahlen aus Kapitel 1, Stück für Stück erklärt.

/-- Die n-te Dreieckszahl 1 + 2 + … + n -/

Ein Kommentar. Text zwischen /-- und -/ ist für Menschen geschrieben, Lean überliest ihn. Einzeilige Kommentare beginnen mit --.

def dreieck : Nat → Nat
| 0 => 0
| n + 1 => dreieck n + (n + 1)

Eine Definition. def führt einen neuen Namen ein, hier dreieck. Hinter dem Doppelpunkt steht, was für ein Ding das ist: Nat → Nat heißt „eine Rechenvorschrift, die aus einer natürlichen Zahl eine natürliche Zahl macht“. Nat sind in Lean die natürlichen Zahlen mit der Null, also $\mathbb{N}_0$ . Die beiden Zeilen mit | sagen, wie gerechnet wird: Die nullte Dreieckszahl ist 0, und die Dreieckszahl von n + 1 ist die von n plus n + 1. In der Schreibweise der Artikel: $T(0) := 0$ und $T(n+1) := T(n) + (n+1)$ .

example : dreieck 4 = 10 := rfl

Ein Beispiel ohne Namen. Vor := steht die Behauptung, dahinter der Beweis. rfl heißt reflexivity: Beide Seiten sind nach dem Ausrechnen einfach gleich. Lean rechnet $T(4) = 10$ nach.

theorem zwei_dreiecke (n : Nat) :
  2 * dreieck n = n * (n + 1) := by

Ein Satz. theorem kündigt ihn an, dann kommt sein Name. (n : Nat) heißt „Sei n eine natürliche Zahl“. Nach dem Doppelpunkt steht die Behauptung $2 \cdot T(n) = n(n+1)$ , mit * für das Malzeichen. := by leitet den Beweis ein, und zwar als Folge von Befehlen, die Lean nacheinander ausführt.

induction n with
| zero => rfl

induction n sagt: Beweis durch vollständige Induktion über n. Lean verlangt dann zwei Teile. zero ist der Induktionsanfang, n = 0. Da ist $2 \cdot 0 = 0 \cdot 1$ , und rfl genügt.

| succ n ih =>
  rw [dreieck, Nat.mul_add, ih]
  grind

succ ist der Induktionsschritt von n auf n + 1 (successor, Nachfolger). ih ist der Name für die Induktionsannahme, also dafür, dass die Formel für n schon stimmt. rw (rewrite) ersetzt Ausdrücke: zuerst dreieck (n + 1) durch seine Definition, dann wird ausmultipliziert (Nat.mul_add ist das Distributivgesetz $a(b+c) = ab + ac$ ), dann wird die Induktionsannahme eingesetzt. Übrig bleibt $n(n+1) + 2(n+1) = (n+1)(n+2)$ , eine Rechnung mit Klammern, die grind selbstständig erledigt.

Die wichtigsten Wörter und Zeichen in Lean auf einen Blick:

Lean	bedeutet	in Artikeln
`Nat`	natürliche Zahlen mit 0	$\mathbb{N}_0$
`Prop`	eine Aussage, die wahr oder falsch sein kann
`n : Nat`	`n` ist eine natürliche Zahl	$n \in \mathbb{N}_0$
`∀ k, …`	für alle `k` gilt …	$\forall k$
`A → B`	aus A folgt B	$A \Rightarrow B$
`A ↔ B`	A genau dann, wenn B	$A \Leftrightarrow B$
`∧`, `∨`	und, oder	$\land, \lor$
`d ∣ n`	d teilt `n`	$d \mid n$
`Nat.gcd n k`	größter gemeinsamer Teiler	$\gcd(n,k)$
`n / 2`	Teilen mit Abrunden	$\lfloor n/2 \rfloor$
`intro h`	„Angenommen h“ oder „Sei …“
`exact h`	das ist genau h
`omega`	löst Gleichungen und Ungleichungen mit + und Zahlen von selbst
`decide`	rechnet endlich viele Fälle vollständig durch
`·`	Anfang eines Falls in einer Fallunterscheidung

Mehr muss man nicht wissen, um den Gang eines Lean-Beweises zu verfolgen. Wer ihn verändern will, kann ihn über den Link im Kasten im Browser öffnen. Lean meldet dann sofort, ob der Beweis noch stimmt.

Woher die Zeichen kommen

Die meisten Zeichen sind jünger, als man denkt. Plus und Minus erscheinen gedruckt zuerst 1489 bei Johannes Widmann in Leipzig. Das Gleichheitszeichen erfand 1557 der Waliser Robert Recorde, „weil keine zwei Dinge gleicher sein können“ als zwei parallele Striche. Das Summenzeichen Σ führte Leonhard Euler 1755 ein. Das Zeichen ∈ für „ist Element von“ stammt von Giuseppe Peano 1889, das ∃ für „es gibt“ 1897 ebenfalls von ihm, das ∀ für „für alle“ von Gerhard Gentzen 1935. Das schwarze Kästchen ∎ am Ende eines Beweises machte der Mathematiker Paul Halmos in der Mitte des 20. Jahrhunderts üblich. Die Pythagoreer kannten keines dieser Zeichen. Sie schrieben alles in Worten oder legten es mit Steinchen.

Quellen und Literatur

Quellen

Robert Recorde, The Whetstone of Witte, London 1557 (das Gleichheitszeichen)
Leonhard Euler, Institutiones calculi differentialis, St. Petersburg 1755 (das Summenzeichen)
Giuseppe Peano, Arithmetices principia, nova methodo exposita, Turin 1889
Gerhard Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1935 (das Zeichen ∀)
Leonardo de Moura u. a., The Lean Theorem Prover, Automated Deduction, CADE-25, LNCS 9195, Cham 2015