Induction

Peut-on démontrer les théorèmes d'incomplétude sans recourir à des raisonnements par induction ? Tous les exposés que je connais font usage de ce procédé, par exemple pour établir des propriétés du formalisme (absoluité des énoncés delta ou sigma, entre autres multiples usages). Lorsqu'on procède ainsi, dans quel "univers" méta  est-on censé se trouver ? Cette induction "intuitive" fait-elle partie de la boite à outils purement "finitaire" que revendiquait le programme de Hilbert ? Merci aux amis pour l'éclairage de lanterne !...

Réponses

  • Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Merci Foys, et cette référence me permet de préciser ma question. Dans le chapitre 1, les auteurs présentent un traitement tout à fait classique de Q. Comme je le disais dans ma question, (et comme tout le monde le fait dans ce type de cours), il se servent d'une induction pour établir des théorèmes relatifs à Q. Ils prennent d'ailleurs le soin de préciser, page 29 : We shall construct the desired proofs by induction. Observe that we shall use no induction within the proofs (since we have no induction in Q). Le mot induction semble clairement désigner ici deux choses différentes !

    Si cette _induction _ (celle de la première phrase) n'est évidemment pas dans Q, où est-elle ? Dans quelle métathéorie (puisqu'il faut bien le dire ainsi) se trouve-t-elle ?

    Il me semble que la hiérarchie "formalisée" de schémas d'induction (I sigma 0, etc.), classiquement exposée dans le ch.5, n'échappe pas non plus à cet usage d'une induction que je me hasarde à qualifier d'intuitive, en tant que raisonnement "basique".

    D'autres points de vue ?

  • @damien09 : je ne suis pas du tout spécialiste de la question, mais tu pourras trouver des informations intéressantes sur les arithmétiques faibles, avec toute une hiérarchie sur les hypothèses d'induction, dans le livre de Benoît Monin et Ludovic Patey : "Calculabilité".

  • Foys
    Modifié (October 2023)
    @damien09 c'est fait au chapitre 5 du livre que j'ai cité; il est possible de définir sans induction le fait qu'un nombre est (ou non) une puissance de 2 et la suite des chiffres en base 2 d'un nombre (non il n'y a pas de cercle vicieux).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Merci à vous deux. Je vais regarder ça de plus près.
  • damien09
    Modifié (October 2023)

    Je me permets de revenir sur ma question. Je ne suis pas certain qu’elle ait été comprise. Je ne demandais pas d’informations sur les hiérarchies de théories arithmétiques avec leurs doses plus ou moins fortes d’induction. Je demandais ce qu’on entend par induction quand on utilise le mot HORS de ces théories, donc quand on fait des raisonnements par récurrence pour étudier des théories formalisées "de l’extérieur". Quel est cet extérieur ?

    J’ai cité un extrait du livre de Petr Hájek, Pavel Pudlák où les auteurs évoquent clairement ce double sens du mot induction, mais sans plus s’avancer en terrain glissant. 

    Martial est plus courageux : dans son grand œuvre (si,si !), au chapitre 4-2.2, je vois un avertissement sur l’induction intuitive. Il y revient au chapitre 16, paragraphes 1.1 et suivants, avec un développement sur la délicate question des modèles de ZFC. Et dans sa "Philosophie de ZFC", le chapitre 8.4 ne masque pas non plus le problème. 

    Je crois comprendre que Martial finit par dire qu’il vit (je le cite) dans un modèle de ZFC. Je le plains car je n’ai pas remarqué qu’il y ait du Pommard ou du vin de Touraine dans un tel modèle, mais au moins, il dispose d’une boite à outils pour étudier les langages formels, les théories de l’arithmétique et leurs limitations (un peu comme Krivine dans son chapitre « Ensemble des formules »).

    Ma question était donc : dans quel "univers" suppose-t-on être quand on fait un raisonnement par récurrence sur, mettons par exemple, la longueur d’une formule, ou un nombre de quantificateurs ?

    Je sais que les questions dites philosophiques suscitent à juste titre de sérieuses réserves chez les mathématiciens, mais sans faire de métaphysique il est cependant nécessaire de savoir de quoi on parle et de quoi on dispose pour en parler, par exemple quand on utilise le mot induction et qu’on éprouve même le besoin de la qualifier d’intuitive pour la distinguer de celles qui relèvent d’une axiomatique formalisée.

    Alors, où vivons-nous quand nous démontrons par exemple les théorèmes de Gödel ? Dans un modèle de ZFC ? Dans PA2 ? Dans un no man’s land ?...

  • Foys
    Modifié (October 2023)
    Il me semble que la hiérarchie "formalisée" de schémas d'induction (I sigma 0, etc.), classiquement exposée dans le ch.5, n'échappe pas non plus à cet usage d'une induction que je me hasarde à qualifier d'intuitive, en tant que raisonnement "basique".

    D'autres points de vue ?

    Non, les exposés en question sont des plans de construction d'un énoncé explicite (qui est de taille énorme dans les présentations habituelles mais court dans ces fragments). Cet énoncé entraîne une contradiction dans la théorie s'il est démontré. On ne suppose pas plus d'induction que celle que la théorie visée propose déjà. En fait l'arithmétique bornée est interprétable dans l'arithmétique de Robinson (les preuves sont à nouveau des plans de construction explicites de formules).

    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Modifié (October 2023)
    Le lien a disparu pendant la nuit, on se demande qui il dérange. Il y a aussi la référence "predicative arithmetic" d'Edward Nelson (pour prendre un ennemi déclaré du schéma d'induction) qui est plus pédagogique mais ne traite pas du théorème de Gödel (mais par contre il faut lire crayon en main au lieu de juste le parcourir en diagonale).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Cette question touche quand même à la raison profonde pour laquelle la logique mathématique est un calvaire intellectuel sans fin. On doit sans cesse faire attention à ce qui relève de la théorie, de la métathéorie, de la métamétathéorie, etc. 

    Selon moi, deux approches sont possibles : 

    • Une approche en deux couches. On étudie un système formel déductif (syntaxique), par exemple PA, Robinson ou tout autre théorie présentée dans le livre de Foys. Et pour pouvoir disserter sur cette théorie et démontrer des "méta-théorèmes" à propos de cette théorie, on utilise un métalangage naïf aussi riche qu'on le souhaite. Ce métalangage contiendra bien sûr le méta-principe d'induction mais aussi pourquoi pas un méta-lemme de Zorn, etc. C'est l'approche utilisée dans les livres de Cori-Lascar. 
    • Une approche fine avec autant de couches qu'on le souhaite. Dans celle-ci on peut étudier une théorie arithmétique formelle comme PA à l'aune d'une métathéorie plus faible et formalisable comme Robinson. Celle-ci à son tour peut être étudiée à partir d'une métamétathéorie formalisable encore plus faible. Ce petit jeu d'emboitement de théories peut alors continuer aussi longtemps qu'on en a envie. La question de l'auteur serait alors la suivante (si je la comprends bien) : est-ce que dans cette hiérarchie de méta-méta-...-méta-théories on peut arriver à un stade où le principe de récurrence a complètement disparu ? De ce que j'en comprends et pour avoir moi-même posé la question à Foys qui m'a également recommandé ce livre, la réponse est non. Ultimement ce principe sera toujours utilisé à un méta-méta-...-méta niveau ne serait-ce que pour raisonner sur le nombre de quantificateurs/connecteurs dans une formule. 
    Cela dit, philosophiquement parlant j'ai fini par accepter l'idée qu'il n'y avait aucune raison de vouloir se priver des récurrences. Après tout, mon ordinateur qui est un objet physique fonctionnant à l'électricité, arrive très bien à accepter les fonctions qui s'appellent elles-mêmes. 

    Ce qui est dur à avaler c'est que, en dernière instance, il y aura toujours une forme de circularité inévitable. On étudiera toujours le principe de récurrence formel avec une récurrence informelle en background. Ceci rejoint des remarques de philosophes comme Hume, Frege (qui était aussi logicien) stipulant que le principe d'induction finissait par s'auto-justifier et que la circularité était ultimement inévitable. Je crois qu'il faut réussir à faire son deuil d'une espèce de fondation absolue des mathématiques "à partir de rien".
  • Je reconnais que Hajek & Pudlak est un monument d'indigence austère et un repoussoir à lire mais si on met les mains dans le cambouis on voit qu'il n'y a pas ces fameuses autoréférences.
    Et puis as-tu regardé "predicative arithmetic" d'Edward Nelson? Ca reste le texte le plus clair sur ces sujets (je pense) même s'il est court et loin d'être exhaustif et malgré ses provocations ("$80^{5000}$ n'existe pas", des choses comme ça mais justement les doutes personnels de l'auteur l'amènent à être très propre dans son exposition).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Foys : Sauf erreur, dans le livre de Nelson, on utilise une récurrence bornée (qui résulte si je ne me trompe pas de la "quasi-surjectivité" du successeur). Cela confirme donc qu'on doit utiliser, a minima de façon très réduite certes, une forme de récurrence. 
    Je conçois d'ailleurs parfaitement que c'est ce genre de récurrence bornée qui apparait en programmation. 
  • Foys
    Modifié (October 2023)
    @cyrano: le texte explique comment interpréter dans Q une théorie ayant un nombre fini d'instances d'induction bornée en plus de Q, c'est fait aux pages 12 à 28 de https://web.math.princeton.edu/~nelson/books/pa.pdf
    L'auteur dit d'ailleurs s'abstenir d'utiliser le procédé plus de quelques fois pour ne pas se retrouver à la place du "caliphe qui avait promis de payer son employé en grains de riz, en doublant le nombre de grains de riz à chaque nouvelle case de l'échiquier".
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Martial
    Modifié (October 2023)
    @damien09 : d'abord, merci de t'intéresser à mon "grand œuvre". Mais je te rassure tout de suite, dans l'univers dans lequel je vis il y a bien du Pommard et du vin de Touraine. Disons que c'est un modèle de ZFC un peu especial. (La marge était trop étroite pour que je puisse en dire plus, snif).
  • Merci à tous pour ces très belles "réponses"... qui n'en sont pas comme le détaille magnifiquement @Cyrano ! Il y a évidemment longtemps que la "fondation" des mathématiques n'est plus l'objectif de tels questionnements, mais ce que notre pratique nous donne à penser sur l'esprit humain est passionnant (et bien sûr auto-référent puisqu'il pense sa pensée, et pense ce qu'il pense de sa pensée...). Sans doute les mathématiques sont-elles le summum de sa capacité de... réflexion. J'ai eu beaucoup de plaisir à vous lire. :)
  • Foys
    Modifié (October 2023)
    je propose à nouveau aux lecteurs de lire les preuves des textes en lien au lieu de les parcourir en diagonale sur la base de préjugés antiformalistes.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Modifié (October 2023)
    La logique mathématique traite (lorsqu'elle aborde ces sujets) grosso modo de deux choses.
    1°) Fonder les mathématiques (donner les règles du jeu, appelées "théories mathématiques", "théories" etc, à partir desquelles on pratique les maths de façon vérifiable).
    2°) Décrire indépendamment les fondements dont il est question au 1°).

    Je reviendrai sur 2°) mais il est tout à fait vrai que 2°) s'exerce lui-même dans le cadre de théories formelles telles que décrites au 1°) (encore que les gens ont tendance à largement à surestimer le nombre de présupposés de telles théories: lorsqu'on voit une induction dans un tel texte, est-ce que l'auteur livre un algorithme de construction de formule ou une méthode de vérification étape par étape que le lecteur pourrait réutiliser au moins dans toutes les situations concrètes abordées dans le livre ou est-ce qu'il s'agit d'autre chose? Il ne faut jamais perdre de vue qu'il y a une différence entre "pouvoir pour tout entier $n$, démontrer $F(n)$" et "démontrer $\forall n F(n)$". Cette différence s'appelle -si l'arithmétique est consistante -le 2ième théorème de Gödel, dans le cas particulier où $F(x)$ est la formule "$x$" n'est pas le numéro d'une démonstration de $0 = 1$. S idans ce cas $\forall n F(n)$ est prouvable, $0=1$ est prouvable par Gödel. Sinon l'arithmétique a au moins une formule non prouvable -cette dernière-, donc elle est consistante et pour tout entier $n$ explicite, on constate $F(n)$). La théorie de la démonstration est elle-même une théorie (qui se sert parmi des instances faibles de Peano parlant de trucs algorithmiques bref $I\Sigma_1$ dans la littérature courante et beaucoup moins dans Hajek&Pudlak). Quelqu'un qui décrit des recettes décrivant des manipulations de formules ne suppose pas plus que quelqu'un qui livre l'algorithme de multiplication posée à des enfants. 


    ############################### 


    Au sujet de 1°). La fondation des maths ne suppose aucune récurrence, pas plus que la construction des ordinateurs n'en suppose.
    la fondation des maths livre des règles dont le respect est vérifiable, c'est tout. Si dans un texte ces règles ne peuvent être vérifiées votre production n'est pas mathématique.

    Si la récurrence devait prééxister aux ordinateurs, ILS N'EXISTERAIENT PAS. Il n'y aurait aucun ordinateur dans le monde (puisqu'avant le premier ordinateur aucun ppareil ne réalisait les mécanismes de récurrence, il a donc bien fallu la construire ex-nihilo). Il existe des ordinateurs physiques réalisant la récurrence dans la mesure de leurs capacités de mémoire et de contraintes de temps fini (je n'ai pas l'impression que le fil discute de la validité de l'attitude courante qui consiste à extrapoler le comportement des machines à des machines de capacité mémoiree arbittrairement grande comme 10^900000 Gigas ou plus) et il existe des logiciels de vérification de preuve comme https://us.metamath.org/ (les gens qui prétendent qu'on ne peut pas faire de récurrence sans récurrence préalable affirment ouvertement que ce site n'existe pas).

    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Cyrano
    Modifié (October 2023)
    Nous ne sommes pas en désaccord Foys, la clé de cette histoire est le caractère borné.
    Tu as raison que dans les faits on ne demande jamais à l'ordinateur de prouver $\forall n F(n).$ Dans les faits, je donne un entier à l'ordinateur, disons $10000$ et il va prouver $F(1),...,F(10000).$ 

    Maintenant dans un livre de logique, on ne va probablement pas vouloir se contenter de ça. Dans tout ce que j'ai pu lire, les auteurs veulent démontrer des méta-théorèmes du type "Pour toute formule $\varphi$ écrite sur le langage $\mathcal{L}$, on a ceci et cela". Or ces méta-théorèmes se démontrent par récurrence sur la longueur de $\varphi.$
  • Foys
    Modifié (October 2023)
    @Cyrano l'arithmétique à quantificateurs bornés est interprétable dans l'arithmétique de Robinson, c'est ce que ces livres démontrent.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Foys : Mais Robinson elle-même permet la quantification bornée non ?
    Donc on interprète une arithmétique à quantification bornée à partir de quantifications bornées et la circularité est quand même bien là.
    Ou alors je ne comprends plus rien mais il faut avouer que c'est compliqué.  :#
Connectez-vous ou Inscrivez-vous pour répondre.