La Complétude

Bon, tout se mélange. Aussi il nous faut parler de la complétude, aussi affirmée par Gödel. Le brigand semble se contredire, mais il ne parlait pas de la même chose. 

D'abord c'est la THESE de Gödel de 1929(il commençait bien).  

Mais d'abord, on définit la "cohérence" comme la "consistance" (ce sont une et une seule chose) comme la capacité d'un système de ne pas produire de contradictions. Encore faut il être capable de produire quelque chose, c'est à dire être un système... On dit aussi qu'il est "non contradictoire", ce qui est logique finalement.

Un point intéressant: une théorie est cohérente si elle a des énoncés non démontrables... Par exemple, la contradiction, doit pouvoir être exprimée dans la théorie, mais il vaut mieux qu'elle ne soit pas démontrable. Il doit y avoir du faux dans une théorie, sinon elle est "triviale" et donc n'a aucun intérêt. 

On en vient alors à la différence syntaxe/sémantique c'est à dire à la notion de "modèle". Un modèle est une structure descriptible -par ailleurs- qui vérifie les axiomes de la théorie. Une interprétation, quoi. Le mot "sémantique", sensé donner du sens, caractérise ainsi ce qui est "commun" à des objets différents et qui va au delà du simple respect potentiel de certaines règles: en plus c'est possible, car CA existe... Du moins dans une acception "réaliste" du mot "sens".

On dit qu'il y a cohérence "au sens sémantique" si il y a un modèle pour la théorie. 

La "logique du premier ordre", décrite par Frege, est le "calcul des prédicats" avec les quantificateurs. Elle permet de décrire l'arithmétique, par exemple. Elle inclut la logique des propositions, bien plus simple.

Le théorème de complétude, le truc de Gödel, dit que SI un théorème est vrai dans TOUS les modèles, alors, on peut le démontrer en appliquant les règles du système. Vrai implique démontrable. Il le prouve pour la logique du premier ordre. Au passage, la réciproque, qui caractérise ce qu'on appelle la "correction" est vraie aussi.

Arithmétiques

A ce stade, on doit réaliser ce qu'est la logique du premier ordre. On a du ou, du et, du non, A, E (les quantificateurs) et des variables en nombre indéfini.

On y peut définir l'arithmétique en choisissant des symboles primitifs et des règles de succession. L'arithmétique, c'est celle de Peano, définit l'addition mais aussi la multiplication. Elle est du "premier" ordre, car elle exclut les quantifications sur les ENSEMBLES de nombres.

Il y a aussi l'arithmétique de Robinson (Raphael, pas Julie), moins puissante que Peano, car "finiment" axiomatisable, mais suffisamment pour être incomplète gödéliennement. Elle a la multiplication, définie pourtant en fonction de l'addition, de manière évidente, quoique récursivement:  x*0 = 0 et  x * s(y) = x*y + y.

Ainsi donc, c'est ce schéma récursif là, (celui de la multiplication) qui "porte" la capacité à faire le monstre (le monstre de Gödel). Et rien d'autre. 

Au passage, l'arithmétique sans multiplication, celle de Presburger (quel nom, il a pour prénom Mojżesz ) est super simple, "complète" et "décidable". Il faudrait en reparler. 

Pour en revenir à Péano, il a -en plus- une infinité d'axiomes qui sont toutes les formes possibles du raisonnement par récurrence, énumérées bestialement car il est impossible (si on veut rester au premier ordre) d'abstraire sur toutes les formules... Péano est ainsi "infiniment" axiomatisé. 

Par contre, toutes ces arithmétiques sont compatibles avec la complétude Gödelienne: il y a bien une démonstration pour tout énoncé vrai dans tous les modèles, PARCEQUE elles sont du premier ordre.

La complétude est donc celle du système de déduction appliqué au système, ou plus exactement celle du système axiomatisé à qui l'on applique la déduction "naturelle", c'est à dire LE raisonnement tout court. Il faut bien comprendre ce qu'est ce fameux "raisonnement": il n'a pas lui, d'"axiomes" à proprement parler, sinon la seule déduction possible à partir de rien, que l'on appelle "axiome", d'ailleurs (héhé).

