Uniform Realizability Interpretations

Resumo Técnico: Interpretações de Realizabilidade Uniforme

1. O Problema

A realizabilidade é uma semântica fundamental para a lógica intuicionista e construtiva, onde fórmulas são interpretadas através de "realizadores" (testemunhas computacionais). Tradicionalmente, desde a realizabilidade de números de Kleene (1945), a interpretação de quantificadores varia significativamente entre diferentes variantes:

• Abordagem Tradicional (Kleene, Kreisel): Os realizadores para fórmulas existenciais ($\exists n A(n)$) devem conter explicitamente o testemunho do número $n$ (ex: um par $\langle n, r \rangle$ onde $r$ realiza $A(n)$). Para o universal ($\forall n A(n)$), o realizador é uma função que, dado $n$, produz um realizador para $A(n)$.
• Abordagens Modernas (Realizabilidade de Herbrand, Realizabilidade de Aprendizado, Realizabilidade Clássica): Em certas variantes, os quantificadores são tratados de forma uniforme. Um realizador para $\exists n A(n)$ não fornece explicitamente $n$, mas sim um objeto que, sob certas condições, implica a existência de tal $n$. Da mesma forma, um realizador para $\forall n A(n)$ deve funcionar uniformemente para todo $n$ sem depender de $n$ como entrada explícita para gerar o realizador.

O problema central abordado pelo artigo é a falta de um quadro unificado que explique e generalize essas diferentes abordagens. Não havia uma definição formal que isolasse o tratamento dos quantificadores da interpretação das fórmulas atômicas, permitindo comparar e integrar variantes como a realizabilidade de Kleene, a modificada de Kreisel, a de Herbrand e a de aprendizado (learning realizability).

2. Metodologia

Os autores propõem um quadro paramétrico de realizabilidade uniforme. A metodologia baseia-se em separar a interpretação dos quantificadores da interpretação dos predicados atômicos.

• Distinção de Quantificadores: O artigo distingue entre quantificadores não qualificados (uniformes) $\exists x A(x)$ e $\forall x A(x)$, e quantificadores qualificados (tipados) $\exists^B x A(x)$ e $\forall^B x A(x)$.
  • A proposta é que os quantificadores não qualificados recebam sempre uma interpretação uniforme.
  • Os quantificadores qualificados são tratados como abreviações: $\exists^B x A(x) \equiv \exists x (B(x) \land A(x))$ e $\forall^B x A(x) \equiv \forall x (B(x) \to A(x))$.
• Interpretação Base: Define-se uma "interpretação base" que associa a cada símbolo de predicado $P$ da teoria fonte uma relação $x \triangleright_P a$ na teoria alvo. Aqui, $a$ são os realizadores (ou testemunhas) para $P(x)$.
• Definição de Realizabilidade Uniforme: A realizabilidade $a \text{ ur } A$ é definida por indução sobre a estrutura de $A$:
  • Atômico: $a \text{ ur } P(x) \iff x \triangleright_P a$.
  • Conjunção: $a, b \text{ ur } A \land B \iff (a \text{ ur } A) \land (b \text{ ur } B)$.
  • Implicação: $f \text{ ur } A \to B \iff \forall a ((a \text{ ur } A) \to (f(a)\downarrow \land f(a) \text{ ur } B))$.
  • Existencial (Uniforme): $a \text{ ur } \exists x A(x) \iff \exists x (a \text{ ur } A(x))$. Nota: O realizador $a$ não precisa conter $x$ explicitamente.
  • Universal (Uniforme): $a \text{ ur } \forall x A(x) \iff \forall x (a \text{ ur } A(x))$. Nota: O mesmo realizador $a$ deve funcionar para todo $x$.

A teoria alvo ($T$) deve ser fechada sob lógica intuicionista e possuir um tipo para realizadores com aplicação de função e $\lambda$-abstração.

3. Principais Contribuições

