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 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 benötigt.

Das Schema der wohlfundierten Induktion ist:

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

Siehe auch