Comments on De quoi parlent les mathématiques ?

Ruxor (2011-10-31T22:51:50Z)

Tiens, oui, Emmanuel Breuillard a fait une faute de logique… L'hypothèse de Riemann est effectivement une affirmation arithmétique Π_1 (c'est-à-dire de la forme ∀n.P(n) avec P(n) à quantificateurs bornés), mais il y a incontestablement des énoncés Π_1 dont on a démontré l'indécidabilité (le plus évident étant la consistance du système dans lequel on travail, disons ZFC). Le raisonnement qu'il avait en tête était sans doute : si l'hypothèse de Riemann est irréfutable, et en particulier si elle est indécidable, alors elle est vraie (parce qu'une réfutation est forcément testable sur un n particulier du ∀n.P(n)), donc si on a montré qu'elle est irréfutable alors on a en fait montré qu'elle était vraie — mais ce raisonnement passe sous silence que quand on dit irréfutable ou indécidable, c'est toujours en supposant la consistance du système sous-jacent.

ooten (2011-10-31T21:38:00Z)

Je suis tombé sur ce résultat qui me semble intéressant : <URL: http://www.math.u-psud.fr/~breuilla/DevoirMaisonRiemann.pdf > et qui affirme l'équivalence de l'hypothèse de Riemann avec la proposition 'Vn P(n)' qui est une proposition logique du premier ordre. Or d'après le théorème de complétude de la logique du premier ordre, alors ces propositions vrais sont démontrables (ou leurs négations si elles ne sont pas vraies). Donc on ne peut pas prouver que l'hypothèse de Riemann est indémontrable (je ne fais que lire le pdf mais peut être qu'il y a une faille là dedans), elle est trop simple pour ça !

damned tiger (2009-11-22T14:28:23Z)

Phi ? et sur Leibniz, et sur le baroque je lis quoi ? Pas facile de montrer patte blanche dans le paradis que Madore a créé !

phi (2009-11-22T09:26:20Z)

Argl, Deleuze et Serres, c vraiment pas ce qui se fait de mieux en philo des maths, même en français… cf. plutôt Russell, Cavaillès, Lautmann, Vuillemin, Dieudonné voire Desanti, Salanskis…

Sur le thm de Gödel, Smith (Peter) An introduction to Gödel's thms est vraiment très bien (quoique un peu court sur le 2e thm?).

Un certain D. Madore aussi avait écrit 2 textes intéressants sur le sujet…

damned tiger (2009-11-21T11:19:46Z)

Et si la mathématique parlait surtout de l'esprit humain à la recherche de la continuité, de l'infini quant la réalité se donne souvent de façon discontinue et finie ?
Deux livres pour ouvrir des perspectives : Le Pli Leibniz et le baroque de Deleuze et Le système de Leibniz et ses modèles mathématiques de Michel Serres.

DM (2009-11-10T07:10:30Z)

