Wohlfundierte Induktion

Kernidee

Die wohlfundierte Induktion ist eine formale mathematische Beweismethode. Sie wird auch in der Informatik verwendet, zum Beispiel in funktionalen Programmiersprachen. Mit ihr beweist man, dass eine Aussage A für alle Elemente gilt.

Das Prinzip lautet: Man zeigt für jedes Element, dass A für dieses Element wahr ist, unter der Voraussetzung, dass A bereits für alle „kleineren“ Elemente wahr ist. Dafür braucht man als Ordnungsrelation „kleiner“ eine wohlfundierte Relation ≺. Eine solche Relation erlaubt Induktionsbeweise, weil man nicht unendlich immer weiter zu kleineren Elementen zurückgehen kann.

Formales Schema

Das Schema der wohlfundierten Induktion lautet:

Aus ∀y(((∀z ≺ y A(z)) ⇒ A(y))) folgt ∀x A(x).

In Worten: Wenn für jedes y gilt, dass aus der Wahrheit von A(z) für alle z ≺ y die Wahrheit von A(y) folgt, dann gilt A(x) für alle x. Die Formel A steht dabei für die zu beweisende Aussage; x, y und z sind Elemente des betrachteten Bereichs; z ≺ y bedeutet, dass z bezüglich der wohlfundierten Relation kleiner als y ist.

Basisfall und Induktionsschritt

Im Unterschied zur strukturellen Induktion gibt es bei der wohlfundierten Induktion keine ausdrücklich getrennte Induktionsbasis und keinen ausdrücklich getrennten Induktionsschritt. Stattdessen muss A(y) für jedes y gezeigt werden, jeweils unter der Annahme, dass A(z) für alle z ≺ y gilt.

Dieser Nachweis entspricht in seiner Rolle dem üblichen vollständigen Induktionsschritt. Ein Basisfall entsteht nur implizit: Wenn die Voraussetzung ∀z ≺ y A(z) leer ist, also wenn es keine kleineren Elemente als y gibt, dann muss A(y) ohne kleinere Vorfälle gezeigt werden. Genau das übernimmt die Funktion eines Basisfalls.