__________ ax

    X,A |- A

Les autres règles, reformulations du raisonnement dit "axiomatique", ne sont que des ré-expressions commodes de ce qu'on appelle la déduction dite "naturelle". Tout ça fut réglé par GG (Gentzen), voir mon exposé sur Girard 

http://francoiscarmignola.hautetfort.com/archive/2015/09/12/girard-jean-yves-5684115.html

 Cette histoire DU "raisonnement" est ce qui obsède Girard... Il faut bien voir que cette idée de la formalisation de ce qui est l'apanage du mathématicien ne va pas de soi. Comment? On voudrait uberiser la forfanterie absconse du "le lecteur démontrera le reste à titre d'exercice", du "tout le reste est évident", "je vous laisse démontrer le reste, c'est du niveau CM2" ? C'est Hilbert qui lança la mode, et les "principia mathematica" qui fournirent la première version d'une notation "complète" formalisée de tous les raisonnements possibles.

Une "logique" (il y en a plusieurs) est ainsi une forme de ce fameux raisonnement. Allez on crache le morceau, chacune de ces logiques est donnée par des conventions (les symboles variés) et surtout des règles de raisonnement (exprimables avec des séquents et la fichue barre horizontale). On a L K (la logique klassike), L J (la logique intuitionniste) et L L (la logique linéaire). 

C'est Kant, qui en 1787, affirma à propos de la logique d'Aristote que selon tout apparence, elle était close et achevée. De fait c'est bien sa formalisation qui ouvrit la voie à sa digitalisation et à son encodage...

Toutes ces logiques, d'ailleurs en gros équivalentes, se définissent avec leurs règles spécifiques, exprimées par des déductions (la fameuse barre horizontale) reliant des séquents d'entrée à des séquents de sorties. Une démonstration dans la logique en question est une suite d'application de ces règles, de fait un arbre dont la racine, loin en bas est ce qu'on est arrivé à démontrer... 

Les séquents

Un point au sujet des séquents, qui restent LA manière d'exprimer des raisonnements généraux, bien que les graphes de Girard (il faudra en reparler) seraient (paraît-il) bien tentants.

Ils ont eux mêmes une partie droite et une partie gauche, séparées par "|-" le "donc" du raisonnement élémentaire, en fait la classique implication, qui se contente de séparer une suite de "et" et une suite de "ou". 

De fait l'assertion élémentaire, le séquent est capable d'exprimer n'importe quoi... Depuis le faux : ( A |- ), et le vrai: (|- A) en passant par tout le reste.

Les séquents sont utilisés pour exprimer une règle particulière, la règle de coupure (cut). Gentzer a démontré lui même, ce fut sa "hauptsatz" qu'elle est redondante, et qu'on peut exprimer tout raisonnement sans elle. Les coupures peuvent toujours être éliminées. Voyons voir le séquent des coupures: 

X |- A, Y       X,A |- Z

__________________ cut

         X |- Z 

A est "coupé" (éliminé). La seule règle qui élimine une hypothèse, c'est celle là. Elle est donc, en principe, une menace: si on arrive à prouver le séquent vide |-, on serait foutu. Or, il se trouve que la contradiction mène au séquent vide. En effet: 

La règle de négation (à droite) bien connue, donne: 

|-  nA

_______

nnA |-

Et on combinant, avec la règle de coupure, on a donc au total:

|- nnA         |- nA

               ________

                 nnA|- 

_______________

       |-

C'est à dire, précisément que (nnA et nA), expression de toutes les contradictions, mène au séquent vide.  Par contraposée, s'il n'y a pas de séquent vide, il n'y aura pas de contradiction. COMME il n'est pas possible de générer de séquent vide, la logique n'est pas contradictoire.

Rassurant,non ? Et bien il a fallut un nazi pour nous le prouver. 

 

Les différents systèmes 

Pour clarifier tout ça, il nous faut préciser que la "déduction" (la grande barre horizontale) a eu plusieurs acceptions: 

