The proof theory and semantics of second-order (intuitionistic) tense logic

Resumo Técnico: A Teoria da Prova e a Semântica da Lógica de Tempo de Segunda Ordem (Intuicionista)

Problema e Motivação
O artigo aborda o desenvolvimento fundamental da lógica de tempo de segunda ordem sobre bases tanto clássicas quanto intuicionistas. Embora a lógica de segunda ordem seja uma ferramenta padrão na lógica matemática e computacional, seus fundamentos metalógicos, particularmente no que diz respeito à teoria da prova e semântica, têm apresentado desafios significativos. Uma dificuldade específica na lógica modal intuicionista é a falta de consenso sobre a axiomatização apropriada da modalidade diamante ($\Diamond$), que não pode ser definida em termos do box ($\Box$) como ocorre na lógica clássica. Diversas propostas existem (por exemplo, CK, IK), mas elas frequentemente envolvem escolhas arbitrárias de axiomas.

Os autores propõem uma abordagem unificada utilizando quantificação de segunda ordem. Uma observação fundamental é que, na lógica de segunda ordem intuicionista, os conectivos positivos podem ser definidos a partir do fragmento negativo. Especificamente, o artigo demonstra que a modalidade diamante (e sua teoria associada) pode ser recuperada usando apenas boxes ($\Box$) e backward boxes ($\blacksquare$), desde que ambas as modalidades de ida e de volta (lógica de tempo) estejam incluídas. Isso permite uma definição de $\Diamond A$ como $\forall X(\Box(A \to \blacksquare X) \to X)$, evitando axiomatizações arbitrárias.

Metodologia
Os autores desenvolvem três definições paralelas para a lógica de tempo de segunda ordem:

1. Axiomática: Os sistemas $Kt2$ (clássico) e $IKt2$ (intuicionista) são definidos. Eles estendem a lógica proposicional de segunda ordem com modalidades normais e axiomas de adjunção para pares de tempo. Crucialmente, eles incluem um axioma de compreensão total, permitindo definições impredicativas.
2. Semântica: O artigo introduz semântica (bi)relacional para o caso intuicionista e semântica relacional para o caso clássico. Essas estruturas incluem uma ordem parcial (para o intuicionismo) e uma relação de acessibilidade. Uma característica central é a exigência de "compreensividade", onde o domínio dos conjuntos inclui as extensões de todas as fórmulas, modelando efetivamente o axioma de compreensão. Os autores também definem "estruturas de predicados" (onde os mundos são modelos modais clássicos) e mostram sua equivalência às estruturas birelacionais.
3. Teoria da Prova: Cálculos de sequente rotulados ($\ell Kt2$ e $\ell IKt2$) são propostos. Esses sistemas utilizam rótulos de mundo e átomos relacionais para internalizar a semântica. Para o caso intuicionista, um cálculo de múltiplos sucessivos intermediário ($m\ell IKt2$) é introduzido para facilitar argumentos de busca de prova, o qual é mostrado como conservativo sobre a versão de sucessivo único.

A estratégia técnica central envolve provar que essas três definições coincidem. Isso é visualizado como "grandes turnês" conectando a provabilidade axiomática, a validade semântica e a derivabilidade teórica da prova. As provas de completude baseiam-se em um argumento de busca de prova adaptado da noção de semi-valuações de Schütte e do conceito de valores possíveis de Prawitz, superando os obstáculos da impredicatividade.

Principais Contribuições e Resultados

• Definição de Diamantes via Quantificação de Segunda Ordem: O artigo estabelece que, na presença de modalidades de tempo, a modalidade diamante é definível em lógica de segunda ordem intuicionista como $\Diamond A \iff \forall X(\Box(A \to \blacksquare X) \to X)$. Isso recupera a teoria de Fischer Servi e a $IK$ de Simpson e a $IKt$ de Ewald sem escolhas arbitrárias de axiomas.
• Correção e Completude:
  • Intuicionista: O sistema $IKt2$ é provado correto e completo em relação à semântica birrelacional compreensiva (Teorema Principal 3.3).
  • Clássica: O sistema $Kt2$ é provado correto e completo em relação à semântica relacional compreensiva (Teorema Principal 3.14).
• Admissibilidade do Corte (Cut-Admissibility): O artigo estabelece a admissibilidade do corte para os cálculos de sequente rotulados $\ell Kt2$ e $\ell IKt2$ (Teorema Principal 4.2). Isso é alcançado via um argumento de busca de prova que constrói contramodelos a partir de buscas de prova falhas.
  • Para o caso clássico, o argumento adapta as semi-valuações de Schütte e os valores possíveis de Prawitz para extrair um contramodelo relacional.
  • Para o caso intuicionista, o argumento é mais complexo, exigindo a construção de uma árvore de busca de prova (em vez de um ramo) para lidar com a ordem parcial dos modelos de Kripke, resultando finalmente em um contramodelo de estrutura de predicado.
• Correção Axiomática de Provas Rotuladas: O artigo fornece uma tradução de provas rotuladas para provas axiomáticas (Teorema 7.1), completando o ciclo de equivalências. Isso envolve interpretar sequentes de politree rotulados como fórmulas de tempo e mostrar que cada regra de inferência corresponde a uma regra admissível no sistema axiomático.
• Relação Clássica-Intuicionista: O artigo estabelece que a lógica de tempo de segunda ordem clássica ($Kt2$) pode ser incorporada no sistema intuicionista ($IKt2$) via uma tradução negativa (Teorema 8.2), semelhante à tradução de Gödel-Gentzen.

Significância
O artigo afirma fornecer uma base robusta e unificada para a lógica de tempo de segunda ordem. Ao demonstrar que as definições axiomática, semântica e teórica da prova coincidem, ele valida a axiomatização mínima escolhida. O trabalho aborda o desafio específico de definir modalidades positivas em um ambiente intuicionista sem axiomas arbitrários, aproveitando o poder expressivo da quantificação de segunda ordem.

A metodologia é apresentada como aplicável tanto ao cenário clássico quanto ao intuicionista, sendo que o caso intuicionista exige adaptações técnicas inéditas para lidar com a impredicatividade e a estrutura dos modelos de Kripke. Os resultados são significativos para o estudo metalógico de lógicas modais, oferecendo uma conta teórica da prova completa (incluindo eliminação de corte) para a lógica de tempo de segunda ordem, um domínio onde tais resultados eram anteriormente ausentes ou restritos à semântica total (que não é recursivamente enumerável). O artigo posiciona-se como uma contribuição para as ferramentas teóricas necessárias para a adoção da lógica modal de segunda ordem em áreas como representação de conhecimento e inteligência artificial, conforme observado em trabalhos relacionados.