GN⁺: New Foundations의 일관성 – Lean을 사용하여 증명된 난해한 수학적 증명
(leanprover-community.github.io)Here is a summary of the key points from the given article, organized using Markdown:
New Foundations 집합론의 무모순성 증명
- 1937년 Quine이 제안한 "New Foundations(NF)" 집합론의 무모순성을 Randall Holmes가 2010년 이후 증명했다고 주장해 왔음
- 이 저장소에서는 대화형 정리 증명기 Lean을 사용하여 Holmes 증명의 어려운 부분을 검증함으로써 NF가 실제로 모순이 없음을 증명함
- 증명은 이제 완료되었으며, 정리 명제는 ConNF/Model/Result.lean에서 찾을 수 있음
목표
- NF는 Tangled Type Theory(TTT)가 무모순일 때 그리고 오직 그때에만 무모순임이 알려져 있음
- Lean에서 TTT의 모델을 형식적으로 구성하여 NF가 무모순임을 증명함
- Holmes의 여러 버전의 증명을 바탕으로 작업하고 있지만 Lean의 타입 이론과 호환되도록 많은 변경과 추가 사항이 있었음
- 이 프로젝트는 Lean으로 작성된 커뮤니티 수학 라이브러리인 mathlib에 의존하여 기수나 군 등에 대한 익숙한 결과를 직접 증명하지 않고 사용할 수 있음
- Lean의 신뢰할 수 있는 커널에 의해 mathlib과 이 프로젝트의 모든 정의와 정리가 검증되었지만, Lean은 정의와 정리의 설명이 의도한 영어 설명과 일치하는지 확인할 수 없으므로 이 프로젝트의 코드에서 결론을 도출할 때는 영어와의 번역에 주의해야 함
뒤엉킨 유형 이론(TTT)
- TTT는 동등 관계 "="와 속한다는 관계 "∈"를 갖는 다중 정렬 집합론임
- 정렬은 극한 순서수 λ로 색인되며, λ의 원소를 유형 지수라고 함
- "x = y" 공식은 x와 y가 같은 유형일 때 잘 형성되고, "x ∈ y" 공식은 x가 y보다 작은 임의의 유형을 가질 때 잘 형성됨
- TTT의 공리 중 하나는 α 유형의 집합이 β < α인 임의의 β 유형의 원소에 의해 고유하게 결정된다는 외연성임
- 예를 들어 α 유형의 두 집합이 다르면 모든 β < α에 대해 서로 다른 β 유형 원소를 갖게 되는데, 이 속성은 TTT 모델을 구축하기 어렵게 만듦
전략
- 모델 구축은 다음과 같은 대략적인 전략을 사용함:
-
기본 유형 구성
- λ를 극한 순서수, κ > λ를 정규 순서수, μ > κ를 적어도 κ의 공극성을 갖는 강한 극한 기수로 설정
- κ보다 작은 집합을 작다고 함
- -1 레벨에서 기본 유형이라는 보조 유형을 구성하고 이는 최종적으로 모델의 일부가 되는 모든 유형 아래에 있음
- 이 유형의 원소를 원자라고 하며(ZFU나 NFU 의미의 원자는 아님), μ개의 원자가 있고 κ 크기의 litter로 분할됨
-
각 유형 구성
- 각 유형 레벨 α에서 TTT의 의도한 모델에 대한 모델 요소 모음을 생성하며, 이를 때로는 t-집합이라고 함
- 허용 순열이라고 하는 순열 그룹을 생성하는데, 이들은 t-집합에 작용함
- 속한다는 관계는 허용 순열의 작용 아래에서 보존됨
- 각 t-집합은 허용 순열의 작용 아래 지지대를 갖도록 규정되는데, 이는 주소라고 하는 작은 개체 집합으로, 허용 순열이 지지대의 모든 요소를 고정할 때마다 t-집합도 고정함
- α 레벨의 각 t-집합에는 β < α 유형의 선호하는 확장이 제공되며, t-집합의 원소에서 어떤 확장을 선호하는지 복구할 수 있음
- 이러한 t-집합의 다른 하위 유형에서의 확장은 β-확장에서 추론할 수 있으며, 이를 통해 TTT의 외연성 공리를 만족시킬 수 있음
-
각 유형의 크기 제어
- 각 유형 α는 모든 유형 β < α의 크기가 정확히 μ라는 가정(다른 가설 외에) 하에서만 구성할 수 있음
- α 레벨에서 t-집합의 모음이 적어도 μ의 기수를 갖는다는 것은 쉽게 증명할 수 있으므로, 이 집합의 원소가 최대 μ개임을 보여야 함
- 이는 허용 순열의 작용 하에서 뒤엉킨 것에 대해 근본적으로 다른 설명이 그렇게 많지 않음을 보임으로써 할 수 있음
- 이에는 허용 순열을 구성할 수 있게 해주는 기술적 보조정리인 작용의 자유 정리가 필요함
- 이 섹션의 주요 결과는 여기에 있음
-
귀납법 마무리
- 위의 과정을 재귀적으로 실행하여 모든 유형 레벨 α에서 뒤엉킨 유형을 생성할 수 있음
- 이는 집합론에서는 쉬운 단계이지만 필요한 다양한 귀납 가설의 상호 연결성 때문에 유형 이론에서는 많은 작업이 필요함
- 그런 다음 우리의 구성이 실제로 TTT의 모델을 생성하는지 이론의 유한한 공리화를 만족하는지 확인함
- 우리는 NF의 포괄 체계에 대한 Hailperin의 유한한 공리화를 TTT의 유한한 공리화로 변환하기로 선택했으며, 이를 결과 파일에 제시함
- 그러나 이 선택은 임의적이며, 이미 마련된 인프라를 사용하여 다른 유한한 공리화를 쉽게 증명할 수 있음
-
GN⁺의 의견
- 이 증명은 지금까지 매우 추상적인 수준에서만 알려져 왔던 NF 집합론의 무모순성을 형식적으로 증명했다는 점에서 매우 의미있는 결과임. 이는 순수 수학적으로 중요할 뿐 아니라 증명 보조 도구의 발전과 자동화된 정리 증명에 실질적인 진전을 보여주는 사례임
- Lean을 사용한 형식화 작업은 증명의 정확성과 완전성을 보장하지만, 동시에 수학자들에게 익숙하지 않은 언어로 작성되어 있어 이해하기 어려울 수 있음. 증명의 핵심 아이디어를 자연어로 명확하게 설명하는 작업이 병행되어야 할 것임
- TTT의 기묘한 외연성 공리가 왜 필요한지, 다른 집합론과의 관계는 어떤지 등 배경 이론에 대한 직관적 설명도 부족한 편임. 형식적 증명 뿐 아니라 철학적, 역사적 맥락에 대한 논의가 보완된다면 NF 이론에 대한 이해도를 더욱 높일 수 있을 것임
- 구축된 모델이 표준적인 ZFC 집합론의 모델과 어떤 관계가 있는지, NF의 무모순성이 다른 공리계의 무모순성과 어떻게 연결되는지 등 향후 추가적인 연구 주제도 흥미로워 보임
- 이런 복잡한 증명을 Lean으로 형식화한 사례는 다른 수학 분야의 증명 자동화에도 귀감이 될 수 있을 것임. 기존에 증명 과정이 잘 알려지지 않은 정리들을 대상으로 비슷한 작업이 시도된다면 수학계에 큰 파급 효과가 있을 것으로 기대됨
Hacker News 의견
- Lean을 사용한 증명이 잘못될 위험은 매우 적음. 그러나 Lean의 버그와 무관하게, 소프트웨어 검증 및 수학에서 알려진 문제인 결론을 주의 깊게 읽고 실제로 증명된 것이 맞는지 확인해야 함.
- 이번 사례는 어려운 증명의 상태를 해결하기 위해 증명 도우미를 사용한 첫 번째 사례로 보임. 이전에는 신뢰할 수 없는 소프트웨어로 처리된 대규모 계산 요소가 포함된 기존 증명을 검증한 프로젝트가 있었지만, 이번 사례는 결과의 인식론적 지위가 수학계에서 불확실했던 첫 번째 사례임.
- Coq와 Lean의 근본적인 차이점과 동일한 종류의 논리에서 작동하는지 여부에 대해 궁금증이 제기됨. 관련 토론에서는 이해하기 어려운 내용들이 언급됨.
- Lean 지지자들은 Lean이 우수한 증명 방법이라는 점을 너무 강하게 사용하는 경향이 있음. Lean은 대안적인 증명 방법일 뿐이며, 프로그래밍 언어 및 시스템으로서 자체 버그가 있고 다른 사람이 작성한 다양한 라이브러리 스택에 크게 의존함.
- Lean이 증명이 좋다고 말했다는 표현보다는, 작성된 증명이 인간 수학자에 의해 검증되었고 증명이 Lean으로 변환되어 거기서도 검증되었다는 표현이 더 정확하고 솔직할 것임. Lean이 유일하고 황금같은 검증을 제공한다는 설명은 정확하지 않거나 그렇게 말하는 설명을 보지 못했음.
- "New Foundations" 집합론 공식화가 다른 공식화에 비해 특별하거나 새로운 점에 대한 대략적인 설명을 수학 학부생이나 엔지니어링 전문가가 읽을 수 있는 형태로 요청함.
- 이러한 접근이 결국 협업 증명과 '버그 수정'으로 이어져 수학을 GitHub의 코드와 유사한 프로세스로 만들지 궁금해 함.
- 괴델의 정리에 따르면 충분히 강력한 모든 시스템은 자신의 일관성을 보여줄 수 없다고 하는데, 이에 대해 질문함.
- mathlib 프로젝트를 계속 따라가고 싶지만 시간이 없음. 매우 소극적인 방식으로 참여할 수 있는 방법이 있는지 궁금해 함.