Até que ponto a matemática dos reais pode ser aplicada aos reais computáveis?

Existe um teorema geral que declararia, com sanitização adequada, que os resultados mais conhecidos sobre o uso de números reais podem realmente ser usados ​​quando se considera apenas reais computáveis? Ou existe uma caracterização adequada dos resultados que permaneçam válidos ao considerar apenas os reais computáveis? Uma questão paralela é se os resultados referentes aos reais computáveis ​​podem ser comprovados sem a necessidade de considerar todos os reais ou qualquer coisa que não seja computável. Estou pensando especificamente em cálculo e análise matemática, mas minha pergunta não se limita a isso.

Na verdade, suponho que exista uma hierarquia de reais computáveis ​​correspondente à hierarquia de Turing (isso está correto?). Então, mais abstratamente, existe uma teoria abstrata do real (não sei qual deve ser a terminologia), para a qual vários resultados poderiam ser provados, que se aplicariam aos números reais tradicionais, mas também aos reais computáveis, e a qualquer nível da hierarquia de Turing de reais computáveis, se existir.

Então, minha pergunta poderia ser declarada como: Existe uma caracterização dos resultados que serão aplicados na teoria abstrata dos reais quando eles forem provados para os reais tradicionais. E esses resultados poderiam ser provados diretamente na teoria abstrata, sem considerar os reais tradicionais.

Também estou interessado em entender como e quando essas teorias dos reais divergem.

PS: Eu não sei onde encaixar isso na minha pergunta. Percebi que boa parte da matemática dos reais foi generalizada com topologia. Portanto, pode ser que a resposta à minha pergunta, ou parte dela, possa ser encontrada lá. Mas também pode haver mais.

Os números reais podem ser caracterizados de duas maneiras: vamos trabalhar com o campo ordenado arquimediano completo de Cauchy . (Nós precisamos ser um pouco cuidadosa exatamente como nós dizemos isso, consulte Definição 11.2.7 e Defintion 11.2.10 do livro Hott .)

O seguinte teorema é válido em qualquer topos (um modelo de lógica intuicionista de ordem superior):

Teorema: Existe um campo ordenado arquimediano completo em Cauchy e, de fato, quaisquer dois desses campos são canonicamente isomórficos.

Além disso, na lógica intuicionista (para não confundir com o intuicionismo ), podemos fazer muitas análises reais (sequências e limites, derivadas, integrais, continuidade, continuidade uniforme etc.) que são válidas em qualquer topos. Se tomarmos o topos de conjuntos, obtemos a análise real usual. Ao adotar um topos diferentes, obtemos um tipo diferente de análise real - e há um topos que produz exatamente os reais computáveis ​​e a análise real computável.

É claro que são os topos efetivos , nos quais os números reais são os reais computáveis ​​(falando vagamente, a razão para isso é que os topos efetivos são construídos de tal maneira que tudo nele é computável automaticamente). A resposta para sua pergunta é

Definições, construções e teoremas na análise real intuicionista são automaticamente traduzidos para definições, construções e teoremas sobre reais computáveis ​​quando os interpretamos nos topos efetivos.

Por exemplo, o teorema "todo mapa uniformemente contínuo atinge seu supremo" é intuicionisticamente válido. Quando o interpretamos nos topos efetivos, obtemos a versão correspondente para mapas computáveis ​​em reais computáveis ​​que são computavelmente uniformes e contínuos.$f : [0,1] \to \mathbb{R}$

Você também pergunta sobre a "divergência" entre a análise real e sua versão computável. A resposta é que os resultados que se baseiam na lei do meio excluído ou no axioma da escolha (embora a escolha contável seja aceitável) não são intuicionistas e, portanto, não podem ser validados nos topos efetivos. No entanto, devemos observar que (ao contrário da opinião popular) a maioria das análises pode ser feita intuicionisticamente.

Os topos eficazes são apenas uma das muitas topos de realização . Quando interpretamos a análise intuicionista em outras topos de realizabilidade, obtemos modelos alternativos de computabilidade de números reais, incluindo computação com oráculos aos quais você alude. O "topos relativos de realizabilidade da função Kleene" (o que quer que seja) fornece a chamada computabilidade do Tipo II em reais, na qual os mapas computáveis ​​operam em todos os reais, não apenas nos computáveis.

Tentei explicar isso uma vez nas notas "Realização como a conexão entre matemática computável e construtiva" , e antes disso no meu doutorado. tese .