Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

기술적 요약: 네 가지 역설과 증명 보조도구

문제 진술
본 논문은 Rocq 증명 보조도구(구 Coq) 의 기반이 되는 타입 이론인 귀납적 계산법 (Calculus of Inductive Constructions, CIC) 의 기초적 경계를 다룹니다. CIC 의 일관성은 잘 확립되어 있지만, 특히 비예측성 (impredicativity), 우주 제약 (universe constraints), 그리고 대규모 제거 (large elimination) 와 관련하여 일관성을 방지하는 구체적인 설계 결정들은 종종 추상적인 공학적 제약으로 취급됩니다. Rocq 와 함께 배포되는 coq-paradoxes 라이브러리에는 Rocq 커널이 거부한 가정에 의존하여 False 를 유도하는 네 가지 기계화된 유도 (Burali-Forti, Diaconescu, Reynolds, Hurkens) 가 포함되어 있습니다. 핵심 문제는 이러한 유도들을 단순히 역사적 호기심이나 고립된 불일치로 해석하는 것이 아니라, 커널이 건전성을 유지하기 위해 경계를 어디에 그어야 하는지를 정확하게 규정하는 '부정적 명세 (negative specification)'로 해석하는 것입니다.

방법론
본 논문은 coq-paradoxes 라이브러리 내의 소스 코드를 면밀히 분석하며, 특히 다음 네 개의 파일을 분석합니다: BuraliForti.v, diaconescu.v, Reynolds.v, Hurkens_Set.v. 방법론은 다음과 같습니다:

1. 공유 메커니즘 해체: 여러 역설에서 사용되는 접근성 술어 (ACC) 와 잘 정렬된 기반 인프라를 이해하기 위해 Logics.v 를 분석합니다.
2. 유도 추적: 각 파일의 논리적 단계를 따라가며 모순으로 이어지는 구체적인 가정 (예: 관계의 보편 타입, 선택 원리, 또는 Prop 에서 단일 명제로의 단사 함수) 을 식별합니다.
3. 커널 거부 매핑: 형식화 내의 모순 지점을 Rocq 커널의 특정 메커니즘 (우주 산술, 제거 규칙, 또는 비예측성 검사) 과 상관관계를 맺어 해당 구성이 컴파일되는 것을 방지하는 요인을 규명합니다.
4. 설계 결정 종합: 발견된 내용을 종합하여 커널의 행동을 지배하는 세 가지 통합된 경계 조건을 도출합니다.

주요 기여 및 결과

본 논문은 네 가지 구체적인 역설을 분석하여, 특정 설계 선택이 변경될 경우 각각이 타입 이론에서 어떻게 고유한 취약점을 드러내는지 보여줍니다:

1. 부랄리 - 포르티 역설 (BuraliForti.v):

   • 메커니즘: 관계의 보편 타입 $A_0$ 와 관계를 $A_0$ 의 원소로 매핑하는 단사 함수 $i_0$ 를 가정합니다. 이를 통해 스스로에 내포된 '모든 순서수의 순서수'($\Omega$) 를 구성할 수 있습니다.
   • 커널 거부: 이 역설은 $A_0$ 를 자신으로 인스턴스화하는 데 의존합니다. Rocq 커널은 타입이 자신의 이미지를 포함하는 것을 방지하기 위해 엄격한 우주 계층화 ($Type_j < Type_i$) 를 강제합니다. 이 구성은 내부 타입에 필요한 우주 수준이 외부 타입보다 적어도 커야 하므로 커널의 누적 제약을 위반하여 '우주 불일치 (Universe Inconsistency)' 오류를 유발합니다.
   • 결과: 고정점 모순으로 이어지는 자기 참조적 타입 정의를 방지하기 위한 우주 계층 제약의 필요성을 확립합니다.

2. 디아코네스쿠 역설 (diaconescu.v):

   • 메커니즘: 명제 $P$ 에 의해 정의된 bool 위의 동치 관계에 대해 선택 공리 (Tchoice) 의 타입 버전 을 사용합니다. 선택 함수 $f: bool \to bool$ 를 사용하여 $f(\text{true})$ 와 $f(\text{false})$ 를 비교함으로써 $P$ 를 결정합니다.
   • 커널 거부: 이 논증은 Prop 의 존재 증명에서 Set 의 계산적 결정 (함수) 을 추출합니다. 이는 Prop 에서 Set 으로 가는 '대규모 제거 (large elimination)'를 구성합니다.
   • 결과: Set 에서 선택 공리를 허용하거나 Prop 에서 Set 으로 대규모 제거를 허용하면 구성적 시스템에 배제된 법칙 (LEM) 이 강제됨을 보여줍니다. 커널은 계산 계층으로 고전 논리가 유입되는 것을 방지하기 위해 대규모 제거를 제한합니다.