1. Unificação Teórica: O quadro proposto unifica variantes aparentemente distintas da realizabilidade. Ao parametrizar a interpretação apenas pelos predicados atômicos (como igualdade, falsidade e o predicado de número natural $N(n)$), o mesmo mecanismo de realizabilidade uniforme gera diferentes interpretações conhecidas.
2. Generalização de Quantificadores: A abordagem formaliza a ideia de que a "uniformidade" dos quantificadores é uma escolha de interpretação, não uma propriedade intrínseca da lógica, permitindo tratar quantificadores internos e externos de maneira consistente.
3. Teorema de Corretude (Soundness) Geral: Os autores provam que, se todos os axiomas não-lógicos de uma teoria fonte $S$ são realizáveis sob uma dada interpretação base, então todos os teoremas de $S$ são realizáveis. Isso reduz a verificação de corretude de uma interpretação complexa à verificação de axiomas básicos.
4. Modelagem de Casos Específicos: O artigo demonstra como instanciar o quadro geral para reproduzir:
   • Realizabilidade de Kleene: Onde $N(n)$ é interpretado precisamente ($n=a$) e a igualdade é estrita.
   • Realizabilidade Modificada de Kreisel: Onde os realizadores são totais e os tipos são definidos recursivamente.
   • Realizabilidade de Herbrand (Não-Standard): Onde $N(n)$ é interpretado uniformemente (sem realizador) e a quantificação sobre números "padrão" ($st(n)$) usa conjuntos finitos como realizadores.
   • Realizabilidade Clássica: Onde o falso ($\bot$) e a igualdade recebem interpretações não triviais (usando uma tradução de Friedman-Dragalin) para extrair conteúdo computacional de fórmulas negadas.
   • Realizabilidade de Aprendizado (Aschieri-Berardi): Onde os realizadores são transformadores de estado que atualizam o conhecimento sobre testemunhas potenciais.

4. Resultados

• Equivalências Formais: O artigo estabelece que, sob as interpretações base corretas, a definição de realizabilidade uniforme ($\text{ur}$) é equivalente às definições clássicas de cada variante (ex: Proposições 3.2, 3.5, 3.7, 3.10, 3.12).
• Tratamento da Indução: O artigo analisa como a indução é realizada em diferentes contextos. Por exemplo, na interpretação aproximada (onde o realizador é um limite superior), a realização da indução requer uma operação de "junção" (join) para combinar realizadores, enquanto na interpretação precisa (Kleene), usa-se recursão primitiva padrão.
• Conservatividade e Extensões: O quadro permite adicionar fórmulas classicamente válidas (como a eliminação de dupla negação para fórmulas uniformes) como axiomas, desde que os predicados envolvidos sejam interpretados uniformemente. Isso levanta questões sobre a conservatividade da teoria estendida sobre a original, um ponto discutido nas conclusões.

5. Significado e Impacto

O trabalho de Berger e Oliva é significativo porque oferece uma metateoria para a realizabilidade. Em vez de tratar cada variante (Kleene, Herbrand, Aprendizado) como um sistema isolado com regras ad-hoc, eles mostram que a complexidade reside na interpretação dos predicados atômicos, enquanto a estrutura lógica (quantificadores e conectivos) pode ser tratada de forma uniforme e abstrata.

Isso permite:

1. Comparação Sistemática: Facilita a comparação e a transferência de resultados entre diferentes interpretações.
2. Novas Interpretações: Fornece um "esqueleto" para construir novas variantes de realizabilidade simplesmente escolhendo uma nova interpretação base para os predicados atômicos.
3. Clarificação Conceitual: Ajuda a entender a natureza da "informação" em provas intuicionistas, distinguindo entre o que é fornecido explicitamente (testemunhas) e o que é inferido uniformemente.

Em suma, o artigo estabelece que a diversidade de interpretações de realizabilidade na literatura é, em grande parte, uma questão de como se escolhe interpretar os predicados básicos e o falso, enquanto a lógica subjacente pode ser unificada sob o princípio da uniformidade dos quantificadores.