Are Dependent Types in Set Theory Feasible?

논문 요약: 집합론 기반의 의존적 타입 (Dependent Types) 구현

1. 문제 제기 (Problem)

• 배경: 수학의 표준 기초는 100 년 이상 ZFC(선택 공리 포함 체르멜로 - 프렝켈 집합론) 가 유지되어 왔으나, 현재 상호작용적 정증명 (Interactive Theorem Proving) 분야는 Rocq(구 Coq) 나 Lean 4 와 같은 의존적 타입 이론 (Dependent Type Theory, DTT) 기반 시스템이 주도하고 있습니다.
• 도전 과제: DTT 기반 시스템은 자동 계산 (built-in computation) 등 실용적 이점이 있지만, 논리적 커널의 복잡성, 추론 규칙의 난해함, 그리고 구현 버그 발견 등 검증 비용이 매우 높습니다. 반면, ZFC 기반의 1 차 논리는 상대적으로 단순하고 검증이 용이합니다.
• 핵심 질문: "집합론 (Set Theory) 기반의 증명 보조기 (Proof Assistant) 에서 의존적 타입을 구현할 수 있는가?" 즉, DTT 의 강력한 기능 (예: 유니버스 계층, 하위 타입 등) 을 집합론의 단순한 기초 위에 구축하면서도 그 타당성을 집합론 공리로부터 완전히 검증할 수 있는가?

2. 방법론 (Methodology)

저자들은 Lisa라는 증명 프레임워크를 기반으로 하여, 집합론 공리 (Tarski-Grothendieck 집합론) 와 등식을 갖춘 스케마 1 차 논리 (Schematic First-Order Logic) 에 의존적 함수 타입과 유니버스 계층을 기계적으로 임베딩했습니다.

• 기반 논리 (λFOL):
  • Lisa 는 1 차 논리를 기반으로 하지만, λ-항과 힐베트의 $\epsilon$ 연산자를 포함한 λFOL을 확장하여 사용합니다.
  • 이를 통해 변수 바인딩 ($\lambda x. e$) 을 집합론적으로 표현할 수 있으며, 고차 항을 1 차 항으로 전개 (unfold) 할 수 있어 시스템의 본질은 여전히 1 차 논리에 머뭅니다.
• 의존적 타입의 집합론적 임베딩:
  • 타입 (Types): 집합 (Sets) 으로 매핑됩니다.
  • 함수 타입 ($\Pi$): 집합론적 함수 관계 (functional relation) 로 정의됩니다.
    • $abs(T)(L)$:$T$내의$x$에 대해$L(x)$를 반환하는 함수의 집합.
    • $app(t)(u)$:$\epsilon$연산자를 사용하여$t$에$u$를 적용한 결과 값을 선택.
    • $Pi(T1)(L)$: 정의역이$T1$이고 공역이$L(x)$인 모든 함수$f$의 집합.
  • $\beta$-축약: 집합론적 정의 하에서 $app(abs(T)(L))(t) = L(t)$가 성립함을 증명하여 계산 규칙을 재현했습니다.
• 유니버스 계층 (Universe Hierarchy):
  • ZFC 만으로는 타입의 계층적 구조 (Type$_i$ : Type$_{i+1}$) 를 표현하기 어렵습니다.
  • Tarski-Grothendieck 공리를 도입하여 무한히 많은 Grothendieck Universe의 존재를 보장하고, 이를 통해 의존적 곱 (Dependent Product) 에 대해 닫혀 있는 유니버스 계층을 모델링했습니다.
• 양방향 타입 체킹 (Bidirectional Type Checking):
  • Lisa 에 Typecheck.prove라는 자동 증명 생성 전술 (tactic) 을 구현했습니다.
  • Check 모드: 주어진 타입에 대해 식이 유효한지 확인 (추론된 타입이 기대 타입의 하위 타입인지 확인).
  • Infer 모드: 식으로부터 타입을 추론.
  • Subset 모드: 하위 타입 (Subtyping) 관계를 자동으로 유도.

3. 주요 기여 (Key Contributions)

1. 집합론 기반 의존적 타입의 기계적 임베딩: Lisa 환경에서 유니버스를 포함한 의존적 함수 타입을 집합론 공리만으로 완전히 검증 가능한 형태로 구현했습니다.
2. 증명 생성형 양방향 타입 체커: 단순히 타입을 검사하는 것을 넘어, Lisa 커널이 검증할 수 있는 증명 객체 (Proof Objects) 를 자동으로 생성하는 전술을 개발했습니다.
3. 하위 타입 (Subtyping) 의 부분적 지원: 집합론적 해석에서 함의되는 하위 타입 규칙 (예: 공변성 Covariance) 을 구현하여, DTT 의 풍부한 타입 시스템을 집합론으로 확장하는 가능성을 시연했습니다.
   • 주의: 반공변성 (Contravariance) 은 집합론적 해석에서 너무 큰 집합을 요구하여 직접적으로 구현되지 않았으며, 불변 도메인과 공변 공역을 가진 제한된 $\Pi$-하위 타입 규칙만 구현되었습니다.
4. Lean/Rocq 에서 Lisa 로의 증명 이전 가능성: 집합론 기반 시스템이 DTT 기반 시스템의 핵심 기능을 시뮬레이션할 수 있음을 보여줌으로써, Lean 4 나 Rocq 에서의 증명들을 집합론 기반 시스템으로 이전 (Proof Transfer) 하는 길을 열었습니다.

4. 결과 (Results)

• 자동화된 증명: 다형성 (Polymorphism) 을 가진 함수 합성 (Composition) 과 항등 함수 (Identity) 와 같은 복잡한 의존적 타입 판정 (Typing Judgments) 을 수동 개입 없이 자동으로 증명하는 데 성공했습니다.
• 정확한 계산: 집합론적 정의가 DTT 의 $\beta$-축약 및 타입 형성 규칙을 정확히 재현함을 증명했습니다.
• 실용성 검증: Lisa 라이브러리와 결합하여 실제 사용 사례 (예: Function.comp와 id의 타입 검사) 를 성공적으로 수행했습니다.
• 공식적 검증: 모든 타입 체킹과 평가 과정이 집합론 공리와 1 차 논리 추론 규칙에 의해 완전히 정당화되었습니다.

5. 의의 및 중요성 (Significance)

• 기초의 단순화: 복잡한 DTT 커널 대신 상대적으로 검증이 쉬운 집합론과 1 차 논리를 기반으로 하면서도 DTT 의 강력한 기능을 활용할 수 있는 새로운 패러다임을 제시합니다.
• 시스템 간 상호운용성: DTT 기반 시스템 (Lean, Rocq) 과 집합론 기반 시스템 간의 증명 이동을 용이하게 하여, 서로 다른 증명 보조기 간의 호환성을 높입니다.
• 확장성: 집합론 기반 위에 DTT 기능을 "소프트 타입 시스템"으로 구축함으로써, 추후 더 복잡한 타입 이론적 기능을 추가하더라도 집합론적 타당성을 유지하며 확장할 수 있는 토대를 마련했습니다.
• 수학계 수용성: 많은 수학자들이 DTT 의 복잡성보다는 집합론에 더 친숙하므로, 집합론 기반의 DTT 구현은 수학자들이 Lean 등의 도구를 더 쉽게 받아들이는 데 기여할 수 있습니다.

결론적으로, 이 논문은 **"집합론 기반의 증명 보조기에서도 의존적 타입이 실현 가능하며, 그 과정에서 생성된 모든 증명은 집합론 공리에 의해 엄격하게 검증될 수 있다"**는 것을 성공적으로 입증했습니다.