새 기초

수리논리학에서 새 기초(영어: New Foundations, 약자 NF)는 공리적 집합론의 일종이다. 윌러드 반 오먼 콰인(Quine)이 《수학 원리》(Principia Mathematica)의 유형론을 단순화시킨 것에서 유래한다. 콰인은 1937년 "New Foundations for Mathematical Logic"에서 처음 NF를 선보였다. 1940년에, 그리고 1951년의 수정판에서, 콰인은 NF의 확장을 소개했고, 이는 집합은 물론 고유 모임도 포함한다.

NF의 중요 변형인 NFU는 로널드 젠슨(Ronald Jensen)이 1969년 도입한 것으로, 이는 원소는 될 수 있으나 집합은 아닌 대상, 즉 원초(urelement)의 존재를 허용한다. 이에 따라 NFU는 전체 집합을 포함하며, … xn ∈ xn-1 ∈ …x3 ∈ x2 ∈ x1 과 같은 원소관계의 무한 강하 사슬을 허용하는 비정초적 집합론(non-well-founded set theory)이다. NFU를 받아들일 시 페아노 산술과의 상대적 무모순성이 증명된다.

NF에서는 러셀의 유형론적 집합론(TST)과 같이 식들을 계층화(stratify)하여 x ∈ x와 같은 식이 원천적으로 불가능하게 되므로 러셀의 역설에 걸리지 않는다. 다만 기존 러셀 유형론과의 중대한 차이는 분류 공리꼴을 이용하여 유형을 간접적으로 나타냄으로써 유형의 개념을 별도로 도입하지 않도록 수정되었다는 점이다.

정의

단순 유형 집합론

단순 유형 집합론(영어: simple type theory (of sets), 프랑스어: théorie simple des types, 약자 TST)은 자연수 종류를 갖는 다종류(영어: many-sorted) 1차 이론이며, 이항 관계 $\in$를 갖는다. $x\in y$가 논리식이려면 $y$의 종류가 $x$의 종류보다 1 커야 한다. TST의 공리계는 다음과 같은 두 공리 기본꼴로 구성된다.

• (확장 공리 기본꼴) $\forall x^{i+1}\forall y^{i+1}(\forall z^{i}(z^{i}\in x^{i+1}\iff z^{i}\in y^{i+1})\implies x^{i+1}=y^{i+1})$
• (분류 공리 기본꼴) $x_{1},x_{2},\dots ,x_{n},z^{i}$를 자유 변수로 갖는 논리식 $\phi$에 대하여, $\forall x_{1}\forall x_{2}\cdots \forall x_{k}\exists y^{i+1}\forall z^{i}(z^{i}\in y^{i+1}\iff \phi )$

꼬인 유형 집합론(영어: tangled type theory (of sets), 약자 TTT)은 TST와 유사하나, 논리식 $x\in y$에서 $y$의 종류와 $x$의 종류의 차가 정확히 1일 필요가 없다. 구체적으로, TTT는 자연수 종류를 갖는 다종류 1차 이론이며, 이항 관계 $\in$을 갖는다. 논리식 $x\in y$에서, $y$의 종류는 $x$의 종류보다 크다. TTT의 공리계는 다음과 같다.

• TST의 공리 $\phi$ 및 단사 증가 함수 $s\colon \mathbb {N} \to \mathbb {N}$에 대하여, $s(\phi )$. 여기서 $s(\phi )$는 $\phi$에 등장하는 임의의 변수 $x^{i}$를 $x^{s(i)}$로 대체한 논리식이다.

새 기초

새 기초는 무종류(영어: unsorted) 1차 이론이며, 이항 관계 $\in$를 갖는다.

새 기초의 논리식 $\phi$에 대하여, 만약 다음 조건을 만족시키는 함수 $f\colon \operatorname {var} (\phi )\to \mathbb {N}$이 존재한다면 ($\operatorname {var} (\phi )$는 $\phi$에 등장하는 변수의 집합), $\phi$를 층화 논리식(영어: stratified formula)이라고 한다.