Je pense qu'une partie de la confusion autour du théorème de Gödel vient du fait qu'on pense généralement qu'on a initialement les axiomes à l'esprit, alors qu'en fait, initialement on a une intuition d'un modèle particulier (ou d'une classe de modèles) et qu'on pond des axiomes qui tendent à le définir.

Cela se voit particulièrement bien quand on propose des systèmes de règles censés permettre la résolution algorithmique de telle ou telle classe de problèmes: on a à l'avance la connaissance de la classe de problèmes, et on essaye de produire un système complet (toute proposition vraie dans le modèle est démontrable), correct (pas de proposition fausse dans le modèle mais démontrable), et où le test « est démontrable » est décidable.

Il me semble qu'une façon simple d'expliquer les idées de Gödel aux informaticiens non logiciens est de présenter l'ensemble des modèles comme la solution d'un problème de contraintes, représentées par les axiomes ou schémas d'axiomes. Plus tu mets d'axiomes, plus tu contrains le problème et tu précises ce que tu veux.

Je prends alors l'analogie avec les convexes. Un polyèdre convexe fermé peut se définir exactement par une famille finie de contraintes linéaires. Cependant, un convexe fermé quelconque nécessite en général une famille infinie de contraintes. Toute tentative de caractérisations exacte par une famille finie de contraintes échoue et conserve des « points en trop ». Finalement, ce que dit Gödel, c'est que pour tout système mathématique intéressant, l'ensemble des modèles est trop biscornu pour avoir une caractérisation aussi simple (ni même récursivement énumérable).

Ruxor (2009-11-09T22:34:02Z)

esteban → exp(π√163) est proche de 640320³+744 parce que l'invariant modulaire j (voir <URL: http://en.wikipedia.org/wiki/J-invariant >) évalué en (1+√−163)/2 vaut exactement 640320³ et que le développement en série j(τ) = 1/q + 744 + 196884q + 21493760q² + … (où q = exp(2iπτ)) est à coefficients entiers et converge très vite pour une telle valeur. Pour expliquer pourquoi j((1+√−163)/2) est exactement un entier (et même pourquoi c'est un cube), il faut faire intervenir le fait que le réseau complexe engendré par 1 et (1+√−163)/2 est à multiplication complexe (c'est-à-dire qu'il existe des similitudes autres que les homothéties qui l'envoient dans lui-même) et, mieux, est l'anneau des entiers du corps de nombres quadratique imaginaire de plus grand discriminant ayant nombre de classes 1 (voir notamment <URL: http://en.wikipedia.org/wiki/Ideal_class_group#Class_numbers_of_quadratic_fields >).

Ce n'est pas un phénomène isolé (exp(π√67), par exemple, est aussi proche d'un entier, puisque ℚ(√−67) a aussi un anneau d'entiers principal, c'est juste moins frappant, et ce l'est encore moins pour exp(π√43), etc), mais c'est le plus remarquable, pour cette explication, pour lequel on trouve vraiment un entier. Mais on peut trouver d'autres entiers algébriques en cherchant au-delà du nombre de classes 1 : par exemple, exp(π√427) est très très proche de 5280³·(236674+30303√61)³ + 744.

esteban (2009-11-09T21:48:27Z)

Inversement, connaissez-vous une "explication" qui ait une once de justification même heuristique au fait que exp(π√163) soit si proche d'un entier ? (Par "si proche" j'imagine que cela signifie que sans calcul numérique on aurait tendance à considérer qu'il faut commencer à considérer N bien supérieur à 163, pour espérer raisonnablement qu'il exite un k compris entre 1 et N pour lequel un des exp(π√k) soit proche à 10^-(le coef qui va bien) d'un entier). Bref, peut-on se dire qu'il ait une chance avant de faire le calcul numérique et comment ?

Ruxor (2009-11-09T14:22:04Z)

Touriste → Je trouve ta réaction typique de l'attitude que beaucoup de gens ont avec le platonisme en mathématiques (une sorte d'attitude un peu offensée, un peu « oh, non, moi je suis adulte, je ne crois plus au père Noël », bien *sûr* que les objets mathématiques n'existent pas ailleurs que dans nos têtes !, comme si on parlait de croire en Dieu), qui se montre aussi intransigeante que possible dès qu'on évoque un compromis (quoi, l'idée qu'on pourrait au moins croire aux très grands entiers naturels, mais c'est comme croire à l'intelligent design pour adoucir le créationnisme) et qui se fait souvent démentir par leurs réactions instinctives (si on ne croit pas aux entiers naturels, on ne peut pas dire que quelque chose est indémontrable, juste qu'on n'en a jamais trouvé de démonstration).

Rien ne dit, évidemment, que les réactions instinctives soient bonnes, ou que « bonne » ait un sens. Mais en tout cas, il ne faut pas caricaturer la position opposée : on ne prétend pas (en tout cas, je ne prétends pas) que les affirmations mathématiques soient des affirmations sur le monde « sensible », au sens où elles auraient forcément des répercussions physiques (même si prétendre qu'elles n'en ont forcément pas est audacieux aussi : il est difficile de dire avec aplomb que l'Univers n'est infini ni dans l'espace, ni dans le temps, ni dans la possibilité de subdiviser l'espace ou le temps, ni dans quelque autre dimension où l'ensemble des entiers naturels pourrait se cacher physiquement). Le point important n'est pas l'« existence » des entiers naturels, mais leur unicité (il existe un seul *bon* ensemble des entiers naturels, et dans celui-ci Consis(Peano) et Consis(ZFC) sont vrais, et *si* un objet de ce genre est physiquement réalisé, alors c'est celui-là). Je ne vois pas d'autre raison de croire à Consis(ZFC) ou même Consis(Peano) (si on ne croit pas que les entiers naturels très grands aient un sens possible, comment expliquer qu'on ne trouve jamais de démonstration de 0=1 dans aucun des systèmes même forts qu'on fabrique ? tant qu'ils font intervenir des concepts complètement imaginés, on ne comprend pas que ça nous bloque pour fabriquer une telle preuve). De façon semblable, j'attends qu'on me fournisse une explication quelconque pour la structure de l'ensemble de Mandelbrot ou le fait que exp(iπ√163) tombe si près d'un entier (constatations expérimentales sensibles) qui ne fasse pas intervenir une once de platonisme.

Arnaud Spiwack (2009-11-08T00:03:18Z)

La question du vrai et du faux me paraît très difficile à aborder. Les mathématiques s'attaque à des questions sur des objets infinis. Le sens de la question "est-ce vrai ou faux ?" pour ce genre de question me paraît délicat.

On pensera facilement à la question "y a-t-il des parties non-mesurables de ℝ ?" (j'omets volontairement des détails). Cette question n'admets pas de réponse dans ZF, et admet la réponse "oui" dans ZFC. En revanche il est naturel de considérer l'extension de ZF où la réponse à cette question est "non". Il ne me paraît pas sensé de considérer que l'une des deux extension a "raison". A ce titre il ne me paraît pas nécessairement légitime de décréter que l'un des deux énnoncés doit être vrai. Et en particulier de considérer que la question de vérité précède les maths (mais je ne crois pas non plus que ce soit pour ça que David pétitionne). Il est à noter, en revanche, que tout système de démonstration ne fait pas nécessairement des maths raisonnables et ZF+mesurabilité ainsi que ZFC sont d'accord sur une quantité raisonnable de choses plus ou moins nécessaires (il ne me paraît pas évident de spécifier celles-ci, bien que l'idée du calcul me paraît jouer un rôle particulier).

Dans le même genre, mais beaucoup plus troublant (ça nous ramène à cette histoire d'imprédicativité dont je parlais plus tôt, bien que de façon confuse, je le reconnais). Un des premier calcul des constructions (il y en a eu pas mal) qui peut porter le doux nom de "calcul des constructions inductives avec élimination forte", a une caractéristique assez funky : il prouve la négation du tiers exclu : ¬∀P.P∨¬P. Ces mathématique se font donc avec la supposition que non seulement on ne "devrait pas" pouvoir appliquer le tiers-exclu à tout va, mais qu'en plus ce serait incorrect (notons que ce n'est pas un axiome inséré arbitrairement dans la théorie, la théorie répond à des contraintes naturelles, et il se trouve (mais ce n'est pas évident en la regardant dans les yeux) qu'elle nie le tiers-exclu). A priori, en revanche, ça reste un système raisonnable pour faire des maths.

La notion de vérité me semble largement dépendente du tiers exclu. Je la manipule, personnellement, avec autant de précaution que possible.

Notons par ailleurs que pour PvsNP il peut, me semble-t-il, vraiment arriver des horreurs. Si on a une preuve de l'existence d'un algorithme polynomiale qui résoud SAT dans ZFC, alors on peut exhiber un tel algorithme (malgré le fait que l'existence dans ZFC ne permet jamais d'exhiber quoique ce soit). Il me semble que ce point est un exercice du Papadimitriou. Cependant cet algorithme ne peut pas nécessairement être prouvé polynômial dans une logique plus faible que ZFC (ZF-tout-court ou les mathématiques intuitionistes de Brouwer, par exemple). Il se peut, a priori (et si je ne dis pas de bêtise), que la question soit indécidables dans certaines théories, que P=NP dans d'autres et que P≠NP dans d'autres encore. Je ne sais pas ce que ça impliquerait en pratique, en revanche (à part que ce serait, sans doute, fortement désagréable)…

Touriste (2009-11-07T13:20:01Z)

Oki, merci pour ta réponse qui en effet clarifie totalement l'entrée de 10 heures 50. Celle-ci est un énoncé mathématique (la conjonction des cinq cas) et non un énoncé relatif au monde sensible, comme je l'interprétais. Comme énoncé mathématique, rien à redire, je suis en effet d'accord qu'en mathématiques P∨¬P. L'ambiguïté venait de savoir de quoi on parlait.

Entre temps j'ai un peu réfléchi à ce que j'écrivais pour voir quels présupposés implicites y étaient (avec ta classification extrêmement clarificatrice de l'article "Platonisme et mathématiques") je parlais comme si j'étais (0,2) platonicien, puisque j'avais un doute sérieux quant à la pertinence de donner un "sens" à l'énoncé Σ2 "P=NP" mais acceptais d'en donner un à l'énoncé Π1 "P=NP est indécidable dans ZFC" (en plus long : "Tout théorème de ZFC est distinct aussi bien de P=NP que de P ≠ NP"). Or je ne suis pas du tout sûr d'être réellement "(0,2) platonicien" voire sûr de ne pas l'être. Ma critique était donc horriblement naïve, inconsciente de ses présupposés : en acceptant que P=NP soit (dans le coin de la caverne de Platon où on stocke les théorèmes de ZFC) ou bien vrai, ou bien faux, ou bien indécidable, je faisais déjà trop de concessions. Je reviens en arrière et durcis mon scepticisme sur la notion de vrai/faux : même cette altenative à trois branches me semble une modélisation du monde sensible utile, comme toute modélisation, mais tout de même pas parfaitement adaptée.

Ruxor (2009-11-07T12:51:12Z)

Touriste → Concrètement, la différence entre les points 2 et 5 c'est que dans le point 5 on peut très bien avoir un algorithme qui marche parfaitement bien en pratique, qui résout vraiment toutes les instances de SAT en, je ne sais pas, n^42 opérations, mais juste on ne trouve aucune preuve du fait qu'il n'y a pas un cas tordu où ça ne marchera pas. Ça pourrait être, bien sûr, aussi, qu'un système plus fort que ZFC (et dans lequel on n'a pas moins de raison de croire qu'en ZFC, typiquement, ZFC + un grand cardinal) prouve les résultats que ZFC ne prouve pas.

Mais bon, de façon générale, il y a une différence entre vrai/faux et démontrable/réfutable. Ce n'est pas une question de platonisme (même si, pour un platoniste modéré, le vrai/faux au moins sur les entiers naturels a quelque chose d'intangible) : le fait qu'on ait P∨¬P (et même, ou exclusif) pour toute proposition P est un théorème de la logique du premier ordre, alors que (ZFC⊢P)∨(ZFC⊢¬P) (si « ⊢ » signifie « démontre », « démontre », et ZFC⊢P est un énoncé arithmétique) n'en est pas toujours un ; ce qui est un théorème, c'est (ZFC⊢P)∨¬(ZFC⊢P) (soit ZFC prouve P soit il ne le prouve pas) et (ZFC⊢¬P)∨¬(ZFC⊢¬P) (idem, pour ¬P). Si on admet (ZFC⊢P)⇒P et (ZFC⊢¬P)⇒¬P (qui ne sont pas, en général, des théorèmes de ZFC), on a quatre possibilités exclusives : soit ZFC prouve P (et alors P est vrai), soit P est vrai mais ZFC ne le prouve pas, soit ¬P est vrai mais ZFC ne le prouve pas, soit ZFC prouve ¬P ; et ceci (le fait qu'une et une seule de ces possibilités tienne) est un théorème formel (sous l'hypothèse que je viens d'indiquer), pas un énoncé philosophique.

Mais bon, le fait de ne pas voir à quoi correspondent le vrai/faux en-dehors du cas où quelque chose est démontrable ou réfutable, ça me semble un petit peu le monde à l'envers : le vrai et le faux, a priori, ce sont des choses auxquelles on veut tendre, et il n'y a aucune raison de penser que ZFC, ou la logique du premier ordre, suffit à les comprendre complètement. Et, de fait, Gödel nous assure que non.

Touriste (2009-11-07T11:24:38Z)

Ta réponse sur "P=NP" clarifie bien ta pensée… et me montre qu'elle est en total décalage avec mes intuitions, elle contient des présupposés sur la réalité dont je n'ai aucune perception naïve.

Je n'arrive pas à comprendre la différence entre ton point 2 et ton point 5 : ("P≠NP, mais ZFC ne le prouve pas," et "P=NP, donc il existe un algorithme polynomial pour SAT, mais ZFC ne prouve qu'aucun algorithme donné est polynomial et ne prouve pas non plus qu'il existe un algorithme polynomial").

Si je comprends bien, tu poses là une subdivision en deux sous-cas du cas P=NP est indécidable dans ZFC" mais je ne comprends pas ce qui les différencie. Si je pige bien, là tu supposes que la question "Est-ce que P=NP ?" a une réponse _non mathématique_, qu'elle concerne une réalité, un peu comme la question "Robert Boulin s'est-il suicidé ou non ?" ?

Ruxor (2009-11-07T09:50:04Z)

Concernant P=NP, les possibilités suivantes existent :

• P≠NP, et ZFC (disons) le prouve,
• P≠NP, mais ZFC ne le prouve pas,
• P=NP, donc il existe un algorithme polynomial explicite pour résoudre par exemple SAT, et ZFC prouve que cet algorithme est polynomial,
• P=NP, donc il existe un algorithme polynomial pour SAT, mais ZFC ne prouve qu'aucun algorithme donné est polynomial, mais il prouve quand même qu'il existe un algorithme polynomial,
• P=NP, donc il existe un algorithme polynomial pour SAT, mais ZFC ne prouve qu'aucun algorithme donné est polynomial et ne prouve pas non plus qu'il existe un algorithme polynomial.

Il me semble que c'est exhaustif.

yogsototh (2009-11-06T20:11:28Z)

@Fab et bien trivialement T' c'est T + l'axiome 'P ≠ NP'

Ca ne fait pas avancer beaucoup le shmilblick. A moins qu'il ne découle de T' un théorème utile.

Par contre j'ai adoré le principe. 'P ≠ NP' indécidable dans ZFC⇒ 'P ≠ NP' dans la réalité parce que :

réalité ⊆ ZFC.

Je ne suis pas certain qu'il y ait une inclusion de la réalité dans ZFC. Même si certains théorèmes sont de toute évidence trop fort pour la réalité (je pense aux ordinaux). Déjà parce qu'il est possible bien qu'improbable que ZFC soit incohérente (je ne suis pas sûr de moi ici). Mais aussi tout simplement parce que certain axiomes qui nous semblent aller de soi sont en fait faux en réalité. Est-ce que je me trompe en disant cela ?

Par contre je partage l'intuition.

valerio (2009-11-06T19:58:40Z)

> Arnaud Spiwack

oui, oui, je ne prétendais pas présenter autre chose que des spéculations, voire des divagations.

malgré tout, quand vous dites que "on n'a pas besoin de récursion pour ne pas terminer", citant l'exmple du lambda calcul, vous exagérez! l'appel d'une fonction à elle-même, même cachée sous un argument (λx.xx) relevait pour moi de la récursion, en mon sens "confus" tout au moins. le lambda calcul est bcp plus puissant que la L1.

même la simple notation fonctionnelle n'est déjà pas anodine: écrire f(g(x)) amène en L1 une quantif existentielle et impose un certain nombre de vérifications supplémentaires.

oui, le paradoxe de Russell s'exprime bien dans le lambda-calcul NON-TYPÉ*! la questions était: même avec un système aussi typé qu'on veut, dans quelle mesure est-il possible de régénérer le le paradoxe de Russell sous forme encodée et dans quelle mesure ça vaut comme paradoxe. si tel était le cas, un certain idéal logiciste serait vraiment totalement vain.

*ouais, enfin, pourvu qu'on postule la négation ou le faux: là encore, ça me semble quintopostulatoire.

Fab (2009-11-06T16:18:15Z)

@JML à propos de P vs. NP: à vrai dire, je ne m'intéresse pas vraiment au sens pratique/« réel » de la question (oui, c'est vrai qu'avoir un algo polynomial n'est pas forcément intéressant), mais plutôt aux questions de logique que ça soulève. Et je suis tout à fait d'accord sur le fait qu'il y a une erreur de logique dans mon raisonnement.

En fait , j'aurais plutôt dû dire : si je me place dans une théorie T fixée (par exemple ZFC), à supposer que celle-ci soit cohérente, soit il existe une démonstration de P diff. NP dans T, soit il existe une démonstration de P=NP dans T, soit il n'y en a ni d'un côté ni de l'autre (i.e., c'est indécidable dans T). Ou alors on réfute le principe du tiers exclu, mais je ne crois pas que ce soit compatible avec T=ZFC, par exple.

Et je ne dis pas qu'il existe une preuve dans T de l'une de ces trois assertions, je dis simplement que l'une de ces trois assertions est vraie.

Maintenant, si on suppose que la question (P vs. NP) est indécidable dans T : pas de démonstration de P=NP dans T. Alors inutile d'espérer pouvoir exhiber un algo poly. qui résout un pb NP-complet (car fournirait une preuve de P=NP). Et je n'hésiterai pas à ajouter : inexistence d'un tel algo (s'il en existait un, on pourrait toujours le trouver « par hasard », non ?). Donc : P diff. NP. Donc la question P vs. NP N'est PAS indécidable. Et c'est à l'avant-dernier « donc » que je commence à m'emmêler les pinceaux ! Si j'ai bien compris , il n'y aurait ici aucun raisonnement par l'absurde. Ce serait similaire à l'exemple de Ruxor :

« G n'est pas un théorème de l'arithmétique de Peano ; et, n'étant pas un théorème, il est vrai (puisque c'est ce qu'il dit). Ça ressemble aussi à une contradiction, mais cette fois ce n'en est pas une : G est vrai, mais l'arithmétique de Peano n'arrive pas à le démontrer — elle est trop faible pour ça. »

Donc admettons, la question P vs. NP peut toujours être indécidable dans T, et sans contradiction. Et mon raisonnement amènerait donc à l'idée que si P vs. NP est indécidable dans T, alors P diff. NP (et donc n'est plus indécidable) dans une autre théorie plus forte T'. Ma question est : c'est quoi, T' relativement à T ? Il y a comme un souci, car à aucun moment dans mon raisonnement je n'ai (implicitement ou non) ajouté un axiome à T, je n'ai fais que des suppositions et utilisé les règles de la logique classique, je n'ai imposé aucune règle. Et pourtant T' est sûrement différent de T, sinon j'aurais démontré par l'absurde que P vs NP n'est pas indécidable et ce dans toute théorie cohérente (tant qu'à faire, puisque je suis parti de T quelconque, hein), ce dont je doute un petit peu quand même ! Alors elle est où la faille ?? Qui peut me dire ce qu'est T' ici ?

Arnaud Spiwack (2009-11-06T12:04:15Z)

@Valerio:

Votre propos me paraît confu. Mais pour répondre à l'une de vos remarque. Il est raisonanblement notoire qu'on n'a pas besoin de récursion pour ne pas terminer.

Le λ-calcul est un tel exemple. Le terme (souvent dénoté par Ω) qui s'écrit (λx.xx)(λx.xx) ne termine pas. Pourtant le λ n'est qu'une opération d'abstraction. (pour ceux qui ne connaissent pas le λ-calcul, j'en précise la sémantique. (λx.u)v s'évalue en remplaçant tous les x dans u par v. En l'occurence donc, l'évaluation de Ω s'obtient en remplaçant tous les x de xx par (λx.xx), c'est-à-dire qu'Ω s'évalue en (λx.xx)(λx.xx) soit lui-même, et c'est parti pour un calcul long (surtout vers la fin)).

De plus on n'a pas besoin d'opérateur de récursion pour faire de la récursion. Le λ-calcul, toujours, a un terme (généralement appelé Y) qui fait de la récursion : λg.((λx.g (x x)) (λx.g (x x))) (exercice, prouver que Yg se réduit (presque) en g(Yg) .
Notons qu'on peut faire des trucs similaire dans des langages typés (on peut coder le point fixe avec des références et des exceptions par exemple)

Pour terminer le paradoxe de Russell s'exprime bien dans ce cadre. Dans sa portée logique (qui, sans type, est à peu près aussi cohérente que la théorie des ensembles de Frege) xy peut se lire comme y∈x. Le paradoxe de Russell s'écrit donc (λx.¬xx)(λx.¬xx) (qui pour les même raisons qu'Ω plus haut, ne termine pas).

valerio (2009-11-06T10:35:30Z)

ya un long chemin du "je ne suis pas prouvable" au thm de Gödel… l'un des points remarquables est que le thm vaut avec des hypothèses minimales (logique premier ordre, addition, multiplication), pas même de récursion (Peano).

<SPECULATION>
à 1ere vue, c contre-intuitif: un peu comme si on pouvait écrire un programme qui ne termine pas avec un langage sans structures de boucle ou de récursion. mais l'analogie est fausse à plusieurs titres. (1) les quantif existentiels font que ça correspond plutôt à des clauses Prolog non impératives. tant que ces quantif existentiels sont en nombre fini, un thm vrai est prouvable puisqu'il suffit de tester toutes les valeurs. Mais (2) l'infinité des entiers avec un codage adéquat (par addition & multiplication) permettrait de démultiplier les quantif existentiels au point qu'on ne pourrait plus tester toutes les valeurs même en zig-zag. mais c pas ça? Plutôt (3) les quantif universels réalisent une récursion tacite que le codage permet de rendre vicieuse. c ça?

autre interrogation: pourrait-on coder le paradoxe de Russell de manière similaire? là l'analogie informatique serait que si on permet des manipulations sur les chaines de caractères, on peut y recréer un langage de programmation et toutes les limitations de typage du langage de base seront contournées.
</SPECULATION>

yogsototh (2009-11-06T10:09:28Z)

Si j'ai bien compris, ce qui est en cause ici c'est la qualité du formalisme utilisé :

Soit il est trop fort comme ZFC, et il est dommage de ne pas utiliser toute sa puissance dans les "vrai" mathématiques.

Soit il est moins puissant comme Peano, mais dans ce cas tous les théorèmes sont quasiment certifiés comme correspondant à une réalité. Par contre travailler dans ce formalisme est plus difficile.

De sorte, l'article prône-t-il une recherche du "bon formalisme" ? C'est-à-dire celui qui est utilisé par les "vrai" mathématiques.

Ou au contraire l'utilisation maximale de ZFC pour peut-être avoir de bonnes surprises ? Même si c'est prendre le risque de s'éloigner des problèmes mathématiques plus proches de la réalité.

JML (2009-11-06T00:50:52Z)

@fab Je ne sais pas si P vs. NP est décidable ou non mais note bien qu'il y a une erreur dans ton affirmation «sinon on aurait P diff. NP, et ce ne serait plus indécidable» : que ça soit "vrai" ou "faux" en "réalité" ne change rien au fait que ça doit décidable ou non, ce qui ne dépend que de la puissance de ZFC à produire ce théorème ou son inverse.
Simplement si c'est "vrai" ou "faux" en "réalité", ben on peut espérer qu'un jour des gens auront construit un système plus fort pour démontrer des propositions concernant la réalité dans lequel cette proposition sera décidable.
Si c'est "P=NP" alors il existe des algos polys dont on ne peut démontrer qu'ils terminent en temps poly bien qu'ils le fassent en pratique. S'il existe des algos inconstructibles ça pourrait bien être "faux" en pratique (tant qu'aucune loi physique ne permet de les implémenter). Et de toutes façons poly ou non n'a de vrai sens qu'en tendant vers l'infini alors qu'en pratique il y a forcément une borne donc tous les problèmes sont linéaires si on admet la réponse "out of memory" ;) ce qui relativise la "réalité" de P vs. NP.
On aura gagné si on démontre P diff. NP (ça fait au moins une classe de problèmes qui sont intrinsèquements difficiles). Sinon on est emmerdé parce qu'au fond on a besoin soit de trouver des algos les plus efficaces possibles (y compris la constante) ; soit de montrer que tel problème a une complexité supérieure a tant (constante du terme dominant comprise) soit pour des applications crypto (temps de calcul min. pour craquer) soit pour montrer que l'algo qu'on utilise est proche de l'optimal et qu'on ferait mieux de se concentrer sur un autre objectif (typiquement se demander si la donnée n'a pas des propriétés particulières à exploiter dans le cadre d'une application).
Évidemment P = NP pourrait être lié à des propriétés ayant leurs applications, mais enfin si on a juste une preuve d'existence non constructive d'un algo poly dont l'exposant a la taille de l'univers on sera bien avancé…

JML (2009-11-05T19:03:12Z)

Ruxor -> hum je crois que tu es toujours dans l'expérience de pensée… Tu écris ton programme et tu lances ta machine :
1) elle continue à tourner… ça correspond à tes croyances sur le comportement du réel. Il s'agit d'une mise à l'épreuve de tes croyances (« ça fait 10 ans que ça tourne, comme prévu ») qui ne permet pas de conclure au-delà du fait que ce programme particulier tourne pendant au moins 10 ans, bon c'est toujours ça.
2) elle s'arrête : là tu as une information forte. Bug du programme, du système de preuve du programme, du hardware… ou de ZFC (preuve que ça s'arrête, finalement !), cas le plus intéressant.
Mais que je croie que 2 risque de se produire ou non, qu'est-ce que ça change ?
J'ai l'impression que ça ne change rien tant que ça ne s'est pas produit, et qu'en ce sens-là ces considérations sont déconnectées du réel (je parle du réel qui est concret et pragmatique et tout hein, pas des autres «réels» :) ).
Pour que cela devienne concret, il faudrait que tu puisses dire par exemple « sous l'hypothèse que 2 ne se produira jamais (pour toute proposition dans telle classe de propriétés indécidables par exemple), le programme suivant est correct », c'est-à-dire que de l'inexistence de points d'arrêts à d'autres programmes on peut tirer la correction d'un algorithme, ou une preuve d'arrêt, quelque chose qui nous donne concrètement prise sur le réel.
Que l'on puisse dire « ça a vraiment l'air de marcher » parce que mon moteur de recherche favori fait vraiment des trucs hallucinants.
Peut-être cela revient à demander : si l'on rajoute à ZFC un schéma d'axiome qui transforme des preuves d'indécidabilité en théorèmes d'inexistence de nombres entiers vérifiant certaines propriétés, est-ce que cela a des conséquences algorithmiques ?

Fab (2009-11-05T17:17:55Z)

J'ai une question assez prosaïque que j'aimerais vous soumettre, à propos de la « conjecture » P vs NP, quel est votre avis ? Serait-ce être bêtement platonicien que d'avoir l'espoir que P=NP ou P diff. NP (dans ZFC, admettons) ?
Et peut-on imaginer que ce soit indécidable ? Parce-que en partant de ce postulat, il devient impossible de trouver un algorithme polynomial qui résout un problème NP-complet. Et par la même occasion, on est obligé d'admettre qu'un tel algorithme existe (sinon on aurait P diff. NP, et ce ne serait plus indécidable). Ca semble contradictoire (à moins que je dise une connerie ci-dessus), mais j'imagine que ça ne l'est pas (j'avoue que je suis paumé). A moins que la question puisse être indécidable (toujours dans dans ZFC, par exemple) mais que ce soit impossible à démontrer ? C'est possible ça ?

J'avoue que tout ça me passionne, mais je me demande si ce ne serait pas dû à une forte incompréhension du sujet. Ca semble magique. J'ai l'intuition que si je commençais à comprendre, à démystifier le sujet, ça ne me semblerait peut-être plus vraiment digne d'intérêt !

Ruxor (2009-11-05T12:27:15Z)

JML → Les énoncés arithmétiques indécidables typiques dont on parle, oui, ils ont un sens très terre-à-terre : ils disent, si je lance telle machine de Turing (que je peux définir explicitement), alors elle ne s'arrêtera jamais. (On appelle ça un énoncé Π_1.) Typiquement : je lance une machine de Turing qui énumère les théorèmes découlant des axiomes de ZFC jusqu'à trouver une éventuelle contradiction — on pense fortement que cette machine ne s'arrêtera jamais, mais si c'est vrai ZFC ne peut pas le prouver. Je peux vraiment la programmer, cette machine, d'ailleurs en un sens c'est ce que font les mathématiciens au jour le jour…

JML (2009-11-05T09:03:26Z)

Hé bien cette discussion me passe complètement au-dessus de la tête…
Ce qui m'avait semblé bizarre dans la construction des maths, c'est la confusion entre "existence" et "utilisation" : je veux dire par exemple on montre qu'on peut construire une notion de produit d'ensemble (à base de (a,b)={a,{a,b}} ou un truc du genre) mais ceci fait on *utilise* cette construction-là au lieu de dire qu'on utilise une théorie avec des opérations formelles et des axiomes de plus (comme (a,b) = (a',b') <=> a=a' et b=b'), indépendamment de la manière dont on peut les construire ; un peu comme si la construction des maths avait été faite par des geeks ne jurant que pas l'assembleur au lieu de faire un boostrap qui s'élève de langages en langages de plus en plus haut niveau, pour tenter d'avoir le même niveau formel que le niveau de réflexion du mathématicien. C'est l'excellente remarque de Stroustrup : ce n'est pas parce qu'un langage permet d'utiliser un paradigme qu'on peut dire qu'il le supporte (on peut toujours tout faire avec un langage Turing-complet), il faut encore que sa syntaxe permette d'employer le paradigme facilement. Et de fait le mathématicien utilise un langage de haut niveau en pratique, mais il n'a pas le même statut de véracité que la preuve bas niveau… Ainsi si l'on apportait des changements à la théorie bas niveau il faudrait "recompiler" toutes les preuves de niveau plus haut même si les relations formelles sur lesquelles elles s'appuient demeuraient inchangées !

Pour moi les théorèmes de Gödel (et de nombreux résultats de logique un peu poussée) ça fait comme une savonnette : à certains moments j'ai pu avoir l'impression de bien les saisir… pour que ça me glisse entre les doigts l'instant d'après, comme s'il y avait un sens profond à tout ça que je n'arrive pas à attrapper, un message sur la vision d'ensemble des maths qui m'échappe.
Bon c'est contre-intuitif que des assertions sur les entiers puissent être indécidables. Mais est-ce qu'elles ont un sens à la base ces assertions ? Sont-elles connectées au réel, ou bien s'est-on aventuré sans s'en rendre compte que le terrain de la philo et du sexe des anges, où l'on a l'impression que l'on parle de quelque chose de précis alors qu'on est dans le vide complet ?
Ce qui est indubitablement réel, c'est quand des propriétés arithmétiques me permettent d'écrire des programmes : possibilité de construire tel nombre, impossibilité de tomber sur une condition qui fasse planter le programme. J'ai l'impression que les théorèmes de Gödel reviennent en pratique à prouver que certains programmes ne peuvent pas exister (aucun prouveur/réfuteur automatique de propositions générales qui répond en temps fini à tous les coups) du moins tant qu'on n'aura pas trouvé d'exploitation d'une loi physique permettant une infinité de calculs en temps fini, et que, si jamais ça se produit un jour, hé bien l'univers nous dira par la même occasion comment compléter la théorie…

Arnaud Spiwack (2009-11-04T13:16:50Z)

Il n'a peut-être pas tort d'insister. Ainsi il suggère, en ombre chinoise, d'autres façons de fonder les mathématiques. La "stratification" est le moyen traditionnel pour casser les paradoxes à la Russell des théories imprédicatives. Il ne me paraît pas fondamentalement clair que ce soit le seul moyen raisonnable, et on pourra espérer avoir d'intéressante surprises.

Il y a sans doute énormément de choses très intéressantes à dire sur les nombres de Conway avec la loupe de la théorie des ensembles. Mais l'argument c'est qu'il y a potentiellement des choses à dire qui y échappent. Évidemment vu de la théorie des ensembles ces "choses" peuvent paraître superficielles (bien que je n'aime pas trop cette tendance de dire "on se place dans une théorie des ensembles avec assez de cardinaux funky"). La question fondationnelle serait plutôt : y a-t-il un fondement qui leur donne un aspect plus profond.

Évidemment il ne paraît pas raisonnable de dire que ces questions sont une particularité des nombres de Conway, mais ils ont le mérite de donner un cadre de réflexion sympathique (c'est probablement moins austère que les catégories de dimension supérieur (à la Baez, par exemple) où ce genre de question réapparaisse). Peut-être qu'on pourrait mettre la réflexion sous l'angle de la remise en question de la notion de "taille" qui me semble typique à la théorie des ensembles (ainsi on a typiquement une catégorie des "petits ensembles" mais pas une catégorie de tous les ensembles), les théories imprédicatives semblent abolir ce genre de notion de façon assez radicale. Mais à ce stade de la réflexion je n'arrive plus vraiment à ordonner mes idées et je me suis bien assez écarté du sujet initial, donc je suppose qu'il me faut arrêter ici.

Fork (2009-11-04T12:44:03Z)

Moi aussi j'aime bien les nombres de Conway avec les opérations de Nim. C'est rigolo.

Ruxor (2009-11-04T01:01:41Z)

Sinon, concernant les Nombres de Conway, je les trouve très intéressants (même si je trouve ceux de caractéristique 2, c'est-à-dire fabriqué avec les opérations de nim, finalement plus intéressant que ceux qui sont totalement ordonnés et réel-clos), mais je trouve que c'est un peu bidon de dire qu'ils échappent au cadre de la théorie des ensembles. Conway les définit par un procédé inductif, qu'on peut arrêter à n'importe quelle étape ordinale, et c'est vraiment pile-poil le genre de choses que la théorie des ensembles sait bien manier ; il insiste pour mettre dans ses Nombres la limite après tous les ordinaux : du coup, évidemment, ça ne forme pas un ensemble, mais on peut dire exactement la même chose de *n'importe quel* procédé inductif strictement croissant, et je peux en trouver plein et ça n'a rien de remarquable. Ce serait intéressant si ses Nombres produisaient quelque chose de significativement nouveau à chaque étape ordinale mais, de mémoire, il ne se passe rien de remarquable (topologiquement ou algébriquement) après ω_1 ou quelque chose comme ça, donc vouloir itérer sur tous les ordinaux, c'est inutile (voire prétentieux). D'ailleurs, s'arrêter à ω_1 doit fournir un corps encore plus intéressant parce que, justement, il n'est pas trop gros. Une des leçons de la théorie des ensembles, c'est que la classe des ordinaux n'est qu'un ordinal comme les autres (vue depuis une théorie plus puissante, enfin, c'est un cardinal inaccessible[#]), juste qu'à un moment il faut décider de couper la hiérarchie.

[#] (Cette affirmation n'est exacte que pour ZFC du second ordre. Mais le lecteur s'en fout.)

Ruxor (2009-11-04T00:48:16Z)

rjolly → Concernant la théorie des types ramifiées de Russell, je recommande l'article <URL: http://plato.stanford.edu/entries/type-theory/ > (il arrive que la Stanford Encyclopedia of Philosophy contienne des articles mathématiquement intéressants, dans le domaine de la logique, et ceci en est un bon exemple). À mettre en perspective avec <URL: http://planetmath.org/encyclopedia/RussellsTheoryOfTypes.html > (qui est moins bon) et avec <URL: http://en.wikipedia.org/wiki/Intuitionistic_type_theory > notamment pour les théories à la Martin-Löf.

Les systèmes de types utilisés en informatique peuvent être arithmétiquement très forts. Si j'ai bien compris (ce n'est pas certain…), la preuve de la normalisation forte du système F (Girard) donne la consistance de l'arithmétique du second ordre (conjecture de Takeuti), qui est déjà au-delà de l'analyse ordinale (enfin, la dernière fois que je m'étais renseigné, Rathjen avait l'air optimiste sur le fait qu'il y arriverait). La thèse d'Alexandre Miquel (<URL: http://www.pps.jussieu.fr/~miquel/publis/these.pdf > donne plus de précisions. Le système Fω avec un objet pour les naturels (ou bien le système Fω.2 avec deux univers de types, permettant de mener la construction de Church) a apparemment la force arithmétique de l'arithmétique de Peano d'ordre supérieur ; avec trois univers de types, Fω.3, on doit avoir la théorie des ensembles de Zermelo d'ordre supérieur (V_ω2 en est un modèle) ; et avec le calcul des constructions est plus ou moins conjecturalement arithmétiquement équivalent à la théorie de Zermelo plus un axiome postulant l'existence d'une suite d'univers contenus les uns dans les autres (V_ω² en est un modèle). Ceci étant, tout ceci reste très faible par rapport à ZFC (c'est là qu'on se rend compte que ZFC est vraiment monstrueux).

Arnaud Spiwack (2009-11-04T00:30:51Z)

@David: Je te trouve un peu sévère quand tu prétends que les mathématiques n'utilisent pas la puissance de ZFC. Si comme tu sembles le croire (et ça me paraît hautement crédible) les preuves arithmétiques des mêmes énoncés n'ont aucune chance d'être intelligibles, un humain n'aurait pas pu faire de preuve sans ZFC. Alors ZFC est peut-être overkill (je pense qu'il est même crédible que ça finisse par être considéré comme un mauvais outil, mais c'est une autre histoire), mais bon, c'est tout de même sévère.

A propos des nombres surréels de Conway. Il s'agit d'un très joli morceau de presque-mathématiques. Ca ne s'inscrit que moyennement bien dans les théories des ensembles (on peut faire la plupart de ce qu'il présente dans une théorie des ensembles, mais ont refuse alors aux nombres surréels la généralité que Conway souhaite leur donner). En fait le nombres surréels s'inscrivent bien dans un cadre mathématique difficile (attention, keyword dropping : "induction-récursion", "imprédicativité"). Si difficile en fait qu'on ne sait pas trop à quoi il est censé ressembler (depuis l'échec (relativement cuisant) de Martin-Löf en 1971, les gens ne touchent à ce genre de choses qu'à reculons).

Pour répondre à la question sur les autres cadres que ZFC et Peano. Il y a d'autres cadres qui sont considérés comme acceptables (en fait superficiellement ils sont assez peu dicernables de ZFC (par exemple) donc pour le mathématicien moyen qui croit faire des preuves dans ZFC (voire ZF tout court) mais qui en fait ne le fait pas vraiment, ça ne fait pas franchement de différence). Les exemples venus de l'informatiques seraient HOL (théorie logique descendant de A. Church, mise en œuvre dans Isabelle par exemple) et les théories des types dépendants (dont les avatars modernes sont principalement Coq et Agda2) ; ces dernières se distinguant par leur cadre constructif - leur utilisation pour des mathématiques traditionnelles est de nos jours symbolisée par le projet Flyspeck, qui consiste à faire une version vérifiée par ordinateur de la preuve de T. Hales de la conjecture de Kepler. A noter que de nombreuses variantes de la théorie des ensembles seraient facile à faire accepter à son voisin (parmi celles-ci, on trouvera ZF+mesurabilité des parties de R, ZF+un cardinal inacessible, ou plus amusant, la substitution de l'axiome de fondation par l'axiome d'antifondation (grâce auquel l'ensemble qui se contient lui-même et uniquement lui-même, par exemple, est bien défini)).

Bref beaucoup de choses à dire sur ce qu'on appelle traditionnellement les "fondements" (et donc, comme l'a fait justement remarqué David, la quasitotalité des mathématicien se fout, à tort ou à raison).

yogsototh (2009-11-03T23:25:12Z)

J'avais déjà pris conscience de la conclusion de ce post. Je me suis d'ailleurs souvent demandé pourquoi, on n'utilisait pas quelque fois des "super mathématiques". Par exemple, pourquoi ne pas utiliser les nombres créés dans ONAG (On Numbers And Games). Avant de lire ce livre, seul Peano et ZFC existaient pour moi. Cette nouvelle construction des nombres m'a permis d'envisager la grande liberté "potentielle" dont disposent les mathématiques. Il est étonnant que les mathématicien en profitent si peu. Si ça se trouve, il y a des problèmes intéressant qui pourront être résolu dans des mathématiques différentes.

Je me souviens que par commodité, j'ai démontré des théorèmes via des théorèmes non constructivistes (Axiome de choix). Et que, par préférences, je les ai démontré à nouveau dans un cadre constructiviste. Quelque part ça m'ennuyais de laisser un théorème flotter dans une vérité qui me semblait floue. Surtout en informatique. Mais il est clair que c'était beaucoup plus facile à faire dans le cadre non constructiviste. Et il me semble que c'est souvent le cas.

Par contre je me demande comment serait reçue une preuve utilisant un autre cadre que Peano ou ZFC en précisant que tout n'est qu'une affaire de consensus ?

rjolly (2009-11-03T23:19:42Z)

Un fait que j'ignorais, que j'ai appris en suivant ce lien donné récemment par D. Monniaux : http://fr.wikipedia.org/wiki/Théorie_des_types , et qui intéressera certainement les informaticiens : "Une première théorie des types (dite "ramifiée") a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles".

Il y a en effet en ce moment une effervescence autour de la question de savoir quels sont les meilleurs languages, statiquement ou dynamiquement typés. Une question intéressante également est celle du rapport entre les prouveurs automatiques de théorèmes et la théorie de la compilation. Particulièrement, le fait de savoir si en compilant un certain programme dans un certain language (probablement statiquement typé), on n'obtiendrait pas une preuve d'un certain énoncé dans un certain système formel, et si oui, laquelle.

Après, je fais le lien avec ce que tu viens d'exposer, et je me dis que si par exemple une telle compilation donnait la preuve du théorème de Fermat, toutes les autres questions le concernant devraient être considérées comme oiseuses. Sauf que bien entendu, on pourrait remettre en cause le fait que le compilateur fait bien ce qu'il est censé faire, et ceci récursivement pour le compilateur du compilateur etc. Ca résume assez bien avec des mots informatiques ce qui vient d'être dit, je trouve.

Ruxor (2009-11-03T22:59:23Z)

Hélène → La majorité des mathématiciens non logiciens se foutent complètement de ce genre de questions, et/ou en ont peur. Mais il y en a quand même que ça amuse, ou qui s'y intéressent sérieusement.

Fork (2009-11-03T20:46:27Z)

Hélène → Je n'ai pas encore lu le post (arg, fichu manque de temps), mais mes réponses à tes questions seraient non / non / pas forcément.
Bon, je ne me base que sur mon expérience d'élève puisque je ne suis pas prof.

Ruxor → Je ne savais pas qu'il y a des énoncés indémontrables. Je suis d'ailleurs très heureux d'apprendre leur existence.

Hélène (2009-11-03T19:15:52Z)

J'aimerais juste savoir si connaître/maîtriser ce genre de choses est utile/indispensable/rare pour une personne qui enseignent les mathématiques dans le supérieur (la cryptographie, par exemple…), ou si c'est juste ton côté geek (en mathématiques) qui ressort. J'imagine que certains de tes collègues se contrefoutent totalement de Gödel et de ZFC (enfin, j'imagine mais je ne sais pas, c'est pour ça que je demande :)

Et je ne parle même pas de tes élèves de Télécom (l'École !) parce que je suis à peu près sûre de la réponse, les concernant…

Touriste (2009-11-03T14:39:27Z)

Il y a plein de présupposés extrêmement "platoniciens" dans ton exposition. Comme toujours dans ce genre de choses les passages où je bloque, ce sont sur les mots du langage courant utilisés dans des sens philosophiques assez techniques (des mots comme "existe", "vraisemblable", "croire") par exemple où le concept que tu utilises ne me semble pas recouper mon expérience.

Mon commentaire porte peut-être plus sur l'entrée "Platonisme et mathématiques" que ça me donne l'occasion de relire (en diagonale) que sur celle-ci, mais tout est lié… Le principal truc qui me gêne, c'est que tu formules des énoncés de philosophie de la connaissance en supposant qu'ils appellent une réponse binaire, sur le modèle des énoncés mathématiques vrais ou faux. Par exemple dans l'article "Platonisme et mathématiques" tu écris : "Il y a sans doute aussi des gens qui objecteront que la question de savoir si le 10↑(10↑(10↑100))-ième nombre premier se termine par 1, 3, 7 ou 9 (…) est une question dénuée de sens" ou ici tu écris : "l'idée, au moins atténuée, que les entiers naturels existent réellement".

Tu as l'air de présupposer que "avoir du sens" ou "exister" sont des concepts de nature binaire, en vrai ou faux. Or pour ma part la conception que j'ai de ces concepts, c'est qu'ils sont de nature plutôt ordinale, et ordinale floue dans le style des préférences en économie ; j'aurais tendance à dire "savoir si le 3ème nombre premier est 5 ou 7" est une question qui a PLUS de sens que "savoir si le 10↑(10↑(10↑100))-ième nombre premier se termine par 1, 3, 7 ou 9" qui a elle même PLUS ou MOINS de sens (selon mon humeur du moment :-)) que "savoir si mes lunettes sont posées à droite ou à gauche de l'écran". De même les entiers peuvent exister DAVANTAGE que les ensembles, mais l'entier "10↑(10↑(10↑100))" exister MOINS que l'entier "42", qui lui-même selon ce que j'ai mangé à midi existera PLUS ou MOINS que mes lunettes.

Et de même quand tu écris "croire à certains énoncés au-delà de ZFC" par exemple : ne peut-on y croire DAVANTAGE qu'à l'énoncé "Elvis Presley est vivant" mais MOINS qu'à l'énoncé "2 + 2 = 4". Pourquoi exiger des réponses binaires pour les choix de la vraie vie comme pour les questions de mathématiques ?

Nick (2009-11-03T13:51:24Z)

zyva! Comment il est prise de tête ton blog.
Tu ne veux pas plutôt nous parler de ce que tu penses du voile de Diam's ou de ton amour du chocolat? :)

Ruxor (2009-11-03T12:36:37Z)

ooten → Il existe des exemples d'énoncés arithmétiques indémontrables dans Peano qui ont une saveur un peu plus arithmétique et plus naturelle que celui de Gödel, par exemple le théorème de Paris-Harrington (<URL: http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem >) ou celui de Goodstein (<URL: http://en.wikipedia.org/wiki/Goodstein%27s_theorem >). Mais d'une certaine manière, ce n'est que du toilettage, au final on se ramène d'une manière ou d'une autre au théorème de Gödel (ou à l'induction de type ε0). Dans ZFC on ne sait même pas vraiment faire ça (l'ordinal de preuve de ZFC est beaucoup trop grand pour qu'on sache le décrire autrement), donc les énoncés arithmétiques indémontrables dans ZFC connus sont vraiment des variations minuscules autour de l'énoncé de Gödel ; il y a bien des techniques puissantes pour montrer que certains résultats de ZFC sont indémontrables (essentiellement, le forcing), mais ces techniques ne touchent pas aux énoncés arithmétiques.

En principe, n'importe quel énoncé vrai de l'arithmétique découle de Peano auquel on aurait ajouté « suffisamment » de niveaux de gödelisation (c'est-à-dire suffisamment de fois l'énoncé « le système <obtenu aux niveaux inférieurs> est cohérent » ou « …ne démontre que des choses vraies » pour enrichir le système), mais en fait c'est une arnaque parce que le « suffisamment » fait intervenir un certain ordinal (le ω1 de Church-Kleene), et toute la structure de la vérité des énoncés arithmétiques est codée dans celui-ci.

Il est plausible qu'il existe énormément d'énoncés indécidable pour lesquels on n'a, au final, aucune manière d'approche. Déjà on sait qu'il existe des énoncés indémontrables (vrais) dont l'indémontrabilité est elle-même indémontrable, et ainsi de suite (au moins jusqu'à n'importe quel niveau fini, ensuite je ne sais plus bien). Probablement beaucoup d'énoncés « naturels » sont de ce genre : on ne peut pas les démontrer, on ne peut pas démontrer qu'on ne peut pas les démontrer, et ainsi de suite (et si en théorie on peut s'en sortir comme expliqué au paragraphe précédent, en pratique ça ne nous avance à rien).

Gabriel (2009-11-03T10:10:43Z)

"Aus dem Paradies, das Cantor uns geschaffen, soll uns niemand vertreiben können."

Je traduirais plutôt par : "Du paradis que Cantor nous a créé, nul ne doit pouvoir nous chasser" (le "können" était passé à la trappe).

ooten (2009-11-03T09:56:57Z)

D'ailleurs la question que je me suis posé est : peut-il exister des propositions arithmétiques, comme l'hypothèse de Riemannn, indécidables ou indémontrables non pas au sens de Gödel qui en explicite quelques une mais peut-être pas toutes ?

tartaglia (2009-11-03T09:07:17Z)

Bravo, tu t'es rapidement affranchi de tes terreurs nocturnes.
Bien sûr les mathématiques relèvent du monde des idées d'où le rapport au platonisme et les sciences molles de l'aristotélisme - sauf qu'on a besoin de les modéliser…

ooten (2009-11-03T08:15:15Z)

Franchement ce genre de post, c'est super et j'ai pas tout lu et compris.


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: da526a


Recent comments