On a Theorem by Bezboruah & Shepherdson

Este artigo discute e refuta a objeção de Kreisel ao teorema de incompletude de Bezboruah e Shepherdson sobre a teoria ${\sf PA}^-$, compara-o com a extensão de Pudlák e apresenta uma nova prova do teorema baseada em um insight de Nielsen e Markov.

O essencial

Imagine que a matemática é como um enorme jogo de construção com regras muito estritas. Existem teorias (conjuntos de regras) de diferentes tamanhos: algumas são gigantes e poderosas (como a Aritmética de Peano), e outras são pequenas e frágeis (como a teoria Q ou PA-).

O grande mistério que os matemáticos tentam resolver é: "Uma teoria consegue provar que ela mesma nunca vai entrar em contradição?"

A resposta clássica de Gödel (o "Teorema da Incompletude") diz que, para teorias grandes e poderosas, a resposta é NÃO. Elas são como castelos de cartas que, se você tentar provar que são estáveis, acabam derrubando-se.

Este artigo, escrito por Albert Visser, é uma investigação sobre um caso muito específico e "esquisito" desse problema, envolvendo teorias muito pequenas e frágeis. Vamos desvendar isso com analogias simples:

1. O Cenário: O Grande Debate

Em 1976, dois matemáticos, Bezboruah e Shepherdson, fizeram uma descoberta ousada. Eles disseram: "Mesmo as teorias mais fracas e pequenas (como a PA-) não conseguem provar que são consistentes."

Mas, antes de publicar, eles encontraram um obstáculo: Georg Kreisel, um "guru" da área, disse: "Isso não faz sentido! A teoria é tão fraca que nem consegue entender o que é uma prova. A frase que vocês chamam de 'consistência' é apenas uma equação matemática sem significado real ali. É como tentar explicar o conceito de 'amor' usando apenas a gramática de um bebê."

Kreisel argumentava que, para a frase "sou consistente" fazer sentido, a teoria precisa ser forte o suficiente para entender as regras do jogo. Como a teoria fraca não entende as regras, a pergunta é sem sentido.

A Visão de Visser (O Autor):
Visser diz: "Espera aí! Isso não cola."
Ele usa uma analogia simples: Imagine que você provou algo complexo usando um supercomputador (ZFC). Alguém pergunta: "Você consegue provar isso usando apenas uma calculadora de mão (ZF)?" Se a resposta for "não", não significa que a calculadora tem um significado diferente de "divisão". Significa apenas que a calculadora é fraca demais para fazer a conta. O significado da conta é o mesmo, só que a ferramenta é insuficiente.
Visser defende que Bezboruah e Shepherdson estavam certos: é um desafio técnico fascinante ver até onde a "calculadora" consegue chegar, mesmo que ela não consiga provar sua própria segurança.

2. A Comparação: O Caminho de Pudlák vs. O Caminho de Bezboruah

O artigo compara duas formas de chegar à mesma conclusão (que a teoria fraca não prova sua própria consistência):

• O Caminho Moderno (Pudlák): É como usar um elevador de alta tecnologia. Você usa teorias avançadas e interpretações complexas para mostrar que, se a teoria fraca provasse sua consistência, ela se tornaria tão forte que entraria em contradição. É elegante, mas requer "equipamento pesado" que não existia em 1976.
• O Caminho de Bezboruah & Shepherdson (O "Truque de Mágica"): Eles não usaram elevadores. Eles construíram um modelo (uma espécie de universo alternativo) onde as regras da teoria fraca são seguidas, mas, de alguma forma, existe uma prova de que "tudo está errado" (uma contradição). É como construir uma casa de brinquedo que, segundo as regras do brinquedo, deveria ser sólida, mas que, se você olhar de perto, tem um buraco no chão que permite que o chão afunde.

3. A Nova Contribuição: O Código de Markov

A parte mais técnica (e genial) do artigo é a Seção 4.
Bezboruah e Shepherdson usaram um método antigo e complicado para codificar sequências (como uma lista de passos de uma prova) chamado "função beta".

Visser decide reescrever a prova usando uma ideia diferente, baseada em Matrizes e no trabalho de um matemático chamado Markov.

• A Analogia das Matrizes: Imagine que cada número ou passo da prova é representado por uma matriz (uma tabela de números).
• O Truque: Visser cria um "universo" (um modelo matemático) onde ele mistura duas sequências infinitas:
  1. Uma sequência gigante de "Axiomas Verdadeiros" (como se fosse uma parede de tijolos).
  2. Uma sequência gigante de "Conclusões Falsas" (como se fosse um buraco no chão).
