Dans quelle mesure les mathématiques des réels peuvent-elles être appliquées aux réels calculables?

Existe-t-il un théorème général qui indiquerait, avec une désinfection appropriée, que la plupart des résultats connus concernant l'utilisation de nombres réels peuvent réellement être utilisés lorsque l'on considère uniquement les réels calculables? Ou existe-t-il une caractérisation appropriée des résultats qui restent valables lorsque l'on considère uniquement les réels calculables? Une question secondaire est de savoir si les résultats concernant les réels calculables peuvent être prouvés sans avoir à considérer tous les réels, ou tout ce qui n'est pas calculable. Je pense spécifiquement au calcul et à l'analyse mathématique, mais ma question ne se limite en rien à cela.

En fait, je suppose qu'il existe une hiérarchie de réels calculables correspondant à la hiérarchie de Turing (est-ce correct?). Ensuite, plus abstraitement, existe-t-il une théorie abstraite du réel (je ne suis pas sûr de la terminologie), pour laquelle un certain nombre de résultats pourraient être prouvés, qui s'appliquerait aux nombres réels traditionnels, mais aussi aux réels calculables, et à n'importe quel niveau de la hiérarchie de Turing des réels calculables, s'il existe.

Alors ma question pourrait éventuellement être formulée comme suit: Y a-t-il une caractérisation des résultats qui s'appliqueront dans la théorie abstraite des réels lorsqu'ils ont été prouvés pour des réels traditionnels. Et, ces résultats pourraient-ils être prouvés directement dans la théorie abstraite, sans tenir compte des réels traditionnels.

Je suis également intéressé à comprendre comment et quand ces théories des réels divergent.

PS Je ne sais pas où mettre cela dans ma question. J'ai réalisé qu'une bonne partie des mathématiques sur les réels ont été généralisées avec la topologie. Il se peut donc que la réponse à ma question, ou une partie de celle-ci, se trouve là. Mais il peut aussi y avoir plus.

Les nombres réels peuvent être caractérisés de deux façons, travaillons avec le champ ordonné archimédien complet de Cauchy . (Nous devons faire un peu attention à la façon exacte dont nous disons cela, voir la définition 11.2.7 et la définition 11.2.10 du livre HoTT .)

Le théorème suivant est valable dans tous les topos (un modèle de logique intuitionniste d'ordre supérieur):

Théorème: Il existe un champ ordonné archimédien complet de Cauchy, et en fait deux de ces champs sont canoniquement isomorphes.

De plus, dans la logique intuitionniste (à ne pas confondre avec l' intuitionnisme ), nous pouvons faire beaucoup d'analyses réelles (séquences et limites, dérivées, intégrales, continuité, continuité uniforme, etc.) qui est alors valable dans tous les topos. Si nous prenons les topos des ensembles, nous obtenons l'analyse réelle habituelle. En prenant un topos différent, nous obtenons un type différent d'analyse réelle - et il y a un topos qui donne précisément les réels calculables et l'analyse réelle calculable.

C'est bien sûr le topos efficace , dans lequel les nombres réels sont les réels calculables (en parlant vaguement, la raison en est que le topos efficace est construit de telle manière que tout ce qu'il contient est automatiquement calculable). La réponse à votre question est

Les définitions, les constructions et les théorèmes de l'analyse réelle intuitionniste sont automatiquement traduits en définitions, constructions et théorèmes sur les réels calculables lorsque nous les interprétons dans les topos effectifs.

Par exemple, le théorème "chaque carte uniformément continue atteint son supremum" est intuitivement valide. Lorsque nous l'interprétons dans les topos effectifs, nous obtenons la version correspondante pour les cartes calculables sur des réels calculables qui sont calculablement uniformément continus.$f : [0,1] \to \mathbb{R}$

Vous vous interrogez également sur la "divergence" entre l'analyse réelle et sa version calculable. La réponse est que les résultats qui reposent sur la loi du milieu exclu ou sur l'axiome du choix (bien que le choix dénombrable soit correct) ne sont pas intuitionnistes et ne peuvent donc pas être validés dans les topos effectifs. Cependant, nous devons noter que (contrairement à l'opinion populaire) la plupart des analyses peuvent être effectuées de manière intuitionniste.

Le topos efficace n'est qu'un des nombreux topos réalisables . Lorsque nous interprétons l'analyse intuitionniste dans d'autres objectifs de réalisabilité, nous obtenons des modèles alternatifs de calcul en nombre réel, y compris le calcul avec des oracles auxquels vous faites allusion. Le "topos relatif de réalisabilité de la fonction de Kleene" (quel qu'il soit) donne la calculabilité dite de type II sur les réels dans laquelle les cartes calculables opèrent sur tous les réels, pas seulement les calculables.

J'ai essayé d'expliquer cela une fois dans les notes "La réalisabilité comme lien entre les mathématiques calculables et constructives" , et avant cela dans mon doctorat. thèse .