Wohlfundierte Induktion
aus Wikipedia, der freien Enzyklopädie
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 A für alle Elemente wahr ist, jeweils unter der Voraussetzung, dass sie für alle kleineren Elemente wahr ist. Kleiner bedeutet hier, dass zunächst eine wohlfundierte Relation < festgelegt werden muss. Das Schema der wohlfundierten Induktion ist dann:
Im Unterschied zur strukturellen Induktion gibt es keine explizite Induktionsbasis und auch keinen Induktionsschritt: Die Aussage A(y) muss für alle y gezeigt werden, jeweils unter der Annahme, das A(z) für alle z < y gilt. (Um diese Allaussage für verschiedene beteiligte Datentypen nachzuweisen, wird man in der Regel eine Fallunterscheidung über die beteiligten Elemente machen). Ist die Prämisse 
leer, das heißt, gibt es keine kleineren Elemente als y, dann liegt implizit ein Basisfall vor.