• Ele usa um código especial (Markov) para colar essas duas sequências. No universo normal, você vê que a colagem não faz sentido (é como colar o teto no chão). Mas, no universo "fraco" que ele construiu, a teoria não consegue ver a falha na colagem. Para a teoria fraca, aquilo parece uma prova válida de que "tudo é falso".

O Resultado: Ele mostra que, mesmo usando esse novo código de matrizes, a teoria fraca falha em perceber que sua própria prova é um erro. Ela "acredita" que provou sua inconsistência, o que é impossível se ela fosse realmente consistente.

4. Por que isso importa? (A Lição Final)

O artigo é importante por três motivos principais:

1. Defesa de uma Ideia: Ele tira o "estigma" de que o trabalho de Bezboruah e Shepherdson era inútil. Mostra que, mesmo que a teoria seja fraca, a pergunta "ela prova sua consistência?" é válida e interessante.
2. Diversidade de Métodos: Mostra que existem várias formas de atacar o mesmo problema. O método de Gödel/Pudlák é como um martelo gigante; o método de Bezboruah/Visser é como um bisturi cirúrgico que constrói modelos específicos.
3. Educação: A prova de Visser é didática. Ela mostra visualmente (através das matrizes e do modelo construído) a diferença entre "tudo é universalmente verdadeiro" e "existe uma exceção". É como mostrar a diferença entre dizer "todos os cisnes são brancos" e encontrar um cisne preto em um lago específico.

Em resumo:
O artigo é uma celebração da persistência matemática. Visser pega uma ideia antiga que foi criticada por um "guru", defende sua validade, e a recria com uma nova ferramenta (código de matrizes) para mostrar que, mesmo nas estruturas matemáticas mais simples e frágeis, a sombra da incompletude de Gödel ainda está presente, impedindo que elas se vejam como perfeitas.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "On a Theorem by Bezboruah & Shepherdson" de Albert Visser, apresentado em português.

1. O Problema e o Contexto Histórico

O artigo centra-se no teorema de incompletude provado por Bezboruah e Shepherdson em 1976 ([BS76]), que estabelece que a teoria fraca $PA^-$ (a teoria da parte não-negativa de um anel comutativo ordenado discretamente) não prova a sua própria consistência, nem a consistência de teorias ainda mais fracas como $Q$ (Aritmética de Robinson) ou $R$.

O problema central abordado por Visser é a objeção de Georg Kreisel a este resultado. Kreisel argumentou que, em teorias tão fracas como $Q$, a fórmula que expressa a consistência ($con(Q)$) não expressa realmente o conceito filosófico de "consistência", pois $Q$ não consegue provar as propriedades desejadas do predicado de prova (como as condições de Hilbert-Bernays ou Löb). Para Kreisel, tal resultado seria apenas uma propriedade algébrica sem interesse filosófico.

Visser rejeita a objeção de Kreisel, argumentando que o significado das fórmulas não deve variar dependendo da teoria em que são interpretadas. Se uma fórmula expressa consistência na aritmética verdadeira, ela deve ser considerada como tal mesmo em sub-teorias, independentemente da capacidade dessas sub-teorias de provar as propriedades do predicado de prova.

2. Metodologia e Abordagem

O artigo utiliza uma abordagem multifacetada que combina lógica matemática, teoria dos modelos e teoria da prova:

• Análise Filosófica e Lógica: Visser desmonta o argumento de Kreisel, defendendo que a validade do Teorema da Incompletude de Segunda Gôdel para $Q$ é um desafio técnico válido e didaticamente valioso, independentemente das condições de "correção intensional" exigidas por Kreisel.
• Comparação de Teoremas: O autor compara o resultado de Bezboruah-Shepherdson com a versão moderna do Teorema da Incompletude de Segunda Gôdel desenvolvida por Pavel Pudlák.
  • A prova de Pudlák baseia-se na interpretação de $S^1_2$ (teoria da computabilidade em tempo polinomial) num "corte definível" dentro de $Q$.
  • A prova de Bezboruah-Shepherdson é construtiva, criando um modelo não-padrão de $PA^-$ que contém uma "prova" de inconsistência.
• Codificação de Sequências (Novidade): A principal contribuição metodológica de Visser é a re-prova do teorema de Bezboruah-Shepherdson utilizando uma codificação de sequências baseada na ideia de Nielsen e Markov, em vez da função $\beta$ tradicional de Gödel.
  • Utiliza o grupo $SL_2(\mathbb{Z}^+)$ (matrizes $2 \times 2$ com entradas inteiras não-negativas e determinante 1).
  • Explora o isomorfismo entre $SL_2(\mathbb{Z}^+)$ e o monoide livre gerado por duas matrizes $A$ e $B$.
  • Define "ur-strings" (sequências primitivas) através de produtos de matrizes, permitindo codificar provas de estilo Hilbert.

