Études-Mathématique/Règle d'induction

From Lazi wiki
Jump to: navigation, search

Question

Comment exprimer la règle d'induction ?

Étude

Forme actuelle de déduction

Une déduction a pour objet : les formules en conditions, la formule déduite.

Principe de l'induction

Le principe de base est d'enchaîner une suite de déduction, l'enchaînement étant paramétré par une chose ressemblant à une liste dite "index".

Liste index

On a deux options: l'index est une représentation ou non.

Habituellement on utiliser un index qui est une représentation. Si on utilisait une liste directe, cela interdirait d'utiliser cette déduction dans une hypothèse puisque alors on ne pourrait pas utiliser la représentation de liste pour avoir une liste directe.

Donc il faut utiliser une représentation de liste.

La règle

Variables

l,p,q

Conditions

  • p(0l)
  • pour tout x de l on a q x
  • d est une déduction utilisant les variables globales "p,m,q,x" qui a pour condition "isList m", "p m" et "q x" et pour conclusion "p (m +le x)"

Conclusion

p l

La règle, sans q

À partir de la règle où l'on en lève la condition q, on peut déduire celle avec q: on remplace p y par "(si pour tout x de y, q x) alors p y"

Réponse

Voir l'étude.