A Calculus of Apartness over Separoids: Effective Convex Representation, Stratified Conservativity, and the Complexity of Entailment

Resumo Técnico: Um Cálculo de Apartheid sobre Separoides

Enunciado do Problema
O artigo investiga a estrutura lógica e combinatória induzida pela disjunção de invólucros convexos de corpos convexos compactos no espaço euclidiano. Dado um conjunto finito de "sítios" $E$, onde cada sítio está associado a um corpo convexo compacto não vazio, o estudo foca na relação binária de apartness (apartheid ou separação) ($A \mathbin{\#} B$) entre subconjuntos disjuntos de sítios. Esta relação ocorre se os invólucros convexos das uniões dos corpos correspondentes a $A$ e $B$ forem disjuntos. O problema central é determinar até que ponto os detalhes geométricos dos corpos (dimensão, forma, coordenadas) podem ser esquecidos enquanto se retém as consequências lógicas de seus padrões de separação. Especificamente, o artigo busca axiomatizar esta relação, fornecer uma representação efetiva e classificar a complexidade do raciocínio sobre ela.

Metodologia
Os autores empregam uma abordagem de múltiplas camadas combinando geometria convexa, topologia combinatória e teoria da prova:

1. Fundação Axiomática: O artigo identifica três leis fundamentais satisfeitas pela relação de apartness de qualquer cena de corpos convexos: Simetria, Subsumção Bilateral (monotonicidade) e Vacuidade (o conjunto vazio é apartado de tudo). Estas leis definem uma estrutura chamada separoide de apartheid, que é mostrada como sendo criptomórfica aos separoides acíclicos encontrados na literatura existente (Strausz et al.), efetivamente visualizando a relação de separação a partir do seu lado complementar de "partição de Radon".
2. Representação Efetiva: Um teorema construtivo é desenvolvido para realizar qualquer separoide de apartness finito usando politopos racionais. Diferente de realizações geométricas anteriores que otimizam para a dimensão mínima, esta construção é "legível por prova" (proof-readable). Ela atribui uma coordenada a cada separação máxima e utiliza coordenadas racionais explícitas com altura de bits limitada. A construção garante uma margem euclidiana uniforme (pelo menos 2) para todas as separações, provendo robustez contra perturbações.
3. Análise de Estabilidade: Usando funções de distância e corpos paralelos externos, o artigo analisa a estabilidade da realização. Demonstra que a relação de apartness é invariante sob o alargamento de corpo paralelo externo por qualquer raio $r < 1$ e que os corpos podem ser engrossados para corpos $C^{1,1}$ de dimensão total sem alterar a relação.
4. Cálculo Lógico e Complexidade: Uma linguagem formal $L_E$ é definida com átomos representando asserções de separação. O artigo introduz um cálculo de sequente positivo ($SC_0$) e um cálculo Booleano ($ACE$). Analisa os problemas de decisão de satisfatibilidade, validade e implicação, estabelecendo sua complexidade computacional.
5. Estratificação: O artigo introduz uma disciplina de estratificação para provar um teorema de conservatividade, mostrando que o estrato Booleano (raciocínio composto) é inerte em relação ao estrato atômico (fatos positivos).

Contribuições Principais e Resultados

• Axiomatização Criptomórfica: O artigo estabelece que as três leis (Simetria, Subsumção Bilateral, Vacuidade) axiomatizam completamente a relação de apartness de corpos convexos. Isso confirma que o "esquecimento" dos detalhes geométricos não custa nada em relação à relação de consequência lógica, desde que a dimensão ambiente seja suficientemente alta.
• Representação Racional Efetiva (Teorema 4.3): Todo separoide de apartness finito é realizado por uma cena de politopos racionais. A construção é sensível à saída:
  • As coordenadas são indexadas por separações máximas.
  • Todas as coordenadas são números racionais com tamanhos de numerador e denominador explicitamente limitados ($O(\log n)$ bits).
  • A realização garante uma marg via de pelo menos 2 para cada separação bilateral.
  • A construção permite a enumeração de separações máximas e partições de Radon mínimas a partir de vários formatos de entrada (tabela completa, geradores ou oráculos de pertinência) com custo de saída exponencial, mas sem explosão aritmética oculta.
• Estabilidade e Robustez (Teorema 4.13): A realização é estável. Se cada corpo na cena for substituído por seu corpo paralelo externo com raio $r < 1$, a relação de apartness permanece inalterada. Além disso, os corpos podem ser suavizados para possuir fronteiras $C^{1,1}$ preservando a relação.
• Hierarquia de Dimensão e Limiar (Teorema 4.17): O artigo caracteriza precisamente a hierarquia de relações de consequência baseada na dimensão ambiente $d$.
  • Para $d < |E| - 1$, as relações de consequência formam uma cadeia estritamente decrescente: $|=_{0} \supsetneq |=_{1} \supsetneq \dots \supsetneq |=_{|E|-2}$.
  • A hierarquia estabiliza exatamente na dimensão $d = |E| - 1$. Para todo $d \ge |E| - 1$, a relação de consequência é idêntica à consequência geométrica livre de dimensão ($|=_{geo}$).
  • Este limiar é provado como sendo agudo; dimensões abaixo de $|E|-1$ ampliam estritamente o conjunto de asserções refutáveis.
• Cálculo Lógico e Complexidade:
  • Implicação Positiva: A implicação positiva colapsa para uma simples subsumção. Uma asserção segue de um conjunto de premissas se, e somente se, ela for vacua ou dominada componente a componente (possivelmente após uma troca) por uma única premissa. Esta verificação é linear no tamanho da entrada para codificações ordenadas.
  • Fechamento Booleano: O cálculo Booleano é sonoro, completo e decidível. A satisfatibilidade é NP-completa, e a validade é coNP-completa.
  • Conservatividade (Teorema 7.3): Uma condição de estratificação formal prova que o estrato Booleano é inerte no estrato atômico. Nenhuma quantidade de raciocínio clássico (negação, disjunção, análise de caso) pode derivar um novo fato de apartness positivo que não seja já uma subsumção dos dados atômicos.

Significância e Alegações
O artigo alega que o "núcleo estável" da fala sobre separação é pequeno, exatamente conhecido e inteiramente subsumptivo. Argumenta que, uma vez que a dimensão ambiente passa o limiar de $|E| - 1$, a geometria específica da cena torna-se irrelevante para as consequências lógicas; a relação é totalmente capturada pelas três leis axiomáticas.

A significância reside em fornecer uma "camada lógica e efetiva" para a teoria combinatória existente de separoides. Enquanto trabalhos anteriores focaram em universalidade e homomorfismos, este artigo fornece:

1. Uma teorema de representação quantitativa com margens racionais, tornando a estrutura lógica inspecionável coordenada por coordenada.
2. Uma classificação de complexidade precisa, distinguindo a trivialidade da implicação positiva da dificuldade introduzida pelas combinações booleanas.
3. Um resultado de conservatividade que separa formalmente os "dados" (separações atômicas) do "raciocínio" (lógica Booleana), mostrando que este último não adiciona novas restrições geométricas.

O artigo posiciona-se não como uma descoberta de novos fenômenos geométricos, mas como uma formalização rigorosa dos limites lógicos da separação convexa, demonstrando que o "esquecimento" do detalhe geométrico é livre de custo em termos de consequência lógica, desde que se permaneça dentro do regime estável e livre de dimensão.