3. Principais Contribuições e Resultados

A. Defesa do Teorema de Bezboruah-Shepherdson

Visser demonstra que a objeção de Kreisel não se sustenta. Ele argumenta que:

1. O significado de uma fórmula não depende da capacidade da teoria de provar as suas propriedades de prova.
2. O resultado tem valor didático: a construção de modelos de Bezboruah-Shepherdson torna visível a inconsistência, algo que não é possível visualizar em modelos de teorias como $S^1_2$.
3. O contraste entre o Teorema de Gôdel (versão Pudlák) e o de Bezboruah-Shepherdson ilumina as diferenças entre sentenças universais e sentenças $\Pi^0_1$.

B. Comparação entre Pudlák e Bezboruah-Shepherdson

O artigo estabelece que, embora ambos os resultados levem à conclusão de que $Q \nvdash con(Q)$, eles são fundamentalmente diferentes:

• Escopo: O teorema de Pudlák generaliza para interpretações e funciona para uma vasta gama de codificações de Gödel. O teorema de Bezboruah-Shepherdson é específico para certas codificações (como a função $\beta$ ou a de Markov) e não se generaliza facilmente para versões de interpretação.
• Mecanismo: Pudlák usa a persistência descendente de sentenças $\Pi^0_1$ e cortes definíveis. Bezboruah-Shepherdson usa a construção de um modelo com uma "prova" de falsidade que é válida no modelo, mas não na aritmética padrão.

C. Nova Prova com Codificação de Markov (Seção 4)

Visser fornece uma prova alternativa do teorema utilizando a codificação de Markov em $SL_2(R^+)$.

• Construção do Modelo: Considera modelos não-padrão da aritmética verdadeira $M$ e $N$ (onde $N$ é uma extensão elementar final de $M$).
• Elementos Chave: Define elementos não-padrão $a \in M$ e $b \in N \setminus M$. Constrói uma matriz $\beta = [n]^a [m]^b$, onde $[n]$ e $[m]$ são matrizes geradoras.
• O Modelo $K$: Constrói um submodelo $K$ (parte não-negativa de um anel ordenado discretamente) gerado pelas entradas de $\beta$.
• O Paradoxo da Prova: No modelo $K$, a sequência $\beta$ é interpretada como uma prova válida de $\bot$ (falso) no sistema BeSh (uma teoria trivial com axioma $\bot \to \bot$ e regra Modus Ponens).
  • A sequência começa com $a$ ocorrências de $(\bot \to \bot)$ e termina com $b$ ocorrências de $\bot$.
  • No entanto, a "prova" falha em $N$ (e na aritmética verdadeira) porque a transição de axiomas para conclusões ocorre num ponto que não existe no corte de números padrão de $K$.
• Resultado Principal (Teorema 4.1): A teoria $PA^-$ (mais todas as sentenças universais verdadeiras) não prova a consistência de BeSh quando se usa a codificação de Markov.

4. Significado e Impacto

• Validação Técnica: O artigo reabilita o trabalho de Bezboruah e Shepherdson, mostrando que o seu resultado é robusto e não depende apenas da função $\beta$, mas pode ser adaptado a outras estruturas algébricas (como matrizes).
• Insights sobre Modelos: A construção do modelo ilustra a diferença sutil entre sentenças puramente universais e sentenças $\Pi^0_1$, mostrando como a consistência pode falhar em modelos não-padrão mesmo quando a teoria parece "correta" universalmente.
• Didática: Oferece uma visualização concreta de como uma prova de inconsistência pode existir num modelo de uma teoria fraca, algo que é abstrato em outras abordagens.
• Colaboração com IA: Visser nota no artigo que utilizou o ChatGPT para auxiliar na dedução das equações de recorrência e na caracterização dos autovalores das matrizes na prova do Lema 4.3, destacando a utilidade de ferramentas de IA em tarefas matemáticas de rotina para acelerar o processo de descoberta.

Em suma, o artigo de Visser não apenas defende a relevância filosófica e técnica do teorema de Bezboruah-Shepherdson contra as críticas de Kreisel, mas também expande o seu alcance através de uma nova prova baseada em teoria de matrizes, enriquecendo a compreensão das limitações das teorias aritméticas fracas.