Comments on De quoi parlent les mathématiques ?

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 !

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

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…

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.

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).

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 ?

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)…

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.

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 ?" ?

@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.

> 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.

@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 ?

@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).

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>

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é.

@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é…

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 ?

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 !

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…

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.

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

@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).

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 ?

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.

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.

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…

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 ?

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? :)

"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).

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 ?

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…

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