🔢 mathematics

A Naive Encoding of Russell's Paradox in Type Theory

이 논문은 타입-인-타입(type-in-type) 우주를 시그마 타입(sigma types) 및 외연적 동일성(extensional identity) 또는 항등 증명의 유일성(uniqueness of identity proofs)을 갖춘 내포적 동일성(intensional identity)과 결합하여 러셀의 역설이 타입 이론에 직접 인코딩될 수 있음을 입증하며, 이를 통해 그러한 체계들의 모순성을 보여준다.

원저자: Zhuoyuan Qu

게시일 2026-08-20

📖 4 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Zhuoyuan Qu

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

수학이라는 광활한 풍경 속에는 아이디어를 조직하는 방식과 그것을 구축하는 데 사용하는 규칙들 사이에 근본적인 긴장이 존재합니다. 백 년이 넘는 시간 동안 수학자들은 자신들의 논리적 구조가 건전하고 모순이 없도록 보장하기 위해 타입 이론(type theory)이라 불리는 프레임워크에 의존해 왔습니다. 이 시스템을 모든 객체가 특정 폴더에 속해야 하며, 폴더는 루프를 생성하는 방식으로 자기 자신이나 다른 폴더를 포함할 수 없는 엄격한 서류 보관함이라고 생각하십시오. 이러한 분리는 1900년대 초반, "자기 자신을 포함하지 않는 모든 집합의 집합은 자기 자신을 포함하는가?"라는 단순한 질문이 시스템을 어떻게 무너뜨릴 수 있는지를 보여준 유명한 논리적 함정인 러셀의 역설(Russell's paradox)을 방지합니다. 현대 수학은 이러한 범주들을 엄격히 분리함으로써 이 함정을 성공적으로 피해 왔지만, 연구자들은 이 시스템들이 정확히 어디에서, 그리고 왜 유지되는지를 이해하기 위해 이러한 경계들을 계속 탐구하고 있습니다.

나고야 대학교의 주 쭈오위안(Qu Zhuoyuan)이 작성한 최근의 노트는 현대 타입 이론 시스템 내에서 어떻게 실수로 그 고대의 역설을 재현할 수 있는지 보여줌으로써 이 경계를 직접적으로 살펴봅니다. 저자는 표준 수학에 결함이 있다고 주장하는 것이 아니라, 특정 안전 장치를 의도적으로 제거했을 때 어떤 일이 발생하는지를 보여줍니다. 이 실험에서 연구자는 "타입의 우주(universe of types)"가 자기 자신을 포함할 수 있도록 허용하는 상황, 즉 "타입-인-타입(type-in-type)"이라 알려진 조건을 구성합니다. 이 조건에 두 대상이 동일하다는 두 개의 증명이 모두 동일하다고 취급하는 특정한 등가성 처리 방식을 결합함으로써, 저자는 원래의 역설을 투영하는 논리적 구조를 성공적으로 구축했습니다. 결과는 명확하고 직접적인 증명입니다. 만약 우주가 자기 자신을 포함하도록 허용하고, 두 대상이 같다는 모든 증명이 동일하다고 가정한다면, 시스템은 모순으로 붕괴한다는 것입니다.

이 구성은 모든 가능한 타입을 모으는 특별한 집합을 정의함으로써 작동하는데, 이는 마치 모든 범주를 모아놓은 마스터 카탈로그와 같습니다. 이 컬렉션 내에서 연구자는 자기 자신에게 속하지 않는 모든 것들의 특정 그룹을 정의합니다. 정상적이고 안전한 시스템에서는 규칙이 범주가 자기 자신의 멤버가 되는 것을 방지하기 때문에 이 그룹은 존재할 수 없습니다. 그러나 이 특정한 설정에서 저자는 이 그룹이 자기 자신에게 속하는지를 묻는 방법을 만들어냅니다. 논리는 엄격하고 피할 수 없는 경로를 따릅니다. 만약 그 그룹이 자기 자신에게 속한다면, 그 정의에 따라 자기 자신에게 속하지 않아야 합니다. 하지만 만약 그 그룹이 자기 자신에게 속하지 않는다면, 정의에 부합하므로 자기 자신에게 속해야 합니다. 이는 문장이 동시에 참이면서 동시에 거짓이 되는 루프를 생성하며, 시스템이 모순적임을 증명합니다.

이 발견을 특히 유의미하게 만드는 것은 역설이 작동하도록 만든 특정한 도구입니다. 저자는 "항등 증명의 유일성(uniqueness of identity proofs)"이라 불리는 원리에 의존하는데, 이는 본질적으로 두 대상이 같다는 것을 증명할 수 있다면 그 방법은 오직 하나뿐이라고 말하는 것입니다. 이 원리는 추론을 단순화하기 위해 많은 표준 수학 시스템에서 흔히 가정됩니다. 논문은 이 가정이 타입이 자기 자신을 포함하는 우주와 결합될 때 어떻게 역설을 촉발하는지를 보여줍니다. 결정적으로, 저자는 이러한 구성이 항등 증명의 유일성을 가정하지 않는 호모토피 타입 이론(homotopy type theory)이라는 더 현대적인 프레임워크에서는 실패할 것이라고 지적합니다. 그 대안적인 시스템에서는 두 대상이 같다는 것을 증명하는 다양한 방법들이 존재하며, 이러한 다양성이 역설이 형성되는 것을 방지합니다.

이 논문은 이 역설을 재현하려는 이전의 시도들과 그 접근 방식을 구분합니다. 다른 연구자들의 초기 작업은 유사한 결과를 얻기 위해 더 복잡한 트리 형태의 구조를 사용했으며, 이는 더 복잡한 기제들을 필요로 했습니다. 이 새로운 접근 방식은 훨씬 단순하고 직접적이며, 복잡한 트리 없이 타입과 논리적 연결이라는 기본적인 구성 요소만을 사용합니다. 이는 문제를 핵심 구성 요소로 단순화하여, 역설이 복잡한 기제의 결과가 아니라 우주가 자기 자신을 포함하도록 허용하면서 모든 등가의 증명을 동일하게 취급할 때 발생하는 직접적인 결과임을 보여줍니다. 전체 논리 체인은 컴퓨터 증명 보조기에 의해 검증되었으며, 단계들이 유효하고 정의된 규칙 내에서 모순이 실재함을 확인했습니다.

궁극적으로 이 연구는 논리적 위험 지대의 정밀한 지도로서 역할을 합니다. 이것은 수학이 망가졌다고 제안하는 것이 아니라, 무엇이 수학을 안전하게 유지하기 위해 필요한 규칙인지를 명확히 해줍니다. 특정 가설들을 통해 역설을 구축할 수 있음을 보여줌으로써, 저자는 그러한 가설들이 논리적 붕괴를 막는 데 얼마나 중요한지를 강화합니다. 이는 수학의 구조에서, 우리가 등가를 다루거나 우주를 조직하는 방식에 관한 단 하나의 완화된 규칙조차도 스스로의 파멸을 지탱하는 구조로 이어질 수 있음을 상기시켜 줍니다. 이 연구는 일관성이 주어진 것이 아니라, 우리가 강제하기로 선택한 구체적인 제약 조건들에 달려 있는, 세심하게 유지되는 상태임을 보여주는 명확한 입증입니다.

기술 요약: 유형 이론에서의 러셀의 역설에 대한 소박한 인코딩

문제 정의
"type-in-type" ( $U : U$ ) 시스템의 불일치는 지라르의 역설(Girard's paradox, 부를리-포르티 역설의 유형론적 대응물)을 통해 잘 확립되어 있으나, 러셀의 역설을 유형 이론으로 직접 인코딩하는 방식은 상대적으로 덜 알려져 있다. W-타입을 사용하여 역설적인 집합에 대응하는 트리를 구성하는 티에리 코칸(Thierry Coquand)의 기존 접근 방식은 귀납적 유형(inductive types)에 의존한다. 본 논문은 귀납적 유형을 사용하지 않고, 단일 유니버스, 시그마 유형( $\Sigma$ -types), 항등 유형(identity types)만을 사용하는 표준 유형론적 구성 요소들을 사용하여 러셀의 역설을 직접 인코딩하는 방안을 제안함으로써 이 간극을 해결한다.

방법론
본 구성은 $U : U$ 를 만족하는 단일 유니버스 $U$ 를 갖는 유형 이론 내에서 작동한다. 방법론은 다음과 같은 단계로 진행된다:

집합의 유니버스 ( $V$ ) 정의:
저자는 "모든 집합의 집합"(또는 더 정확하게는 모든 타입의 부분집합)을 나타내는 타입 $V$ 를 종속 합 유형(dependent sum, sigma type)으로 정의한다:
$V := \sum_{A:U} (A \to U)$
여기서 $V$ 의 원소는 타입 $A$ 와 $A$ 위의 술어 $P$ 의 쌍인 $(A, P)$ 이다. 이러한 쌍을 나타내기 위해 $\{x : A \mid P(x)\}$ 라는 표기법을 사용한다.
멤버십( $\in$ ) 정의:
역설을 다루기 위해서는 멤버십 관계 $(\in_A) : A \to V \to U$ 가 필요하다. 멤버십 관계의 왼쪽 항( $A$ )과 오른쪽 항의 기저 타입( $B$ )이 다를 수 있으므로, 변환(coercion) 메커니즘이 필요하다.
- 변환(Coercion): 저자는 의존 패턴 매칭을 사용하여 타입 $A$ 와 $B$ 사이의 원소를 운송(transport)하기 위한 coe를 정의한다. 이때 $h : \text{Id}_U(A, B)$ 인 항등 증명을 사용한다.
- 항등 증명: coe-eq의 동작에 대한 정의는 항등 증의 유일성(Uniqueness of Identity Proofs, UIP) (Axiom K와 동치)에 의존한다. 본 논문에서 사용된 내포적(intensional) 접근 방식은 외연적(extensional) 유형 이론과 달리 직접적인 변환 정의 없이 운송을 수행할 수 없으므로, 변환이 기대대로 작동하도록 하기 위해 엄격하게 UIP를 요구한다.
- 멤버십 정의: 멤버십 관계는 다음과 같이 정의된다:
  $a \in_A \{x : B \mid P(x)\} := \sum_{h: \text{Id}_U(A, B)} P(\text{coe}(h, a))$
  이를 통해 집합이 멤버십 관계의 양변에 나타날 수 있게 하며, 이는 역설의 전제 조건이다.
역설적 집합 ( $R$ ) 구성:
러셀 집합은 다음과 같이 정의된다:
$R := \{x : V \mid x \notin x\}$
여기서 $x \notin x$ 는 $x \in x \to \bot$ 로 정의된다.
모순 도출:
- 보조정리 1 ( $R \notin R$ ): $R \in R$ 이라고 가정하면 (이는 경로 $h$ 와 증명 $p$ 를 포함하는 시그마 타입을 풀어내는 것이다), 증명은 coe-eq(UIP에 의존함)를 사용하여 $p$ 의 타입을 재작성(rewrite)한다. 이 재작성은 가정을 $R$ 의 정의와 모순되는 형태로 변형하여 $R \notin R$ 을 증명한다.
- 보조정리 2 ( $R \in R$ ): 보조정리 1의 결과를 사용하여, 저자는 반사성 경로(reflexivity path)와 $R \notin R$ 의 증명을 쌍으로 묶어 $R \in R$ 의 타입을 갖는 항을 구성한다.
- 결과: $R \in R$ 과 $R \notin R$ 에 대한 증명이 동시에 존재한다는 것은 모순( $\bot$ )을 야기하며, 이는 시스템의 불일치를 입증한다.

주요 기여

직접 인코딩: 본 논문은 W-타입을 사용하는 코칸의 방식과 달리, $\Pi$ -타입, $\Sigma$ -타입, 항등 유형만을 사용하여 러셀의 역설을 직접 형식화할 수 있음을 보여준다.
구조적 분석: 저자는 지라르(Girard), 후르켄스(Hurkens), 코칸의 트리 역설(Coquand's tree paradox) 등 다양한 역설을 통합하는 일반적인 구조( $V$ , intro, match, 그리고 $\beta$ -등가성)를 식별한다. 본 논문은 intro가 집합 추상화(set abstraction)로, match가 멤버십(membership)으로 정의될 때 러셀의 역설이 이 구조에 부합함을 입증한다.
단순화: 다른 역설들에서 흔히 보이는 복잡한 $P_2 U$ (유니버스의 멱집합) 구조를 피함으로써, 구성을 더욱 직관적이고 이해하기 쉽게 제시한다.

결과 및 한계
본 구성은 type-in-type 시스템에서 성공적으로 모순을 도출한다. 그러나 논문은 중요한 의존성을 명시한다: 이 증명은 **UIP (Axiom K)**에 의존한다. 결과적으로, 이 특정 인코딩은 UIP를 거부하는 **호모토피 유형론(HoTT)**에서는 형식화될 수 없다. 본 구성은 유니버스 체크가 비활성화된 상태에서 Agda 및 Rocq 프로버를 통해 검증되었다.

의의
본 논문은 UIP가 가정될 경우 표준적인 구성 요소들을 사용하여 유형 이론에 러셀의 역설을 소박하게 인코딩하는 것이 가능하다고 주장한다. 이는 귀납적 유형 기반의 역설들에 대한 대안을 제공하며, 불일치가 $U:U$ , 시그마 유형, 그리고 강력한 항등 원리(UIP)의 결합으로부터 발생함을 강조한다. 또한, 이 작업은 러셀의 역설과 다른 유형론적 불일치들 사이의 구조적 유사성을 명확히 하여, 이들이 유니버스의 도입 규칙(introduction rules)과 제거 규칙(elimination rules)이라는 통일된 관점을 통해 바라볼 수 있음을 보여준다.

기술 요약: 유형 이론에서의 러셀의 역설에 대한 소박한 인코딩

유사한 논문