새 기초 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]에서 '''새 기초'''({{llang|en|New Foundations}}, 약자 NF)는 [[공리적 집합론]]의 일종이다.<ref name="Forster">{{서적 인용|이름=Thomas Edward|성=Forster|제목=Set theory with a universal set. Exploring an untyped universe|판=2|언어=en|총서=Oxford Logic Guides|권=31|출판사=Clarendon Press|위치=Oxford|날짜=1995|isbn=0-19-851477-8|mr=1366833|zbl=0831.03027}}</ref> [[윌러드 반 오먼 콰인]](Quine)이 《[[수학 원리]]》(''Principia Mathematica'')의 [[유형 이론|유형론]]을 단순화시킨 것에서 유래한다. 콰인은 1937년 "New Foundations for Mathematical Logic"에서 처음 NF를 선보였다. 1940년에, 그리고 1951년의 수정판에서, 콰인은 NF의 확장을 소개했고, 이는 [[집합]]은 물론 [[고유 모임]]도 포함한다.

NF의 중요 변형인 '''NFU'''는 [[로널드 젠슨]](Ronald Jensen)이 1969년 도입한 것으로, 이는 원소는 될 수 있으나 집합은 아닌 대상, 즉 원초(urelement)의 존재를 허용한다.<ref>{{웹 인용|url=https://plato.stanford.edu/entries/quine-nf/|제목=Quine's New Foundations|언어=en|이름=Thomas|성=Forster|웹사이트=[[스탠포드 철학 백과사전|Stanford Encyclopedia of Philosophy]]}}</ref> 이에 따라 NFU는 [[전체 집합]]을 포함하며, … xn ∈ xn-1 ∈ …x3 ∈ x2 ∈ x1 과 같은 원소관계의 무한 강하 사슬을 허용하는 비정초적 집합론(non-well-founded set theory)이다. NFU를 받아들일 시 [[페아노 산술]]과의 [[무모순성|상대적 무모순성]]이 증명된다.

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

== 정의 ==
=== 단순 유형 집합론 ===
'''단순 유형 집합론'''({{llang|en|simple type theory (of sets)}}, {{llang|fr|théorie simple des types}}, 약자 TST)은 자연수 종류를 갖는 다종류({{llang|en|many-sorted}}) [[1차 논리|1차 이론]]이며, 이항 관계 <math>\in</math>를 갖는다. <math>x\in y</math>가 논리식이려면 <math>y</math>의 종류가 <math>x</math>의 종류보다 1 커야 한다. TST의 공리계는 다음과 같은 두 공리 기본꼴로 구성된다.
* (확장 공리 기본꼴) <math>\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})</math>
* (분류 공리 기본꼴) <math>x_1,x_2,\dots,x_n,z^i</math>를 자유 변수로 갖는 논리식 <math>\phi</math>에 대하여, <math>\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)</math>

'''꼬인 유형 집합론'''({{llang|en|tangled type theory (of sets)}}, 약자 TTT)은 TST와 유사하나, 논리식 <math>x\in y</math>에서 <math>y</math>의 종류와 <math>x</math>의 종류의 차가 정확히 1일 필요가 없다. 구체적으로, TTT는 자연수 종류를 갖는 다종류 [[1차 논리|1차 이론]]이며, 이항 관계 <math>\in </math>을 갖는다. 논리식 <math>x\in y</math>에서, <math>y</math>의 종류는 <math>x</math>의 종류보다 크다. TTT의 공리계는 다음과 같다.
* TST의 공리 <math>\phi</math> 및 [[단사 함수|단사]] [[증가 함수]] <math>s\colon\mathbb N\to\mathbb N</math>에 대하여, <math>s(\phi)</math>. 여기서 <math>s(\phi)</math>는 <math>\phi</math>에 등장하는 임의의 변수 <math>x^i</math>를 <math>x^{s(i)}</math>로 대체한 논리식이다.

=== 새 기초 ===
'''새 기초'''는 무종류({{llang|en|unsorted}}) [[1차 논리|1차 이론]]이며, 이항 관계 <math>\in</math>를 갖는다.

