Langage du premier ordre : de la complétude à l'incomplétude

f_g
f_g
Modifié (May 2023) dans Fondements et Logique
Bonjour à tous
C'est mon premier post ici et je vous détaille rapidement mes intentions. Je ne suis pas mathématicien, mais disons un "praticien des mathématiques" (ingénieur, thèse en simu pour la mécaflu Lattice Boltzmann etc...). Depuis quelques mois je me passionne pour la logique ainsi que pour la fameuse "querelle des fondements", que je souhaiterais arriver à "vulgariser" de façon assez littéraire (donc forcément un peu floue) mais surtout, surtout sans faire de véritable erreur (j'ai donc besoin de beaucoup lire, y compris des livres techniques, pour dire le moins de c@!##* possibles).
Il y a une partie de ce sujet qui me paraît essentielle et que je ne suis pas sûr du tout d'avoir comprise, et que je trouve très peu explicitée (du moins comme je l'attendrais) : la question de l'émergence de l'incomplétude (par exemple de Peano) à partir d'un langage du premier ordre qui, lui, est complet (complétude de Gödel). Je voulais vous partager la manière dont j'interprète cette question et savoir si je délire ou non.
Mettons que je prenne pour base la logique des prédicats du premier ordre, et que je me place en calcul des séquents LK. A ce que j'ai compris, ce système est complet, correct et cohérent (sur les relations correct/cohérent, cf. ma question***) (d'ailleurs je vois peu souvent cette complétude là reliée avec celle du théorème de complétude de Gödel, mais on est bien d'accord que c'est directement lié?).
Sachant tout cela, et sachant aussi le fait que le seul axiome logique à proprement parler de ce système est $A \vdash A$ (j'ai vu qu'il y avait une variante additive pour la règle d'axiome où il y a des contextes, mais je suppose que ça ne change pas fondamentalement les choses?), alors est-ce qu'il est correct de dire que pour une théorie formée sur la base de ce langage avec ces règles d'inférence LK (système logique?), la survenue de l'incomplétude provient simplement du fait que l'on restreint drastiquement les possibilités pour les fameuses formules $A$ écrites plus haut, par le biais du choix des axiomes de ladite théorie? (ou plutôt de la manière dont cette restriction est faite, puisqu'il est connu que des axiomes encore plus restreints que ceux de Peano forment des théories complètes?). J'ai le sentiment que le rapport avec la choucroute existe mais que ça n'est pas vraiment ça. Je trouve aussi que le "simple" fait que retirer la multiplication à l'arithmétique de Peano pour obtenir une théorie complète est assez fascinant et perturbant quant à ce "seuil" entre complétude et incomplétude à partir d'une même logique sous-jacente..
***Je trouve que le paragraphe "cohérence et complétude" de Wikipédia m'embrouille, est-ce normal? (peut être est-ce parce que je ne comprends pas) https://fr.wikipedia.org/wiki/Correction_(logique)
Si je prends par exemple le calcul des séquents LK, le fait qu'il soit correct n'implique-t-il pas immédiatement qu'il est cohérent puisqu'en LK le séquent absurde n'est pas prouvable? Est-il faux de dire que pour un système logique comme LK (et comme d'autres), cohérence et correction sont une seule et même notion? Est-ce une pure question de mots, comme parfois sont amalgamés indépendant et indécidable (je ne parle pas de l'indécidabilité algorithmique).
Je suis preneur de toute référence intéressante ou pagination particulière qui pourrait m'aider (j'ai à dispo et déjà parcouru Cori-Lascar, le livre de Nour (j'ai du mal), de Van Dalen, celui de Dehornoy, le très bon cours de Sylvain Schmitz, celui d'Olivier Laurent, les textes de Girard, et le livre du forumeur Martial mais que je n'ai pas encore eu le temps de regarder). De manière générale, je ne sais pas pourquoi mais j'ai vraiment du mal avec les présentations techniques sur la théorie des modèles (sauf le Schmitz)
Merci à vous !

Réponses

  • Alain24
    Modifié (May 2023)
    Dans mes souvenirs : en logique du premier ordre toute théorie consistante (non contradictoire) est incomplète, on peut alors sans contradiction ajouter au système d'axiomes un indécidable ou son contraire.
    Le terme correct, qui fait plus ou moins allusion à politiquement correct  n'est pas utilisé, car on ne demande pas en logique formelle aux axiomes de se conformer à une réalité matérielle  ou même historique car la logique formelle n'est pas du domaine de la morale ou de l'éthique. Ce qui suit est un exemple de système consistant.
    Ainsi dans le système axiomatique : "tous les animaux qui ont des ailes volent, les manchots ont des ailes, les manchots sont des animaux, les chauve-souris sont des animaux". L'affirmation
    "les manchots volent" est un théorème et l'affirmation "les chauves souris volent" est indécidable car   il manque l' axiome "les chauve-souris ont des ailes", on peut donc sans contradiction rajouter pour troisième axiome son contraire qui est : "il y a des chauve-souris sans aile" et qui n'est pas "aucune chauve-souris n'a d'aile".
    Et si on affirme  qu'on peut sans contradiction rajouter l'axiome "aucune chauve souris n'a d'aile" ou son contraire "Toutes les chauve souris ont des ailes" alors on est un sophiste et on rentre dans le domaine de la rhétorique très utilisée par les avocats et les politiques en campagne électorale.
  • Médiat_Suprème
    Modifié (May 2023)
    Alain24 a dit :
    Dans mes souvenirs : en logique du premier ordre toute théorie consistante (non contradictoire) est incomplète,
    Complètement faux, la théorie des ordres totaux, denses, sans extrémums est complète, elle est même $\aleph_0$-catégorique, et l'arithmétique de Robinson,Presburger cité dans le message de f_g est aussi complète (alors qu'il pourrait sembler, à première vue, que le coupable serait plutôt le schéma de récurrence).
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Alain24
    Modifié (May 2023)
    Médiat_Suprème
    Quelqu'un peut-il mettre en lien un article public qui contient  les preuves des affirmation de @Médiat Suprème ?
    [Inutile de reproduire le message précédent. AD]
  • Foys
    Modifié (May 2023)
    Médiat_Suprème
    L'arithmétique de Robinson est incomplète (le premier théorème de Gödel y est démontrable; voir par exemple ce livre au chapitre 2: https://projecteuclid.org/eBooks/perspectives-in-logic/Metamathematics-of-First-Order-Arithmetic/toc/pl/1235421926).
    @f_g voulait parler plutôt de l'arithmétique de Presburger je pense.
    Pour un exemple concret d'énoncé dont la validité varie suivant les modèles d'arithmétique de Robinson, il y a $\forall n \exists p, \ 2p = n (n+1)$ qui est prouvable dans PA (par récurrence) mais faux dans l'ensemble des polynômes de $\Z[X]$ nuls ou de coefficient dominant strictement positif (prendre $n:=X$; tous les axiomes de Peano à part le schéma de récurrence sont satisfaits dans cette structure avec les opérations usuelles).
    [Inutile de recopier l’avant dernier message. AD]
    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$.
  • Médiat_Suprème
    Modifié (May 2023)
    Oui, bien sûr, d'ailleurs mon commentaire sur le coupable de l'incomplétude va dans ce sens, puisque même sans schéma de récurrence, Robinson est essentiellement incomplète.
    Si j'ai bonne mémoire (c'est pas gagné), la commutativité de l'addition est indécidable dans Robinson.
    J'avais écrit, il y a longtemps, un petit document sur le sujet.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Foys a dit :
    f_g voulait parler plutôt de l'arithmétique de Presburger je pense.
    Tout à fait !
  • Médiat_Suprème
    Modifié (May 2023)
    J'ai retrouvé :smile:
    Soit la structure $\mathbb{M} = (\{0\} \times \mathbb{N}) \, \bigcup \, (\mathbb{Q}^{*+} \times \, \mathbb{Z})$, on définit sur $\mathbb{M}$ une $\mathcal{L}(0, s, +, \cdot)$-structure (c'est-à-dire qu'il faut interpréter 0, $s$, + et $\cdot$ dans cette structure) :
    $0_\mathcal{L} $     est interprété par  $(0, 0) $
    $s_\mathcal{L}$     est interprété par  $s_\mathbb{M}(\alpha, n) = (\alpha, n + 1)$ 
    $+_\mathcal{L}$      est interprété par  $(\alpha, n) +_\mathbb{M} (\beta, m) = (\alpha, n + m)$  
    $\cdot_\mathcal{L}$  est interprété par  $(\alpha, n) \cdot_\mathbb{M} (\beta, m) = (\alpha + \beta, n.m)$ si $(\beta, m) \neq (0, 0)$
                                             $(\alpha, n) \cdot_\mathbb{M} (0, 0) = (0, 0) $  
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Dans le message d'Alain24, il faut corriger en "en logique du premier ordre toute théorie récursivement énumérable consistante capable de formaliser l'arithmétique est incomplète", c'est le premier théorème d'incomplétude de Gödel comme tu le sais certainement.
  • Alain24
    Modifié (May 2023)
     Médiat_Suprème,
    je ne vois rien sur l'arithmétique de Robinson dans le lien. En français  l'usage est que si une opération, au sens de la théorie des ensembles s'appelle addition alors on sous-entend qu'elle est commutative.
    [Inutile de recopier l’avant dernier message. AD]
  • Alors, il va falloir prévenir Robinson qu'il ne sait pas ce qu'il fait.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Alain24
    Modifié (May 2023)
    Médiat_Suprème
    Sauf si Robinson ne publie pas en français !
    [Inutile de reproduire le message précédent. AD]
  • Inutile aussi de polluer un fil.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Heuristique
    Modifié (May 2023)
    Pour revenir au sujet de @f_g et sous le contrôle de bon nombre de gens de ce forum qui sont plus au point que moi en logique.
    Un système est correct ssi toute formule prouvable est valide. Un système est cohérent ssi on ne peut pas démontrer "Faux" dedans. On en déduit donc correct $\Rightarrow$ cohérent. La réciproque s'obtient, de mémoire, pour les systèmes complets. Pour la quasi-totalité des systèmes de preuves logiques, la cohérence et la correction sont un peu la moindre des choses (sinon cela signifie que tu prouves des trucs faux...).
    Attention aux mot complet/incomplet qui désignent beaucoup de choses en maths.
    Un système de preuve est complet ssi toute formule valide est prouvable. Par exemple, le système $LK_1$ est complet (et correct) donc c'est un "bon" système de preuve car une propriété est vraie ssi elle est prouvable (les deux sens correspondent à correct et complet).
    Une théorie est complète ssi pour toute proposition $\phi$, $\phi$ est valide ou $\neg \phi$ est valide. Dire que l'arithmétique de Peano est incomplète signifie donc qu'il existe des formules $\phi$ qui ne sont pas prouvables et dont la négation ne l'est pas non plus, bref il existe des propriétés indécidables (attention à ce terme qui a aussi 2 sens très différents selon le contexte...).
    Les différentes variantes de $LK$ que tu as pu rencontrer sont en général équivalentes, sauf si l'auteur s'est planté.
  • f_g
    f_g
    Modifié (May 2023)
    Alain24 a dit :
    Ainsi dans le système axiomatique : "tous les animaux qui ont des ailes volent, les manchots ont des ailes, les manchots sont des animaux, les chauve-souris sont des animaux".

    En fait, j'ai trouvé ce petit exemple très intéressant^^ En le formalisant style prédicats du premier ordre il y a de quoi expliquer des choses très simples mais très pertinentes (indécidabilité, cohérence, modèle ...).

    Heuristique a dit :
    On en déduit donc correct $\Rightarrow$ cohérent. La réciproque s'obtient, de mémoire, pour les systèmes complets.  

    Oui donc effectivement, cela me confirme que pour un système à la LK, cohérent est tout simplement équivalent à correct, merci !

    J'ai réfléchi à partir de l'axio-zoologique d'Alain et ma question de base s'éclaire sous un jour nouveau. Imaginons que l'on parte d'un système générique à trois axiomes, $A \vdash A$, $B \vdash B$, $C \vdash C$. Une manière de concevoir l'émergence d'une contradiction ou d'une indécidabilité dans LK pour une telle axiomatique (sachant LK pourtant cohérent et complet), est d'utiliser la propriété de la sous-formule. Pour la contradiction : il existe dans l'un des (infinis) théorèmes de LK que l'on peut former à partir de ces trois axiomes une sous-formule de la conclusion qui fait apparaître une contradiction entre les sous-formules de $A$, $B$ et $C$. Pour l'indécidabilité d'une formule $D$ donnée : aucun des infinis théorèmes de LK formés à partir de ces trois axiomes, une fois "déplié" à partir des sous-formules de $A$, de $B$ et de $C$, ne fait apparaître la formule $D$ ou la formule $\neg D$.
    Ça n'intéressera peut-être personne mais ça m'aide de l'écrire :DMerci.

  • f_g
    f_g
    Modifié (May 2023)
    Re-bonjour
    Au cas où des gens retomberaient sur cette discussion, j'ai fait pas mal de progrès sur la compréhension du problème, notamment grâce à deux papiers lumineux de G. Longo, qui traite quasi exactement des questions de ce fil, en rentrant aussi dans la technique. Voici les liens :
    On peut aussi ajouter ses contributions au livre "Mathematics And The Natural Sciences: The Physical Singularity Of Life" (en particulier le chapitre 2, qui reprennent de façon moins techniques quelques thèmes des deux articles en question).

    Deux principales choses à souligner qui concernent ce fil de discussion :
    • Longo discute du problème du "bon ordre" des entiers, et de sa rétivité à la pure formalisation. Il prend des exemples concrets de démonstrations de théorèmes (notamment la Forme Finie de Friedman du théorème de Kruskal) où l'indécidabilité dans PA surgit si l'on ne s'autorise pas un jugement de bon ordre, non formalisable (au sens d'un codage formel).
      Il interprète l'incomplétude mathématique des formalismes comme le fossé entre les "principes de preuve" (formels) et les "principes de construction" (qui se basent fondamentalement sur des "jugements", en particulier les "jugements géométriques", fortement enchaînés à des représentations de l'espace ou du temps)
    • Le second point est une extrapolation personnelle mais que je pense valide, par rapport à la complétude d'un système comme l'arithmétique de Presburger. Il y a bien dans ce système un schéma d'axiome de récurrence et pourtant il est complet. Que se passe-t-il?
      J'ai compris grâce aux papiers de Longo qu'apparaît dans la démonstration du théorème de Kruskal-Friedman une fonction qui croît si vite qu'elle « majore définitivement toute fonction récursive qu’on démontre totale dans AP (et aussi dans ses extensions fortes) ». Pour ce qui est de la vitesse maximale de croissance des fonctions prouvablement totales et Turing-calculables, cela fait référence à la hiérarchie de Wainer et à certains théorèmes qui sont rappelés ici https://fr.wikipedia.org/wiki/Hi%C3%A9rarchie_de_croissance_rapide . Il se produit donc le même genre de phénomène qui produit l'indécidabilité dans PA du théorème de Goodstein.
      Donc, si j'extrapole intuitivement, le fait que Presburger puisse être complète est lié à l'impossibilité de dépasser l'ordinal de preuve de PA ($\epsilon_0$) du fait de l'absence de la multiplication, qui limite la croissance des fonctions. C'était intuitable, mais là l'intuition me paraît solidement confirmée. Il n'est pas nécessaire de faire une récurrence au delà de $\epsilon_0$, donc on évite l'incomplétude à cet endroit.
    N'hésitez pas si vous avez des commentaires.
    À bientôt !
  • Merci pour ces liens !  de  quoi méditer ......
Connectez-vous ou Inscrivez-vous pour répondre.