Toute fonction calculable est continue
Bonsoir,
On a parlé plus ou moins récemment du principe selon lequel toute fonction calculable est continue, et on s'était demandé si dans ZFI l'assertion "toute fonction totale de $\mathbb R$ dans $\mathbb R$ est continue" est consistante (c'était ici http://www.les-mathematiques.net/phorum/read.php?16,1530786,1572842#msg-1572842 ).
Est-ce que finalement on connaît la réponse?
On a parlé plus ou moins récemment du principe selon lequel toute fonction calculable est continue, et on s'était demandé si dans ZFI l'assertion "toute fonction totale de $\mathbb R$ dans $\mathbb R$ est continue" est consistante (c'était ici http://www.les-mathematiques.net/phorum/read.php?16,1530786,1572842#msg-1572842 ).
Est-ce que finalement on connaît la réponse?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Le problème de cet art c'est que les choses ne se passent pas dans ZFI, mais dans quelque chose qui est revendiqué "faire office de" pour ce à quoi ça sert.
Du coup, je pense que la question formelle est ouverte, dès lors que tu lui auras donné une tournure formelle (ie que tu l'auras écrite avec des $\forall, \to, \in$, précisé que tu gardes bien $(x,y):= \{\{x\}; \{x;y\} \}$, etc). Et attention, pas de $\exists$ non documenté, le $\exists$ "officiel" est $(\exists x:R(x)) := <<\forall ,u,v : [(\forall x:[R(x)\to u\in v])\to u\in v]>>$ et si tu veux en prendre un autre, à toi de préciser (de le définir).
PS: avis personnel, à franchement parler, je pense que dès qu'on passe en LI, la notion de fonction devient de toute façon beaucoup moins intéressante, on le voit d'ailleurs très bien avec le forcing où les "fonctions" n'en pas, bien qu'une fois "réduit le paquet d'onde" via le générique, elles le deviennent. Et bin en LI ça doit être pareil, la plupart des relations intéressantes*** ne sont pas des fonctions, mais le deviennent quand tu RLPO (ie quand tu fais un elctroc à l'univers pour qu'il vérifie le RPA)). Il s'en suit que c'est une sorte de décoration "complètement vide" que de dire que les quelques rescapées (ie les relations qui parviennent à rester des fonctions coûte que coûte) sont toutes continues
*** un objet unique (par exemple un entier) apparait comme une antichaine qui "étale" cet entier sur tout IN, autrement dit, c'est une application $f$ de $\N$ dans $B$ (B est l'algèbre de Boole ambiante), ie chaque $f(n)$ te dit la "proba" que l'entier "virtuel" soit $n$. Cet objet est un entier quand les $f(k)$ sont deux à deux disjoints et quand leur disjonction est $1_B$. Or en forcing, on est "gentil" dans le sens qu'on a juste remplacé $\{vrai; faux\}$ par $B$ alors que les modèles de ZFI sont les mêmes choses sauf qu'on remplacé $\{vrai; faux\}$ par une algèbre de Heyting (ie une topologie si tu préfères, ça revient au même).
Sur l'autre fil, j'ai donné une référence où un topos est construit et il s'y passe ce qu'on veut : il n'y a qu'à suivre la démonstration (mais je ne l'ai pas encore fait) !
Mais je n'ai pas encore assouvi mon envie de comprendre pourquoi un topos pourrait être envisagé comme un "univers d'ensembles intuitionniste", quoi que ceci veuille dire.
Je crois avoir fini par comprendre que les topos ne servent pas à "interpréter" $ZF$ au sens où je voulais l'entendre ; je crois que ça permet "juste" de donner de manière cohérente des "valeurs de vérité" (dans une algèbre de Heyting, si j'ai bien compris) à des énoncés d'un langage du premier ordre avec plein de sortes, qui est tel que si $A$ est une sorte, on a une sorte $\mathcal{P}(A)$, et il y a un symbole d'arité $(A,\mathcal{P}(A))$ qui représente l'appartenance (c'est peut-être ce que voulait dire talal quand il ou elle parlait de "quantifications bornées" ?), et puis pour des sortes $A$ et $B$, on a la sorte $A\times B$ et des symboles de fonctions $A\times B \rightarrow A,B$ qui représentent les projections sur les coordonnées, etc.
L'ennui, c'est que je n'ai pas vu ce point de vue exprimé dans mes lectures (je n'ai peut-être pas bien lu !).
Ca m'a un peu déçu des topos, et ça ne m'a pas motivé à m'y remettre. Mais je vais le faire !
Par contre, toutes les questions que tu te poses concernant ZFI peuvent à mon avis être traduites en toposerie en regardant ce que TOUS les topos disent de leurs inaccessibles, car là, on est en mode "quantifications bornées" consensuellement acceptées comme fiables.
Tu n'as pas besoin de faire un petit programme qui produit du langage interne pour définir*** ce qu'est un inaccessible, par contre, c'est conseillé (à mon avis) pour son ensemble vérité.
*** en gros, c'est un couple $(E,R)$ où $E$ est un objet du topos et où $R$ est une flèche allant de $E\times E$ dans $\Omega$. L'inaccessibilité s'exprime en demandant que pour tout objet $A$ tel qu'on n'a pas** $A\geq E$ et tout monomorphisme $f: A\to E$, il existe une flèche $g: 1\to E$ telle que (exercice traduire, j'ai la flemme) les deux sous-objets de $E$ représentés par $f$ et par la flèche induite par "l'élément" $g$ de $E$ à travers $R$ sont "la même partie de $E$" à quoi il faut ajouter que si $P(A)\geq E$ alors $A\geq E$, etc.
** j'abrège par $<<X\geq Y>>$ la phrase $<<$ il existe un épimorphisme de $X\to Y>>$.