• $\phi$에 등장하는 각 변수 $x$를 유형이 $f(x)$인 변수로 여기면 TST의 논리식을 얻는다. 즉, 만약 $x=y$가 $\phi$의 부분 논리식이라면 $f(x)=f(y)$이며, 만약 $x\in y$가 $\phi$의 부분 논리식이라면 $f(y)=f(x)+1$이다.

새 기초의 공리계는 다음과 같다.

• (확장 공리) $\forall x\forall y(\forall z(z\in x\iff z\in y)\implies x=y)$
• (층화 분류 공리 기본꼴, 영어: axiom schema of stratified comprehension) $x_{1},x_{2},\dots ,x_{n},z$를 자유 변수로 갖는 층화 논리식 $\phi$에 대하여, $\forall x_{1}\forall x_{2}\cdots \forall x_{n}\exists y\forall z(z\in y\iff \phi )$

층화 분류 공리 기본꼴은 무한한 수의 층화 분류 공리들로 이루어지지만, 어떤 유한 개의 층화 분류 공리와 동치임을 보일 수 있으며, 따라서 새 기초는 유한 공리화 가능 이론이다. 물론, 새 기초를 유한 공리화하는 방법은 유일하지 않다.

근원소를 갖는 새 기초

근원소를 갖는 새 기초(영어: New Foundations with urelements, 약자 NFU)는 새 기초와 유사하나, 근원소(영어: urelement)의 존재를 허용한다. 즉, 새 기초의 공리계에서 확장 공리를 다음과 같은 공리로 대체한 집합론이다.

• (공집합이 아닌 집합에 대한 확장 공리) $\forall x\forall y((\exists z(z\in x)\land \forall w(w\in x\iff w\in y))\implies x=y)$

마찬가지로, 근원소를 갖는 단순 유형 집합론(영어: simple type theory with urelements, 약자 TSTU)과 근원소를 갖는 꼬인 유형 집합론(영어: tangled type theory with urelements, 약자 TTTU)을 정의할 수 있다.

상대적 무모순성

다음과 같은, TST(U)의 언어로 된 명제 집합을 정의하자.

• (모호 공리 기본꼴, 영어: ambiguity scheme, 약자 Amb) 문장 $\phi$에 대하여, $\phi \iff \phi ^{+}$. 여기서 $\phi ^{+}$는 $\phi$에 등장하는 임의의 변수 $x^{i}$를 $x^{i+1}$로 대체한 논리식이다.

그렇다면, 다음 이론들이 서로 등무모순적이다.

• ${\mathsf {NF}}$
• ${\mathsf {TST}}+{\mathsf {Amb}}$
• ${\mathsf {TTT}}$

마찬가지로, 다음 이론들이 서로 등무모순적이다.

• ${\mathsf {NFU}}$
• ${\mathsf {TSTU}}+{\mathsf {Amb}}$
• ${\mathsf {TTTU}}$

매클레인 집합론(영어: Mac Lane set theory, 약자 Mac)은 체르멜로 집합론(Z)에서 분류 공리 기본꼴을 모든 한정이 집합에 대한 한정인 논리식에 대한 분류 공리 기본꼴로 약화한 집합론이다. 케이-포스터 집합론(영어: Kaye–Forster set theory, 약자 KF)은 체르멜로 집합론(Z)에서 분류 공리 기본꼴을 모든 한정이 집합에 대한 한정인 층화 논리식에 대한 분류 공리 기본꼴로 약화한 집합론이다. KF는 Mac의 부분 이론이다.

${\mathsf {Inf}}$와 ${\mathsf {Choice}}$가 (각 이론에서의) 무한 공리와 선택 공리라고 하자. 그렇다면, 다음 이론들이 서로 등무모순적이다.

