새 기초

틀:위키데이터 속성 추적 수리논리학에서 새 기초(틀:Llang, 약자 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와 같은 식이 원천적으로 불가능하게 되므로 러셀의 역설에 걸리지 않는다. 다만 기존 러셀 유형론과의 중대한 차이는 분류 공리꼴을 이용하여 유형을 간접적으로 나타냄으로써 유형의 개념을 별도로 도입하지 않도록 수정되었다는 점이다.

정의

단순 유형 집합론

단순 유형 집합론(틀:Llang, 틀:Llang, 약자 TST)은 자연수 종류를 갖는 다종류(틀:Llang) 1차 이론이며, 이항 관계 $\in$를 갖는다. $x\in y$가 논리식이려면 $y$의 종류가 $x$의 종류보다 1 커야 한다. TST의 공리계는 다음과 같은 두 공리 기본꼴로 구성된다.

• (확장 공리 기본꼴) $\mathrm{\forall }{x}^{i+1}\mathrm{\forall }{y}^{i+1}(\mathrm{\forall }{z}^i(z^i\in x^{i+1}⟺z^i\in y^{i+1})⟹x^{i+1}=y^{i+1})$
• (분류 공리 기본꼴) $x_1,x_2,\dots ,x_n,z^i$를 자유 변수로 갖는 논리식 $\varphi$에 대하여, $\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\cdots \mathrm{\forall }{x}_k\mathrm{\exists }{y}^{i+1}\mathrm{\forall }{z}^i(z^i\in y^{i+1}⟺\varphi )$

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

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

새 기초

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

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

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

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

• (확장 공리) $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x⟺z\in y)⟹x=y)$
• (층화 분류 공리 기본꼴, 틀:Llang) $x_1,x_2,\dots ,x_n,z$를 자유 변수로 갖는 층화 논리식 $\varphi$에 대하여, $\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\cdots \mathrm{\forall }{x}_n\mathrm{\exists }y\mathrm{\forall }z(z\in y⟺\varphi )$

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

근원소를 갖는 새 기초

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

• (공집합이 아닌 집합에 대한 확장 공리) $\mathrm{\forall }x\mathrm{\forall }y((\mathrm{\exists }z(z\in x)\wedge \mathrm{\forall }w(w\in x⟺w\in y))⟹x=y)$

마찬가지로, 근원소를 갖는 단순 유형 집합론(틀:Llang, 약자 TSTU)과 근원소를 갖는 꼬인 유형 집합론(틀:Llang, 약자 TTTU)을 정의할 수 있다.

상대적 무모순성

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

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

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

• $𝖭𝖥$
• $𝖳𝖲𝖳+𝖠𝗆𝖻$
• $𝖳𝖳𝖳$

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

• $𝖭𝖥𝖴$
• $𝖳𝖲𝖳𝖴+𝖠𝗆𝖻$
• $𝖳𝖳𝖳𝖴$

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

$𝖨𝗇𝖿$와 $𝖢𝗁𝗈𝗂𝖼𝖾$가 (각 이론에서의) 무한 공리와 선택 공리라고 하자. 그렇다면, 다음 이론들이 서로 등무모순적이다.

• $𝖳𝖲𝖳+𝖨𝗇𝖿$
• $𝖳𝖲𝖳+𝖨𝗇𝖿+𝖢𝗁𝗈𝗂𝖼𝖾$틀:Rp
• $𝖭𝖥𝖴+𝖨𝗇𝖿$틀:Rp
• $𝖭𝖥𝖴+𝖨𝗇𝖿+𝖢𝗁𝗈𝗂𝖼𝖾$틀:Rp
• $𝖬𝖺𝖼$
• $𝖪𝖥$

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

다음이 성립한다.

• $𝖭𝖥𝖴⊢\mathrm{Con}(𝖰)$ [$𝖰$는 로빈슨 산술(틀:Llang)]
• $𝖭𝖥⊢\mathrm{Con}(𝖯𝖠)$
• $𝖯𝖠⊢\mathrm{Con}(𝖭𝖥𝖴)$틀:Rp
• $𝖯𝖠⊢\mathrm{Con}(𝖳𝖲𝖳)$틀:Rp
• $𝖯𝖠⊢\mathrm{Con}(𝖳𝖲𝖳+𝖨𝗇𝖿)⟹\mathrm{Con}(𝖭𝖥𝖴+𝖨𝗇𝖿)$틀:Rp
• $𝖯𝖠⊢\mathrm{Con}(𝖳𝖲𝖳+𝖨𝗇𝖿+𝖢𝗁𝗈𝗂𝖼𝖾)⟹\mathrm{Con}(𝖭𝖥𝖴+𝖨𝗇𝖿+𝖢𝗁𝗈𝗂𝖼𝖾)$틀:Rp
• $𝖹⊢\mathrm{Con}(𝖳𝖲𝖳+𝖨𝗇𝖿)$
• $𝖹𝖥⊢\mathrm{Con}(𝖭𝖥)$

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

역사

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

참고 문헌

• 틀:서적 인용

외부 링크

• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용