El principio de que si una relación R en un conjunto es bien fundada (no existen cadenas R-descendentes infinitas) y cada elemento x posee una propiedad siempre que todos los elementos R-menores la tengan, entonces todos los elementos poseen esa propiedad; generaliza la inducción ordinaria en los naturales a órdenes bien fundados arbitrarios.

Principio

Inducción sobre una relación bien fundada: para probar P(x) para todo x basta probar que para un x arbitrario, si P(y) se cumple para todo y con y R x (o y < x), entonces P(x) se cumple. La bien fundación impide la paradoja del contraejemplo mínimo.

Demostración

Para probar la terminación de un sistema de reescritura, se define una medida bien fundada que asigna ordinales o números naturales a los términos y se demuestra que cada reducción disminuye estrictamente la medida; por inducción bien fundada sobre la medida no es posible un descenso infinito y por tanto todas las secuencias de reducción terminan.

Aplicación incorrecta

Aplicar la inducción bien fundada a relaciones que no lo son (por ejemplo los enteros con el orden usual), o asumir que la inducción estructural sobre sintaxis implica automáticamente inducción bien fundada sin verificar la bien fundación de la relación elegida.

Consecuencia

Proporciona un método uniforme para demostrar propiedades y terminación en diversos dominios (ordinales, reescritura de términos, terminación de programas); permite pruebas por contraejemplo mínimo y justifica definiciones recursivas indexadas por medidas bien fundadas.

Inversión

Si la relación no es bien fundada, la inducción puede fallar: pueden existir elementos sin argumento de contraejemplo mínimo y propiedades que se pensaban válidas por argumentos de descenso pueden ser falsas debido a cadenas descendentes infinitas.

Límite

Requiere que la relación sea bien fundada en el dominio en cuestión; no se aplica a órdenes parciales arbitrarios con cadenas descendentes infinitas y no proporciona por sí misma un testigo constructivo a menos que la relación y las hipótesis de inducción sean efectivas.

Tensión semántica

Tensión con la inducción estructural y la inducción matemática ordinaria: la inducción estructural es un caso particular cuando la estructura induce una relación bien fundada, mientras que la inducción bien fundada se aplica más ampliamente pero puede requerir medidas bien fundadas u ordinales no triviales para ser exhibidas.

Síntesis

La inducción bien fundada abstrae el núcleo de la inducción: sustituyendo la relación de predecesor de los naturales por cualquier orden bien fundado, reduce las afirmaciones globales a comprobaciones locales por descenso—si cada elemento se sigue de todos los menores según una relación bien fundada, la propiedad vale universalmente, posibilitando pruebas de terminación y razonamientos por contraejemplo mínimo.