3. 레이놀즈 역설 (Reynolds.v):

   • 메커니즘: 시스템 F 에 집합론적 모델이 없다는 레이놀즈의 결과를 재구성합니다. 이는 $Heyt$(단일 명제) 로부터의 단사 함수$I: Prop \to Heyt$를 가정하고, 함자$\Phi$ 에 대한 사전 초기 대수 (Church 인코딩) 를 구성합니다. Lawvere 의 고정점 정리를 사용하여 부정의 고정점을 유도하여 False 에 도달합니다.
   • 커널 거부: 이 구성은 Prop 의 비예측성 (내부에서 모든 명제를 양화) 에 의존합니다. 그러나 이 역설은 Prop 에서 단일 명제로의 단사 함수를 필요로 하는데, 커널은 논리적 모순에 도달하기 전에 우주 근거로 이를 거부합니다.
   • 결과: Prop 내의 비예측성의 역할을 강조합니다. Prop 이 비예측적이지만, 커널은 칸토어의 대각선 논법이 명제의 우주를 붕괴시킬 수 있게 하는 특정 구조적 단사 함수를 방지합니다.

4. 허르켄스 역설 (Hurkens_Set.v):

   • 메커니즘: 지라르 역설의 허르켄스 단순화 버전입니다. 이는 (이중 부정을 통해) Prop 과 bool 사이의 재귀 (retract) 를 가정하고, Set 의 비예측성 (활성화된 경우) 과 대규모 제거를 결합하여 False 로 이어지는 자기 참조적 잘 정렬된 관계를 구성합니다.
   • 커널 거부: 이 역설은 Set 의 비예측성과 명제 내용에서 불리언을 추출하는 대규모 제거를 모두 필요로 합니다. 기본 Rocq 커널은 Set 을 예측적으로 유지하고 Prop 으로의 대규모 제거를 제한합니다.
   • 결과: Set 에서 비예측성과 대규모 제거의 결합은 고전 논리 (LEM) 와 모순됨을 보여줍니다. 커널이 Set 을 예측적으로 유지하고 제거를 제한하는 결정이 안전장치입니다.

의의 및 주장

본 논문은 coq-paradoxes 패키지가 Rocq 커널의 부정적 명세 역할을 한다고 주장합니다. 단순히 불일치를 나열하는 것이 아니라, 이 패키지는 실패한 예시를 통한 형식적 증명을 통해 커널의 건전성을 입증합니다.

• 세 가지 경계 조건: 본 논문은 네 가지 역설을 커널이 강제하는 세 가지 구체적인 설계 결정으로 종합합니다:

  1. 우주 계층: 고정점을 생성하는 방식으로 타입이 자신을 양화하는 것을 방지합니다 (부랄리 - 포르티).
  2. 비예측성의 배치: 비예측적 양화를 Prop(선택적으로 예외가 있는 Set) 으로 제한하여 레이놀즈와 허르켄스 모순을 방지합니다.
  3. 대규모 제거의 규율: bool 나 Set 내의 함수와 같은 계산적 내용을 명제 증명에서 추출하는 것을 제한하여 디아코네스쿠와 허르켄스 모순을 방지합니다.

• 초기수학적 역할: 본 논문은 해당 패키지를 문서화하는 시스템 내부에 작성된 초기수학의 독특한 사례라고 주장합니다. 이는 응용을 위한 정리를 증명하는 것이 아니라 특정 가정의 비충족성을 증명합니다. 커널의 '거부'는 임의의 수정이 아니라 우주 산술, 제거 규칙과 같은 일관된 정책의 결과임을 보여줍니다.

• 결론: 그 의의는 Rocq 커널이 이러한 구성을 컴파일하지 않는 것이 임의적인 것이 아니라, CIC 의 일관성을 유지하기 위해 필요한 정확한 구조적 메커니즘임을 입증하는 데 있습니다. 이 패키지는 커널의 설계 결정이 '올바른 이유'로 이루어졌음을 검증하여, 시스템의 경계를 외부에서 내부로 정확히 그어냅니다.