Le principe selon lequel, pour une relation R bien fondée (il n’existe pas de chaînes R-descendantes infinies) sur un ensemble, si chaque élément x possède la propriété à la condition que tous les éléments R-inférieurs le possèdent, alors tous les éléments ont cette propriété ; il généralise l’induction usuelle sur les naturels à des ordres bien fondés arbitraires.

Principe

Induction sur une relation bien fondée : pour prouver P(x) pour tout x, il suffit de démontrer que pour un x arbitraire, si P(y) vaut pour tout y tels que y R x (ou y < x), alors P(x) vaut. La bien-fondation évite les paradoxes du contre-exemple minimal.

Démonstration

Pour prouver la terminaison d’un système de réécriture, on peut définir une mesure bien fondée attribuant des ordinaux ou des naturels aux termes et montrer que chaque réduction diminue strictement la mesure ; par induction bien fondée sur la mesure, aucune descente infinie n’est possible et toutes les suites de réduction terminent.

Mauvaise application

Appliquer l’induction bien fondée à des relations qui ne le sont pas (par exemple les entiers relatifs avec l’ordre usuel), ou supposer que l’induction structurelle sur une syntaxe implique automatiquement l’induction bien fondée sans vérifier la bien-fondation de la relation choisie.

Conséquence

Fournit une méthode uniforme pour démontrer des propriétés et la terminaison dans divers domaines (ordinaux, réécriture de termes, terminaison de programmes) ; elle autorise les preuves par contre-exemple minimal et justifie des définitions récursives indexées par des mesures bien fondées.

Inversion

Si la relation n’est pas bien fondée, l’induction peut échouer : il peut exister des éléments sans argument de contre-exemple minimal, et des propriétés supposées tenir par descente peuvent être fausses en raison de chaînes descendantes infinies.

Limite

Exige que la relation soit bien fondée sur le domaine considéré ; elle ne s’applique pas aux ordres partiels arbitraires comportant des suites descendantes infinies et ne fournit pas en elle-même de témoin constructif sauf si la relation et les hypothèses d’induction sont effectives.

Tension sémantique

Tension avec l’induction structurelle et l’induction ordinaire : l’induction structurelle est un cas particulier lorsque la structure induit une relation bien fondée, tandis que l’induction bien fondée s’applique plus largement mais peut nécessiter l’exhibition de mesures bien fondeés ou d’ordinaux non triviaux.

Synthèse

L’induction bien fondée abstrait l’essentiel de l’induction : en remplaçant la relation prédécesseur sur les naturels par un ordre bien fondé quelconque, elle réduit des assertions globales à des vérifications locales par descente — si chaque élément découle de tous les plus petits selon une relation bien fondée, la propriété tient globalement, permettant preuves de terminaison et raisonnements par contre-exemple minimal.