Conceptual completeness for subgeometric logics

제목: 하위기하학적 논리에 대한 개념적 완전성 (Conceptual Completeness for Subgeometric Logics)
저자: Ivan Di Liberti, Umberto Tarantino, Lingian Ye

1. 문제 및 동기

본 논문은 하위기하학적 논리(subgeometric logics, 기하학적 논리의 파편들)의 틀 내에서 **개념적 완전성(conceptual completeness)**이라는 개념을 다룬다. 전통적으로, Makkai가 코히어런트 1차 논리[Mak87]에 대해 확립한 개념적 완전성은 재구성 정리(reconstruction theorem)로 해석된다. 즉, 모델의 범주(category of models)에 추가적인 구조(구체적으로는 울트라곱(ultraproduct)으로부터 유도된 '울트라구조(ultrastructure)')가 부여된다면, 이론의 구문론(syntax)을 그 의미론(semantics)으로부터 복구할 수 있다는 것이다.

저자들은 이러한 전통적인 관점에 한계가 있음을 지적한다. 이는 집합 기반 의미론(set-based semantics)에 과도하게 의존하며, 범주에 인위적인 구조(울트라구조)를 부과한다는 점이다. 또한, 다양한 논리적 파편들에 대해 개념적 완전성을 증명하기 위한 기존의 접근 방식들은 각 파편마다 독립적이고 임시방편적인(ad-hoc) 기술들을 요구해 왔다. 본 논문은 다음과 같은 목적을 가진다:

1. 개념적 완전성을 집합 기반 모델로부터의 재구성이 아니라, 이론과 그 분류 토포스(classifying topoi) 사이의 듀얼리티(duality)로서, 즉 순수하게 구문론적인 현상으로 재정식화한다.
2. Makkai의 원래 재구성 정리에 의존하거나 의미론에 인위적인 구조를 부과하지 않고도, 다양한 하위기하학적 논리에 대해 개념적 완전성을 증명할 수 있는 모듈형 프레임워크를 제공한다.
3. 이 새로운 구문론적 개념과 Makkai의 전통적인 의미론적 재구성 사이의 관계를, 집합 기반 모델에 대한 완전성 가정이 성립하는 경우를 중심으로 명확히 한다.

2. 방법론 및 프레임워크

저자들은 자신들의 이전 연구[DLY25]에서 개발된 토포스($\mathbf{Topoi}$)의 2-범주 내에서의 우측 칸 인젝티브성(right Kan injectivity) 프레임워크를 기반으로 한다.

• 모피즘의 클래스로서의 논리: 논리 $\mathcal{H}$는 토포스들 사이의 기하학적 모피즘(geometric morphisms)의 클래스로 정의된다. 토포스 $\mathcal{X}$가 $\mathcal{H}$-모피즘에 대해 (약하게) 우측 칸 인젝티브하다면, 해당 토포스는 $\mathcal{H}$에 "형식적으로 속한다"고 한다. 이는 토포스의 일반화된 점들이 논리에 의해 규정된 구조를 가짐을 포착한다.
• 구문 범주와 분류 토포스:
  • 토포스 $\mathcal{X}$가 $\mathcal{H}$에 형식적으로 속할 때, 구문 범주(syntactic category) $\text{Syn}_{\mathcal{H}}(\mathcal{X})$는 기하학적 모피즘 $\mathcal{X} \to \text{Set}[\mathcal{O}]$ (여기서 $\text{Set}[\mathcal{O}]$는 대상 분류기이다)의 범주로 정의된다.
  • $\mathcal{H}$와 연관된 것은 작은 유한 완전 범주(small finitely complete categories, $\mathbf{Lex}$) 위의 구문 모나드(monad of syntax) $T_{\mathcal{H}}$이다.
  • 분류 토포스(classifying topos) $\text{Cl}_{\mathcal{H}}(A)$는 $T_{\mathcal{H}}$-대수(algebra) $A$에 대해 구성된다.
