A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus

기술 요약: 토포스 인과 모델의 큐비컬 정식화 (A Cubical Formalisation of Topos Causal Models)

문제 및 동기
본 논문은 Mahadevan [Mah25c, Mah25b, Mah25a]이 제안한, 인과 추론을 토포스의 범주 내로 재구성한 프레임워크인 "토포스 인과 모델(Topos Causal Models, TCM)"의 검증을 다룬다. 이 프레임워크에서 인과 세계는 프리-셰프(presheaf)이며, 개입(intervention)은 서브오브젝트 분류기 $\Omega$로의 특성 사상(characteristic map)이고, 추론은 직관주의 내부 언어에서 수행된다. 원본 자료는 개입, 메커니즘 조립, 반사실(counterfactuals)과 같은 표준 인과 기제들이 토포스 이론적 보편 성질에 대응하는 개념적 재구성을 제공하지만, 이는 논문 기반의 전개에 머물러 있다. 원본의 핵심 주장들은 증명 없이 진술되어 있으며, 일부 공리들은 추상적이거나 잠재적으로 불완전하게 남겨져 있다. 본 연구의 목적은 이 1-토포스 코어를 기계적으로 체크된 방식으로 검증하여, 프레임워크의 논리적 일관성을 보장하고 원본의 공리적 제시에서 발견된 결함을 식별하는 것이다.

방법론
저자들은 큐비컬 타입 이론(cubical type theory)에 기반한 증명 보조기인 Cubical Agda를 사용하여 정식화를 구현하였다. 이 개발은 확률 모나드와 Pearl의 do-calculus 규칙을 검증한 동반 논문 [Sar26]의 직접적인 후속 작업이다.

• 기초(Foundations): 본 작업은 추상적 컨텍스트 범주 $\mathcal{C}$에 대한 프리-셰프 토포스 $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ 위에서 작동한다.
• 안전성 및 공리(Safety and Axioms): 전체 개발 과정은 Agda의 --safe 플래그 하에서 타입 체크가 되며, 이는 postulat(가정), hole(구멍), 또는 안전하지 않은 기능을 포함하지 않음을 의미한다. 기초가 되는 순서 체(ordered field)는 추상적 공리를 피하기 위해 유리수 집합 $\mathbb{Q}$로 구체적으로 인스턴스화되었다.
• 구조(Structure): 정식화는 sieve(체)의 프리-셰프로서 $\Omega$를 구축하고, Kripke-Joyal forcing을 통해 내부 언어를 정의하며, $j$-do-calculus 양상(modality)을 모델링하기 위해 Lawvere-Tierney 위상(topology)을 구성한다.

핵심 기여 및 결과

1. 개입 분류기 (섹션 3):
   저자들은 $\Omega$를 sieve의 프리-셰프로서 구축하고, 개입 $do(X := x_0)$를 $\chi: X \to \Omega$라는 특성 사상으로 실현한다. 저자들은 양방향으로 분류 정리(classification theorem)를 증명한다: $\chi_c(b) = \top \iff b = x_0^c$. 결정적으로, 이 구성이 토포스 내부적(topos-internal)이기 위해서는 고정된 값 $x_1$이 단순히 컨텍스트 인덱스 패밀리가 아니라 자연스러운 전역 원소(natural global element), 즉 컨텍스트에 대해 자연스러운 값이어야 함을 밝혀냈다. 이는 $\Omega$가 모든 제한-폐쇄적(restriction-closed) 서브-프리-셰프를 $\Omega$로 가는 유일한 사상에 의해 분류된다는 보편 성질을 만족하는 서브오브젝트 분류기임을 증명한다.

2. 독립적 메커니즘의 셰프 글루잉 (섹션 4):
   원본 자료는 겹치는 부분에서 일치하는 국소적 메커니즘들이 유일한 전역 메커니즘으로 "결합(collated)"될 수 있다고 주장하지만 증명을 제공하지 않는다. 저자들은 이를 프리-셰프 토포스에서의 **풀백 극한(pullback limit)**으로 증명한다. 두 메커니즘 $p: X \to Z$와 $q: Y \to Z$에 대하여, 풀백 $X \times_Z Y$가 컨텍스트별로 존재하며, 일치하는 메커니즘들의 임의의 코ーン(cone)이 이 풀백을 통해 유일하게 인수(factor)됨을 입증한다. 이는 Grothendieck 위상이나 셰프화(sheafification)를 요구하지 않고도 "글루잉" 성질이 성립함을 확인시켜 준다.

3. 내부 언어 (섹션 5):
   논문은 내부 논리를 위한 Kripke-Joyal forcing을 정의하고, 모든 연결사($\top, \bot, \land, \lor, \Rightarrow$) 및 양화사($\forall, \exists$)에 대한 절(clause)들을 기계적으로 검증한다. 저자들은 forcing이 제한(restriction) 하에서 안정적(stable)임을 보장하는 국소성(locality/monotonicity) 성질을 검증하며, 이는 Kripke 의미론의 정의적 특징이다.

