Wohlfundierte Induktion

Die wohlfundierte Induktion ist eine formale mathematische Beweismethodik, welche auch in der Informatik (zum Beispiel in funktionalen Programmiersprachen) Anwendung findet. Das Prinzip lautet: Zeige, dass eine Aussage $\operatorname {A}$ für alle Elemente wahr ist, jeweils unter der Voraussetzung, dass sie für alle „kleineren“ Elemente wahr ist. Als Ordnungsrelation „kleiner“ wird eine wohlfundierte Relation $\prec$ benötigt.

Das Schema der wohlfundierten Induktion ist:

${\frac {\forall y{\Big (}{\big (}\forall z\prec y\ \operatorname {A} (z){\big )}\Rightarrow \operatorname {A} (y){\Big )}}{\forall x\ \operatorname {A} (x)}}$

Im Unterschied zur strukturellen Induktion gibt es keine explizite Induktionsbasis und auch keinen expliziten Induktionsschritt: Die Aussage $\operatorname {A} (y)$ muss für alle $y$ gezeigt werden, jeweils unter der Annahme, dass $\operatorname {A} (z)$ für alle $z\prec y$ gilt. (Letzterer Nachweis ist analog zum gewohnten Vollständigen Induktionsschritt.) Ist die Prämisse $\forall z\prec y\ \operatorname {A} (z)$ leer, was heißt, dass es keine kleineren Elemente als $y$ gibt, dann liegt implizit ein Basisfall vor.

Siehe auch

• Wohlfundierte Relation
• Fundierte Menge#Noethersche Induktion
• Vollständige Induktion