• 개념적 완전성 정의: 유계된 논리(bounded logic) $\mathcal{H}$가 개념적으로 완전하다는 것은 2-함자 $\text{Cl}_{\mathcal{H}}: \text{Alg}(T_{\mathcal{H}})^{\text{op}} \to \mathbf{WRInj}(\mathcal{H})$가 2-전단사(2-fully faithful)임을 의미한다.
• 핵심 통찰: 저자들은 개념적 완전성이 인접성(adjunction) $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$가 반성(reflection)(즉, counit이 동치(equivalence)인 것)인 것과 동치임을 보여준다. 이는 모든 $T_{\mathcal{H}}$-대수가 그 분류 토포스의 구문 범주와 본질적으로 같음을 의미한다. 이 공식화는 개념을 집합 기반 모델로부터 분리하여, 구문(대수)과 구문 기반 의미론(분류 토포스) 사이의 관계에 집중하게 한다.

3. 주요 기여 및 결과

A. 개념적 완전성의 특징짓기

본 논문은 논리 $\mathcal{H}$가 개념적으로 완전할 필요충분조건이 모든 작은 $T_{\mathcal{H}}$-대수 $A$에 대하여 임베딩 $A \hookrightarrow \text{Syn}_{\mathcal{H}}(\text{Cl}_{\mathcal{H}}(A))$가 범주의 동치인 것이다(정리 2.2.3)라는 점을 확립한다. 이는 문제를 구문 범주가 원래의 대수를 복구하는지 여부를 결정하는 것으로 재구성한다.

B. 네 가지 논리에 대한 개념적 완전성 증명

축소 르마(Reduction Lemma)(명제 3.1.2)를 사용하여, 저자들은 특정 논리들을 알려진 독트린(doctrine)들과 동일시하고 그들의 구문 범주가 대수를 복구함을 보임으로써 네 가지 특정 논리에 대한 개념적 완전성을 증명한다. 증명 과정에서는 분석을 단순화하기 위해 특정 하위 클래스 모피즘(sublogics)을 활용한다:

1. 코히어런트 논리 ($\mathcal{H}_{\text{flat}}$): 개념적으로 완전함을 증명하였다. 저자들은 독트린 $T_{\mathcal{H}_{\text{flat}}}$이 자유 프리프리토포스(free pretopos) 구성과 일치함을 보인다. 그들은 코히어런트 토포스의 구문 범주를 코히어런트 대상들의 전부분 범주(full subcategory)로 특징지으며, 원래의 프리프리토포스를 복구한다.
2. 레귤러 논리 ($\mathcal{H}_{\text{matte}}$): 개념적으로 완전함을 증명하였다. 이 독트린은 자유 (Barr-)정확 범주(exact category) 구성에 대응한다. 구문 범주는 레귤러 대상들로 구성됨을 보인다.
3. 거짓(falsum)을 포함한 본질적 대수 논리 ($\mathcal{H}_{\text{dom}}$): 개념적으로 완전함을 증명하였다. 이 독트린은 엄격한 초기 대상(strict initial object)을 가진 자유 렉스(lex) 범주에 대응한다. 증명은 조밀한 임베딩(dense embeddings)을 분석하고 구문 범주의 대상들이 표현 가능 대상(representables)의 은퇴(retracts)임을 보이는 과정을 포함한다.
4. 유한 분산 논리 ($\mathcal{H}_{\text{pure}}$): 개념적으로 완전함을 증명하였다. 이 독트린은 자유 렉스텐시브(lextensive) 범주 구성에 대응한다. 증명은 "순수 임베딩(pure embeddings)"과 범주를 그 결정 가능한 서브터미널 대상들의 불리언 대수와 결합하는 과정을 활용한다.

이러한 결과들은 Makkai의 원래 정리에 의존하지 않는 이 논리들에 대한 새로운 특징을 제공한다.

C. 보존적으로 매립된 논리들 (Conservatively Embedded Logics)

