Livre Pierre Ageron.

Dans son livre "logique, ensembles, catégories,  le point  de vue constructif, Ageron écrit que l'égalité dans N est décidable sans tiers exclu. Il ajoute "Postuler que l'égalité dans N est décidable n'est pas anodin: c'est la traduction mathématique d'une position philosophique, celle selon laquelle notre connaissance des entiers naturels se passe de tout intermédiaire ." Mais ne peut-on pas démontrer cette décidabilité de l'égalité par récurrence, par exemple?
Et puis s'appuyer sur la philosophie pour exprimer une vérité mathématique, n'est-ce pas un peu louche? Il n'y a que Badiou (que j'adore malgré ses positions  très extrème-gauchistes...) pour faire cela.
Qu'en pensez-vous? (et accessoirement quand pensez-vous?)
Cordialement. Voire amicalement. (je déplore cette atmosphère violente que je sens parfois sur le forum)

Réponses

  • Thierry Poma
    Modifié (23 Apr)
    Ce n'est pas du tout ce qu'écrit l'auteur. Voici ce qu'il écrit exactement : C'est bien sûr un énoncé qui va de soi dans l'environnement mathématique classique [sous-entendu avec (TE)], mais plus du tout dès lors que nous souhaitons nous passer de (TE). Il faut savoir qu'en mathématiques intuitionnistes, l'égalité entre ensembles ou l'égalité entre nombres réels ne sont pas décidables. (...)
    Nous sommes loin de ce que tu cites !
    Voici l'énoncé dont il est question : quels que soient $a$, $b$ dans $\N$, l'on a toujours $a=b$ ou $a\ne{}b$.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Salut Thierry, mais ce que je cite c'est juste après et c'est ça qui concerne le fait qu'on ne démontre pas la décidabilité de l'égalité dans N; ce que tu cites ne concerne justement pas N . J'ai du mal à comprendre ta remarque.
    Cordialement.
    Jean-Louis.
  • Thierry Poma
    Modifié (23 Apr)
    Tu as écrit :
    Ageron écrit que l'égalité dans $\N$ est décidable sans tiers exclu.

    Ce n'est pas ce qu'a écrit Pierre Ageron.

    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • O. Je retire "sans tiers exclu.
  • samok
    Modifié (23 Apr)
    Ce qui donne : Ageron écrit que l'égalité dans $\mathbb{N}$ est décidable.

    Qu'est-ce que cela signifie Jean-Louis ?

  • Foys
    Modifié (23 Apr)
    L'énoncé $\forall x (\forall y, x = y \vee x \neq y)$ est démontrable en arithmétique de Heyting (i.e. Peano sans tiers exclu), par récurrence sur $x$. Les axiomes de l'arithmétique de Heyting contiennent:
     $\forall x, x = 0 \vee \exists y, S y = x$, 
    $\forall x, S x \neq 0$ et 
    $\forall x \forall y, S x = S y \Rightarrow x = y$.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • C'est moral puisque informatiquement $\N$ (ou concrètement l'ensemble fini qui lui tient lieu de substitut dans les situations réelles concrètes) est une structure discrète.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Alesha
    Modifié (24 Apr)
    Jean-Louis, je ne comprends pas non plus ce que te reproche Thierry Poma. Pierre Ageron veut bien dire que, même en adoptant un point de vue constructiviste selon lequel l'égalité n'est pas décidable dans un ensemble quelconque, l'égalité est bien décidable dans l'ensemble des entiers naturels (sans qu'on ait à supposer le tiers exclu).
    On peut prouver de manière intuitionniste que l'égalité est bien décidable dans l'ensemble des entiers naturels une fois qu'on s'est donné une axiomatique des entiers naturels (comme le fait Foys). Pierre Ageron, ici, considère le problème de manière plus générale. Il ne considère pas une axiomatique particulière. Indépendamment de toute formalisation axiomatique, il pose la question de manière philosophique. En effet, une fois qu'on se donne une axiomatique, on peut prouver des théorèmes, mais qu'est-ce qui te dit que c'est une "bonne" axiomatique? Par exemple, on peut se donner une axiomatique des réels; si cette axiomatique (quelle qu'elle soit) te permet de prouver que l'égalité des réels est décidable, on pourrait dire que cette axiomatique viole le point de vue constructiviste; ce que dit Pierre Ageron ici est qu'un tel argument n'est pas valable pour les entiers naturels. 
    L'argument donné par Foys dans son second message est du même ordre : c'est un argument épistémologique très général (et très valide) concernant toutes les structures discrètes en l'absence d'axiomatisation de telles structures, et pour cause, comment vas-tu considérer à la fois toutes les axiomatisations possibles de toutes les structures discrètes? Tu as un argument très général philosophique sur toutes les structures discrètes, ce qui ne t'empêchera pas, par ailleurs, de prouver que l'égalité est décidable dans une telle structure (en l'absence de tiers exclu) une fois que tu t'es donné une axiomatisation d'une structure discrète particulière.
    Historiquement et épistémologiquement, le point de vue intuitionniste précède l'axiomatisation de Heyting, celle-ci se veut être une axiomatisation conforme à ce point de vue, on doit donc pouvoir exprimer ce point de vue indépendamment de toute axiomatisation et c'est ce qui est fait ici. 
  • Merci Alesha, tu me rassures.
  • Alesha, un doute me taraude. Qu'est-ce que N en dehors de toute axiomatique? C'est sans doute bête ce que je dis mais je n'ai plus l'esprit vif de mes 20ans...
  • Une axiomatique telle que celle de Heyting n'a pas pour but de définir N (tu connais le théorème de Gödel, inutile d'insister là-dessus). N est relatif à un univers. Si on veut un énoncé formel correspondant à l'énoncé "N est un modèle de l'axiomatique de Heyting", on peut, par exemple, énoncer que tout objet des entiers naturels dans un topos (tu peux voir la définition d'un tel objet comme une axiomatique, mais, à la différence de celle de Heyting, tous ses modèles sont isomorphes) est un modèle de l'axiomatique de Heyting. Parmi ces objets, tu as, par exemple, le plus petit ordinal infini d'un modèle de ZF. Si tu considères deux modèles différents de ZF, tu auras deux N qui partageront beaucoup de choses en commun (par exemple, que ce sont des objets des entiers naturels et donc des modèles de l'axiomatique de Heyting).
Connectez-vous ou Inscrivez-vous pour répondre.