새 기초의 논리식 <math>\phi</math>에 대하여, 만약 다음 조건을 만족시키는 함수 <math>f\colon\operatorname{var}(\phi)\to\mathbb N</math>이 존재한다면 (<math>\operatorname{var}(\phi)</math>는 <math>\phi</math>에 등장하는 변수의 집합), <math>\phi</math>를 '''층화 논리식'''({{llang|en|stratified formula}})이라고 한다.
* <math>\phi</math>에 등장하는 각 변수 <math>x</math>를 유형이 <math>f(x)</math>인 변수로 여기면 TST의 논리식을 얻는다. 즉, 만약 <math>x=y</math>가 <math>\phi</math>의 부분 논리식이라면 <math>f(x)=f(y)</math>이며, 만약 <math>x\in y</math>가 <math>\phi</math>의 부분 논리식이라면 <math>f(y)=f(x)+1</math>이다.
새 기초의 공리계는 다음과 같다.
* (확장 공리) <math>\forall x\forall y(\forall z(z\in x\iff z\in y)\implies x=y)</math>
* (층화 분류 공리 기본꼴, {{llang|en|axiom schema of stratified comprehension}}) <math>x_1,x_2,\dots,x_n,z</math>를 자유 변수로 갖는 층화 논리식 <math>\phi</math>에 대하여, <math>\forall x_1\forall x_2\cdots\forall x_n\exist y\forall z(z\in y\iff\phi)</math>
층화 분류 공리 기본꼴은 무한한 수의 층화 분류 공리들로 이루어지지만, 어떤 유한 개의 층화 분류 공리와 [[동치]]임을 보일 수 있으며, 따라서 새 기초는 유한 공리화 가능 이론이다.<ref name="Hailperin">{{저널 인용|성1=Hailperin|이름1=Theodore|제목=A set of axioms for logic|언어=en|저널=The Journal of Symbolic Logic|권=9|쪽=1–19|날짜=1944|issn=0022-4812|doi=10.2307/2267307|mr=0009753|zbl=0060.02201}}</ref> 물론, 새 기초를 유한 공리화하는 방법은 유일하지 않다.

=== 근원소를 갖는 새 기초 ===
'''근원소를 갖는 새 기초'''({{llang|en|New Foundations with urelements}}, 약자 NFU)는 새 기초와 유사하나, 근원소({{llang|en|urelement}})의 존재를 허용한다. 즉, 새 기초의 공리계에서 확장 공리를 다음과 같은 공리로 대체한 집합론이다.
* (공집합이 아닌 집합에 대한 확장 공리) <math>\forall x\forall y((\exists z(z\in x)\land\forall w(w\in x\iff w\in y))\implies x=y)</math>

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

== 상대적 무모순성 ==
다음과 같은, TST(U)의 언어로 된 명제 집합을 정의하자.
* (모호 공리 기본꼴, {{llang|en|ambiguity scheme}}, 약자 Amb) 문장 <math>\phi</math>에 대하여, <math>\phi\iff\phi^+</math>. 여기서 <math>\phi^+</math>는 <math>\phi</math>에 등장하는 임의의 변수 <math>x^i</math>를 <math>x^{i+1}</math>로 대체한 논리식이다.
그렇다면, 다음 이론들이 서로 [[등무모순적]]이다.
* <math>\mathsf{NF}</math>
* <math>\mathsf{TST}+\mathsf{Amb}</math><ref name="SpeckerTypAmb">{{서적 인용|성=Specker|이름=Ernst P.|장=Typical ambiguity|제목=Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.)|언어=en|쪽=116–124|출판사=Stanford University Press|위치=Stanford, CA|날짜=1962|mr=0157901|zbl=0156.02101}}</ref>
* <math>\mathsf{TTT}</math><ref name="HolmesWilshaw"/><ref name="HolmesWilshawArxiv"/>

마찬가지로, 다음 이론들이 서로 [[등무모순적]]이다.
* <math>\mathsf{NFU}</math>
* <math>\mathsf{TSTU}+\mathsf{Amb}</math><ref name="HolmesWilshaw"/><ref name="HolmesWilshawArxiv"/>
* <math>\mathsf{TTTU}</math><ref name="HolmesWilshaw"/><ref name="HolmesWilshawArxiv"/>

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