1) La déduction (ou système) Hilbertien avec une seule règle, le modus ponens

2) la déduction "naturelle" qui introduit les connecteurs un à un.

3) le calcul des séquents, décrit plus haut.

 Voir (2) et aussi (3). 

Les modèles

Naturellement, l'expression "vraie dans TOUS les modèles" a un caractère intriguant: qu'est ce que cette vérité là? De fait, il s'agit de la vérité "combinatoire", celle qui, pour le calcul des propositions, s'exprime avec les tables de vérité. On a donc les distinctions entre toujours faux, parfois faux, (et donc parfois vrai), et toujours vrai (valide).

Au passage, c'est semble-t-il Wittgenstein lui même qui inventa les fameuses tables... 

Le mot valide est un peu faible, le "toujours vrai" ou "absolument vrai" est qualifié de "universellement valide". Alors que l'invalide lui est plus simplement "absolument faux".

En gros une proposition porte sur des variables, et un modèle, forcément dénombrable, est une liste de variables, la validité d'une proposition étant vérifiée par la constatation qu'elle est déclarée vraie dans TOUS les modèles... Pour qu'une telle absurdité soit possible, il faut donc que la proposition soit non atomique ou bien un "axiome", évidemment démontrable. P(x) vrai toujours, avec P un symbole, par exemple. 

Une proposition "validable" est donc composite, et utilise les structures du premier ordre pour se formuler.

La "conséquence logique", au sens des modèles, notée "|=", est donc une relation entre deux assertions de validité, qui se "calcule" de manière basique. 

C'est Paul Bernays, qui démontra en 1926 que pour les propositions, la démontrabilité découle de la validité.  

 Notons que, on aurait pu commencer par là, que la réciproque est vraie: une démonstration (au sens de Gentzen), (notée "|- ") implique que tout modèle de l'hypothèse est aussi modèle de la conclusion. La chose parait assez naturelle, la déduction dit "naturelle" étant bien compatible avec l'attribution de la vérité dans les opérateurs logiques élémentaires.  C'est le théorème de "correction", de "korrektheit", de "soundness", qui s'applique à une logique, ou à un "système logique". Par exemple, la logique intuitionniste est "correcte".

Incomplétudes

Il faut maintenant évoquer LES théorèmes d'incomplétude... Car en plus, il y en a DEUX...Le truc est multiple. 

Mais surtout le sens (du mot "complet") est DIFFERENT, on va y revenir.

D'abord, le premier d'entre eux, qui est le plus fameux, dit que toute théorie consistante incluant l'arithmétique, cela inclut le calcul des prédicats, est "incomplète": il y existe des énoncés indécidables. Non pas faux, ça on le savait (voir plus haut), mais non susceptibles d'être démontré avec les axiomes de la théorie, c'est à dire qu'il n'en existe pas de démonstration avec cette théorie là. 

Notons que le théorème de complétude s'applique et n'a en fait rien à voir avec cette choucroute, le mot est juste traitre. Ainsi l'énoncé "indécidable" dont on parle (non démontrable, donc) est faux dans un modèle particulier (suivant la contraposée de la complétude gödélienne: si non démontrable alors pas vrai dans tous les modèles donc faux dans au moins un). Par contre, ce modèle violateur, qui donc existe forcément, est "non standard" car le code de Gödel (attention, on s'accroche aux branches) de l'assertion "la théorie n'est pas consistante" n'est pas représentable par un simple entier, du moins dans ce modèle là. Les modèles non-standards de l'arithmétique sont ainsi en fait inévitables... 

L'incomplétude gödélienne est donc distincte de la complétude du même (auteur), en ce qu'elle ne s'applique pas à la même notion à compléter.

C'était ce que je voulais dire.

Allons directement au "monstre" de Gödel, qui utilise l'expressivité de l'arithmétique pour encoder l'assertion qu'il n'est pas prouvable. Cette assertion ne trouve indécidable par définition: si elle est prouvable, c'est qu'elle est vraie et donc elle se contredit; elle est donc non prouvable et se trouve réfutée, c'est à dire par définition prouvée, compte tenu de ce qu'elle affirme. Le monstre est donc bien indécidable et Gödel a raison de dire ce qu'il dit.

