Comments on Deux remarques sur l'intuition du théorème de Gödel

Ruxor (2016-05-12T08:36:41Z)

Non, je préfère vraiment dire qu'un système formel est « consistant » plutôt que « cohérent » (cohérent, c'est pour les faisceaux), et tant pis (ou tant mieux, en fait) si c'est un anglicisme.

Odile B (2016-05-12T06:01:43Z)

Bonjour

Merci pour vos articles très intéressants.

Juste une remarque formelle : dans celui-ci, je remplacerais "consistant" par "cohérent".

Bien cordialement, et librement

Ruxor (2016-01-05T18:20:47Z)

@ooten: Franck Wolff a bien raison : certes il y a une infinité d'axiomes de récurrence[#], mais chaque utilisation qu'on fait de la récurrence dans une démonstration donnée ne fait appel qu'à un nombre fini d'entre eux, et donc qu'à un nombre fini d'axiomes. (Tout simplement parce qu'une démonstration est finie : ce n'est tout simplement pas possible de faire appel à une infinité d'axiomes dans une seule démonstration.) C'est bien tout le cœur de l'argument.

(La seule exception c'est quand on démontre des « schémas de théorèmes », c'est-à-dire un modèle permettant de fabriquer des théorèmes, où là on utilisera potentiellement une infinité d'axiomes dans le schémas. Notamment l'affirmation que j'ai encadrée dans mon entrée. Mais si on imagine une démonstration d'une contradiction dans PA ou ZFC, elle utilise un nombre fini d'axiomes vu qu'il y a une seule conclusion.)

[#] Enfin, ça c'est dans PA, dans ZFC la récurrence s'écrit comme un seul énoncé, et ce sont d'autres axiomes (sélection et remplacement) qui sont des schémas infinis ; mais peu importe ici.

ooten (2016-01-05T17:05:39Z)

Je doute fortement de la validité de la proposition de Franck Wolff "Tout ce que est démontrable dans ZFC n’utilise qu’un nombre fini d’axiomes.". En effet quand on utilise l'axiome d'induction du premier ordre, c'est en fait une infinité d'axiomes qui sont invoqués. Sur la page wikipédia <URL: https://en.wikipedia.org/wiki/Peano_axioms#First-order_theory_of_arithmetic >, il est marqué : "In addition to this list of numerical axioms, Peano arithmetic contains the induction schema, which consists of a countably infinite set of axioms… The first-order induction schema includes every instance of the first-order induction axiom, that is, it includes the induction axiom for every formula φ.".

Franck Wolff (2016-01-05T13:36:42Z)

Ah ben oui tiens. Je n'ai pas relu un nombre de fois suffisant avant de lever le doigt. Sorry!

Ruxor (2016-01-05T13:27:22Z)

@Franck Wolff: Ben oui, c'est exactement ce que je dis…

Franck Wolff (2016-01-05T13:14:08Z)

>je suis prêt à admettre comme mathématiquement vrais et certains les résultats — au moins arithmétiques — dont j'ai une démonstration dans ZFC, et je me sentirais plus rassuré si j'étais certain qu'il n'y a pas de démonstration de résultats absurdes dans ZFC

Tout ce que est démontrable dans ZFC n’utilise qu’un nombre fini d’axiomes. « L’ensemble » de tout ce qui est démontré sera toujours fini. Il existera donc toujours un nombre fini d’axiomes « enveloppes » de ZFC suffisants pour atteindre tous les résultats obtenus avec ZFC.

Alors pourquoi s’inquiéter ?

Ruxor (2015-12-27T19:58:05Z)

@ooten: Oui, c'est tout à fait analogue : PA, ZFC, et ZFC + tel ou tel grand cardinal, sont des théories qui produisent des prédictions expérimentales, à savoir les choses testables sur les entiers de taille raisonnable. (Par exemple, « il n'existe pas de contradiction dans ZFC » est une prédiction expérimentale de ZFC + il existe un cardinal inaccessible. Et « il n'existe pas de solution non-triviale de x^n+y^n=z^n pour n>2 » en est une de ZFC et vraisemblablement PA.) Et on peut tester expérimentalement ces prédictions expérimentales.

En un certain sens, le fait qu'on ne trouve pas de contradiction dans ZFC peut être considéré comme une confirmation expérimentale de la théorie « ZFC + il existe un cardinal inaccessible » (après, la bizarrerie due au théorème de Gödel, c'est qu'à chaque fois, le fait de ne pas trouver de contradiction dans une théorie T pourra être considéré comme confirmation expérimentale d'une théorie T′ plus forte que T, mais que du coup, on a envie de croire que T′ est vraie, donc consistante, donc de postuler une théorie encore plus forte, T″, qui prouve que T′ est consistante, et on ne s'arrête jamais…).

ooten (2015-12-27T17:35:34Z)

@Ruxor: donc en fait on peut dire que si ZFC est consistant on ne pourra jamais le savoir alors que s'il est inconsistant on a un espoir de le découvrir un jour. Ca me fait penser aux théories expérimentales qui sont vraies tant qu'elles ne sont pas contredites par l'expérience mais qui doivent être testées sans arrêt pour les renforcer ou pas.

Couard reviens (2015-12-24T01:46:34Z)

Pour toute grammaire contextuelle / dépendante du contexte / context-sensitive, on a toujours su trouver un algorithme polynomial pour la parser… et pourtant on sait qu’il n’existe pas d’algorithme polynomial pouvant parser toute grammaire contextuelle.

jonas (2015-12-24T01:13:42Z)

I might have an intermediate position between ultrafinitism and considering ZFC as real, including allowing ultrafinitism but not the full ZFC. I think that there's some large enough cardinal that gives an upper bound for what we can physically test, and any statement that involves sets bigger than this can't have physical consequences. The cleanest version of this would be if the universe was computationally as powerful as a Turing-machine, so you could test anything that involves a finite computation, but not anything higher than that. However, given that we don't know physics enough, I can also imagine that the real world has a power larger or smaller than that. Larger if the extended Turing thesis fails and we can (in theory) measure something more powerful than an ordinary computer can; smaller if the universe only does a finite and bounded amount of computation until its death by running out of entropy, after which any physical statement becomes meaningless.

The argument that “si les ensembles n'existent pas vraiment, comment se fait-il qu'ils prédisent des choses vraies sur des entiers sur lesquels on peut tester” is interesting, but I think it ultimately doesn't work, because of the unbounded quantization in those statements. Imagine one of those statements, which claim for example that some natural number x has the property P(x), where P is computable for any x. I take a Turing-equivalent computer, and I run it. If the statement is true in the real world, then I will find that the computer halts, but in that case it halts after a finite number of steps, one that can be defined in Peano arithmetic exactly by tracing the run of the program. If that is the case, then Peano arithmetic already proves this statement. Else, if the statement is false in the real world, then I will never see the computer halt, but I'll also never know that it won't halt in the future, so the statement does not have a physical meaning. If I only observe that the computer has not yet halted at a particular time, that reflects only a statement that Peano arithmetic can prove, not the full statement.

In any case, ZFC is interesting enough to me that it's worth to study its mathematics, even the parts that aren't relevant to the physical world. I certainly hope that it has no contradiction, even though we can never be completely sure about this.

If we do find a contradiction though, then I think that would be a big problem that we won't be able to solve by just minor adjustments. I believe that the consistency of ZFC is robust to a certain types of minor adjustment: namely removing the axiom of choice and the axiom of foundation, which can't affect its consistency. (I think we have proofs for this, even proofs not using those two axioms, but I'm not quite sure.) The rest of ZFC apart from those two axioms is there for a very good reason, used a lot, and it's hard to imagine any minor modification that can change consistency and doesn't affect most of mathematics.

VéDé (2015-12-23T22:54:22Z)

J'essaye d'apporter d'autres positions sur ce débat en réagissant à certains points.

« Je trouve que cela illustre très bien la manière dont on a tendance à mal se représenter le théorème d'incomplétude comme traduisant un problème profond de « manque de force » »

Cette tendance est justifiée par le fait suivant: PA² prouve la consistance de PA de manière plus subtile qu'en la postulant simplement. PA² contenant PA, la preuve (formelle) de consistance de PA nécessite bien un système plus fort.

« on ne se fatigue pas à vérifier par ordinateur si par hasard on ne peut pas trouver x,y,z,n tels que x^n+y^n = z^n »

C'est peut-être une des raisons pour lesquelles on n'a jamais trouvé de contradiction dans PA/ZFC/etc.: on n'en cherche pas ! La robustesse d'un système ne se justifiant pas par l'absence de contradiction en faits uniquement.
Sans compter que les preuves informelles ne sont formalisées que depuis peu (et pas souvent dans ZFC). Donc jusque là on n'était même pas sûr qu'elles étaient bien formalisables dans un système donné, et donc pas en bonne position de trouver une contradiction formelle.

« comme on a torturé ZFC dans tous les sens pour tenter d'y trouver une contradiction »
Connais-tu des exemples/noms/articles ?

Il me semble que «La position des ultrafinitistes» décrite ressemble davantage aux arguments défendant les logiques paraconsistantes. Je crois que la vision ultrafinitiste est plus pragmatique: par exemple de très grands nombres ne sont accessibles que par leur expression syntaxique qui est elle finie. Il doit donc bien exister un moyen fini de parler de tout ça, ce qui doit faire débat et engendrer diverses formes de finitismes (dont l'ultra).

« si les ensembles n'existent pas vraiment, comment se fait-il qu'ils prédisent des choses vraies sur des entiers sur lesquels on peut tester ? »

J'imagine qu'on peut faire une analogie avec «la déraisonnable efficacité des mathématiques» dans les sciences expérimentales, qu'on peut expliquer par un effort intellectuel d'appréhension d'événements physiques dans un langage humainement compréhensible et manipulable, langage sur lequel on peut raisonner et donc prévoir.
Et quand les prévisions ne sont pas vérifiées par l'expérience, on change les fondements mathématiques de la théorie physique. En maths c'est pareil: on changera ses fondements.
Et puis il faut aussi se rendre compte que cette phrase n'est pas un très bon argument: il ne suffit pas que la notion d'ensemble formalisé dans ZFC permettent de «prédire des choses vraies» mais qu'elle puisse ne «prédire» que ça (i.e. ZFC cohérent) !

Au passage:
- Serait-il possible d'avoir des pointeurs sur la méthode de construction d'un théorie T qui affirme sa propre consistance par un axiome (sans que ce soit une nouvelle théorie T+) ?
- À partir de quand est (ré ?)apparue la «position pratique du mathématicien en exercice» ?

À propos de la dernière question, il y a eu une crise des fondements au début du 19e siècle, des écoles formalistes, anti-formalistes (dont l'intuitionnisme), finitiste (Hilbert ?), etc., et maintenant on reviendrait à du tout mou (et voulu en plus) ? C'est vrai juste en France ou ailleurs aussi ? Aux États-Unis on dirait qu'il y a une conscience de l'importance des fondements des mathématiques (chez les mathématiciens): par exemple Voevodsky et ses «Univalent Foundations of Mathematics» qu'il semble mettre en place pour se prémunir de l'erreur dans son domaine de recherche (l'intuition semble n'y pas suffire), tout en insistant sur l'aspect praticable du système formel.

Ruxor (2015-12-22T21:46:46Z)

@ooten: Ah ben ça c'est la question à beaucoup de zorkmids… La réponse courte est qu'on n'en sait rien ; mais plein de gens ont plein d'arguments à proposer selon le plan sur lequel on se place (mathématique, philosophique, épistémologique, heuristique…), selon leur inclinaison philosophique (plus ou moins platonicienne, plus ou moins formaliste, plus ou moins finitiste), et selon qu'on parle de PA, de ZFC (qui est strictement plus fort), ou encore de ZFC + tel ou tel axiome de grands cardinaux (qui est encore plus fort). Voici quelques uns des points de vue qu'on peut proposer :

✱ D'abord, mathématiquement et « officiellement », on n'en sait rien : l'orthodoxie mathématique est « sauf précision expresse du contraire, on travaille dans ZFC, on appelle "théorème" ce qui est un théorème de ZFC dont la démonstration est publiée dans la litérature mathématique, et Consis(ZFC) n'en est pas un, en tout cas on ne peut pas l'utiliser dans un raisonnement mathématique (sauf à le préciser explicitement) ; et d'après le théorème de Gödel, on sait qu'on ne pourra jamais le démontrer sauf si, en fait, il est faux ». ✱ Ceci est proche du point de vue formaliste qui, à l'extrême, est : « les mathématiques ne sont de toute façon qu'un jeu typographique dont les règles sont fixées par ZFC et qui n'a aucun rapport avec la réalité, et peut-être que les règles permettent de fabriquer le théorème 0=1, qui est alors la conclusion ultime qui met fin au jeu, et nous n'avons aucun moyen de le savoir (et si ça se produit, on passera à un jeu différent) ».

✱ La plupart des mathématiciens (au moins ceux qui ne sont pas ultrafinitistes, et même ceux-ci dans une certaine mesure que je ne comprends pas très bien) pensent qu'il y a a quelque chose de « vrai » dans les mathématiques, donc que si ZFC, ou en tout cas PA, démontre un énoncé sur les entiers naturels qui peut être testé algorithmiquement, alors cet énoncé est vrai. Par exemple, maintenant qu'on a une preuve de ∀x,y,z,n∈ℕ n≥3∧xyz>0 ⇒ x^n+y^n≠z^n (le théorème de Fermat) dans ZFC (et vraisemblablement dans des systèmes plus faibles même si personne n'a vérifié de bout en bout), on ne se fatigue pas à vérifier par ordinateur si par hasard on ne peut pas trouver x,y,z,n tels que x^n+y^n = z^n : on admet donc que ZFC dit, au moins dans une certaine mesure, au moins dans ce cas, des chose vraies — du coup, la question intéressante n'est pas « [pourquoi] ZFC est-il non-contradictoire ? » mais « pourquoi ZFC dit-il des choses vraies ? » (et s'il ne dit que des choses vraies, au moins en arithmétique, il ne va certainement dire que 0=1).

✱ La position des plus platoniciens est la suivante : ZFC n'est pas contradictoire parce qu'il est complètement *vrai*, les ensembles existent vraiment (en un sens idéal), notamment les grands infinis, et ZFC dit des choses vraies à leur sujet (il dit la vérité, et rien que la vérité, mais il ne dit pas toute la vérité : il faut ajouter des axiomes de grands infinis, et aussi sans doute des axiomes sur l'« épaisseur » du monde des ensembles, et même comme ça, on n'aura évidemment jamais fini car la vérité est inépuisable par une théorie axiomatique, mais on peut quand même aller nettement plus loin que ZFC).

✱ La position des ultrafinitistes, si je la comprends bien (ce qui n'est pas certain) est quelque chose comme ceci : ZFC est probablement inconsistant, et même PA probablement. Il se trouve qu'on peut quand même en tirer des conséquences justes parce que la contradiction dans ZFC/PA est subtile alors que beaucoup de raisonnements qu'on peut mener dedans, tant qu'ils ne font pas intervenir des nombres trop grands ou des infinis trop bizarres, seraient recopiables dans un système beaucoup plus faible et non-contradictoire car vrai (car portant uniquement sur des entiers de taille raisonnable, et dont les axiomes seraient donc essentiellement « testables »). Mais [d'après ces ultrafinitistes, toujours] on finira par trouver des contradictions comme on en a trouvé dans la théorie des ensembles de Frege (pré-ZFC, et fondée sur essentiellement un seul axiome: « pour tout P, on peut former l'ensemble des x tels que P(x) »), qui avait pourtant l'air intuitivement sensée et qui supportait, de fait tout un tas de conclusions justes (comme beaucoup de travaux mathématiques pré-ensemblistes).

✱ Beaucoup de gens peuvent, évidemment, avoir une position intermédiaire entre ces deux dernières (« ZFC est *vrai*, les ensembles existent vraiment » et « ZFC n'est que superficiellement juste et probablement contradictoire, seuls existent les entiers naturels de taille raisonnable »). Toutefois, ces positions intermédiaires (et même, à mon avis, celle des ultrafinitistes) buttent dans une certaine mesure contre l'objection : « si les ensembles n'existent pas vraiment, comment se fait-il qu'ils prédisent des choses vraies sur des entiers sur lesquels on peut tester ? »

✱ Heuristiquement, on peut raisonnablement penser : comme on a torturé ZFC dans tous les sens pour tenter d'y trouver une contradiction, et qu'on a même étendu ses axiomes par des axiomes de grands cardinaux gigantesques, s'il y avait une contradiction, on l'aurait trouvée. Il serait très surprenant qu'une preuve de contradiction sur quelque chose qui est, au final, assez simple, soit immensément difficile à dériver et qu'on n'y soit pas arrivé malgré tout l'examen auquel on a soumis ZFC. (On a trouvé une contradiction dans un certain axiome de grands cardinaux, les « cardinaux Reinhardt », et encore, seulement contre ZFC, pas contre ZF seul, et surtout, elle était assez facile à exhiber, comme quand Russell a trouvé une contradiction dans la théorie des ensembles de Frege, donc on peut espérer que, heuristiquement, les contradictions dans les théories assez simples sont assez simples à trouver.)

✱ Dans le cas de PA (mais pas de ZFC), on a une preuve de non-contradiction, due à Gentzen, qui repose sur un principe combinatoire « simple » (en l'occurrence, le fait que l'ordinal ε₀ a bien un sens). (Bon, on a aussi une preuve de Consis(PA) dans ZFC, mais elle n'est pas très instructive, elle formalise juste l'argument « PA est vrai, or 0≠1, donc PA ne prouve pas 0=1 ». La preuve de Gentzen, elle, utilise des principes plus simples que ZFC, et surtout plus compréhensibles intuitivement.) Cette preuve s'étend à des systèmes un peu plus forts que PA (comme la théorie des ensembles de Kripke-Platek), mais on est très loin de ZFC à l'heure actuelle (on n'atteint même pas l'arithmétique du second ordre, c'est-à-dire essentiellement la théorie des ensembles restreinte aux entiers naturels et ensembles d'entiers naturels).

✱ Et, bien sûr, la position pratique du mathématicien en exercice, c'est généralement quelque chose comme : « on s'en fout complètement : si quelqu'un trouve une contradiction dans ZFC, ce sera sur un "problème légal", c'est-à-dire en utilisant un type de raisonnement qui n'apparaît jamais dans les mathématiques vivantes en-dehors de la théorie des ensembles, donc il suffira de corriger un peu ZFC et tout ce qu'on aura démontré restera correct ». (L'idée qu'on puisse trouver une contradiction dans PA, à cet égard, est sans doute beaucoup plus gênante, parce qu'il est difficile d'imaginer que ça ne mette pas à terre tout l'édifice des mathématiques existantes, quoi que les ultrafinitistes puissent dire à ce sujet.)

Voilà, maintenant sans doute que d'autres lecteurs peuvent apporter encore d'autres positions sur ce débat.

ooten (2015-12-22T18:26:02Z)

Mais alors comment savoir si ZFC n'est pas inconsistant. Je crois que tu avais dit grosso modo que depuis le temps qu'on fait des maths avec ZFC on aurait dû s'en rendre compte, mais je n'en suis plus sûr.


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: b619e9


Recent comments