ZFC prouve la consistance de Peano

Cyrano

Dans la littérature, quand on rencontre l'expression $ZFC \vdash Cons(PA)$, j'ai le sentiment que deux interprétations sont possibles : 

1) Une vision méta : On se sert de ZFC comme théorie background, dès lors on a le droit d'utiliser une sémantique à base de modèles ensemblistes et on a accès à l'ensemble $\N$. A partir de là, il est facile d'exhiber un modèle de Peano et ainsi d'établir sa consistance. Je n'aime pas l'utilisation de $\vdash$ dans ce contexte car pour moi il est réservé aux preuves formelles au sein du système formel ZFC.

2) Une vision vraiment formelle qui justifie l'utilisation de $\vdash.$ Dans ce cas l'expression $ZFC \vdash Cons(PA)$ signifie simplement que ZFC prouve une formule interne au langage qui est un "code" arithmétisé de la phrase "PA est consistante". 

Ma question est la suivante : est-ce que 1) et 2) sont en fait équivalents ? 

Foys

Cyrano a dit :
Ma question est la suivante : est-ce que 1) et 2) sont en fait équivalents ? 

Oui parce qu'elles sont vraies toutes les deux.

Après est-ce que ces énoncés disent la même chose?

En fait dans les deux cas ZFC est utilisé en théorie background. Et le lien entre les deux énoncés est fait par le théorème de complétude de la logique du premier ordre qui est formalisable et démontrable dans ZFC (comme tous les énoncés de théorie de la démonstration en raison de la grande souplesse de ZFC). En conséquence de ça, par exemple, dans un modèle non standard de ZFC, "$\N$" est une certaine structure non standard satisfaisant tous les axiomes de Peano y compris les instances du schéma de récurrence qui sont elles-mêmes de longueur non standard

Il y a plus simple (conceptuellement, car en pratique ça doit être assez fastidieux): on a une preuve syntaxique de ce que si Peano est contradictoire alors ZF l'est aussi. Il y a une traduction de la logique du premier ordre sur le langage $(0,succ, +, \times)$ dans le langage de la théorie des ensembles (on définit $\N$ comme le premier ordinal infini etc) et on démontre chaque axiome de Peano via cette traduction; puis on prend une preuve de $0=1$ dans Peano et on la traduit suivant le même mécanisme.

Cyrano

En fait oui, ma question porte plutôt sur la signification, c'est une question semi-philosophique. J'essayais hier de me plonger dans la preuve technique du théorème d'incomplétude et tout ce que je voyais, en définitive, c'était une formule extrêmement compliquée à base d'une tonne de codes, qu'on nomme $CONS(ZFC)$ et qui est telle que $ZFC \nvdash CONS(ZFC).$ 

Tout ça est bel et bon mais est-ce que ça prouve vraiment en définitive que, partant de ZFC comme métathéorie, je ne pourrai jamais trouver de modèle ensembliste (naïf) du ZFC formel ? Autrement dit, est-ce que $CONS(ZFC)$ veut vraiment dire ce qu'elle est censée vouloir dire ?

Martial

@Cyrano : je n'ai pas bien compris tes dernières questions, mais ce qu'il faut savoir c'est qu'il existe plusieurs façons de définir Cons(ZFC). Tu peux la voir à la sauce Gödel sous la forme $\neg$ il existe une formule de 3 km de long telle que blablabla, comme tu l'expliques ci-dessus, mais tu peux aussi la voir comme $\neg$ il existe une démonstration de $0=1$ à partir des axiomes de ZFC. (Le tout étant, bien sûr, encodé dans l'arithmétique). L'équivalence entre ces 2 énoncés n'a rien de trivial, mais Patrick Dehornoy en glisse un mot dans son livre, et si mes souvenirs sont bons c'est assez compréhensible.