<math>\mathsf{Inf}</math>와 <math>\mathsf{Choice}</math>가 (각 이론에서의) 무한 공리와 [[선택 공리]]라고 하자. 그렇다면, 다음 이론들이 서로 [[등무모순적]]이다.
* <math>\mathsf{TST}+\mathsf{Inf}</math>
* <math>\mathsf{TST}+\mathsf{Inf}+\mathsf{Choice}</math><ref name="Jensen"/>{{rp|252, Remark}}
* <math>\mathsf{NFU}+\mathsf{Inf}</math><ref name="Jensen"/>{{rp|252, Remark}}
* <math>\mathsf{NFU}+\mathsf{Inf}+\mathsf{Choice}</math><ref name="Jensen"/>{{rp|252, Remark}}<ref name="stanfordalt">{{웹 인용|url=https://plato.stanford.edu/entries/settheory-alternative/|제목=Alternative Axiomatic Set Theories|언어=en|이름=Melvin Randall|성=Holmes|웹사이트=[[스탠포드 철학 백과사전|Stanford Encyclopedia of Philosophy]]}}</ref>
* <math>\mathsf{Mac}</math><ref name="MathiasStrength">{{저널 인용|성=Mathias|이름=A. R. D.|제목=The strength of Mac Lane set theory|언어=en|저널=Annals of Pure and Applied Logic|권=110|호=1-3|쪽=107–234|날짜=2001|issn=0168-0072|doi=10.1016/S0168-0072(00)00031-2|mr=1846761|zbl=1002.03045}}</ref>
* <math>\mathsf{KF}</math><ref name="MathiasStrength"/>
반면, NF는 선택 공리의 부정을 함의하며, 따라서 무한 공리를 함의한다.<ref name="Specker">{{저널 인용|성=Specker|이름=Ernst P.|제목=The axiom of choice in Quine’s new foundations for mathematical logic|언어=en|저널=Proceedings of the National Academy of Sciences of the United States of America|권=39|쪽=972–975|날짜=1953|issn=0027-8424|doi=10.1073/pnas.39.9.972|mr=0059214|zbl=0051.03705}}</ref>

다음이 성립한다.
* <math>\mathsf{NFU}\vdash\operatorname{Con}(\mathsf Q)</math> [<math>\mathsf Q</math>는 로빈슨 산술({{llang|en|Robinson arithmetic}})]
* <math>\mathsf{NF}\vdash\operatorname{Con}(\mathsf{PA})</math>
* <math>\mathsf{PA}\vdash\operatorname{Con}(\mathsf{NFU})</math><ref name="Jensen">{{저널 인용|성=Jensen|이름=R. B.|제목=On the consistency of a slight (?) modification of Quine’s ’New Foundations’|언어=en|저널=Synthese|권=19|쪽=250–263|날짜=1968|issn=0039-7857|doi=10.1007/BF00568059|zbl=0202.01001}}</ref>{{rp|252}}
* <math>\mathsf{PA}\vdash\operatorname{Con}(\mathsf{TST})</math><ref name="Jensen"/>{{rp|252}}
* <math>\mathsf{PA}\vdash\operatorname{Con}(\mathsf{TST}+\mathsf{Inf})\implies\operatorname{Con}(\mathsf{NFU}+\mathsf{Inf})</math><ref name="Jensen"/>{{rp|252, Theorem 1}}
* <math>\mathsf{PA}\vdash\operatorname{Con}(\mathsf{TST}+\mathsf{Inf}+\mathsf{Choice})\implies\operatorname{Con}(\mathsf{NFU}+\mathsf{Inf}+\mathsf{Choice})</math><ref name="Jensen"/>{{rp|252, Theorem 1}}
* <math>\mathsf{Z}\vdash\operatorname{Con}(\mathsf{TST}+\mathsf{Inf})</math><ref name="KemenyPhD">{{학위논문 인용|성=Kemeny|이름=John George|제목=Type-theory vs. set-theory|언어=en|종류=박사 학위 논문|출판사=Princeton University|날짜=1949}}</ref><ref name="KemenyAbstract">{{저널 인용|성=Kemeny|이름=John George|제목=Type theory vs. set theory|종류=박사 학위 논문의 초록|언어=en|저널=Journal of Symbolic Logic|권=15|쪽=78|날짜=1950|issn=0022-4812}}</ref>
* <math>\mathsf{ZF}\vdash\operatorname{Con}(\mathsf{NF})</math><ref name="HolmesWilshaw">{{웹 인용|성1=Holmes|이름1=M. Randall|성2=Wilshaw|이름2=Sky|제목=NF is consistent|언어=en|날짜=2024|웹사이트=Randall Holmes's Home Page|url=https://randall-holmes.github.io/Nfproof/maybedetangled2.pdf|확인날짜=2024-10-01|dead-link=no|보존url=https://web.archive.org/web/20240731020222/https://randall-holmes.github.io/Nfproof/maybedetangled2.pdf|보존날짜=2024-07-31}}</ref><ref name="HolmesWilshawArxiv">{{arXiv 인용|성1=Holmes|이름1=M. Randall|성2=Wilshaw|이름2=Sky|제목=NF is consistent|언어=en|날짜=2024|전자문서=1503.01406|id={{doi 2|10.48550/arXiv.1503.01406}}}}</ref>
(마지막 결과는 아직 정식 출판되지 않았다.)

== 역사 ==
단순 유형 집합론(TST)은 1930년대에 [[알프레트 타르스키]]가 처음 정의하였다.<ref name="TarskiBetrachtungen">{{저널 인용|성1=Tarski|이름1=Alfred|저자링크=알프레트 타르스키|제목=Einige Betrachtungen über die Begriffe der ω-Widerspruchsfreiheit und der ω-Vollständigkeit|언어=de|저널=Monatshefte für Mathematik und Physik|권=40|쪽=97–112|날짜=1933|issn=0026-9255|doi=10.1007/BF01708855|mr=1550192|jfm=59.0053.01}}</ref> 1968년 논문에서 [[로널드 젠슨]]({{llang|en|Ronald Jensen}})은 근원소를 갖는 새 기초(NFU)를 도입하였으며, NFU가 [[페아노 산술]](PA)에 [[상대적 무모순성|상대적으로 무모순적]]임을 증명하였다.<ref name="Jensen"/> (젠슨의 증명은 [[모형 이론]]적이지만, PA에서 기술 가능한 특정 모형들만 사용하기 때문에 PA에서 형식화할 수 있다.)

== 참고 문헌 ==
{{각주}}
* {{서적 인용
|장url=http://virtualmath1.stanford.edu/~feferman/papers/ess.pdf
|보존url=https://web.archive.org/web/20211020203028/http://virtualmath1.stanford.edu/~feferman/papers/ess.pdf
|보존날짜=2021-10-20
|url-status=live
|이름=Solomon
|성=Feferman
|장=Enriched Stratified Systems for the Foundations of Category Theory
|언어=en
|제목=Foundational Theories of Classical and Constructive Mathematics
|총서=The Western Ontario Series in Philosophy of Science
|권=76
|출판사=Springer
|위치=Dordrecht
|날짜=2011
|isbn=978-94-007-0430-5
|issn=1566-659X
|doi=10.1007/978-94-007-0431-2_6
|mr=2867085
|zbl=1315.18001
}}

== 외부 링크 ==
* {{웹 인용|url=https://plato.stanford.edu/entries/settheory-alternative/|제목=Alternative Axiomatic Set Theories|언어=en|이름=Melvin Randall|성=Holmes|웹사이트=[[스탠포드 철학 백과사전|Stanford Encyclopedia of Philosophy]]}}
* {{웹 인용|url=https://randall-holmes.github.io/|보존url=https://web.archive.org/web/20211015075456/https://randall-holmes.github.io/|보존날짜=2021-10-15|url-status=live|제목=Randall Holmes's Home Page|언어=en}}
* {{웹 인용|url=https://randall-holmes.github.io/nf.html|보존url=https://web.archive.org/web/20201031232020/https://randall-holmes.github.io/nf.html|보존날짜=2020-10-31|url-status=live|제목=New Foundations home page|언어=en}}
* {{웹 인용|url=https://randall-holmes.github.io/Bibliography/setbiblio.html|보존url=https://web.archive.org/web/20210210102123/https://randall-holmes.github.io/Bibliography/setbiblio.html|보존날짜=2021-02-10|url-status=live|제목=Bibliography of Set Theory with a Universal Set|언어=en}}
* {{웹 인용|url=https://randall-holmes.github.io/Nfproof/newattempt.pdf|보존url=https://web.archive.org/web/20210831083350/https://randall-holmes.github.io/Nfproof/newattempt.pdf|보존날짜=2021-08-31|url-status=live|제목=A new pass at the NF consistency proof|언어=en|이름=Melvin Randall|성=Holmes}}
* {{웹 인용|url=https://mathoverflow.net/questions/132103/the-status-of-the-consistency-of-nf-relative-to-zf|제목=The status of 'the consistency of NF relative to ZF'|웹사이트=MathOverflow}}
* {{웹 인용|url=https://www.logicmatters.net/2022/08/23/nf-is-consistent/|제목=NF is consistent|웹사이트=Logic Matters|이름=Peter|성=Smith|날짜=2022-08-23}}
* {{웹 인용|url=https://www.logicmatters.net/2024/04/21/nf-really-is-consistent/|제목=NF really is consistent|웹사이트=Logic Matters|이름=Peter|성=Smith|날짜=2024-04-21}}
{{집합론}}

[[분류:집합론 체계]]
[[분류:수학기초론]]