Números Grandes e Maiores Ainda (5)

Passando disso tudo, fica difícil de prosseguir. Parece muito difícil achar artigos na internet com notação razoavelmente compreensível de ordinais que vá além da notação C do Taranovsky. Procurei bastante, parece tudo embolado e sem sentido, faltou paciêcia pra procurar algo melhor, ou mesmo tentar entender as notações esquisitas que eu vi por aí, que parecem ir bem além do dito cujo (mesmo o próprio artigo que descrevi possui uma notação mais poderosa, mas de difícil compreensão e clareza).Assim, na maioria das vezes encerro minha jornada em ordinais computáveis no CX (nome que o autor do artigo não deu).

Pensemos então, em um novo método de definir números grandes. Ainda estamos no escopo do computável. Vou falar de algo desconhecido (entre não matemáticos) agora, o sistema axiomático ZFC (teoria dos conjuntos). O sistema axiomático em si é bem definido assim como a lógica de primeira ordem, então não vou enumerar os axiomas agora. Procure na Wikipédia em inglês "Zermelo–Fraenkel set theory". Assim, definamos ZFC_C(n)=O maior número k para o qual existe um algoritmo que calcula k e é tal que exista uma demonstração de tamanho menor ou igual a n (número de caracteres), que esse algoritmo pára. Como o conjunto dos números naturais, entendemos o conjunto (onde 0 é conjunto vazio) {0,{0}(num 1),{0,{0}}(num 2), {0,{0},{0,{0}}}(num 3), etc}.Assim,0 é o conjunto vazio, 1={0}, 2={0,1}, 3={0,1,2}, etc. Usamos em ZFC os carcteres básicos {Existe (E de costas), ParaTodo (A de cabeça pra baixo), Ou (v), Não (¬), E(^), Implica(->), Parênteses (()), Igual(=), Pertence (e), Variáveis(x,y,z,... podemos tomar infinitas)}. Definir o que seria uma demonstração é meio complicado, não vou fazer isso agora. Daí para algum conjunto de regras de inferência nos daria alguma função bem definida ZFC_C(n), ficando assim nossa função indefinida a priori. Mas imaginando que temos um conjunto de regras de inferência, fica definida demonstração como uma sequência de teoremas onde cada teorema ou é um axioma (daí é necessário especificar como ficarão os axiomas, já que existem vários equivalentes resultando no mesmo sistema ZFC), ou se deduz diretamente de uma regra de inferência dos axiomas anteriores. Veja também que faltou precisar o que é um algoritmo (veremos isso daqui a pouco). Assim, temos nossa referida função. Essa função é computável (se ZFC for consistente, o que a maioria dos matemáticos espera ser) . É só rodar um programa que verifica todas as demonstrações que possuem tamanho menor ou igual a n, de que algum referido algoritmo pára. Assim é só depois rodar todos esses algoritmos e ver quem calcula o número maior. Acho que o tamanho do programa que faz isso é imenso, imagino que daria alguns megabytes pra escrever isso em Pascal, por exemplo. Por isso, é difícil ver pessoas usando esse tipo de função em disputas de número maior na internet. Eu mesmo não pude determiná-lo com precisão, já que precisaria escrever a notação dos algoritmos e as regras de inferência. (imagino que essa deva ser a parte mais difícil de entender de um aspirante a matemático nesse texto).
Queria muito definir ZFC_C(número de Graham) como o "Compzfcgol" mas não posso, por enquanto. Fica pra próxima.