10. World 10: Induction
Statements about natural numbers 0, 1, 2, …, where n + 1 is the number after n. One new rule:
-
Induction (Ind): to prove
∀ n, ?1 n, prove the start?1 0, and the step:?1 (c₁ + 1)from the hypothesis?1 c₁, for an arbitrary numberc₁(an eigenvariable, as in ∀I). In Lean:Nat.rec, or the tacticinduction n.
The levels have no arithmetic: properties like P, Even, Odd are only described by the
assumptions.
Aussagen über natürliche Zahlen 0, 1, 2, …, wobei n + 1 die Zahl nach n ist. Eine neue Regel:
-
Induktion (Ind): Um
∀ n, ?1 nzu beweisen, beweise den Anfang?1 0und den Schritt:?1 (c₁ + 1)aus der Annahme?1 c₁, für eine beliebige Zahlc₁(eine Eigenvariable, wie bei ∀I). In Lean:Nat.rec, oder die Taktikinduction n.
Die Levels enthalten keine Arithmetik: Eigenschaften wie P, Even, Odd sind nur durch die
Annahmen beschrieben.
The induction rule itself: connect the start and the step.
Die Induktionsregel selbst: Verbinde den Anfang und den Schritt.
The same, with the start as a hypothesis.
Dasselbe, mit dem Anfang als Annahme.
Induction for P (n + 1): here the start is P (0 + 1).
Induktion für P (n + 1): Hier ist der Anfang P (0 + 1).
Every number is even (Even) or odd (Odd). In the step, distinguish the two cases of the hypothesis.
Jede Zahl ist gerade (Even) oder ungerade (Odd). Unterscheide im Schritt die beiden Fälle der Annahme.
Two properties at once: prove both together.
Zwei Eigenschaften auf einmal: Beweise beide zusammen.
The final level: the start is a case distinction too.
Das letzte Level: Auch der Anfang ist eine Fallunterscheidung.