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 <math>\operatorname{A} </math> 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 <math>\prec</math> benötigt.
Das Schema der wohlfundierten Induktion ist:
- <math>\frac{\forall y\Big(\big(\forall z \prec y \ \operatorname{A}(z)\big) \Rightarrow \operatorname{A}(y)\Big)}{\forall x\ \operatorname{A}(x)}</math>
Im Unterschied zur strukturellen Induktion gibt es keine explizite Induktionsbasis und auch keinen expliziten Induktionsschritt: Die Aussage <math>\operatorname{A}(y)</math> muss für alle <math>y</math> gezeigt werden, jeweils unter der Annahme, dass <math>\operatorname{A}(z)</math> für alle <math>z \prec y</math> gilt. (Letzterer Nachweis ist analog zum gewohnten Vollständigen Induktionsschritt.) Ist die Prämisse <math>\forall z \prec y\ \operatorname{A}(z)</math> leer, was heißt, dass es keine kleineren Elemente als <math>y</math> gibt, dann liegt implizit ein Basisfall vor.