Le deuxième théorème de Gödel se déduit (presque) immédiatement du premier: les théories plus puissantes ou égales que l'arithmétique sont trop expressives: elle ne peuvent prouver leur propre cohérence car l'expression de leur cohérence s'y trouve indémontrable. En effet, la démonstration du premier théorème d'incomplétude est elle même encodable dans la théorie sous la forme de l'implication "si une théorie est cohérente alors le monstre n'est pas démontrable". Comme le monstre dit précisément "le monstre n'est pas démontrable", et bien il est donc (dans la théorie, c'est ça qui compte) vrai, et donc il est démontré... 

Donc on a démontré par une double mise en abîme (on a le droit de l'écrire comme ça) que si on peut exprimer, dans la théorie, que la théorie est cohérente alors le monstre est démontré. Comme la conclusion est fausse, la théorie ne peut exprimer sa propre cohérence. CQFD. Il faut bien voir l'aspect extrêmement vicieux de la chose: SI on accepte de dire, dans le cadre d'une théorie, qu'elle est cohérente, ALORS, on démontre le monstre. Donc, on ne peut même pas "dire" une chose pareille et donc à fortiori, on ne peut pas la démontrer. 

A l'issue de l'exposé en public du premier théorème, Von Neumann, dans l'assistance, en déduisit immédiatement le deuxième théorème et le fit remarquer. Il était super fort, Von Neumann...

Diophante et l'ordinateur

En parlant de complétude, l'équivalence faite par Matiassevitch entre les équations diophantiennes (sur les polynômes à coefficients entiers) et les ensembles récursivement énumérables montre que ces équations là ne peuvent être décidées solvables en général, et donc que le dixième problème de Hilbert est résolu, négativement. 

On fera remarquer que Matiassevitch, né en 1947 comme Girard, trouva cela en 1970, et que c'est à Paris que Hilbert (David) formula son programme. Que toute l'informatique, c'est à dire le calcul chosifié qui occupe tellement les esprits soit équivalent aux équations diophantiennes restera toujours fascinant (au moins pour moi).

On en vient donc à ce qui est "récursivement énumérable", en gros ce qui calculable par une machine de Turing qui s'arrête à la fin, même si ça prend un temps infini.

Le terme "récursif" s'applique aux ensembles des programmes qui s'arrêtent effectivement après un nombre fini d'étapes: et il n'y a pas de programme qui puisse le décider en temps fini, c'est l'indécidabilité du problème de l'arrêt. En gros, on ne peut pas décider de l'appartenance à un ensemble récursif, et ce qui est marrant c'est que "recursif" et "décidable" sont synonymes. "récursif" est donc bien plus limitant que "semi décidable" (récursivement énumérable).

En 1936, Turing, pour prouver que halt(prog(x)) n'existe pas, en fait ne peut pas terminer en temps fini en répondant oui, définit le programme fonctionnel vicieux suivant:

vice(x)= if (halt(x,x) loopforever else ok

Prenons vice(vice). Si ça termine, halt le sait, retourne "true" et vice(vice) ne termine pas. Donc ça ne termine pas, et donc halt (vice) repond nok et donc vice(vice) retourne ok,c'est à dire termine. Dans tous les cas, contradiction. Héhé: Turing est super fort aussi. Un hacker de première.

Les conditions de l'incomplétude

Cette petite disgression, pour bien préciser les conditions des théorèmes d'incomplétude. Gödel a besoin d'exprimer des énoncés méta mathématiques pour encoder le monstre. Pour cela, il faut Péano bien sur, mais pas seulement. Il faut que l'ensemble des axiomes de la théorie qui inclut l'arithmétique soit récursif. En effet, c'est LA condition sine qua non pour que Gödel puisse utiliser la théorie afin d'encoder le monstre. Peano pur, par exemple a bien des axiomes (en nombre infini) dont l'ensemble est récursif. Robinson, bien sur aussi (ses axiomes sont en nombre fini). Par contre, ce sont bien les théorèmes qui eux  ne sont que récursivement énumérables...

Pour finir, quelques remarques générales de plus. D'abord que l'encodage de Gödel est parfaitement du premier ordre et il est tout à fait faux d'imaginer que la complétude c'est du premier ordre et l'incomplétude, du second. Pire! Ce que démontre Gödel c'est que le fameux "méta langage " est en fait DEJA présent dans l'arithmétique, celui ci n'existe donc pas, et Girard a raison de le dénoncer.

Ensuite que la notion de "vrai" n'a de sens que relativement à un modèle. Par exemple, les théorèmes de Gödel ne disent pas du tout qu'il existe une vérité -absolue- non démontrable mais qu'il existe des indécidables et donc des énoncés vrais dans certains modèles et faux dans d'autres. Stricto sensu, c'est donc le contraire qui est dit, et du fait de la complétude !

Le XXème siècle fut un siècle complet (elle est bien bonne celle là).

 

P.S. J'ai passé beaucoup de temps à bien séparer les deux sens du mot "complétude". Ce n'est que dans la version anglaise de l'article wikipedia qu'on parle d'appliquer le théorème de complétude à l'assertion indécidable issue du deuxième théorème d'incomplétude... De plus, la "omega" inconsistence dont Rosser peut se passer pour démontrer le théorème d'incomplétude d'une autre manière n'a rien à voir avec la choucroute, contrairement à ce que semble laisser sous entendre Girard... Il y a donc toujours un doute, mon sentiment est mitigé, incomplet en quelque sorte...

La discussion en  https://sciencetonnante.wordpress.com/2013/01/14/le-theoreme-de-godel/ est particulièrement éclairante sur tout ça.

La syntaxe et la sémantique

Object des fantasmes de Girard, l'abolition de la distinction sémantique/syntaxe est bien mystérieuse et constitue un horizon sur lequel je me fracasse. 

Disons que c'est le coeur du propos de ce papier: le modèle est la sémantique, et le raisonnement la syntaxe (à moins que ce ne soit l'inverse). L'un est le réel de l'autre et c'est ce que veut dire Girard, qui veut abolir le réel, c'est à dire l'essence des choses. 

Dans sa fabuleuse "nécrologie" Nécrologie http://iml.univ-mrs.fr/~girard/titres.pdf il met en avant la chose, et prétend l'avoir résolue (ou pas).

Philosophie des mathématiques

Plus que jamais, la question de la nature du monde est posée et il semble bien que ces apories du raisonnement lui même en question agissent en faveur de deux points de vues à opposés, mais adversaires simultanés des relativistes et autres conventionnalistes  scientistes (et oui) qui veulent "écraser" la notation et faire du monde une simple mécanique.

Ces deux points de vue sont  le platonisme mathématique, et oui, c'était ce que pensait Gödel lui même, et ce que pensent les mathématiciens en général: un monde de réalité abstraite contraint la raison et se trouve à explorer, le faillibilisme, contrairement à ce que pense Girard, en étant le critère d'exploration. Le monde mathématique EST naturel, et se trouve peuplé de monstres à découvrir. C'était ce que pensait Bach pour la musique, du moins j'en suis sur. 

L'autre point de vue est similaire, mais aussi radicalement opposé: un intuitionnisme forcené, qui ramène tout à la seule chose qui compte, l'ensemble des entiers naturels, seule chose crée par Dieu, totalement donné, totalement naturel (comme son nom l'indique) et qui contiendrait tout... 

P.S.

(4) confirme tout à fait ma révolte sur l'application et la question de la complétude: Gödel est bien une source de création/conception de modèles "non standards".

(1) Toutes les démonstrations: http://perso.ens-lyon.fr/natacha.portier/enseign/logique/GoedelParAlex.pdf

(2) https://www.normalesup.org/~bagnol/notes/sequents.pdf

(3) https://tel.archives-ouvertes.fr/tel-00382528/document 

(4) http://www.madore.org/~david/weblog/d.2012-12-15.2093.verite-en-mathematiques.html#d.2012-12-15.2093.modeles-et-completude