Aller au contenu
Topos Uranos
Français

Récurrence sur les entiers et induction sur les formules

Résumé

Les formules de la logique propositionnelle sont en nombre infini, et toute affirmation portant sur toutes exige une méthode qui ne consiste pas à les examiner une par une. Cette leçon la construit en deux étages. Le premier est la récurrence sur les entiers naturels, sous sa forme simple et sous sa forme forte, qui se déduit de la simple ; le second est l’induction sur la complexité des formules, ou induction structurelle, qui se justifie par récurrence forte sur la longueur. Avec elle on démontre le lemme du poids de la langue des cercles et des disques (toute formule pèse +1+1 et tout préfixe par mots propre et non vide pèse au plus 00), et l’on en déduit qu’aucune formule n’est préfixe propre d’une autre et, de là, la lecture unique : chaque formule composée se décompose d’une seule façon en son disque initial et ses deux composantes. La lecture unique légitime enfin les définitions par récurrence sur les formules (longueur, nombre de variables et de disques connecteurs, sous-formules, profondeur) et la substitution d’une sous-formule par une autre.

Objectifs d’apprentissage

  1. Démontrer par récurrence simple et par récurrence forte des propriétés des entiers naturels, en vérifiant l’initialisation et en localisant la faille d’une récurrence incorrecte.
  2. Démontrer que toutes les formules ont une propriété par induction sur leur complexité, en traitant les variables et l’unique règle de formation comme les seuls cas.
  3. Démontrer le lemme du poids et en déduire qu’aucune formule n’est préfixe propre d’une autre et que toute formule composée a la propriété de lecture unique.
  4. Définir des fonctions sur les formules par récurrence (longueur, profondeur, sous-formules, substitution) et démontrer par induction des relations entre elles.

Des affirmations sur toutes les formules

Dans la leçon sur le langage de la logique propositionnelle, on a construit les formules à partir de deux symboles, ∘\sigO et ∙\sigI, que nous appelons cercle et disque, et d’une seule règle de formation. Il y a une infinité de formules, et beaucoup des affirmations qui importent portent sur toutes : que toute formule se termine par un disque, qu’aucune formule ne se lit de deux façons, que dans toute formule il y a une variable de plus que de disques connecteurs. De telles affirmations ne sont pas des formules du langage que nous étudions, mais des énoncés sur lui, formulés dans le métalangage (le français, aidé de la notation mathématique) ; leur démonstration n’est donc pas une déduction à l’intérieur d’un système formel, mais un raisonnement mathématique ordinaire dont l’objet est le système formel. C’est pourquoi on les appelle démonstrations métathéoriques, ou externes.

Or aucune quantité d’exemples vérifiés ne démontre une affirmation sur une infinité d’objets. Il s’ensuit qu’il faut un principe qui permette de conclure, à partir d’un nombre fini de vérifications, qu’une propriété est vraie dans une infinité de cas. Ce principe est la récurrence. On le présente d’abord sur les entiers naturels, où il est plus familier, puis sur les formules, où il prend appui sur le précédent. Le même instrument démontrera, dans l’unité de métathéorie, la correction et la complétude du système déductif.