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 ${\displaystyle \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 ${\displaystyle \prec }$ benötigt.

Das Schema d​er wohlfundierten Induktion ist:

${\displaystyle {\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 ${\displaystyle \operatorname {A} (y)}$ muss für alle ${\displaystyle y}$ gezeigt werden, jeweils unter der Annahme, dass ${\displaystyle \operatorname {A} (z)}$ für alle ${\displaystyle z\prec y}$ gilt. (Letzterer Nachweis ist analog zum gewohnten Vollständigen Induktionsschritt.) Ist die Prämisse ${\displaystyle \forall z\prec y\ \operatorname {A} (z)}$ leer, was heißt, dass es keine kleineren Elemente als ${\displaystyle y}$ gibt, dann liegt implizit ein Basisfall vor.

Siehe auch

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