From Herbrand schemes to functional interpretation

Resumo Técnico: De esquemas de Herbrand para interpretação funcional

Problema
O artigo aborda o desafio de extrair disjunções de Herbrand diretamente de provas do cálculo de sequentes clássico sem depender da eliminação de cortes. O teorema de Herbrand é tradicionalmente provado via eliminação de cortes (gerando um "meio-sequente"), mas trabalhos recentes de Afshari, Hetzl e Leigh demonstraram que as disjunções de Herbrand podem ser extraídas diretamente usando "esquemas de Herbrand" — um método que trata as provas como esquemas de recursão de ordem superior. No entanto, essa abordagem depende de regras de reescrita específicas baseadas em gramática. Por outro lado, as interpretações funcionais (como as de Gerhardy e Kohlenbach) operam tipicamente sobre sistemas axiomáticos de estilo Hilbert. O artigo busca unir esses dois domínios: pode o mecanismo central dos esquemas de Herbrand ser reformulado como uma interpretação funcional do cálculo de sequentes clássico, proporcionando uma interpretação computacional natural de provas de sequentes, semelhante às abordagens teóricos-dos-jogos?

Metodologia
Os autores desenvolvem uma interpretação funcional para o cálculo de sequentes clássico baseada em um lambda-cálculo tipado estendido com um operador de distinção de casos. A metodologia procede da seguinte forma:

1. Estrutura de Tipos: O sistema utiliza uma teoria de tipos com dois tipos atômicos: $\iota$ (indivíduos) e $\square$ (tipo nulo). Tipos complexos são formados via produtos e espaços de funções. Crucialmente, cada fórmula $A$ é associada a dois tipos distintos:

   • Um tipo de evidência $[A]$ (representando uma testemunha ou estratégia para o "Provador").
   • Um tipo de contra-evidência $\langle A \rangle$ (representando uma contra-testemunha ou estratégia para o "Refutador").
     Estes tipos são definidos recursivamente com base na estrutura lógica de $A$ (ex: $[\exists x A] = \iota \times \langle \neg A \rangle$, $[\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle$).

2. Extração de Termos (Transformadores de Termos): Os autores definem um "transformador de termo" para cada ocorrência de fórmula em um sequente. Dada uma prova $p$ de um sequente $A_1, \dots, A_n$, a extração associa cada índice $i$ a um transformador de termo $F^p_i$. Este transformador recebe termos de tipos de contra-evidência $\langle A_1 \rangle, \dots, \langle A_n \rangle$ como entrada e produz um termo de tipo de evidência $[A_i]$.

   • A extração é definida por recursão estrutural na prova $p$, correspondendo à última regra de inferência utilizada (ex: $\exists$, $\neg\exists$, $\vee$, $\neg\vee$, corte, contração).
   • Ao contrário dos esquemas de Herbrand, que exigem regras de reescrita ad-hoc para símbolos não-terminais, o comportamento dos termos extraídos aqui é governado inteiramente pelas regras de reescrita padrão da teoria de tipos subjacente (redução beta, projeção e distinção de caso).

3. Estrutura Lógica: A extração opera dentro de um sistema livre de quantificadores $QF$ aumentado com axiomas para o operador de distinção de casos $[u \text{ se } A \text{ senão } v]$. O resultado principal estabelece que, para qualquer prova $p$ de um sequente $A_1, \dots, A_n$, e para quaisquer termos de contra-evidência fechados $u_1, \dots, u_n$, a disjunção das fórmulas interpretadas ocorre:
   $$\vdash_{QF} A_1 \frac{F^p_1 \vec{u}}{u_1} \vee \dots \vee A_n \frac{F^p_n \vec{u}}{u_n}$$
   Aqui, a notação $A \frac{t}{u}$ representa a fórmula $A$ onde a evidência $t$ é confrontada com a contra-evidência $u$.

Principais Contribuições

• Reformulação de Esquemas de Herbrand: O artigo demonstra que os esquemas de Herbrand podem ser reconfigurados como uma interpretação funcional do cálculo de sequentes. Os "símbolos não-terminais" de um esquema de Herbrand correspondem aos transformadores de termos extraídos aqui, e as "regras de reescrita" do esquema são substituídas pelas regras de redução intrínsecas do lambda-cálculo.
• Extração Direta sem Eliminação de Cortes: O método fornece um algoritmo direto para extrair termos realizadores (e, subsequentemente, disjunções de Herbrand) de provas de cálculo de sequentes sem realizar a eliminação de cortes.
• Construção Modular: O processo de extração é modular; o transformador de termo para uma prova é construído uniformemente a partir dos transformadores de suas sub-provas imediatas, baseando-se na regra de inferência aplicada.
• Tratamento de Contração: Os autores utilizam o operador de distinção de casos (de Gerhardy e Kohlenbach) para lidar com a estrutura de ramificação introduzida pelas regras de contração no cálculo de sequentes, evitando a necessidade de estruturas de tipos mais complexas ("Herbrandizadas") envolvendo conjuntos finitos.

Resultados

• Teorema 1 (Correção/Soundness): Para qualquer prova $p$ de um sequente $A_1, \dots, A_n$, os transformadores de termo extraídos satisfazem a propriedade de interpretação funcional: a disjunção das fórmulas interpretadas é provável em $QF$ para quaisquer entradas de contra-evidência fechadas.
• Teorema 2 (Teorema de Herbrand): Como corolário, se uma fórmula existencial $\exists x A$ (com $A$ livre de quantificadores) é provável, a extração produz um conjunto finito de termos fechados $t_1, \dots, t_n$ tal que a disjunção de Herbrand $A[t_1/x] \vee \dots \vee A[t_n/x]$ é provável. Isso é alcançado reduzindo o termo extraído à sua forma normal e analisando sua estrutura.
• Normalização Forte: O sistema de termos subjacente é mostrado como sendo fortemente normalizador, garantindo que os termos extraídos sempre reduzam a uma forma canônica.

Significado e Alegações
O artigo afirma que este trabalho fornece uma "interpretação computacional natural do cálculo de sequentes clássico". Ao reformular os esquemas de Herbrand como uma interpretação funcional, os autores argumentam que a conexão entre o teorema de Herbrand e a interpretação funcional é mais fundamental do que anteriormente percebido.

Especificamente, o artigo destaca uma ligação conceitual com abordagens teóricas-dos-jogos (como as de Alcolei et al.). Nesta visão:

• Os termos extraídos representam estratégias para um "Provador" em um jogo concorrente.
• As entradas (termos de contra-evidência) representam estratégias para um "Refutador".
• A estrutura da prova corresponde a processos concorrentes onde o Provador pode observar os movimentos do Refutador em uma "thread" (cópia paralela do jogo) e usar essa informação para determinar seus próprios movimentos em outra "thread".

Os autores posicionam este trabalho como a conclusão de uma imagem emergente onde os esquemas de Herbrand, as interpretações funcionais e a semântica de jogos convergem para explicar o conteúdo computacional da lógica clássica. Eles afirmam explicitamente que os resultados são autossuficientes e não requerem conhecimento prévio de esquemas de Herbrand, embora o procedimento de extração tenha sido derivado através de um exame detalhado da estrutura de tipos da literatura existente de esquemas de Herbrand.