La vérité d'une proposition de Gödel
J'ai une question sans doute assez basique concernant le premier théorème de Gödel, mais qui me perturbe depuis que j'ai appris ce théorème il y a des décennies.
Si j'ai bien compris ce théorème, dans un système formel de premier ordre et une axiomatique suffisante pour inclure l'arithmétique de Péano, on fait tout un travail pour pouvoir énumérer toutes les propositions du langage ainsi que leurs preuves formelles, et on construit ainsi la proposition numéro N, qui dit "la proposition numéro N ni sa négation n'est prouvable".
Ceci prouve effectivement qu'il y ait des propositions dans ce système qui ne sont pas prouvables ni fausses, car si cette proposition serait prouvable ou fausse, on obtiendrait un paradoxe du menteur. Jusque là, je suis.
Cela veut aussi dire que notre raisonnement, qui se passe en dehors du système, a bien prouvé cette proposition.
Mon problème est cependant, le suivant. On semble donc "savoir" que cette proposition, non-prouvable dans L, est quand-même vraie. Imaginons maintenant que nous construisons un autre système, L', dans lequel nous introduisons la NÉGATION de cette proposition comme axiome supplémentaire. A priori (c'est peut-être mon erreur), L' est aussi consistent que L, car nous n'avons pas introduit de contradiction, étant donné que l'axiome supplémentaire est indépendant des autres (s'il est superflu, la proposition aurait été prouvable, et s'il est en contradiction, sa négation aurait été prouvable). J'ai aussi compris que, en introduisant un nouvel axiome, on a complètement changé la numérotation, et donc la *signification* comme "numéro d'une proposition dans la langue" n'est plus valable. Donc la méta-interprétation "cette proposition dit quelque chose sur la provabilité d'une proposition" n'est plus vraie.
Mais cette proposition reste quand-même une proposition du système L' aussi bien que L, et on sait qu'elle est fausse dans L', puisque cette négation était le nouvel axiome dans L', donc avec une preuve triviale dans L'.
Cependant, et c'est ma question: comment fait-on pour pouvoir "prouver" la vérité de cette proposition en "méta-mathématiques" quand on considère les axiomes dans L, et pouvoir dire que dans L', cette même proposition serait fausse ?
Imaginons que L était Péano. La proposition est donc "une proposition concernant les nombres entiers" qu'on ne peut pas *formellement* prouver à partir de Péano. Mais "informellement", en dehors de Péano purement formel, en suivant l'argumentaire de Gödel, on a donc une démonstration de cette proposition. C'est donc un truc vrai sur les nombres entiers dont on prend comme point de départ, Péano "et le raisonnement méta-mathématique" de Gödel. On pourrait qualifier cela comme une preuve mathématique "informelle".
Et maintenant, il serait possible d'avoir une extension des axiomes de Péano, avec la négation de cette propriété, dans le système formel L' qui est aussi cohérent que Péano ? Mais notre raisonnement "Gödellien" sur les n-1 axiomes (donc dans L) reste quand-même valable aussi et il dit que cette propriété est vraie ?
Si j'ai bien compris ce théorème, dans un système formel de premier ordre et une axiomatique suffisante pour inclure l'arithmétique de Péano, on fait tout un travail pour pouvoir énumérer toutes les propositions du langage ainsi que leurs preuves formelles, et on construit ainsi la proposition numéro N, qui dit "la proposition numéro N ni sa négation n'est prouvable".
Ceci prouve effectivement qu'il y ait des propositions dans ce système qui ne sont pas prouvables ni fausses, car si cette proposition serait prouvable ou fausse, on obtiendrait un paradoxe du menteur. Jusque là, je suis.
Cela veut aussi dire que notre raisonnement, qui se passe en dehors du système, a bien prouvé cette proposition.
Mon problème est cependant, le suivant. On semble donc "savoir" que cette proposition, non-prouvable dans L, est quand-même vraie. Imaginons maintenant que nous construisons un autre système, L', dans lequel nous introduisons la NÉGATION de cette proposition comme axiome supplémentaire. A priori (c'est peut-être mon erreur), L' est aussi consistent que L, car nous n'avons pas introduit de contradiction, étant donné que l'axiome supplémentaire est indépendant des autres (s'il est superflu, la proposition aurait été prouvable, et s'il est en contradiction, sa négation aurait été prouvable). J'ai aussi compris que, en introduisant un nouvel axiome, on a complètement changé la numérotation, et donc la *signification* comme "numéro d'une proposition dans la langue" n'est plus valable. Donc la méta-interprétation "cette proposition dit quelque chose sur la provabilité d'une proposition" n'est plus vraie.
Mais cette proposition reste quand-même une proposition du système L' aussi bien que L, et on sait qu'elle est fausse dans L', puisque cette négation était le nouvel axiome dans L', donc avec une preuve triviale dans L'.
Cependant, et c'est ma question: comment fait-on pour pouvoir "prouver" la vérité de cette proposition en "méta-mathématiques" quand on considère les axiomes dans L, et pouvoir dire que dans L', cette même proposition serait fausse ?
Imaginons que L était Péano. La proposition est donc "une proposition concernant les nombres entiers" qu'on ne peut pas *formellement* prouver à partir de Péano. Mais "informellement", en dehors de Péano purement formel, en suivant l'argumentaire de Gödel, on a donc une démonstration de cette proposition. C'est donc un truc vrai sur les nombres entiers dont on prend comme point de départ, Péano "et le raisonnement méta-mathématique" de Gödel. On pourrait qualifier cela comme une preuve mathématique "informelle".
Et maintenant, il serait possible d'avoir une extension des axiomes de Péano, avec la négation de cette propriété, dans le système formel L' qui est aussi cohérent que Péano ? Mais notre raisonnement "Gödellien" sur les n-1 axiomes (donc dans L) reste quand-même valable aussi et il dit que cette propriété est vraie ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
La phrase arithmétique P de Godel qui dit je ne suis pas prouvable dans Peano est telle que
P si et seulement si [Peano consistant]
par exemple. Les gens qui la pensent vraie sont les gens qui pensent Peano consistant.
Je note G la formule de Gödel (celle qui dit je ne suis pas démontrable).
Ce que tu proposes de faire en ajoutant nonG à Peano ne peut pas marcher, pour la raison suivante.
Il y a 2 cas de figure.
1er cas : Peano est consistante. Comme dit Christophe, dans ce cas G est vraie, donc si tu rajoutes à Peano l'axiome nonG tu obtiens une théorie inconsistante.
2ème cas : Peano est inconsistante. Dans ce cas tu peux lui rajouter ce que tu veux, ta théorie restera inconsistante. (Et elle démontrera tout ce que tu veux, en particulier qu'elle est consistante).
CQFD
(si PA+ non G est inconsistante alors PA démontre non non G donc PA démontre G donc PA est inconsistante ...)
Mais cette remarque n'est pas en contradiction avec ce qui précède : si tu rajoutes l'axiome nonG à PA cela revient à nier l'existence d'un modèle standard... et ça se saurait, non ?
Non, ça ne change rien, la numérotation, aussi "cryptique" qu'elle ait l'air n'est pas bien méchante.
Non, pas du tout. Ce qu'on a c'est une dichotomie très simple:
ou bien (1) Peano est consistante et G est vrai et non prouvable
ou bien (2) Peano est contradictoire et G est fausse et prouvable
(pour la phrase G vérifiant G == (G est non prouvable) )
Tu es libre de choisir entre (1) et (2), mais comme tu peux le voir, (2) n'emballe pas les conformistes :-D . Et attention, le fait de supposer que Peano est contradictoire, qui est un énoncé (par Matiyasevic) de la forme $\exists xP(x)=0$, ne te donne pas pour autant une solution à l'équation $P(x)=0$ qui soit un uplet d'entiers "pas trop gros". Tu n'as aucun contrôle sur sa taille, en gros, tu n'as rien (ou pas grand chose).
A noter que Peano démontre l'existence de $U(1000,1000)$ (où $U$ est la fonction d'Ackermann), mais "in some sense", :-D , cet entier n'est pas franchement ce qu'on peut qualifier d'accessible. Bon, mais à tout le moins il agit sur les phrases quantifiées (ie Peano le démontre "facilement"), ce qui n'est même pas le cas d'une supposition de l'existence d'une preuve de $0=1$ dans Peano.
Pour le reste, je ne te comprends pas vraiment, tu es trop flou.
je pensais que pour que PA + non-G soit inconsistant (si PA seul est consistent), il faudrait que G soit prouvable dans PA, justement (mais effectivement je ne suis pas sûr de cela).
Comment on peut obtenir:
- PA tout seul consistant
- PA + non-G non consistant
sans avoir que PA => G ?
Car ce serait quand-même une preuve: "on va prouver que G suit de PA par réduction à l'absurde". Imaginons non-G dans le cadre de PA ; alors absurdité. Donc G.
Mais cela voudrait dire que G suit bel et bien de PA. G est donc bien "prouvable" de PA, alors que Gödel à fait tout son baratin pour dire qu'on ne pouvait pas formellement prouver G de PA.
En fait, j'avais toujours compris ça comme: "les méta-mathématiques non-formelles utilisées sont sans doute aussi formalisables avec des axiomes en plus, ce qui nous permet de prouver G dans "méta + PA" ". En d'autres termes, c'est parce qu'on utilise des méta mathématiques "plus riches" qu'on était capable de dériver que G était vrai. On n'a donc pas prouvé G de PA tout seul, mais dans le cadre d'un système (non formel mais peut-être formalisable) plus riche.
Seulement, ces méta-mathématiques semblent pouvoir considérer le système formel PA + non-G aussi bien que le système formel PA ? Car le système formel PA + non-G en soi doit être consistant (si PA l'est), et je ne vois pas comment les "méta mathématiques" peuvent devenir inconsistantes en considérant un système formel cohérent. On s'imagine les "méta -mathématiques" capables de considérer tout système formel cohérent quand-même. On ne s'imagine pas qu'un système formel L "ne puisse pas être considéré" par les méta mathématiques que Gödel utilises (sinon il se tire une balle dans le pied).
Donc ça me perturbe.
Peux-tu poser une question à la fois, mais précise, de façon à ce qu'on puisse y répondre sans se perdre dans des circonvolutions interminables ?
Tu as un modèle de Peano + G
Tu as un modèle de Peano + nonG c'est tout.
De plus DANS ZF ou tout autre sous théorie de ZF un peu riche ce que tu appelles "la vérité de G perçue metamathematiquement " n'a rien de metamathematique: c'edt juste que IN est un modèle de Peano +G
0/ tous les individus sont nommés
1/ un prémodèle est un ensemble de phrases.
2/ un modèle est un ensemble de phrases compatible avec les connecteurs et contenant $non(\forall xR(x))$ si et seulement si il existe un nom d'individu $a$ tel que $non(R(a))$ aussi est dans le modèle.
edit j'ai corrigé une coquille signalée par foy ci-dessous, donc elle n'apparait plus. Demain, je corrigerai en changeant le statut "ensemble" en application dans {vrai;faux}, parce que sinon c'est très inélégant.
Prenons maintenant la phrase $G$ qui est de la forme $\forall xR(x)$
3/ Ainsi un modèle de Peano ressemble un peu à un semi-anneau. Les modèles $M$ de Peano + nonG sont tels qu'il existe un individu $a$ tel que $nonR(a)$.
4/ La confusion la plus fréquente, chez les néophytes est de confondre $a$ avec un "vrai entier".
Un énoncé (formule sans variable libre) de N (théorie complète constituée des énoncés vérifiés par les entiers naturels) est soit vraie, soit fausse.
Un énoncé de la théorie PA est soit vraie, soit fausse, soit indécidable.
On part du principe que PA est consistante.
Etre prouvable par PA, c'est être PA-vrai.
Dire qu'un énoncé F n'est pas pas être prouvable par PA, c'est donc être PA-fausse ou PA-indécidable,
ce qui est aussi équivalent à avoir PA + (non F) cohérente (ou consistante : je ne fais pas bien la distinction)
Quand on dit que F est un "énoncé vrai non prouvable par PA",
on doit comprendre que F est N-vrai mais pas PA-vrai,
c'est à dire N-vrai et « soit PA-indécidable, soit PA-fausse ».
Pour certaines théories, "l'énoncé de Gödel" G (N-vrai) est tel que G est PA-indécidable, donc PA+G et PA+(non G) sont consistantes.
Pour certaines théories, "l'énoncé de Gödel" G (N-vrai) est tel que G est PA-fausse, donc PA prouve (non G).
Dernière remarque, G a été construit de telle sorte qu'on ait "G N-vrai ssi PA est consistante".
En fait, on a G N-vrai, ssi PA consistante, ssi PA ne prouve pas G.
Bref, c'est un sujet assez délicat et j'espère sincèrement ne pas avoir raconté de bêtises.
Cordialement
Pour moi, un langage formel de type L1 est un jeu de chaînes de caractères, qui doivent obéir à des règles syntaxiques, qui est équipé d'axiomes (certaines chaînes de caractères ont le tampon "vrai"), et des règles d'inférence (de "fabrication" d'autres chaînes de caractères syntaxiquement correctes qui héritent alors le tampon "vrai").
En d'autres termes, on peut associer 2 bits à chaque "chaîne de caractères":
- est syntaxiquement correct (bit 1): on appelle ces chaînes "des phrases"
- est vrai (hérite vérité des axiomes et des règles d'inférence) : on appelle ces chaînes: "des théorèmes".
Bit 2 implique bit 1. On peut même se demander pourquoi on y va en deux étapes, sauf que les règles syntaxiques sont simples à vérifier, alors que l'héritage de vérité (une preuve formelle donc) ne l'est pas.
Aussi, on ne considère des langages formels que quand les règles d'inférence correspondent à une interprétation logique et qu'il y a une partie au moins de la syntaxe qui permet d'interpréter les phrases comme des propositions potentielles.
Ainsi, il y a donc, parmi toutes les chaînes possibles, un sous-ensemble de chaînes syntaxiquement correctes (les phrases), et là-dedans encore un sous-ensemble de chaînes "vraies", les théorèmes (qui ont hérité de la "vérité d'axiome" et les règles d'inférence). Dans la mesure où la syntaxe permet aussi d'exprimer la "négation logique" systématiquement, on peut attribuer le bit "faux" (troisième bit) aux phrases dont la négation possède le deuxième bit (vrai par héritage).
Alors nous avons donc:
- les chaînes
- sous ensemble: les chaînes ayant bit 1 : les phrases (syntaxe)
- sous ensemble: les phrases ayant bit 2 ou bit 3 ("les propositions")
- sous ensemble: les phrases ayant bit 2 ("les théorèmes)
C'est à peu près tout ce que je comprends.
Essentiellement, Gödel dit que dans des langages formels qui contiennent un certain nombre de symboles, d'axiomes et de règles d'inférence qu'il y ait des phrases qui n'ont ni le bit 2, ni le bit 3, et ce n'est pas étonnant. L'inverse serait plutôt fascinant. Il dit que l'ensemble des propositions est plus petite que l'ensemble des phrases.
Si j'ai bien compris, un système ou toutes les phrases sont aussi des propositions, sont des systèmes complets.
Je suis beaucoup plus vague sur "un modèle". Pour moi, c'est "une implémentation du système formel" dans un système de pensée à priori non-formel, mais dont les axiomes interprétés sont "vrai" et les règles d'inférence sont acceptés valables. Alors, toute proposition du système formel est alors aussi une proposition dans le modèle ; si elle est vraie, cette proposition est vraie dans le modèle, et si elle est fausse, cette proposition est fausse dans le modèle.
En ce qui concerne les phrases formelles qui ne sont pas des propositions (dont on ne peut donc pas prouver qu'elles sont vraies ou fausses dans le système formel), le système formel ne nous apprend rien sur le statut de vérité de cette proposition dans le modèle.
Mais ça me reste vague.
On peut quelque part dire que "ce qu'on a en tête quand on parle d'entiers naturels" est un modèle pour le système formel Péano: tout ce qu'on peut prouver formellement dans Péano, est alors aussi "vrai" pour "les nombres naturels entiers comme on les conçoit".
Voila, j'ai résumé grosso modo le peu que je pense savoir sur les langages formels.
- le fait d'être démontrable à partir des axiomes, autrement dit d'être un théorème ; c'est une notion syntaxique.
- le fait d'être vrai, qui est une notion sémantique et qui n'a de sens que quand on interprète le langage dans un modèle des axiomes.
Exemple : prenons le langage des groupes, avec les axiomes de la théorie des groupes. Un modèle, c'est un groupe. L'énoncé $\forall x\ \forall y\ xy=yx$ est vrai ou faux dans un modèle de la théorie (un groupe) si et seulement ci celui-ci est abélien. C'est un énoncé indécidable de la théorie des groupes.
Autre exemple : prenons le langage des corps ordonnés, avec les axiomes de corps réels clos (corps ordonné maximal). Un modèle est un corps réel clos. Cette fois, si un énoncé est vrai dans un modèle, il est vrai dans tous les autres et par conséquent (théorème de complétude) il est démontrable dans la théorie des corps réels clos. La théorie des corps réels clos est complète, elle n'a pas d'énoncé indécidable.
Encore autre exemple : le langage de la théorie des ensembles, avec les axiomes de ZF ...
NON !!!!
Encore une confusion entre notion sémantique et notion syntaxique.
Un énoncé est soit vrai, soit faux dans un modèle. Point barre.
Par ailleurs un énoncé est soit démontrable (un théorème), soit à négation démontrable, soit indécidable dans une théorie.
J'ai écrit "Un énoncé de la théorie PA est soit vraie, soit fausse, soit indécidable" car PA n'est pas complète ;
il y a donc des énoncés PA-indécidables (ex : G)
Pour simplifier, on récupère une théorie complète quand on a un modèle.
J'aurais dû écrire Th(N) pour théorie (complète) sous-jacente au modèle N, au lieu de N.
Bien évidemment, aucun énoncé n'est N-indécidable : comme tu l'écris, c'est soit N-vrai, soit N-faux.
Le théorème de complétude de Gödel dit que pour un énoncé être N-vrai (sémantiquement parlant) est être équivalent à être Th(N)-vrai (syntaxiquement parlant).
J'ai évité de parler de modèle (pour "N") pour ne pas perdre @Patrick.
Je le répète, c'est délicat. C'est pourquoi je distingue toujours dans mes raisonnements "N-vrai" ou "PA-vrai",
la plupart des fautes de raisonnements venant du fait qu'on parle de vrai pour "N-vrai" mais rapidement on pense alors que c'est "PA-vrai".
Cordialement.
Edit 1 : quelques mots barrés après une remarque de GBZM.
NON !!! La théorie d'une structure (théorie dont les axiomes sont tous les énoncés vrais dans cette structure) est complète par définition, le théorème de complétude de Gödel n'a rien à voir là-dedans.
Le théorème de complétude de Gödel dit qu'un énoncé vrai dans tous les modèles d'une théorie est démontrable dans cette théorie.
Sur ce point, tu as entièrement raison. Je barre immédiatement.
Je crois qu'on est en train de zoomer sur mon problème de compréhension, donc je m'accroche.
Je n'ai donc pas compris exactement ce que c'est, un modèle, visiblement, mais du coups, je ne sais plus ce que cela pourrait bien vouloir dire.
On est bien d'accord que, dans un langage (ou système, je ne connais pas exactement la terminologie) formel, on distingue (je trouve cela un peu artificiel, mais bon), les "phrases" (syntaxiquement correctes), et puis les théorèmes (donc "prouvables") et les "négations de théorèmes" (nécessite qu'il y ait "interprétation logique d'une partie de la syntaxe", donc qu'il y ait une partie sémantique logique), et que pas toutes les phrases syntaxiquement correctes, sont des théorèmes ou des négations de théorèmes: il y a des phrases qui sont syntaxiquement correctes, mais "qui ne veulent rien dire" dans le système formel, car dans le système, elles sont indécidables. Je ne vois pas trop à quoi sert le fait qu'on ait fait une distinction entre "chaîne non-syntaxique" (donc suite de symboles qui ne respecte pas la syntaxe du système) et "phrase indécidable", sauf pour le fait sans doute qu'alors que les règles syntaxiques sont facilement décidables, les phrases indécidables ne le sont pas, et donc, souvent, on ne sait pas s'ils sont indécidables ou pas. On doit donc pouvoir quand-même les exprimer. Mais pour moi, ce sont aussi des "rejetons" du système formel, au même niveau que les chaînes syntaxiques erronées. Ce ne sont donc pas des propositions, même s'ils sont syntaxiquement correctes. C'est comme ça que je vois cela, est-ce erroné ?
Mais "un modèle", c'est moins clair maintenant. Pour l'exemple du groupe, pour moi, un modèle, c'est "une application" du langage formel, tel que "tout ce qui est prouvable dans le système formel, est aussi vrai dans le modèle, mais bien sûr, pas vice versa".
Ainsi, le groupe abstrait possède des phrases "indécidables" qui ne veulent donc rien dire dans le système formel, mais qui peuvent vouloir dire quelque chose dans un modèle. Par exemple, l'addition dans $\Z$ est un "modèle" pour le système formel "groupe". Mais il y a bien sûr beaucoup plus de choses à dire dans $\Z,+$ que dans le système formel "groupe", comme tu dis: il y a la commutativité, c'est un groupe à un générateur, etc.... quelque chose qui n'est pas décidable dans le système formel. Tout ce qui est "vrai" (prouvable) dans le système formel, sera vrai dans $\Z,+$, mais pas l'inverse.
Est-ce bien ça ?
Une proposition (donc une phrase prouvable vraie) dans le système formel, implique toujours la "vérité" dans le modèle de la proposition correspondante (et donc aussi une proposition fausse, qui est simplement la négation d'un théorème). Mais l'inverse n'est donc pas valable: ce n'est pas parce que quelque chose est vrai, ou faux, dans le modèle, que cela implique le même statut de vérité de la phrase correspondante dans le système: la phrase peut aussi ne pas être une proposition (donc ne pas être décidable) dans le système formel.
Si on a donc 2 modèles du système formel, un dans lequel une phrase est vraie, et un autre dans lequel la même phrase est fausse, alors il faudra bien que cette phrase soit indécidable (ne soit pas une proposition) dans le système formel.
Mais en fait, les différences se situent donc seulement sur le plan des "phrases qui ne sont pas des propositions" dans le système formel: pour certains modèles, ils peuvent 'devenir des propositions vraies", pour d'autres, "devenir des propositions fausses", mais dans le système formel, ils ne veulent rien dire (ne sont ni vraies, ni fausses, donc pas de propositions).
Il en suit alors que si le système formel est complet (toute phrase est aussi une proposition, c.à.d. est décidable), alors tous les modèles sont "les mêmes" sur le plan de la vérité de tout ce qui est exprimable en phrases. Il se pourrait que les modèles possèdent plus de choses, qui ne sont simplement pas exprimables par le langage formel en question, et qui fait quand-même que les modèles sont différents, sur un aspect qui n'est pas modélisé par le langage formel. Exemple trivial: {1, 2, 3, 4, 5, 6} et {2, 3, 5, 7, 11, 13} équipés de leurs ensembles de permutations sont tous les deux des modèles pour le langage formel "groupe de symétrie à 6 éléments" ; mais on voit que le deuxième ensemble est aussi un sous-ensemble des nombres premiers ; ceci n'est pas exprimable, cependant, dans le langage formel "groupe de symétrie à 6 éléments".
Je suis toujours bon ? (à part peut-être la terminologie, que je ne maîtrise pas).
Visiblement on ne dit pas qu'un théorème dans un système formel est "vrai" mais on dit qu'il est "prouvable" - je ne sais pas pourquoi, mais c'est une convention de terminologie, je suppose.
Je ne comprends pas pourquoi un "modèle serait complet". Je ne sais pas trop ce que cela voudrait dire, car je pensais qu'un modèle n'était pas un système formel, justement.
En théorie des modèles, il y a deux mondes (intimement liés bien sûr) :
La syntaxe, c'est-à-dire les formules, et la sémantique, c'est-à-dire les interprétations de formules dans une structure. Les formules peuvent être prouvables ou non à partir d'une certaine théorie (un ensemble de formule), et elles peuvent être vraies ou fausses dans une structure. Ça s'arrête là.
Pour parler de formules, on se donne un langage (des symboles de constantes, de relations et de fonctions). Une structure sur ce langage c'est juste un ensemble dans lequel on interprète chacun de nos symboles. Un modèle d'une théorie (ensemble de formules) est une structure dans laquelle chaque formule de la théorie est vraie. Ainsi, dans le langage $\{*, e\}$ où $e$ est un symbole de constante et $*$ est un symbole de relation binaire, un modèle de la théorie des groupes $\{\forall x, y, z, (x*y)*z = x*(y*z); \forall x, \exists y, x*y=y*x = e; \forall x, x*e=e*x=x\}$ est un bête groupe.
Il existe des formules qui ne sont pas prouvables, et dont la négation n'est pas prouvable non plus. C'est le cas de l'exemple donné par GBZM plus haut. En vertu du théorème de complétude de la logique du premier ordre, une formule est démontrable à partir d'une théorie $T$ si et seulement si elle est vraie dans tout modèle de $T$. Comme il existe des modèles de la théorie des groupes ne vérifiant pas la formule $\forall x, y, x*y=y*x$ (les groupes non abéliens), c'est que cette formule n'est pas démontrable à partir de la théorie ci-dessus. Sa négation non plus n'est pas démontrable à partir de la théorie des groupes, puisqu'il existe des groupes abéliens.
Pour donner quelques idées, voici une façon d'aborder les choses.
Je ne prétends pas que c'est la meilleure et je passe sous silence beaucoup de détails ...
Soit $\mathcal L = \{=,O,+,\times,S\}$ le langage de l'arithmétique.
A partir de celui-ci, on peut construire des termes et des formules en respectant des règles syntaxiques.
Les formules sans variables liées libres sont appelées "énoncés".
Une théorie $\mathscr T$ est un ensemble d'énoncés, appelés axiomes de $\mathscr T$, par exemple PA.
Un $\mathscr T$-théorème est une formule $F$ obtenue par des règles "syntaxiques" de déduction etc.
On dira qu'une formule est :
a) $\mathscr T$-vraie si c'est un $\mathscr T$-théorème, c'est à dire qu'elle figure dans une preuve syntaxique "de $\mathscr T$" ;
b) $\mathscr T$-fausse si sa négation est $\mathscr T$-vraie ;
c) $\mathscr T$-indécidable si elle n'est ni $\mathscr T$-vraie ni $\mathscr T$-fausse.
A partir de l'ensemble des entiers naturels $\mathbb N$, on va construire un modèle N sur le langage $\mathcal L$.
Cela revient :
à associer à $O$ l'entier $0$ ;
à associer au symbole + l'application $\mathbb N^2 \to \mathbb N$ qui à $(n,m)$ associe la somme de n et m ;
à associer au symbole $\times$ l'application $\mathbb N^2 \to \mathbb N$ qui à $(n,m)$ associe le produit de n et m ;
à associer au symbole $S$ l'application $\mathbb N \to \mathbb N$ qui à $n$ associe $n+1$ ;
à associer au symbole $=$ la diagonale $D$ de $\mathbb N$, à savoir $D=\{(x,x)\mid x\in\mathbb N\}$.
On a ainsi "interprété" chaque symbole du langage $\mathcal L$.
On dit que l'entier $n$ satisfait la formule $x=SSSSO$ si quand on "remplace" (en quelque sorte) $x$ par $n$ et $SSSSO$ par son interprétation $4$ on a $(n,4)\in D$, c'est à dire $n=4$.
De même, on peut en raisonnant de proche en proche sur la longueur de la formule $F$ donner un sens à « $(m_1,\ldots,m_n)$ satisfait $F\{x_1,\ldots,x_n\}$ », où $x_1,\ldots,x_n$ sont les variables libres de $F$.
Par exemple, on dit que $m$ satisfait $(\exists x)F\{x,y\}$ s'il existe effectivement un entier naturel $a$ tel que $(a,m)$ satisfait $F\{x,y\}$.
En appelant N le modèle, on a une notion sémantique de la vérité :
a) on dit qu'une formule $F\{x_1,\ldots,x_n\}$ est N-vraie si "tous les n-uplets d'entiers la satisfont",
b) on dit qu'elle est N-fausse si sa négation est N-vraie.
Il y a bien entendu des formules qui ne sont ni N-vraies, ni N-fausses, mais pour les énoncés, on a le fait suivant :
Fait : un énoncé est soit N-vrai, soit N-faux.
Comme chaque axiome de PA est satisfait dans N, c'est à dire est N-vrai, on dit que N est un modèle de PA.
Ceci étant, il existe d'autres modèles de PA qui ne sont pas isomorphes à N ...
Le théorème de complétude de Gödel montre qu'un énoncé est PA-vrai ssi il est M-vrai pour tout modèle M de PA.
Edit 1 : correction d'un "SOOOO" en "SSSSO"
Edit 2 : correction d'un "liées" en libres", merci @Patrick123
Personne n'emploie cette terminologie (sauf toi). Je vois bien que tu essaies ainsi de rattraper l'erreur que j'avais signalée plus haut.
Si si, j'étais sincère et je n'ai pas cherché à rattrapper une quelconque erreur.
J'en suis resté à la définition de Bourbaki que j'ai lu il y a longtemps et que j'ai peut-être mal comprise.
C'est vrai que le fait de parler de formule T-vraie ou T-fausse m'a permis de m'exprimer plus fluidement en maintes occasions, mais seul dans mon coin avec mes maigres ressources. Visiblement, je ne connais pas la terminologie utilisée actuellement.
Cordialement
Autant Bourbaki est une bonne source d'information pour le reste des maths, autant la logique n'était pas leur truc (*).
Même en théorie des ensembles le symbole $\tau$ qui semble vouloir tout régler en contournant l'axiome du choix est source de restriction de la pensée, et surtout d'une théorie totalement démodée. Dans son livre, Patrick Dehornoy qualifie la vision bourbakiste de la set theory comme une vision pré-gödélienne.
@Tous : c'est qui shadok ?
(*) Ce choix a été imposé par Dieudonné, qui était le grand manitou du groupe. Selon lui la logique faisait partie intégrante de la philo, non des maths. Et pourtant, cent ans avant, Boole...
@GaBuZoMeu, je présume. ;-)
> Pourrais-tu faire plus court et plus lisible ?
C'est verbeux parce que je ne connais justement pas les bons termes, alors je brode autour pour essayer de faire comprendre ce que je veux dire, sans utiliser le mot technique, dont je ne suis pas sûr qu'il couvre ce que je veux dire.
j'essaie donc de comprendre les définitions des mots utilisés en les mettant en relation avec "un descriptif" qui est, par manque d'autre chose, verbeux.
Je vais donc essayer d'y aller en petits pas.
Un alphabet, c'est un ensemble fini de symboles.
Une chaîne, c'est une succession finie de symboles prises dans l'alphabet
Une syntaxe, ce sont des règles qui disent quelles genres de chaîne sont des "phrases", c'est ce qu'on appelle "formule" ? Une chaîne syntaxiquement correcte ?
Puis, et c'est là que visiblement je manque de vocabulaire/concepts: je pensais qu'il y avaient "des règles d'inférence syntaxique" qui permettaient de "construire des preuves formelles". Donc, à partir de certaines formules, en fabriquer d'autres qui "héritaient" de "prouvabilité" ? Elles sont supposées implémenter des inférences logiques, mais formulées de façon purement syntaxiques.
Donc des algorithmes finis, qui peuvent prendre une ou un nombre fini de formules, et en fabriquer d'autres, et si c'est le cas, on dit que la formule fabriquée est "prouvée" par cette règle d'inférence à partir des formules d'entrée.
Par exemple, le remplacement d'une variable liée, par une règle d'inférence "le symbole après le signe $\forall$ peut être remplacé par un autre symbole du type "nom" si on remplace ce même symbole partout dans le reste de la chaîne, si ce nouveau symbole n'apparaît pas déjà dans la chaîne".
Est-ce que c'est ça, une langue formelle: un truc donc avec un alphabet, des règles syntaxiques, et des règles d'inférence (syntaxiques/logiques) ?
Je crois que j'ai reformulé ce que tu as dit, jusqu'à ta phrase:
"Les formules sans variables liées sont appelées "énoncés". "
Est-ce que ce ne doit pas être "variables libres" ? Et est-ce un concept purement syntaxique, "variable" ?
Le trou qui me reste, se trouve sur "l'implémentation formelle de la logique", est-ce que ma façon de dire que ce sont des règles d'inférence syntaxique qui implémentent des inférences logiques "sans le dire" (car on n'a visiblement pas la notion de "vérité" dans un système formel), correct et est-ce qu'il y a un terme accepté pour cela ?
Par exemple, si on a la formule "$\forall x, y: x + y = y + x$" que je peux en déduire la formule: $\forall x, y, z: (x+z) + y = y + (x + z)$ par pure jeu syntaxique et dire que cette dernière "hérite" alors le statut de "prouvé" de la première" par la règle d'inférence syntaxique, puisque je ne peux pas parler de "vrai" ou de "faux" ?
Alors une "théorie" c'est une "langue" plus un jeu d'axiomes, choisi parmi les formules de la langue ?
Oui, c'est à peu près comme ça que je voyais les choses aussi, sauf que je ne savais pas exactement ce qu'on appelait "langue", et ce qu'on appelait "théorie".
Alors, les règles d'inférence syntaxiques (qui sont sensés implémenter les inférences logiques) "propagent" à partir du statut "T-vraie" des axiomes, un statut de T-vrai dans pas mal de formules, oui.
Il faut encore pouvoir dire qu'une formule serait la "négation" d'une autre formule ; c'est sans doute quand-même un élément "sémantique" qu'on attribue à une syntaxe. Là, on sort du purement formel, et on accepte bien une sorte de "valeur logique" au statut de T-vrai, qui, jusque là, était purement formel et syntaxique.
Oui, j'avais déjà vu cette page, mais ce qui semble "bugger", c'est que j'ai d'un coté l'impression qu'il faudrait passer par un modèle pour construire des démonstrations, alors que justement, je pensais que c'était un pur jeu syntaxique, avec des règles d'inférence de "modification de chaîne de symboles" qui implémente (sans pouvoir le dire) des règles d'inférence logique.
C.à.d. qu'une preuve formelle était un pur jeu syntaxique, indépendant de tout "modèle".
> Oui, j'avais déjà vu cette page, mais ce qui
> semble "bugger", c'est que j'ai d'un coté
> l'impression qu'il faudrait passer par un modèle
> pour construire des démonstrations, alors que
> justement, je pensais que c'était un pur jeu
> syntaxique, avec des règles d'inférence de
> "modification de chaîne de symboles" qui
> implémente (sans pouvoir le dire) des règles
> d'inférence logique.
Tu as une lecture incomplète de la page. Tu as zappé la partie sur les systèmes de déduction.
1) une "variable" est-elle une notion purement syntaxique ? Je ne sais pas quoi répondre. J'aurai envie de dire oui, d'autant plus que seuls les énoncés font un lien « net » entre les théories et les modèles via le théorème de complétude. Bon, ce n'est qu'un avis "fumeux" ...
2) pour les règles de déduction d'une théorie $T$, par exemple : $F$ est $T$-prouvé ("$T$-vrai" avec mon vocabulaire) si
a) $F$ est un énoncé de $T$
b) $F$ est un axiome logique
c) $G$ est $T$-prouvé et $G\Rightarrow F$ aussi (coupure)
d) $G$ est $T$-prouvé et $F$ est $(\forall x)G$ (généralisation)
Les règles concernant la négation d'une formule sont contenus dans b) ; ici c'est purement syntaxique.
3) Evidemment, il y a d'autres systèmes de déduction. En fonction de ce qu'on choisit, on le paie à un moment donné en terme de lourdeur.
4) Pour moi, une théorie est un ensemble d'énoncés construits sur un langage.
Cordialement
Ben, ce n'était pas clair si "système de déduction" parlait de règles purement syntaxiques (comme je le vois/voyais), ou si c'est déjà "sémantique" et fait donc déjà parti d'un modèle.
Est-ce que je peux considérer que c'est bien un truc "purement syntaxique" à l'intérieur du langage ? Ou à l'intérieur d'une théorie ?
Les règles syntaxiques "de bonne formation d'un énoncé" (ce que j'appelais "phrase") font partie du langage si je comprends bien. Les axiomes, par contre, font partie d'une théorie. Les règles d'inférence, dont je demande donc ci-dessus si ce sont bien des pures "manipulations syntaxiques", il font partie du langage, ou de la théorie ?
S'ils font partie du langage (ce que je pensais), alors une théorie = le couple "langage" + "liste d'axiomes prises dans les énoncés" alors ?
Donc, essentiellement, une théorie T:
1) contient des énoncés (ce que j'appelais des phrases, donc des chaînes de symboles syntaxiquement correctes)
2) contient un "mécanisme syntaxiquement vérifiable" de propagation d'une propriété (un "bit d'activation T-vrai")" qu'on appelle la T-prouvabilité ou la T-vérité, à partir de la liste d'axiomes et en utilisant les règles d'inférence.
3) contient une règle pour dire que l'énoncé A est la négation de l'énoncé B, et tout énoncé à un énoncé qui est sa négation. Si un énoncé est T-prouvable par 2), alors on dit que sa négation est T-fausse. (un autre "bit d'activation T-faux").
4) certains énoncés sont décidables, c.à.d. ils sont T-vrai ou T-faux, d'autres, non. On appelle ces derniers: "T-indécidables".
J'appelais les énoncés décidables des "propositions" (car ils avaient un statut de vérité), un sous-ensemble des phrases.
5) la théorie est consistante si aucun énoncé est en même temps T-vrai et T-faux.
6) la théorie est complète si tout énoncé est T-vrai ou T-faux (qu'il n'y a pas d'énoncés indécidables).
OK, jusque là, je suivais sans avoir les bons mots.
Là où je coince, c'est l'idée de modèle.
Un modèle est donc une "application/interprétation" des symboles et de la syntaxe d'une théorie T dans une structure mathématique "non-formelle", de telle façon que dans cette structure mathématique, on considère les règles d'inférence comme logiquement valables, les variables comme étant substituables par des éléments des ensembles de base de la structure et les axiomes comme étant postulés vrais. Le modèle peut être bien plus riche que juste la partie "interprétée" par la syntaxe de la théorie, du moment où les déductions syntaxiques restent vraies quand elles sont interprétées dans le modèle, et les axiomes sont vrais quand on les interprète.
Alors, il est relativement évident que tout ce qui était T-vrai dans la théorie T, doit correspondre à un théorème dans le modèle, et tout ce qui était T-faux dans la théorie T, doit correspondre à une proposition fausse dans le modèle. Et cela donc pour tout modèle de la théorie.
Si on a deux modèles de la même théorie T, disons M1 et M2, et un énoncé de la théorie est une proposition vraie dans M1, et une proposition fausse dans M2, alors cet énoncé doit donc être T-indécidable. Car s'il était T-vrai, son interprétation dans M1 aussi bien que son interprétation dans M2 devraient être vrais, et on dit le contraire.
Jusque là, ça va.
Mais ce que je n'arrive pas à saisir, c'est qu'on dit que tout énoncé, donc aussi les énoncés T-indécidables, devraient être vrais ou faux dans un modèle. Un modèle peut quand-même aussi contenir des énoncés indécidables ? D'ailleurs, la seule façon d'avoir un modèle, c'est quand-même de l'identifier à une autre théorie, sinon on ne peut rien dire concernant les énoncés du modèle et ne pas savoir s'ils sont vrais ou faux ou qu'ils n'ont pas été décidés ?
On a juste travaillé de façon plus informelle, mais avec l'idée que derrière, il y a quand-même une formalisation qui était implicite ?
Si je dis que "les entiers naturels" sont un modèle pour PA, alors ce que j'entends par "entiers naturels" est une façon informelle de parler, éventuellement, d'une autre théorie que j'ai nommé "entiers naturels", non ? Sinon, je ne saurais pas ce qui pourrait bien être vrai ou faux concernant "ces entiers naturels" ? Et qui me dit que la théorie que j'ai implicitement de ces entiers naturels, soit complète ? Il y a donc bien des énoncés concernant mon "modèle" des entiers naturels qui ne sont ni vrais ni faux et qui sont tout aussi indécidables, non ?
Dans un modèle M, un énoncé est soit M-vrai, soit M-faux. C'est un fait non trivial.
Intuitivement, un modèle est une "situation" parfaitement connu.
Relis mon poste où j'interprète le langage de l'arithmétique dans $\mathbb N$ ; j'ai donné quelques idées sur la "vérité sémantique " sans parler ni de preuve ni de théorie.
Pour ce qui est (de la nature "réelle") des entiers naturels que l'on considère ... c'est un autre débat (tout comme le fait de considérer les modèles comme des "ensembles", etc. D'ailleurs, si quelqu'un a une preuve du théorème de complétude de Gödel sans utiliser l'axiome du choix, je suis preneur). Au besoin ouvrir d'autres fils, mais je préviens : je ne suis pas compétent !
NON, c'est un fait trivial.
Un langage comprend des symboles de fonction et des symboles de relation. Une structure pour ce langage est un ensemble $M$ avec des fonctions pour interpréter les symboles de fonction et des relations pour interpréter les symboles de relations.
Toute formule du langage a alors une interprétation dans la structure. Une formule à variables libres $x_1,\ldots,x_n$ a une interprétation qui est un sous-ensemble de $M^n$, et en particulier un énoncé (formule sans variable libre) a une interprétation qui est un sous-ensemble de $M^0$, donc soit "vrai", soit "faux".
Ok
Cordialement
Eh, ben c'est ça, justement que je n'arrive pas à saisir, qu'on puisse décréter que dans un modèle, tout énoncé "interprété" d'une théorie T "compatible" puisse avoir un statut de vérité. On le tient d'où, ce statut de vérité, à part d'une démonstration dans une autre théorie ?
Prenons effectivement $\N$. Ce qui est vrai ou faux pour une phrase dans $\N$, est quand-même purement dépendant de la théorie formelle (implicite quand on parle de $\N$ d'une façon "informelle") qui me définit, dans les détails, ce que j'entends par $\N$ ? Si 1 + 1 = 2 ou non ou est indécidable, dépend quand-même totalement de la théorie formelle (implicite) que j'ai décidé qui définissait $\N$ ? Alors, les énoncés dans cette théorie (qui me dit donc précisément ce que j'entends informellement par $\N$) peuvent donc aussi être indécidables et donc, si ces énoncés sont aussi exprimables dans la théorie T pour laquelle $\N$ est un modèle, tout aussi indécidables et donc ni faux ni vrais ?
$\N$ n'a quand-même pas d'autre signification que comme une autre théorie formelle sauf qu'on ne l'explicite pas ?
Dans ce que j'ai fait, je n'ai pas défini $\mathbb N$ par le côté syntaxique, mais au contraire il "préexiste", et on interprète dedans ce qui nous intéresse. On peut ensuite parler de la théorie de $\mathbb N$, comme étant l'ensemble de toutes les formules (du premier ordre, sur un certain langage, disons $\mathcal L_{ann}$) vraie dans $\mathbb N$, mais c'est une autre histoire.
On peut critiquer mon choix de définition de $\mathbb N$, mais je ne connais pas d'autres manières satisfaisantes de le définir en théorie des ensembles.
En dehors de cette théorie formelle, on ne saurait quand-même pas ce que c'est, $\N$ ? Cette théorie formelle qui sert à dire ce que $\N$ pourrait bien vouloir dire, est quand-même alors tout ce qu'on peut en savoir ?
Le $\N$ pré-existe, ça ne veut quand-même rien dire ? Ou tu veux parler "dans la physique" ? Sans définition formelle, on ne peut quand-même pas parler de $\N$ et donc certainement pas attribuer des valeurs de vérité à des énoncés concernant $\N$ ou ces éléments ?
Tout énoncé du langage a une valeur de vérité dans ce modèle, vrai ou faux.
Exemple : un modèle de la théorie des groupes. c'est un groupe. Dans un groupe, l'énoncé $\forall x\forall y\ xy=yx$ est vrai ou faux : le groupe est abélien, ou il n'est pas abélien. Point barre.
Un modèle de l'arithmétique de Peano (du premier ordre), c'est un ensemble $N$, avec un élément $0$, une fonction $s:N\to N$ et des fonctions $+,\times : N\times N\to N$ pour lesquels les axiomes de Peano sont vrais. Et dans un tel modèle, tout énoncé du langage de l'arithmétique est soit vrai, soit faux. C'est tout de même bizarre qu'une telle trivialité pose problème.
Tu es visiblement très troublé. On va prendre un cadre beaucoup plus simple. Les objets avec lesquels je vais travailler seront des ensembles d'une théorie des ensembles qui te convient. Je considère un ensemble $E=\{a, b\}$ à deux éléments. Je considère maintenant le langage $\mathcal L_{ann} = \{0, 1, +, \times\}$. Je considère l'interprétation suivante de mon langage dans $E$ : l'interprétation de $0$ est $a$, l'interprétation de $1$ est $b$, l'interprétation de $+$ est la fonction $f=\{((0,0),0), ((0,1),1), ((1,0),1), ((1,1),0)\}$ et l'interprétation de $\times$ est la fonction $g=\{((0,0),0), ((0,1),0), ((1,0),0), ((1,1),1)\}$.
Quel que soit l'énoncé $\varphi$ écrit dans mon langage $\mathcal L_{ann}$, je peux me poser la question de si cet énoncé, interprété dans $E$ est vrai ou faux, et cette question aura toujours une réponse. La vérité (on parle plutôt de satisfaction) d'un énoncé dans une structure est définie récursivement (j'ai la flemme de tout taper, mais par exemple l'énoncé $1=0$ est faux dans $E$ car $a \neq b$, tandis que l'énoncé $(1+1)+1=1$ y est vrai car $f(f(b,b),b)=b$), mais il est important de comprendre que tout énoncé a ainsi une valeur de vérité dans une structure donnée.
"Tout énoncé du langage a une valeur de vérité dans ce modèle, vrai ou faux."
Je ne comprends pas d'où viendrait ce statut de vérité, autre que de la théorie qui définit notre modèle (qui n'est pas la théorie *pour laquelle* on est en train de trouver un modèle).
et
@poirot:
" le statut de vrai ou faux dans un modèle n'a rien à voir avec une démonstration formelle"
je ne comprends pas cette idée. Comme nous ne sommes pas dans "la réalité physique" où on peut faire une expérience, mais dans un monde abstrait, "vérité = démonstration" est la seule source de "vérité" quand même ? Sinon, "vérité" ne veut rien dire, car il n'y a pas d'autre façon de potentiellement établir cette vérité ?
Dans ton exemple trivial, le modèle spécifique avait lui-même une théorie formelle complète, donc oui, cette théorie-là, utilisé comme modèle, était complète. Il y a donc dans ton exemple "la théorie T1 de l'anneau", et puis, il y a une autre théorie, T2, celle qui nous définit un anneau sur {a,b}. T2 est bien une théorie complète, et peut fonctionner comme modèle pour T1. Mais il fallait bien avoir T2 pour avoir un modèle en premier lieu. Souvent, des théories sur un ensemble fini sont complètes. T2 était T1, augmenté par un axiome: il y a deux éléments dans l'ensemble de base. Avec cet axiome supplémentaire, T2 devient complet.
Mais, et cela revient au début du fil, justement, et mon problème que je voulais exposer, mais pour ne pas faire un message trop long, je le dis en étapes. Je voyais les choses ainsi:
Imaginons que pour moi, $\N$ est *défini* comme étant Péano. Je ne saurais pas ce que $\N$ peut bien être, si ce n'est pas à partir de Péano. Gödel me dit que, dans ce $\N$, il y a bien des énoncés, formulables dans le langage Péano, qui ne seront pas démontrables. Pour moi, donc, ce sont des énoncés dans mon $\N$ qui n'ont pas de statut de vérité, et je me dis donc que je peux maintenant CHOISIR si je veux qu'ils soient vrais ou faux. Je peux définir un nouveau $\N_1$, dans lequel j'ai choisi que cet énoncé est vrai, et définir un autre $\N_2$, dans lequel j'ai choisi que cet énoncé serait faux. Par donc, un nouvel axiome, Péano + G ou Péano + not(G). J'ai maintenant deux "systèmes de nombres entiers naturels" légèrement différents. Les deux sont des modèles pour Péano. Ils conviennent tous les deux pour satisfaire l'intuition de base que j'avais vaguement pour "nombre entier naturel (compter des vaches)".
Mais Gödel me dit que dans $\N_1$, il y a à nouveau un énoncé qui est indécidable et un autre dans $\N_2$. Je peux maintenant choisir de nouveau si je décide qu'il soit vrai ou faux, cela me fera 4 différents systèmes de nombres naturels, $\N_{11}$, $\N_{12}$, $\N_{21}$ et $\N_{22}$. Ces 4 différentes versions des nombres naturels sont tous les 4 des modèles de Péano.
Etc...
Une théorie est donnée par ensemble d'énoncés (ses axiomes). Une théorie ne définit pas un modèle ; ta phrase n'a pas de sens. Un modèle d'une théorie est une structure pour le langage de la théorie dans laquelle les axiomes sont vrais.
Chaque groupe est un modèle de la théorie des groupes.
Tu sembles avoir des préjugés dont tu ne veux pas démordre, tu refuses complètement tout le calcul des prédicats et la théorie des modèles et tu préfères continuer ta logorrhée. Tu es inaccessible à une discussion scientifique sur ce sujet.
Sur ce constat d'échec, je sors.
Je tente de te convaincre une dernière fois puis j'arrête : je me donne un langage $\mathcal L$ et $M$ une structure sur ce langage. Pour tout énoncé $\varphi$ sur $\mathcal L$, je peux définir récursivement une valeur de vérité dans $M$, qui voudra dire si $\varphi$ est vraie ou non dans $M$. En particulier, il n'y a pas de "formule indécidable dans $M$", une formule y est vraie, ou fausse, point. Au-delà de la définition formelle, ça devrait être intuitivement trivial que, une fois mon "univers" $M$ fixé, une formule y est soit vérifiée, soit non vérifiée. Si ça ne te paraît pas évident, je te laisse relire la définition récursive d'une formule.
Tu me rétorques que mon exemple simple avait déjà une théorie complète, mais c'est le cas de toute structure ! Et comme l'a dit GBZM, une théorie ne définit pas une structure, tout au plus on peut faire l'inverse, mais ce n'est même pas la question ici. Quand tu dis "$\mathbb N$ est défini comme étant Peano" ça ne veut rien dire, puisqu'il existe une infinité de modèles de Peano. Pour la $n$-ième fois, tu confonds la syntaxe (les formules qui constituent la théorie dite "axiomatique de Peano") et la sémantique (les modèles de cette théorie, qui n'ont aucune raison d'être "le" $\mathbb N$, en particulier on sait qu'il existe des modèles non standards de Peano).
Une formule $\varphi$ est indécidable dans l'arithmétique de Peano si on ne peut trouver aucune déduction formelle de $\varphi$ ni de $\neg \varphi$ à partir de l'ensemble des formules qui constituent la théorie de Peano. Gödel nous dit qu'il existe de telles formules. Il n'empêche que quel que soit le modèle de Peano que je prends, une telle formule aura une valeur de vérité, vraie ou fausse. Et justement, d'après le théorème de complétude, il doit exister un modèle de PA dans lequel cette formule est vraie, et un modèle de PA dans lequel cette formule est fausse.
Je répare rapidement car j'ai vu que Patrick se voit reprocher une confusion à ce propos.
Patrick: je ne change pas ma version initiale, au cas où tu aurais passé du temps dessus, mais je te donne des traductions des choses qui semblent (sans les avoir lues, pardon) t'être reprochées.
EXIGENCE FONDAMENTALE dans ce que je t'ai décrit: tout objet est nommé. Et comme il peut y avoir une infinité...
Pour le reste c'est très simple:
1/ une théorie est un ensemble d'énoncés, dits "axiomes de la théorie" (pour simplifier, disons que ça voudra dire stable par règles*** de déduction)
2/ une Mhéorie (ce que j'ai appelé modèle) est un ensemble COMPLETS d'énoncés
3/ il t'est reproché de confondre Mhéorie et Théorie.
5/ être complet veut dire (en plus de morpher avec les connecteurs) pour toute phrase, en déclarer une des deux vraie et l'autre fausse.
6/ Le fait qu'existent des énoncés indécidables dans des théories diverses et variées est juste dû au fait que QUASIMENT TOUTES les théories récursivement énumérables sont INCOMPLETES. Tout ceci, ça se prouve, ce n'est pas évident".
7/ Dans ce paradigme, une Mhéorie M est un modèle d'une théorie T signifie juste $T\subset M$
Pour t'expliquer la dualité syntaxe/sémantique, attendre un autre jour de ma part :-D
*** il n'y en a que deux en fait, mais passons sur les amènagement pragmatiques qui vinnent en aval:
a/ Le modus ponens
b/ La conjonction inifnie: si tu sais prouver $R(a)$ sans connaitre $a$, ni faire aucune hypothèse sur $a$, alors tu as le droit de dire que tu as prouvé $\forall xR(x)$$
Et quand tu fais une ultrapuissance de modèle, qu'est-ce qui se passe ?
Bref, ni fait ni à faire, les modèles selon Christophe.