Concernant tes deux dernières lignes, je ne vois aucun espoir. Si ZFC est consistante, par complétude elle a un modèle, disons de cardinalité $\kappa$. Par Löwenheim-Skolem descendant elle a aussi un modèle dénombrable, disons $M$. Donc $M$ est en bijection avec $\mathbb{N}$. Tu peux donc voir $\in$ comme un sous-ensemble de $\mathbb{N} \times \mathbb{N}$. Et, comme il y a une bijection (récursive) de $\mathbb{N}^2$ sur $\mathbb{N}$, cela signifie qu'il existe une partie $R \subseteq \mathbb{N}$ qui témoigne de la consistance de ZFC. Mais, comme $R$ est "fortement non récursive", tu vas avoir du mal à l'exhiber.

AD

Pour persister à troller les discussions, bannissement de 24h de Samok, le temps qu'il reprenne ses esprits.
AD

Cyrano

@Martial : En fait je crois que mon problème est le suivant : 
$Cons(ZFC)$ (ou autre chose que ZFC d'ailleurs) est une formule arithmétique codant la phrase "ZFC ne prouve pas $0=1$" et ce suite à un codage bien particulier. Mais si ça se trouve, en utilisant un tout autre codage, la même formule arithmétique $Cons(ZFC)$ encodera quelque chose de bien différent et de bien moins intéressant que la première phrase.
Au final la formule arithmétique $Cons(ZFC)$ est-elle réellement intrinsèquement liée à la consistance de ZFC ou non ?

Alesha

Étant donné un certain encodage $c1$, on définit $Cons_{c1}(T)$ et on montre les théorèmes :

T1) On a $\mathbb{N} \vDash Cons_{c1}(T)$ ssi il n'existe pas de preuve formelle de 0 = 1 pour $T$.

T2) On a  $\mathbb{N} \vDash Cons_{c1}(T)$.

On a donc prouvé : il n'existe pas de preuve formelle de 0 = 1 pour $T$, et c'est ce qui nous intéresse. Même si $Cons_{c1}(T)$ n'est pas "réellement intrinsèquement liée à" la consistance de T et n'a peut-être aucun intérêt pour un autre encodage $c_2$, il n'en reste pas moins vrai que le théorème T1) a été prouvé une fois pour toutes (je veux dire même si $Cons_{c1}(T) = Trivial_{c2}$ et qu'on prouve  qu'on a $\mathbb{N} \vDash Trivial_{c2}$ ssi il existe une preuve formelle de 1 = 1).

Cyrano

@Alesha : Ok ça ça m'intéresse beaucoup. Je pensais que le théorème d'incomplétude de Gödel n'affirmait QUE T2. (Enfin, la version négative)
Tu pourrais me donner un embryon de l'idée de la preuve de T1 ?

Alesha

La définition de $Cons_{c1}(T)$ est basée sur l'existence d'une relation binaire $Preuve_{c_1, T} \subseteq \mathbb{N} \times \mathbb{N}$ qui satisfait la propriété suivante : pour tous entiers $n$ et $m$, on a $\mathbb{N} \vDash Preuve_{c_1, T}(n, m)$ ssi il existe une preuve formelle $\Pi$ dans $T$ de la formule $\Phi$ telle que $c_1(\Pi) = m$ et $c_1(\Phi) = n$.

La définition de cette relation binaire est fastidieuse, mais fondamentalement, si on considère une preuve formelle comme une suite finie de formules (satisfaisant de bonnes propriétés) et son encodage comme l'encodage de la suite des encodages des formules, alors on va avoir  $\mathbb{N} \vDash Preuve_{c_1, T}(n, m)$ ssi $m$ encode une suite correspondant bien à une preuve formelle et $n$ est le dernier entier de la suite encodée par $m$.

samok

Pardon, mais je ne comprends pas.
Qui comprend ?

Cyrano

J'ai à peu près compris grâce à Alesha.

Du coup j'en rajoute une couche avec une dernière question. Quand on dit que $ZFC \vdash Cons(PA)$ en général on procède comme suit : Soit $M$ un modèle de ZFC. Dans ce modèle on peut construire $\omega^M$ qui peut lui-même servir de modèle pour PA. Donc on a prouvé Cons(PA). Mais, me semble-t-il, en faisant ce raisonnement ce qu'on a prouvé c'est $ZFC + Cons(ZFC) \vdash Cons(PA)$ non ?

