종종 인터넷을 돌다 보면 type theory가 왜 다른 기초론 (특히 set theory)보다 나은 지에 대한 이야기들을 보고는 하는데, 그 반대에 대한 이야기는 잘 못 봤던 것 같다. 집합론 하는 사람들이 이에 신경을 안 쓰는 지점도 있을 것 같고, type theory의 기초론적 역할을 주장하는 사람들은 일종의 도전자 입장이니 좀 더 공격적으로 논지를 펼쳐야 한다는 지점도 있지 않을까 싶다. 이 글에서는 그럼에도 왜 집합론이 “기초론적인 측면에서” 더 나은 지 생각했던 의견들을 모아 보려고 한다. 이런 글은 좀 더 반응을 모아 보고 싶다면 영어로 쓰는 게 맞긴 하겠지만, 일단 이 논지 자체에 힘을 싣고 싶은 것은 아니라서 일단 한국어로 정리해둔다. 매우 당연한 이야기지만, 해당 글의 주장들은 사견이며 비판적으로 읽을 여지가 있음을 밝혀 둔다. 그리고 특히, type theory 관련된 부분은 내 지식 부족으로 잘못된 논증을 포함하고 있을 위험도 있음을 밝혀 둔다.
글을 시작하기 전에 주의를 달고 시작하자. “기초론적”이란 표현의 뜻이 무엇인가. 나는 이 글에서 집합론이나 type theory 어느 쪽이 더 “수학을 하는 데” 적합한 지를 논하려고 하지 않는다. 지금까지 쌓아온 감으로는, 대수학 (특히 category 느낌이 강한 structural한 대수학)이나 컴퓨터 과학 몇몇 분야의 경우 type theory가 좀 더 유리하고, 해석학이나 일반위상, 측도론 따위는 set theory가 좀 더 유리한 기초론이라는 생각은 하고 있다. 증명의 검증의 측면이나 inductive definition을 바로 쓸 수 있다는 등의 측면에선 type theory가 유리할 지도 모르고, type theory 커뮤니티, 특히 Lean 커뮤니티에서 방대한 수학 라이브러리를 만들었다는 면도 생각해볼 수 있다. Lean이 과연 우아한 이론인가는 별개로 하더라도. 하지만 나는 이 논점들을 전부 이 글에서 안 다룰 것이다. 그러면 도대체 “기초론적으로 낫다”는 게 무슨 의미인가? 한 줄로 요약하면, “주어진 이론들이 다른 이론들의 세기를 재는 데 유용한 잣대 역할을 할 수 있느냐”는 것이다.
19세기 후반부터 20세기 초반까지 수학의 무모순성을 확립하려는 수많은 시도가 있어왔다. 물론 그 많은 시도들, 특히 힐베르트의 형식주의적 프로그램은, 괴델의 불완전성 정리 때문에 불가능하다는 것이 드러났다. 하지만 한편으로, 괴델의 불완전성 정리는 단일한 완벽한 형식적 이론 대신 “이론들간의 계층”이 있어야 한다는 것을 시사한다고 본다. 한 번 러셀의 역설을 생각해보자. 러셀의 역설은 모든 집합의 집합이 없다는 것을 보여준다. 이에 대한 통상적인 해결책은, 새로운 집합을 구성할 때 이전 집합들로부터 구성할 것을 요구하는 것이다. 이를 좀 더 형식적으로 적어 보자면
$C$가 우리들이 갖고 있는 집합들의 모임일 때, 새로운 집합은 $C$의 부분모임이여야 한다.
다르게 써 보면, 만약 $C’$가 $C$로부터 구성해낸 새로운 집합들의 모임일 때, $C’ = \mathcal{P}(C)$여야 한다는 것이다. 이 아이디어를 공집합에서부터 적용해서 올라가면, 통상적인 cumulative hierarchy를 얻는다. 요약하면, “러셀의 역설은 집합들간 계층이 있음을 시사한다.”
러셀의 역설은 일종의 자기 참조 역설이다. 괴델의 불완전성 정리도 똑같은 성격을 지니는데, 위의 러셀의 역설로부터 cumulative hierarchy로 가는 과정”으로 귀추해보면, 괴델의 불완전성 정리는 이론 간의 계층이 있음을 시사하지 않을까 생각해볼 수 있다. 그리고 괴델의 제2 불완전성 정리를 대충 적으면 $T \nvdash \mathsf{Con}(T)$이며, 러셀의 역설도 대충 적으면 $V\notin V$이다. 집합들을 비교할 때 $\in$을 가지고 비교하니, 두 이론 $S$와 $T$를 비교할 때는
\[ S <_{\mathsf{Con}} T \iff T\vdash \mathsf{Con}(S) \]
와 같이 비교하는 것이 옳다고 할 수 있겠다.
$<_{\mathsf{Con}}$는 꽤 “불규칙하게” 행동하지만, “자연스러운” 이론들에 대해서는 $<_{\mathsf{Con}}$이 정렬순서를 이룬다고 흔히 주장되어왔다.
만약 “자연스러운” 이론들 간의 “세기”를 항상 비교할 수 있다면, 그 세기를 어떻게 표현할 지도 물을 수 있다. 집합의 경우, 이것이 유일한 방법은 아니긴 해도, 집합의 rank를 이용해서 얼마나 복잡한 지 잴 수 있다. 하지만 이론들의 경우에는 상황이 좀 더 복집하다. 가령 증명론적 서수를 사용해서 비교하겠다고 하면, 서로 “세기가 다른” 두 이론이 같은 증명론적 서수를 갖기도 하고, 굉장히 센 이론들의 증명론적 서수는 우리들이 모르기도 하다. 그럼에도, 마치 모스 굳기계를 이용해서 다른 광물들의 상대적 굳기를 표현하듯, 특정한 이론들을 내세워서 다른 이론들의 세기를 표현할 수 있다. 집합론에서는 $\mathsf{ZFC}$에 large cardinal axiom을 더한 이론들이 그 역할을 하고, 역수학에서는 소위 big five라고 불리는 이차 산술들의 subsystem이나 그 변형들이 그 역할을 한다. 가령 이런 식으로:
정리.
- (Solovay) 만약 $\mathsf{ZFC}$ + “inaccessible cardinal이 있다”가 무모순하면, $\mathsf{ZF+DC}$ + “모든 $\mathbb{R}$의 부분집합이 르벡 가측이다” 도 무모순하다.
- (Shelah) $\mathsf{ZF+DC}$는 다음을 증명한다: 만약 모든 $\mathbf{\Sigma}^1_3$ 집합이 르벡 가측이면 $\omega_1^V$는 $L$ 위에서 inaccessible cardinal이다. 특히, $\mathsf{ZF+DC}$ + “모든 $\mathbb{R}$의 부분집합이 르벡 가측이다”가 무모순하면 $\mathsf{ZFC}$ + “inaccessible cardinal이 있다”도 무모순하다.
여기서는, $\mathsf{ZF+DC}$ + “모든 $\mathbb{R}$의 부분집합이 르벡 가측이다” 라는 이론의 세기를 $\mathsf{ZFC}$ + “inaccessible cardinal이 있다”라는 $\mathsf{ZFC}$의 확장을 이용해서 표현하고 있다. 다만 이렇게 깔끔하게 딱 떨어지는 경우는 많지는 않고, upper bound만 아는 경우도 많다. 가령,
정리 (Baumgartner) Supercompact cardinal로부터 시작해서 $\mathsf{PFA}$를 force할 수 있다. 특히, $\mathsf{ZFC}$ + “supercompact cardinal이 있다”가 무모순하면 $\mathsf{ZFC+PFA}$도 무모순하다.
많은 집합론자들이 두 이론이 equiconsistent하다고 생각하지만 추측일 뿐이다. 여하튼, 위 정리는 $\mathsf{ZFC+PFA}$가 “어느 정도 무모순할 지” $\mathsf{ZFC}$의 확장을 이용해서 표현하고 있다.
그러면 왜 집합론자들은 $\mathsf{ZFC}$ + “적당한 large cardinal axiom”을 써서 다른 이론들의 세기를 나타내는가? 나도 “이것이여야만 한다”는 이유는 모른다. 그럼에도 가능한 이유를 설명해보자면, 우선 “좀 더 좋은 서수나 기수가 있다” 외의 주장을 별다른 정당성 없이 추가해서 얻은 이론을 가지고 다른 이론의 세기를 비교하는 것이 온당치 않게 들린다는 점이 있다. 집합론자들 사이에서 $\mathsf{ZFC}$의 공리 정도는 받아들일 수 있다고 합의가 되어 있고, large cardinal axiom들도 “$\mathsf{ZFC}$만으로는 알 수 없는, 좀 더 큰 서수들의 성질을 말하는 공리” 정도로 받아들일 수 있겠지만, 낮은 레벨에서 일어나는 결정 불가능한 명제들 (가령 연속체 가설) 을 임의로 추가해서 이론의 세기를 비교하는 것은 논란의 소지가 있지 않을까 하는 것이다. 다른 이유는, $\mathsf{ZFC}$ + large cardinal axiom으로 시작해서 다른 이론들의 무모순성을 확보하는 것이 상대적으로 쉽다는 데에 있다. 여기서 주의하자. “상대적으로” 쉽다는 것이다. 보통은 절대로 쉽지 않다. 하지만 그 반대 방향, 즉, 다른 이론들로부터 시작해서 $\mathsf{ZFC}$ + 적당한 large cardinal axiom의 무모순성을 확보하는 것은 보통 꽤 어렵다. 이론이 일정 수준 이상 세지면 (대략 measurable cardinal 좀 넘어가는 수준) inner model theory적인 방법 없이는 뭔가 하기 거의 불가능하다.
이런 측면에서, $\mathsf{ZFC}$와 large cardinal axiom들이 다른 $\mathsf{ZFC}$의 확장의 “무모순성 세기”를 표현하는 데 더 나은 도구라고 생각할 수 있다. Large cardinal을 이용해서 다른 이론들의 세기의 upper bound를 표현하는 것은 그나마 쉽지만, 반대 방향은 어렵기 때문이다. 나는 이런 관점에서, $\mathsf{ZFC}$ + large cardinal axiom들이 다른 $\mathsf{ZFC}$의 확장보다 더 나은 기초론적 이론이다라고 본다.
여기서 잠깐 집합론을 벗어나서, 배중률을 놓고 생각해보자. 몇몇 사람들은 배중률을 반대하고, 나도 배중률이 없는 수학을 좀 배워본 적이 있다. 하지만, 배중률이 있는 이론들이 배중률이 없는 이론들보다 기초론적으로 낫다. 가령, 배중률을 부정하는 이론들이나 배중률이 없는 이론 (가령, 마틴뢰프 type theory) 들을 배중률이 있는 이론에서 해석하는 것은 상대적으로 쉽다. 이를 할 수 있는 방법론도 많다. (가령 realizability model 따위.) 하지만 그 반대 방향은 보통 뾰족한 방법이 없다. Double-negation translation이 안 되면, 그 다음으로 시도할 수 있는 방법이 서수 분석 그 자체나 그에 근접해 보이는 방법밖에 남지 않는 경우도 부지기수이다.
나는 집합론이 그런 의미에서 type theory보다 더 나은 기초론적인 이론이라 본다. 집합론에서 type theory를 해석하는 것은 비교적 쉽다. 그 반대 방향은 보통 Aczel’s tree interpretation 비슷한 것을 써야 하는데, impredicative type theory 정도 되면 배중률이나 특정 형태의 선택공리 따위가 없으면 이것만 가지고 $\mathsf{ZFC}$ 정도 되는 집합론을 해석하는 데 무리가 있어 보인다. 하지만 type theory에 배중률이나 특정 형태의 선택공리가 “자연스럽게 항상 있어야만 하는” 공리라고 보기에는 무리가 있지 않나 싶다. 어떤 면에서는 “배중률이 있는 이론이 없는 이론보다 기초론적으로 낫다”는 주장을 따라가는 셈인데, 여기에 “type theory의 자연스러운 형태는 배중률이 없는 것”이란 주장이 붙어 있는 셈 아닐까 싶다.
그리고, type theory가 제공하는 “줄자의 길이는 그렇게 길지 않다.” 말인즉슨, $\mathsf{ZFC}$와 그 large cardinal에 의한 확장의 경우 굉장히 강력한 이론들의 세기도 묘사할 수 있다. (Supercompact cardinal이 그 예시이다.) 하지만, 아직까지 type theory에서 measurable cardinal이나 Woodin cardinal에 대응할 만한 개념을 본 적이 없다. Vopenka principle 비슷한 것을 type theory에 추가하면 어찌저찌 될 지도 모르겠지만, 여전히 “줄자의 눈금이 그렇게 세밀하지 않다”는 문제는 남는다. Type theory의 확장들의 위계는 아직 “잘 안 알려져 있고” 알려진 쪽도 “거칠다.” 이는 다만 얼마나 많은 사람들이 이에 관심을 갖고 연구를 하느냐의 문제겠지마는, type theory 하는 사람들이 이 쪽으로 관심을 갖고 연구를 하는 것 같지는 않다. 기술적으로 어려운 부분도 있겠지만, 필요성을 못 느끼는 지점도 있지 않나 싶다.
글을 끝마치기 전에, 그러면 “기초론적으로 나아서 좋은 것이 무엇인가” 혹은 “이론의 세기를 측정하는 게 왜 중요한가” 물을 수 있다. 사실 나도 그 답이 궁금한 질문이다. 그래도 한 마디 해 보자면, “대충 어느 고도까지 올라가야 고산병에 안 걸릴 지” 높이를 표시해둔 게 그냥 “높이 올라가면 고산병에 걸릴 위험이 높다”고 말하는 것보다 낫지 않겠냔 것이다. 마찬가지로, “어느 이론 정도까지 무모순하다 믿으면 그 밑으로는 다 무모순하다”고 말할 수 있는 게 그냥 아무 말도 안 하는 것보다는 낫지 않을까 싶다.