본 논문은 보존적으로 매립된 논리(섹션 4)라는 개념을 도입한다. 논리가 보존적으로 매립되었다는 것은 인접성 $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$가 멱등적(idempotent)임을 의미한다.

• 결과: 모든 개념적으로 완전한 논리는 보존적으로 매립되어 있다.
• 의의: 이 성질은 증명론적 해석을 제공한다: 구문 범주의 이론을 분류 토포스의 이론으로 포함시키는 것은 보존적이다. 이는 개념적 완전성이라는 의미론적 개념을 증명론적 보존성과 직접 연결한다.

D. Makkai의 정리와의 관계

섹션 5에서 저자들은 자신들의 구문론적 정의를 코히어런트 논리에 대한 Makkai의 전통적인 의미론적 재구성 정리와 화해시킨다.

• 프레임워크: 저자들은 의미론적 규정(semantic prescriptions)을 정식화하기 위해 가상 울트라 범주(virtual ultracategories) 이론([Sa25, Ham25, vGMT26])을 활용한다.
• 동치성: 저자들은 코히어런트 논리에 대하여 자신들의 개념적 완전성 개념이 Makkai의 결과와 동치임을 입증한다(결론 5.3.3).
• 메커니즘: 이 동치성은 분류 토포스들이 **충분한 점들(enough points)**을 가진다는 가정(집합 기반 모델에 대한 완전성) 하에 성립한다. 저자들은 이 결과를 다음과 같이 분해한다:
  1. 구문론적 성분: 논리는 그들의 의미에서 개념적으로 완전하다 (대수와 분류 토포스 사이의 듀얼리티).
  2. 의미론적 성분: 분류 토포스와 집합 기반 모델들의 울트라 범주 사이의 동치 (충분한 점들에 의한 유도).
• 일반화: 저자들은 일반적인 논리에 대한 "Makkai 방식의 개념적 완전성"(정의 5.4.1)을 정의하고, 논리가 충분한 집합 기반 모델을 가진다면 이것이 그들의 구문론적 개념과 동치임을 증명한다(정리 5.4.2).

4. 의의 및 주장

본 논문은 개념적 완전성에 대한 새로운 증명론적 관점을 제공한다고 주장한다.

• 모듈성: (칸 인젝티브성을 통한) 통합된 프레임워크를 제공하여, 다양한 하위기하학적 논리에 걸쳐 개념적 완전성을 연구할 때 필요한 임시방편적 기술의 필요성을 줄여준다.
• 집합 기반 의미론으로부터의 분리: 개념적 완전성의 주요 정의는 집합 기반 모델과는 독립적인, 논리 자체의 성질(이론과 분류 토포스 사이의 듀얼리티)로서 제시된다. Makkai의 정리와의 연결은 집합 기반 모델에 대한 완전성이 성립할 때 나타나는 결과이지, 정의 자체가 아니다.
• 고전적 결과의 복구: 본 논문은 구문론적 듀얼리티가 울트라 범주를 통한 의미론적 재구성과 일치하는 특수한 경우로서 Makkai의 원래 코히어런트 논리 정리를 성공적으로 복구한다.
• 보존성: 개념적 완전성이 강력한 보존성 성질을 함의함을 밝힘으로써, 모델론적 성질을 증명론적 성질과 연결한다.

저자들은 자신들이 여러 파편에 대해 개념적 완전성을 증명했으나, 모든 기하학적 논리의 파편이 개념적으로 완전한지에 대한 문제는 여전히 미해결 상태임을 언급하며 연구의 범위를 겸손하게 제한한다. 또한, 요약 표의 $\mathbf{WRInj}_{pw}(\mathcal{H})$ 열의 특징짓기는 향후 연구 과제로 남겨둔다. 그들은 현재의 예시들이 코히어런트 파편의 "아래"에 위치하고 있음을 언급하면서도, 이 이론이 더 넓게 적용될 것이라는 추측을 제시한다.