D'ailleurs, de manière générale, comme on fait cet acte de foi que ZFC admet un modèle, notre théorie background est tout le temps $ZFC + Cons(ZFC)$ non ?

Alesha

On peut affirmer $ZFC \vdash Cons(PA)$ par application du théorème de complétude : si on montre que, pour tout modèle $\mathfrak{M}$ de $ZFC$, on a $\mathfrak{M} \vDash \Phi$, alors on a $ZFC \vdash \Phi$.

Martial

@Cyrano : c'est exactement comme dit Alesha. Mais à mon avis ce qui te gêne c'est la question suivante : "Oui mais qu'est-ce qui se passe si par malheur ZFC est inconsistante ?".

La réponse est : RIEN. Ton théorème $ZFC \vdash Cons(PA)$ reste vrai mais il ne te sert plus à rien puisqu'alors $ZFC$ démontre n'importe quoi, y compris $Cons(ZFC)$. Donc dans ce cas tu n'a plus aucune certitude sur la consistance de Peano.

Cyrano

Ok donc en réalité, on est pas réellement obligé de faire l'acte de foi que ZFC est consistant. Au pire s'il ne l'est pas, les implications deviendront trivialement vraies car la prémisse sera fausse.

Foys

Il n'y a pas un seul moment où on est obligé de faire un acte de foi en maths, pour la simple raison qu'on déclare des axiomes. Par exemple en logique classique quand on a établi "$(A_1 \wedge A_2 \wedge ... \wedge A_n) \Rightarrow B$" (qui n'est rien d'autre que $(\neg A_1) \vee  (\neg A_2) \vee ... \vee (\neg A_n) \vee B $; où les $A_1,...,A_n$ sont mettons la liste finie des axiomes d'une théorie permettant les maths, comme la théorie des ensembles NBG par exemple), on a en fait établi la fausseté possible d'un des énoncés $(A_i)_{i= 1...n}$ et dans la sémantique des jeux, le défenseur de l'énoncé $(A_1 \wedge A_2 \wedge ... \wedge A_n) \Rightarrow B$ peut tout à fait choisir de jouer contre l'un des énoncés $(A_i)_{i=1 ... n}$.

La pratique de ZF (ou NBG, ou Peano etc) est in fine l'établissement d'un dossier à charge géant contre les axiomes de ZF (NBG, Peano ...).

samok

C'est une vision des choses.

théorème :  assemblage de symboles qui ne signifient rien mais vérifiant une syntaxe.

Mathématicien : producteur de théorème.

La preuve demeurera si par malheur tout est prouvable.

AlainC

Je dois être sûrement aussi con que n'importe quel collégien qui sait qu'à tout entier on peut toujours ajouter $1$ pour obtenir le suivant : y a vraiment besoin de tout ZFC pour ça?

Cyrano

Je me pose la question suivante : Dans Peano, la formule $\text{Cons}(PA)$ est indécidable. Ce n'est pas vrai dans une théorie du premier ordre $T$ quelconque. Sous les hypothèses habituelles on a seulement $T \nvdash \text{Cons}(T)$ mais on a pas nécessairement $T \nvdash \neg \text{Cons}(T).$ Peut-on créer une formule indécidable de $T$ à partir de $\text{Cons}(T)$ ?

Martial

@Cyrano : je ne comprends pas ta question. OK pour $T \not \vdash Cons(T)$. Venons-en à $T \not \vdash \neg Cons(T)$. On va distinguer deux cas.

1) Si $T$ est inconsistante, elle démontre n'importe quoi, y compris $Cons(T)$ et $\neg Cons(T)$.

2) Si $T$ est consistante et si elle démontre $\neg Cons(T)$, alors elle démontre un énoncé faux, donc elle est inconsistante, contradiction.

