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 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:

$\frac{(\forall y)((\forall z < y) A(z)) \Rightarrow A(y)}{(\forall x) A(x)}$

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 $(\forall y)(\forall z < y) A(z))$ leer, das heißt, gibt es keine kleineren Elemente als y, dann liegt implizit ein Basisfall vor.