4. Lawvere-Tierney 공리의 수정 (섹션 6):
   본 연구의 중요한 발견은 원본에서 제공된 표준 Lawvere-Tierney 위상의 정의에 결함이 있다는 점이다. 세 가지 표준 공리($\top$ 보존, $\land$ 보존, 그리고 idempotence)는 **팽창성(inflationarity, $S \leq j(S)$)**을 함의하지 않는다. 저자들은 팽창성이 실패하는 세 원소 체인(three-element chain)을 반례(counter-model)로 제시하여, 해당 연산자가 반드시 폐쇄 연산자(closure operator)인 것은 아님을 보여준다. 따라서 저자들은 $j$가 폐쇄 연산자(nucleus)가 되도록 팽창성을 네 번째 공리로 추가한다.

   • 구체적 사례: 저자들은 **이중 부정 위상(double-negation topology, $\neg\neg$)**을 비퇴화적인 구체적 사례로 제시한다.
   • 안정성(Stability): 저자들은 개입과 Pearl의 세 가지 do-calculus 규칙이 모든 위상에 대해 $j$-closed(안정적)임을 증명한다. 그러나 이는 결론이 등식(진릿값 $\top$)으로 증명된 규칙들에 대해서는 자명하다는 점을 언급한다. 실질적인 결과는 우발적 주장(contingent claims, 예: 특정 체제에서는 성립하지만 다른 체제에서는 성립하지 않는 조건부 독립성)에 관한 것으로, 이들의 진릿값이 이중 부정 위상 하에서 $j$-closed임을 보여준다.

5. 맥락성 장애 (Contextuality Obstruction, 섹션 7):
   저자들은 원본 프로그램에서 고려되지 않은 현상인 **코호몰로지적 장애(cohomological obstruction)**를 도입한다. 두 메커니즘은 항상 글루잉되지만, 세 개의 컨텍스트는 쌍별로 일치하더라도 전역 모델을 갖는 데 실패할 수 있다. 저자들은 Specker의 삼각형(Specker's triangle)(쌍별 반상관 관계를 가진 세 개의 Boolean 관측량)을 최소 위증인(minimal witness)으로 사용하여 이를 기계적으로 검증한다.

   • 저자들은 이 장애를 $\mathbb{Z}_2$ 계수를 가진 커버(cover)의 제1 체흐 코호몰로지($H^1$)의 0이 아닌 클래스로 정식화한다.
   • 또한 전역 섹션(global section)의 존재 여부는 코사이클(cocycle)의 홀로노미(holonomy)가 자명한 것과 동치임을 증명한다. Specker의 삼각형은 비자명한 홀로노미를 가지며, 이는 전역 모델의 부재를 확증한다.

6. 전이 가능성으로서의 불변성 (Transportability as Invariance, 섹션 8):
   논문은 여러 체제의 커버에 걸친 반사실의 **전이 가능성(transportability)**을 **$j$-안정성(invariance)**과 연결한다. 반사실이 전역적으로 성립(전이 가능)하려면 그 내부 진릿값이 $j$-closed여야 한다. 저자들은 만약 어떤 반사실이 $j$-안정하고 $j$-조밀한(j-dense) 환경에서 성립한다면, 그것은 전역적으로 성립한다는 건전성(soundness)을 증명한다.

의의 및 주장
본 논문은 두 가지 주요 영역에서 의의를 갖는다:

1. 확신(Assurance): TCM 프레임워크의 핵심 주장들이 단순한 단언이 아닌 검증된 상태가 되었다. 이는 자동화를 위해 필수적인데, 기계 생성형 인과 모델을 체크하기 위해서는 검증된 코어가 필요하기 때문이다.
2. 실질적 발견: 기계화 과정은 두 가지 실질적인 통찰을 드러냈다:
   • 모달 레이어(modal layer)의 보장은 $j$가 폐쇄 연산자여야 한다는 점에 의존하며, 기존의 공리들은 불충분했다.
   • 인과 메커니즘의 모듈형 조립(map-reduce 스타일)은 쌍별 일치만으로는 보장되지 않으며, 코호몰로지적 장애(맥락성)를 탐지하기 위한 전역 일관성 검사가 필요하다.

범위 및 한계
저자들은 범위를 1-토포스(프리-셰프) 파편으로 명시적으로 제한한다.

• 타입 레벨의 셰프화(associated-sheaf reflector)를 다루지 않는다.
• 인과의 비대칭성(현재의 프리-셰프 모델은 인과 화살표가 대칭적임)을 모델링하기 위해 필요한 방향성/$\infty$-범주적 리프트(directed or $\infty$-categorical lift)를 다루지 않는다.
• 전이 가능성 결과는 특정 조밀성 가설에 대한 불변성과의 동치 관계로 설정되었으나, 그래피컬 $s$-hedge 기준과의 완전한 동치성 입증은 향후 과제로 남겨두었다.

이 개발은 공개적으로 이용 가능하며, 토포스 인과 모델의 1-토포스 코어에 대한 최초의 기계 검증된 기록으로서, 모달 공리를 수정하고 검증되지 않았던 글루잉 및 장애 성질을 증명한다.