• ${\mathsf {TST}}+{\mathsf {Inf}}$
• ${\mathsf {TST}}+{\mathsf {Inf}}+{\mathsf {Choice}}$^{:252, Remark}
• ${\mathsf {NFU}}+{\mathsf {Inf}}$^{:252, Remark}
• ${\mathsf {NFU}}+{\mathsf {Inf}}+{\mathsf {Choice}}$^{:252, Remark}
• ${\mathsf {Mac}}$
• ${\mathsf {KF}}$

반면, NF는 선택 공리의 부정을 함의하며, 따라서 무한 공리를 함의한다.

다음이 성립한다.

• ${\mathsf {NFU}}\vdash \operatorname {Con} ({\mathsf {Q}})$ [${\mathsf {Q}}$는 로빈슨 산술(영어: Robinson arithmetic)]
• ${\mathsf {NF}}\vdash \operatorname {Con} ({\mathsf {PA}})$
• ${\mathsf {PA}}\vdash \operatorname {Con} ({\mathsf {NFU}})$^:252
• ${\mathsf {PA}}\vdash \operatorname {Con} ({\mathsf {TST}})$^:252
• ${\mathsf {PA}}\vdash \operatorname {Con} ({\mathsf {TST}}+{\mathsf {Inf}})\implies \operatorname {Con} ({\mathsf {NFU}}+{\mathsf {Inf}})$^{:252, Theorem 1}
• ${\mathsf {PA}}\vdash \operatorname {Con} ({\mathsf {TST}}+{\mathsf {Inf}}+{\mathsf {Choice}})\implies \operatorname {Con} ({\mathsf {NFU}}+{\mathsf {Inf}}+{\mathsf {Choice}})$^{:252, Theorem 1}
• ${\mathsf {Z}}\vdash \operatorname {Con} ({\mathsf {TST}}+{\mathsf {Inf}})$
• ${\mathsf {ZF}}\vdash \operatorname {Con} ({\mathsf {NF}})$

(넷째 결과는 아직 정식 출판되지 않았다.)

역사

단순 유형 집합론(TST)은 1930년대에 알프레트 타르스키가 처음 정의하였다. 1968년 논문에서 로널드 젠슨(영어: Ronald Jensen)은 근원소를 갖는 새 기초(NFU)를 도입하였으며, NFU가 페아노 산술(PA)에 상대적으로 무모순적임을 증명하였다. (젠슨의 증명은 모형 이론적이지만, PA에서 기술 가능한 특정 모형들만 사용하기 때문에 PA에서 형식화할 수 있다.)

참고 문헌

• Feferman, Solomon (2011). 〈Enriched Stratified Systems for the Foundations of Category Theory〉 (PDF). 《Foundational Theories of Classical and Constructive Mathematics》. The Western Ontario Series in Philosophy of Science (영어) 76. Dordrecht: Springer. doi:10.1007/978-94-007-0431-2_6. ISBN 978-94-007-0430-5. ISSN 1566-659X. MR 2867085. Zbl 1315.18001. 2021년 10월 20일에 원본 문서 (PDF)에서 보존된 문서. 

외부 링크

• Holmes, Melvin Randall. “Alternative Axiomatic Set Theories”. 《Stanford Encyclopedia of Philosophy》 (영어). 
• “Randall Holmes's Home Page” (영어). 2021년 10월 15일에 원본 문서에서 보존된 문서. 
• “New Foundations home page” (영어). 2020년 10월 31일에 원본 문서에서 보존된 문서. 
• “Bibliography of Set Theory with a Universal Set” (영어). 2021년 2월 10일에 원본 문서에서 보존된 문서. 
• Holmes, Melvin Randall. “A new pass at the NF consistency proof” (PDF) (영어). 2021년 8월 31일에 원본 문서 (PDF)에서 보존된 문서. 
• “The status of 'the consistency of NF relative to ZF'”. 《MathOverflow》. 
• Smith, Peter (2022년 8월 23일). “NF is consistent”. 《Logic Matters》. 
• Smith, Peter (2024년 4월 21일). “NF really is consistent”. 《Logic Matters》.