Conceptual completeness for subgeometric logics

Título: Completude Conceitual para Lógicas Subgeométricas
Autores: Ivan Di Liberti, Umberto Tarantino e Lingyuan Ye

1. Problema e Motivação

O artigo aborda a noção de completude conceitual dentro do arcabouço das lógicas subgeométricas (fragmentos da lógica geométrica). Tradicionalmente, a completude conceitual, estabelecida por Makkai para a lógica coerente de primeira ordem [Mak87], é interpretada como um teorema de reconstrução: a sintaxe de uma teoria pode ser recuperada de sua semântica (a categoria de modelos), desde que esta última seja dotada de uma estrutura adicional (especificamente, uma "ultraestrutura" derivada de ultraprodutos).

Os autores identificam uma limitação nesta visão tradicional: ela depende fortemente de semânticas baseadas em conjuntos e da imposição de estrutura extra (ultraestrutura) sobre categorias de modelos. Além disso, abordagens anteriores para provar a completude conceitual para vários fragmentos lógicos frequentemente exigiam técnicas independentes e ad-hoc para cada fragmento. O artigo busca:

1. Reformular a completude conceitual como um fenômeno puramente sintático, especificamente como uma dualidade entre teorias e seus topoi classificadores, em vez de uma reconstrução a partir de modelos baseados em conjuntos.
2. Fornecer um arcabouço modular para provar a completude conceitual para várias lógicas subgeométricas sem depender do teorema de reconstrução original de Makkai ou impor estruturas artificiais na semântica.
3. Esclarecer a relação entre esta nova noção sintática e a tradicional reconstrução semântica de Makkai, particularmente sob a suposição de completude em relação a modelos baseados em conjuntos.

2. Metodologia e Arcabouço

Os autores baseiam-se no arcabouço da injetividade de Kan à direita na 2-categoria dos topoi ($\mathbf{Topoi}$), conforme desenvolvido em seu trabalho anterior [DLY25].

• Lógicas como Classes de Morfismos: Uma lógica $\mathcal{H}$ é definida como uma classe de morfismos geométricos entre topoi. Um topo $\mathcal{X}$ "pertence formalmente" a $\mathcal{H}$ se ele é (fracamente) injetivo de Kan à direita em relação aos morfismos de $\mathcal{H}$. Isso captura a ideia de que os pontos generalizados do topo admitem a estrutura prescrita pela lógica.
• Categorias Sintáticas e Topoi Classificadores:
  • Para um topo $\mathcal{X}$ formalmente em $\mathcal{H}$, a categoria sintática $\text{Syn}_{\mathcal{H}}(\mathcal{X})$ é definida como a categoria de morfismos geométricos $\mathcal{X} \to \text{Set}[\mathcal{O}]$ (onde $\text{Set}[\mathcal{O}]$ é o classificador de objetos).
  • Associado a $\mathcal{H}$ está um monad de sintaxe $T_{\mathcal{H}}$ na categoria das pequenas categorias finitamente completas ($\mathbf{Lex}$).
  • O topos classificador $\text{Cl}_{\mathcal{H}}(A)$ é construído para uma $T_{\mathcal{H}}$-álgebra $A$.
• Definição de Completude Conceitual: Uma lógica limitada $\mathcal{H}$ é conceitualmente completa se o 2-functor $\text{Cl}_{\mathcal{H}}: \text{Alg}(T_{\mathcal{H}})^{\text{op}} \to \mathbf{WRInj}(\mathcal{H})$ é 2-totalmente fiel.
• Insight Chave: Os autores mostmostram que a completude conceitual é equivalente ao fato de a adjunção $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ ser uma reflexão (isto é, a unidade é uma equivalência). Isso significa que toda $T_{\mathcal{H}}$-álgebra é essencialmente a categoria sintática de seu topo classificador. Esta formulação desvincula o conceito da semântica baseada em conjuntos e foca na relação entre sintaxe (álgebras) e semântica baseada em sintaxe (topoi classificadores).

3. Principais Contribuições e Resultados

A. Caracterização da Completude Conceitual

O artigo estabelece que uma lógica $\mathcal{H}$ é conceitualmente completa se, e somente se, para toda pequena $T_{\mathcal{H}}$-álgebra $A$, o embedimento $A \hookrightarrow \text{Syn}_{\mathcal{H}}(\text{Cl}_{\mathcal{H}}(A))$ é uma equivalência de categorias (Corolário 2.2.3). Isso reformula o problema como determinar se a categoria sintática do topo classificador recupera a álgebra original.

B. Prova da Completude Conceitual para Quatro Lógicas

Utilizando um Lema de Redução (Proposição 3.1.2), os autores provam a completude conceitual para quatro lógicas específicas, identificando-as com doutrinas conhecidas e mostrando que suas categorias sintáticas recuperam as álgebras. As provas utilizam subclasses específicas de morfismos (sublógicas) para simplificar a análise:

1. Lógica Coerente ($\mathcal{H}_{\text{flat}}$): Provada como conceitualmente completa. Os autores mostram que a doutrina $T_{\mathcal{H}_{\text{flat}}}$ coincide com a construção de pré-topos livre. Eles caracterizam a categoria sintática de um topo coerente como a subcategoria plena dos objetos coerentes, recuperando o pré-topos original.
2. Lógica Regular ($\mathcal{H}_{\text{matte}}$): Provada como conceitualmente completa. A doutrina corresponde à construção de categoria (Barr-)exata livre. Mostra-se que a categoria sintática consiste de objetos regulares.
3. Lógica Essencialmente Algébrica com Falsum ($\mathcal{H}_{\text{dom}}$): Provada como conceitualmente completa. A doutrina corresponde à categoria lex livre com um objeto inicial estrito. A prova envolve a análise de embedimentos densos e mostra que os objetos na categoria sintática são retratos de representáveis.
4. Lógica Disjuntiva Finitária ($\mathcal{H}_{\text{pure}}$): Provada como conceitualmente completa. A doutrina corresponde à construção de categoria lextensiva livre. A prova utiliza "embedimentos puros" e a união de uma categoria com sua álgebra booleana de subobjetos subterminais decidíveis.

Estes resultados fornecem novas caracterizações para estas lógicas que não dependem do teorema original de Makkai [Mak87].

C. Lógicas Conservativamente Embebidas

O artigo introduz a noção de lógicas conservativamente embebidas (Seção 4). Uma lógica é conservativamente embebida se a adjunção $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ é idempotente.

• Resultado: Toda lógica conceitualmente completa é conservativamente embebida.
• Significância: Esta propriedade possui uma interpretação prova-teórica: a inclusão da teoria da categoria sintática na teoria do topo classificador é conservativa. Isso liga a noção semântica de completude conceitual diretamente à conservatividade prova-teórica.

D. Relação com o Teorema de Makkai

Na Seção 5, os autores reconciliam sua definição sintática com o tradicional teorema de reconstrução semântica de Makkai para a lógica coerente.

• Arcabouço: Eles utilizam a teoria de ultracategorias virtuais (de [Saa25, Ham25, vGMT26]) para formalizar prescrições semânticas.
• Equivalência: Eles demonstram que, para a lógica coerente, sua noção de completude conceitual é equivalente ao resultado de Makkai (Corolário 5.3.3).
• Mecanismo: A equivalência ocorre sob a suposição de que os topoi classificadores possuem pontos suficientes (completude em relação a modelos baseados em conjuntos). Os autores decompõem o resultado em:
  1. Um componente sintático: A lógica é conceitualmente completa em seu sentido (dualidade entre álgebras e topoi classificadores).
  2. Um componente semântico: A equivalência entre topoi classificadores e ultracategorias de modelos baseados em conjuntos (induzida pela suposição de "pontos suficientes").
• Generalização: Eles definem a completude conceitual à la Makkai para lógicas gerais (Definição 5.4.1) e provam que ela é equivalente à sua noção sintática se a lógica possuir pontos baseados em conjuntos suficientes (Teorema 5.4.2).

4. Significância e Alegações

O artigo alega oferecer uma nova luz prova-teórica sobre a completude conceitual.

• Modularidade: Fornece um arcabouço unificado (via injetividade de Kan) para estudar a completude conceitual através de diferentes lógicas subgeométricas, reduzindo a necessidade de técnicas ad-hoc.
• Desvinculação da Semântica Baseada em Conjuntos: A definição primária de completude conceitual é apresentada como uma propriedade da própria lógica (uma dualidade entre teorias e topoi classificadores), independente de modelos baseados em conjuntos. A conexão com o teorema de Makkai é mostrada para ser uma consequência da completude em relação a modelos baseados em conjuntos, não a definição em si.
• Recuperação de Resultados Clássicos: O artigo recupera com sucesso o teorema original de Makkai para a lógica coerente como um caso especial onde a dualidade sintática se alinha com a reconstrução semântica via ultracategorias.
• Conservatividade: Estabelece que a completude conceitual implica uma forte propriedade de conservatividade, ligando propriedades de modelos a propriedades prova-teóricas.

Os autores mantêm a modéstia quanto ao escopo, observando que, embora tenham provado a completude conceitual para vários fragmentos, a questão de se todas as partes da lógica geométrica são conceitualmente completas permanece aberta, e a caracterização da coluna $\mathbf{WRInj}_{pw}(\mathcal{H})$ em seu quadro resumo é deixada para pesquisas futuras. Eles também notam que seus exemplos atuais situam-se "abaixo" do fragmento coerente, embora conjeturem que a teoria se aplique de forma mais ampla.