Intuitionnisme et fonctions continues

De mon téléphone : GBZM parlait d'un topos ou un certain objet est revendiqué s'appeler IR. Par ailleurs un article que j'ai trouvé je ne sais plus par qui il y a 2ans de mon téléphone écrit en 1980 construit (en le disant vite) un modèle de ZF à partir de l'univers et d'un topos dedans stable par "petites limites)

Je te precesireai ça d'un PC.

Il reste les questions documentaires que je n'ai moi même (de l'HP) pas résolues à l'époque: l'énoncé du langage L(in) habituel qui traduit formellement exactement ton énoncé concerne-t-il et est-il vraiment ce que par ailleurs les algébristes "voient" avec leur "IR" ad hoc. (Autrement dit la évaleur dans l'algèbre de Heyting du topos évoqué par GBZM de ton énoncé telle que définie dans l'article de 1980 est-elle "le pur vrai" du topos? En principe ça devrait car c'est un énoncé presque borné mais bon le diable est dans les détails.

GA a écrit:

C'est pas la "base" de ce qu'on voudrait pour un ensemble d'interprétations ? Le mot est "correction", non ?

Oui, mais la littérature n'est pas du tout claire à ce sujet (ou alors ma manière de jouer au documentaliste est mauvaise) de la relation "topos" et "modèle de ZF". La preuve d'ailleurs dans l'article, un tel article ne pourrait pas exister si les choses allaient bien (1980 quand-même).

Attention, je ne dis pas que ça ne marche pas, mais je dis que tous les échanges que j'ai eus avec les gens n'ont jamais permis d'aboutir (à moi) à la conclusion que "tout va bien").

Les toposeurs n'utilisent pas les topos pour y évaluer des énoncés mathématiques normaux, ils se restreignent DRASTIQUEMENT aux seuls énoncés "vides" c'est à dire "bornés" (qui sont absolus, donc "vides" pour les ensemblistes). D'où la pertinence de la publication de l'article de Fourman (il annonce bien quelque chose qui a un "gros conetnu"). Bien sûr, leur justification est que les matheux hors logique du quotidien font des maths-à-énoncés-bornés, donc ils sont légitimes. Mais du point de vue logique, ça ne résout pas le problème de la consistance de ZFI + machintruc que des gens comme toi voudraient peut-être savoir.

J'ai eu aussi (et hélas, ma vélléité m'a conduit à reporter depuis 14 mois au lendemain) un indice très très fort qu'il y a un bug dans tout ça, donc certainement (à moins que ZF ne soit contradictoire) un passage subtil et discret qui fait se séparer deux visions de la problématique, mais je n'ai pas trouvé où avec mon survol philosophique superficiel, voici cet indice: l'été 2016, un intervenant alesha m'a fait remarquer que $a=b$ implique linéairement $(a=b$ ET $a=b)$ au sens du "et" comment dire "fort", à savoir le produit tensoriel logique (l'autre "et" est inoffensif, $a=inf(a,a)$)
Or on peut exprimer très facilement et robustement toutes les surlogiques (affines, intuitionnistes, classiques) à partir de la linéaire (en fait la "bonne" logique est la linéaire et les autres sont des "théories axiomatiques", c'est ça "la bonne" vision des choses disons). Mais mais mais, la remarque d'Alesha conduit, en rajoutant une tout petit petit petit truc à

[size=x-large]$$ZFL^*\Rightarrow ZF\ (Alesha's\ theorem)$$[/size]

petit truc qu'a priori personne n'aurait l'idée de nier. (ZF désigne ZF + logique classique, et ZFL désigne ZF linéaire et l'étoie est une espèce d'ajout d'un "rien du tout du genre affine" qui change tout)

Or, comme il n'est pas vrai que tous les topos (complets**) sont des modèles de ZF (ZF classique), et comme il est vrai que ZFL implique ZFI ZFI => ZFL (edit: coquille), il y a un problème quelque part quand on dit et quand l'article semble confirmer que $ZFI\subset \cap_{T\in ToposComplets} TheoriePurVrai(T)$

** stable par "petites limites" (et pas juste par limites finies)

* Précision: grace à l'extensionnalité, toute phrase peut se mettre sous la forme $a=0$

@talal : je ne m'y connais pas assez, mais attention : en plus d'exhiber une fonction il faut réussir à prouver intuitionnistement qu'elle est non continue ! C'est peut-être là que se cache la difficulté. Sinon je fais pareil pour l'hypothèse du continu : j'exhibe $\omega_1$, et dans un modèle où HC est fausse, c'est bel et bien un contrexemple à HC.

Bonjour et merci Georges,

j'essaierai de choper cet extrait du livre. Mais ta dernière phrase est vraiment essentielle. Du peu que je le connaisse, le langage interne est très limité (quantifications bornées uniquement), et le $\R$ évoqué n'est pas le $\R$ qu'on voudrait vraiment, mais c'est une question de gout. Ce qui serait plus intéressant c'est de savoir si on peut ou non prouver l'existence de fonctions discontinues sans utiliser le raisonnement par l'absurde, mais en ne supprimant rien d'autre (à part aussi l'axiome du choix bien sûr) de ce qu'on a l'habitude d'utiliser.

Bonne journée, Talal

Exemples de quoi ?
Comment définis-tu la partie entière sans test d'égalité ?

C'est bien ce que je disais : tu utilises que $\vdash \forall x\ (x<0 \vee x=0\vee x>0)$, et s'il y a une chose sur laquelle les intuitionnistes sont d'accord, c'est que les réels ne satisfont pas ça.

Le problème avec la fonction de talal, c'est : qu'est-ce que la borne supérieure d'une partie de $\Q$ ?
Il y a un modèle qu'il est utile d'avoir en tête : l'objet "réels de Dedekind" dans le topos des faisceaux sur un espace topologique $X$. C'est le faisceau sur $X$ des fonctions continues à valeurs dans $\R$. L'objet "rationnels", c'est le faisceau constant $\Q$. Un sous-faisceau de ce faisceau constant n'a aucune raison d'avoir une borne supérieure. Par exemple, prenons $X=\R$, et le sous-faisceau du faisceau constant $\Q$ dont la fibre en tout $x<0$ est $]-\infty, 1] \cap \Q$ et la fibre en tout $x\geq 0$ est $]-\infty, 0] \cap \Q$. Aucun réel de Dedekind dans le topos n'acceptera d'être la borne supérieure de ce sous-faisceau, à cause de ce qui se passe au voisinage de l'origine.

