An Intuitionistic Glance at Primes

Resumo Técnico: Um Olhar Intuicionista sobre os Primos

Enunciado do Problema
O artigo aborda a classificação proof-teórica de inteiros positivos em unidades, primos e compostos dentro do arcabouço da lógica intuicionista (especificamente, a Aritmética de Heyting, HA). Enquanto a aritmética clássica trata essas categorias como extensões mutuamente exclusivas e exaustivas, o artigo investiga as formas distintas de evidência necessárias para estabelecer essas propriedades construtivamente. O problema central é formalizar como a "compositividade" (uma afirmação existencial) e a "primalidade" (uma afirmação de refutação universal) funcionam como predicados decidíveis quando o espaço de busca é limitado, e distinguir entre as regras sintáticas de uma teoria formal, o acordo interno de um modelo e a interpretação semântica relativa aos números naturais padrão $\mathbb{N}$.

Metodologia
O autor emprega uma abordagem construtiva e proof-teórica fundamentada na lógica intuicionista. A metodologia procede através de várias camadas:

1. Classificação Ternária via Formas de Evidência: O artigo define três predicados — Unidade ($U$), Composto ($C$) e Primo ($P$) — baseados em tipos de evidência específicos:

   • $U(n)$: Evidência da igualdade $n=1$.
   • $C(n)$: Evidência de uma fatoração interior $n=ab$ com $a,b > 1$ (uma testemunha existencial).
   • $P(n)$: Evidência de $n > 1$ combinada com uma refutação limitada de toda possível fatoração interior (um negativo universal).
     Como o domínio de potenciais fatores para qualquer $n$ é finito e decidível, tanto $C(n)$ quanto $P(n)$ são mostrados como predicados decidíveis.

2. Apresentações de Blocos Estagiadas: Para operacionalizar a busca limitada, o artigo introduz "configurações de blocos estagiadas". Estas são listas finitas e ordenadas de pares de candidatos a fatores. O artigo analisa as relações de "defeito" (omissões, duplicações, violações de ordenação) que surgem ao estender esses estágios. Ele distingue entre habitação local (uma decisão válida em um estágio específico) e totalização uniforme (um seletor global para todos os estágios).

3. Escape Euclidiano e Crivos: O artigo utiliza uma variante construtiva do argumento de Euclides ("Escape Euclidiano") para demonstrar que nenhum conjunto finito de "pegadores" (geradores de números compostos) pode capturar todos os compostos. Isso leva a uma construção de crivo recursivo onde o menor sobrevivente de um conjunto finito de pegadores é promovido a um novo gerador, efetivamente enumerando os primos.

4. Análise Algébrica e Semântica: O artigo examina as consequências algébricas dessa classificação, especificamente o contraste entre o cancelamento modular (para primos) e a aniquilação por divisores de zero (para compostos). Em seguida, move-se para uma análise semântica, distinguindo entre:

   • Conformidade de Regra: Verificação sintática de provas.
   • Acordo Multiplicativo Interno: A satisfação de definições dentro de um modelo fixo.
   • Acordo Deficional Padrão: O alinhamento de uma teoria com a estrutura padrão $\mathbb{N}$, o que requer representação metateórica.

Principais Contribuições e Resultados

• Decidibilidade da Primalidade: O artigo estabelece que a primalidade é uma propriedade decidível em HA porque o quantificador universal em sua definição é limitado pelo dado de entrada $n$. A distinção entre primo e composto é de "polaridade de prova" (testemunha existencial vs. refutação universal) em vez de complexidade de hierarquia aritmética (ambos são $\Delta_0$).
• A Fronteira da Unidade: É fornecido um tratamento rigoroso da unidade ($1$), mostrando que a oposição binária $\neg P(n) \to C(n)$ falha em $n=1$. A classificação ternária $U(n) \lor P(n) \lor C(n)$ é provada construtivamente.
• Pegadores Finitos e Transição de Crivo: Prova-se que qualquer conjunto finito de geradores compostos perde alguns compostos (especificamente, o quadrado do menor sobrevivente). Este mecanismo impulsiona um crivo recursivo que gera a sequência dos primos ordinários.
• Caracterização Algébrica: O artigo vincula a definição número-teórica de primos à propriedade algébrica de cancelamento no anel $\mathbb{Z}/n\mathbb{Z}$. Um número $n > 1$ é primo se, e somente se, a multiplicação por qualquer resíduo não nulo for injetiva.
• Hierarquia Semântica: O artigo delineia uma hierarquia de certificação:
  1. Evidência Local: Testemunhas ou refutações finitas para um $n$ específico.
  2. Acordo do Modelo: A extensão de predicados em um modelo fixo.
  3. Representação Metateórica: A asserção de que uma teoria concorda com o $\mathbb{N}$ padrão.
     O artigo demonstra que, embora a teoria local seja uma extensão conservativa de HA, estabelecer o acordo com o modelo padrão requer dados metateóricos externos.
• Limites da Uniformidade: O artigo aplica o Teorema de Rice e o Segundo Teorema da Incompletude de Gödel para mostrar que, embora testes individuais de primalidade sejam decidíveis, a certificação bilateral uniforme (produzindo provas tanto para primalidade quanto para compositividade para todos os $n$) ou limites de completude uniformes para problemas de parada carregam força computacional equivalente ao oráculo de parada ($0'$).

Significância e Alegações
O artigo alega fornecer um "relato proof-teórico" da classificação de inteiros, enfatizando que a distinção entre primos e compostos é estrutural e evidencial, e não meramente extensional.

• Rigor Intuicionista: Argumenta-se que a "fronteira da unidade" e a natureza da busca limitada são cruciais para entender o conteúdo construtivo da primalidade. O artigo esclarece que a "falta de fatoração interior" para primos não é um infinito negativo, mas uma refutação finita e exaustiva.
• Separação de Níveis: Uma contribuição primária é a separação explícita da conformidade de regra sintática, da satisfação do modelo interno e da representação da estrutura padrão. O artigo asserta que o "acordo com os primos" é uma noção relativa dependente da metateoria e interpretação escolhidas.
• Primos como "Miragem": Na conclusão, o artigo oferece uma caracterização metafórica: relativo à multiplicação interior, os compostos formam a imagem positivamente gerada, enquanto os primos são os "buracos" nessa imagem. O artigo alega que conjecturas globais sobre primos (como a Conjectura dos Primos Gêmeos ou a Conjectura de Goldbach) pedem organização entre esses "buracos" sem fornecer um gerador positivo para sua distribuição, destacando uma assimetria fundamental em sua apresentação construtiva.

O artigo não propõe novos algoritmos para fatoração ou teste de primalidade, nem alega resolver conjecturas abertas. Em vez disso, oferece uma análise fundamental de como esses conceitos são construídos, verificados e interpretados dentro da aritmética intuicionista, distinguindo o que é provável internamente do que depende da interpretação padrão dos números naturais.