Conclusion : si $T$ est une théorie récursive, consistante et interprétant l'arithmétique, alors $T \not \vdash Cons(T)$ et $T \not \vdash \neg Cons(T)$. En d'autres termes, $Cons(T)$ est indécidable dans toute telle théorie.

En particulier je ne vois pas ce que $PA$ a de "spécial" par rapport à une autre théorie $T$.

Alesha

Martial a dit :

2) Si $T$ est consistante et si elle démontre $\neg Cons(T)$, alors elle démontre un énoncé faux, donc elle est inconsistante, contradiction.

Je ne comprends pas l'argumentation : que veut dire : "$\neg Cons(T)$ est un énoncé faux"? Il peut y avoir des modèles de $T$ où $\neg Cons(T)$ est vrai. En outre, par exemple, $Peano + \neg(Cons(Peano))$ est consistante et démontre $\neg(Cons(Peano))$ qui est faux dans $\mathbb{N}$.
Pour montrer que si $T$ est consistante et si elle démontre $\neg Cons(T)$, alors elle est inconsistante, il faut sûrement un argument plus subtil, non?

Foys

@Martial Soit $T$ une théorie consistante et récursive contenant PA. Alors $T$ ne démontre pas $Cons(T)$. Donc il existe des modèles $M$ de $T+\neg Cons (T)$. Soit $T':= T +\neg Cons(T)$. Alors $T'$ est récursive, consistante (elle a un modèle) et entraîne $\neg Cons (T')$ (car $Cons(T') \Rightarrow Cons(T)$ est une tautologie).

Oui c'est très étrange mais $\neg Cons(T')$ veut vraiment dire "il existe une preuve d'une contradiction de $T'$, peut-être de longueur non standard". Et tout s'éclaire.

Regarder aussi la modification par Rosser du théorème de Gödel (elle évite ces bizarreries) avec la phrase autoréférente suivante:  $R:=$ "s'il existe une preuve de $\lceil R \rceil$, alors il existe aussi une preuve plus courte de sa négation" et sa conséquence ("Théorème de Gödel-Rosser").

Cyrano

Ok donc c'est bien ce qu'il me semblait. En réalité le second théorème d'incomplétude de Gödel n'implique pas le premier, puisqu'il ne fournit pas explicitement un énoncé indécidable.

Alesha

Pourquoi ne veux-tu pas de $Cons(T)$? L'argumentation de Martial était peut-être maladroite, mais on a bien que $T \nvdash \neg Cons(T)$.

Cyrano

@Alesha : Il semble que non, puisque si $T = \text{PA} + \neg \text{Cons}(\text{PA})$ alors $T \vdash \neg \text{Cons}(T).$

Alesha

Pourquoi? Es-tu en train d'affirmer que $T \vdash \neg Cons(PA)$ implique $T \vdash \neg Cons(PA + \neg Cons(PA))$? 

Cyrano

Comme $T$ contient $\text{PA}$, $T$ prouve $\text{Cons}(T) \Rightarrow \text{Cons}(\text{PA}).$ Par contraposée, $T$ prouve aussi $\neg \text{Cons}(\text{PA}) \Rightarrow \neg \text{Cons}(T).$ Mais comme $\neg \text{Cons}(\text{PA})$ est dans les axiomes de $T$, par modus ponens on en déduit que $T \vdash \neg \text{Cons}(T).$

Alesha

 Est-ce que tu veux bien détailler le passage suivant?

Cyrano a dit :

Comme $T$ contient $\text{PA}$, $T$ prouve $\text{Cons}(T) \Rightarrow \text{Cons}(\text{PA}).$

Foys

@Alesha toute preuve dont les axiomes appartiennent à $PA$ est une preuve dont les axiomes appartiennent à $T$ (immédiat dans toutes les formalisations de preuve imaginables, systèmes de Hilbert, déduction naturelle etc)

Cyrano

Plus de détails sur ce fil https://math.stackexchange.com/questions/4056599/does-g%C3%B6dels-second-incompleteness-theorem-provide-a-specific-sentence-for-his-f
Clairement le second théorème d'incomplétude n'implique pas le premier.