Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Wir hatten letztes Mal bewiesen das sogenannte Critical Paralemma.

Das lautete, wenn alle kritischen Paare eines Systems zusammenführbar sind, dann bekomme ich Weak-Church Russell.

Unser heutiges Ziel ist zu beweisen etwas, das nennt sich Newman's Lemma.

Das haben wir schon mal an der Tafel stehen gehabt, das habe ich nur nicht so genannt.

Das ist vielleicht in der Übung schon erwähnt worden, dass das so heißt.

Wenn ich lokale Konfluenz habe, also Weak-Church Russell, und außerdem noch starke Normalisierung,

dann bekomme ich Church Russell, also Konfluenz schlechthin, insbesondere also Eindeutigkeit von Normalform.

Wenn man da ist, also Newman's Lemma angewendet hat, dann ist man also gewissermaßen bezüglich der Natursandesthermen-Ersetzungssystems im Nirwana.

Da kann jetzt nichts mehr passieren, ich kann das Thermen-Ersetzungssystem laufen lassen.

Ich weiß, es terminiert immer, okay, das stecke ich in dieses Lemma schon rein, das muss ich mir irgendwie anders verschaffen,

indem ich z.B. starke Normalisierung über eine Polynomordnung beweise.

Und egal, wo das dann stehen bleibt, ich erreiche immer die eindeutige Normalform eines Terms

und kann damit insbesondere dann die Gleichheit von Termen in meinem System entscheiden, also Gleichheit im Sinne von Konvertierbarkeit.

So, das hatten wir schonmal angeschrieben, aber wir hatten es nicht bewiesen. Und wir werden es jetzt beweisen.

Um es zu beweisen, brauchen wir eine neue Form von Induktion, die kommt jetzt.

So, das nennt sich wohlfundierte Induktion, das daran liegt, dass sie an dem Vorhandensein einer wohlfundierten Relation hängt.

Und das ist praktisch die Mutter aller Induktionsprinzipien. Wir werden auch am Beispiel sehen,

also jedes uns bekannte Induktionsprinzip wird man herleiten können als eine Instanz von wohlfundierter Induktion.

So, und das wollen wir formulieren als Satz.

So, wie angekündigt, wir brauchen eine wohlfundierte Relation auf unserer Grundmenge, über die wir wohlfundierte Induktion betreiben können.

So, jedes Induktionsprinzip ist von der Form, wenn ich einen Induktionsschritt durchdrücken kann, dann bekomme ich universelle Gültigkeit einer bestimmten Aussage.

So, das heißt, der Satz hat der Form, wenn, dann, wenn Induktionsschritt, dann universelle Gültigkeit der Induktionsbehauptung.

So, for later reference nenne ich den Induktionsschritt, den man durchführen muss, mal Stern.

Also, wie immer muss ich mir hernehmen ein beliebiges Element des Grundbereichs, so wie ich mir in normaler Induktion eine natürliche Zahl n hernehme.

So, und ich muss dann, ich kann dann etwas annehmen, und zwar, dass für alle Nachfolger von x in dieser Relation, also für alle y, sodass x, r, y gilt, dass für alle diese y bereits irgendeine Eigenschaft gilt.

So, ich denke mir diese Relation r als komplizierter als, mit anderen Worten diese y, die sind einfacher als x.

Also, ich nehme hier an, dass alle einfacheren y als x p schon erfüllt.

Das ist die Induktionsvoraussetzung in diesem Schritt.

Unter dieser Induktionsvoraussetzung muss ich zeigen, dass x selbst die Eigenschaft erfüllt, also das tun, was ich immer machen muss.

Also, ich nehme an, die Induktionsbehauptung gilt für alle einfacheren Dinge schon, und ich zeige dann, sie gilt für mein Ding, das ich gerade in der Hand habe.

So, das hier nennt man den Induktionsschritt.

So, und dann kommt, wie immer, das, was ich davon habe, dass ich mühsam den Induktionsschritt durchgeführt habe, nämlich universelle Gültigkeit meiner Induktionsbehauptung.

Also, es gilt für alle x aus dem Grundbereich p von x, und das nenne ich für Zwecke des Beweises mal Doppelstern.

So, das hier ist das Prinzip der wohlfundierten Induktion.

So, der Beweis ist unter anderem deswegen, weil wohlfundiertheit einer Relation so merkwürdig von hinten durch die Brust ins Auge über eine negative Aussage definiert ist, am bequemsten tatsächlich mal über Widerspruch zu führen. Machen wir also.

Also, unsere Annahme ist Doppelstern gilt nicht. So, was heißt das? Es gibt also ein Element des Grundbereichs, das die Induktionsbehauptung nicht erfüllt.

Das heißt also, es existiert ein x0 aus groß x, das p nicht erfüllt.

So, es gilt aber Stern, der Induktionsschritt. Also, im Induktionsschritt steht, wenn alle einfacheren y die Induktionsbehauptung erfüllen, dann auch x selbst.

x erfüllt die Induktionsbehauptung, oder x0 erfüllt die Induktionsbehauptung, aber nicht. Also erfüllen nicht alle einfacheren y die Induktionsbehauptung.

Anders gesagt, es gibt ein einfaches y, das die Induktionsbehauptung nicht erfüllt.

Also, wegen Stern, weil wir den Induktionsschritt ja schon durchgeführt haben. Existiert ein einfaches y, also, das will ich nicht y nennen, das will ich x1 nennen.

Mit x0 r x1, also ein einfaches x1, das die Induktionsbehauptung auch schon nicht erfüllt. Also, es gilt nicht p x1.

Aha, ich bin also in derselben Situation wie vorher für x0, nur jetzt für ein einfaches x1. Das Spiel kann ich natürlich weitertreiben.

Ich sage also, das treibe ich jetzt als Infinitum weiter. Ich konstruiere mir immer neue Elemente, die halt einfacher sind als vorher und eben die Induktionsbehauptung p nicht erfüllt.

Ich bekomme also so eine Kette von immer einfacheren Dingen, die alle meine Induktionsbehauptung nicht erfüllen.

Kann aber nicht sein, weil r ja wohlfundiert war.

R ja wohlfundiert heißt ja gerade, dass es keine solche unendliche R-Kette gibt.

Fertig.

So, das war schnell bewiesen. Wenn ich vorhin gesagt habe, das sei die Mutter aller Induktionsprinzipien, ist das natürlich ein bisschen geschummelt.