Ce n'est pas vrai en général pour l'objet "réels de Dedekind" d'un topos.
De même qu'on n'a pas de théorème des valeurs intermédiaires, du moins sous sa forme classique (par exemple un polynôme $P$ du troisième degré tel que $P(-1)<0$ et $P(1) >0$ n'a pas forcément de racine réelle).

Je n'ai pas de position philosophique à ce sujet. Je me contente fort bien d'avoir une sémantique avec laquelle je peux travailler.

Comme disait Lawvere, "The theory of topoi is the basis for the study of continuously variable structures" . Des réels qui varient continûment, autrement dit des fonctions continues à valeurs réelles, c'est ça l'objet des réels de Dedekind dans un topos de faisceaux.

Rebonjour,

il y a une façon simple de ne pas se laisser trop abuser quand on a d'abord été familier avec les ensembles et non avec des théories appliquées.

Le topos des ensembles, il vaut mieux ne pas le voir comme tous les ensembles comme objets et toutes les fonctions comme flèches. Il me semble préférable d'en prendre un squelette: les objets sont uniquement les cardinaux (ie les ordinaux ne s'injectant pas dans un de ses éléments, par exemple) et les flèches les applications d'un cardinal dans un autre.

Le voir comme ça permet peut-être d'éviter des attentes chimériques excessives. Par exemple, si $a,b$ sont des cardinaux infinis avec $a\leq b$, le seul objet mobilisable dans un produit cartésien c'est $a$ lui-même. Ce sont les flèches qui assurent tout le travail et qui sont les chevilles ouvrières dans l'histoire. De même, c'est le même objet qui sert à la fois de $a^b$ et $2^a$ (noté $\Omega^a$ ou $P(a)$ dans un topos). Là encore, tout repose sur les flèches.

Dans ce contexte la seule façon réellement honnête (ça ne veut rien dire) de se donner un ensemble, c'est de se donner un relation binaire sur un "support" (j'appellerai ça un "nom d'ensemble) , qui est un cardinal et d'imaginer en pensée qu'on s'intéresse au transitive collapse de ladite. Sauf que, par théorème, seuls les bien fondés ont un transitive collapse prouvable en théorie classique des ensembles et seul un axiome "arbitraire" par exemple peut forcer deux "atomes" (des ensembles $x$ vérifiant $x=\{x\}$) à être égaux.

Evidemment, on peut exprimer (c'est assez long) qu'un ensemble (désigné par son nom) appartient à un autre (idem), puisque ce n'est qu'une affaire de morphismes. Mais en l'absence de bonne fondation, il faut ajouter des axiomes, dont on ne sait pas s'ils seront supportés par le topos ou s'il les recrachera violemment (un topos n'étant pas une théorie mais un modèle, il décide de lui-même, on ne peut pas le forcer).

Un article de 1974, écrit par Ozius, a exploité ça pour reconstruire l'univers à partir de son topos. Mais, dans mon souvenir, il ne s'étale pas ensuite sur l'extrapolation, à savoir "appliquons ce processus à n'importe quel topos pour regarder "l'univers exotique" que ça donne".

Cordialement,
Talal

En fait c'est pragmatique plus que philosophique disons que ça peut peut être aider les personnes habituées aux ensembles.

Ce ne sont pas les axiomes, c'est le langage. Mais de toute façon non je n'ai pas identifié au millimètre près ce qu'on ne peut pas utiliser dans les topos pour prouver que linéaire implique classique donc que intuitionniste implique classique. Entre autre car il y a DEUX façons de traduire : une bonne et une mauvaise, l'intuitionniste en linéaire, soit par prolongement pur et simple soit par réécriture du implique avec les exponentielles. Or les exponentielles déraillent (elles ne sont pas compatibles avec l'ensemblisme puisque, poussées à bout , elles impliquent qu'il y a au moins autant de valeurs de vérité que d'objets dans l'univers.