유형론에 관한 학습 자료와 두 가지 물음

논리학
1

유형론 학습 자료

위의 자료 중에서 저는 "린 4로 하는 정리 증명"밖에 읽지 않았고, 이 교재는 린 증명 보조기로 정리를 진술하고 증명하는 데 필요한 만큼만 의존 유형론[dependent type theory]을 다루고 있습니다. 그러다 보니 린을 이용할 줄은 알아도, 여전히 유형론에 관한 제 궁금증이 그리 해소가 안 됐습니다. 의존 유형론을 더 알아보고 싶은데 그럴 시간이 아직 부족해요.

유형론에 관한 두 가지 물음

왜 대부분의 증명 보조기는 집합론 말고 유형론에 기반을 두는가?

I am not saying that it is impossible to design a proof assistant based on set theory. After all, Mizar, the most venerable of them all, is designed precisely in this way – set theory with a layer of type-theoretic mechanisms on top. But I cannot help to wonder: why bother with the set-theoretic kernel that requires a type-theoretic fence to insulate the user from the unintended permissiveness of set theory? (Bauer 2020)

안드레이 바우에르(Andrej Bauer) 교수님은 "어차피 유형론이 제공하는 '안전장치'가 필요한데 뭐 하러 집합론 기반의 커널을 만드느냐?"라고 반문하십니다. 순전한 호기심 말고는 집합론 기반의 증명 보조기를 '또' 개발할 이유가 별로 많지 않다는 데 저도 동의합니다.

그런데 제가 걱정하는 것은 현재 대부분의 한국 대학에서 집합론보다 유형론을 배울 기회가 훨씬 적다는 점입니다. 이 때문에 한국 학생들이 증명 보조기와 수학 라이브러리를 배우기가 더 어렵다고 생각합니다. 집합론을 형식 논리학과 함께 다양한 수준에서 가르치는 한국어 교재와 수업이 많듯이, 유형론도 그렇게 가르치는 한국어 교재와 수업이 많아져야 합니다.

한국어로 된 유형론 입문서와 상급자용 교재는 몰라도, 한국 대학에서 유형론 수업을 볼 일은 앞으로도 한동안 거의 없을 것 같습니다. 그래서 집합론 기반의 증명 보조기는 필요하지 않지만, 집합론 기반의 수학 라이브러리는 여전히 필요합니다. 그런 라이브러리를 매스리브(Mathlib)처럼 유형론에 기반을 둔 라이브러리와 비교하는 학습 자료가 많아진다면, 학생들이 두 부류의 수학 라이브러리를 모두 이해하기가 수월해질 것입니다.

집합론 말고도 유형론을 배울 이유가 있는가?

  1. 집합론을 활용하는 자기 연구 분야를 유형론의 관점에서 바라보기 위함.
  2. 증명 보조기를 이용해 자신이 연구하는 이론을 형식화하기 위함.
  3. 자신이 연구하는 분야가 이미 유형론을 활용하고 있기 때문임.

위의 세 가지 이유밖에 떠오르지가 않네요. 저는 집합론과 유형론 중에서 더 선호하는 기초론이 따로 없습니다. 원래는 유형론에 관심이 없었는데, "린 4로 하는 정리 증명"을 읽다 보니 유형론에 관한 궁금증이 생겼을 뿐이에요.

참고 문헌

Bauer, Andrej. 2020. “What makes dependent type theory more suitable than set theory for proof assistants?” Last modified 2020-12-07. https://mathoverflow.net/q/376973.

2

유형론의 발전 과정에 대한 (어느 정도 철학적 관점에서의) 개략을 살펴보고 싶으시다면 SEP의 유형론 항목을 읽어보시길 추천드립니다.

그리고 (링크해주신 MathOverflow 답변에서 언급된 증명보조기의 특징과는 독립적인 것 같기도 합니다만) 역사적으로 증명보조기는 유형론, 특히 직관주의적/구성적 유형론과 함께 발전해온 것 같네요 (SEP). 만약에 구성적 수학이 증명보조기 개발에 핵심적이라고 한다면, 고전 집합론에 기반한 증명보조기 개발이 어려운 이유가 되지 않을까 싶습니다. (구성적 집합론은 그에 반해 어떨지는 또 다른 문제겠네요.)

위 MathOverflow 링크의 다른 답변에서 언급된 Lawrence Paulson의 언급도 이런 인식을 반영하지 않나 싶습니다. (Paulson 본인은 이게 어디까지나 일종의 사회적 편견이라고 보는 것 같지만요.)

It's not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don't store proof objects? Really?”

2개의 좋아요
3

나중에 다음 물음의 해답을 찾고 싶네요.

  • 증명 보조기가 이용하는 각각의 유형론과 러셀의 유형론은 세부적으로 어떤 점이 다른가?
  • 왜 (수학 기초론 밖의 분야에서 연구하는) 수학자와 달리, 많은 논리학자와 이론 컴퓨터 과학자는 유형론에 오랫동안 관심을 기울였는가?
  • 왜 많은 이론 컴퓨터 과학자들은 고전 논리와 집합론보다 구성 논리와 유형론을 선호하는가?

구성 유형론[constructive type theory]을 만든 페르 마르틴-뢰프(Per Martin-Löf)와, 구성 계산[calculus of constructions, CoC]이라는 유형론을 만든 티에리 코캉(Thierry Coquand)의 영향이 매우 컸던 것 같습니다.

한편 로런스 폴슨(Lawrence Paulson)이 개발한 이저벨(Isabelle) 증명 보조기의 가장 대표적인 사례[인스턴스]가 이저벨/HOL인데, 이것은 고전 논리에 기반을 두고 있습니다. HOL은 고차 논리[higher-order logic]를 가리킵니다.

린은 구성 계산과 고전 논리 모두에 기반을 두고 있습니다. (조금 더 정확히 말하면, 현재로서는 고전 논리를 피하면서 린을 이용하기가 어렵습니다. 아마 이 상태가 한동안 지속될 거예요.)

증명 보조기를 개발하는 데 구성 논리가 핵심적인 역할을 한다기보다는, 고전 논리보다 구성 논리를 선호하는 이론 컴퓨터 과학자들을 위한 증명 보조기가 널리 쓰이는 것 같습니다. 물론 그들은 유형론 없이 집합론을 다루고 싶지 않을 것입니다.

수학 기초론 밖의 분야에 종사하는 대부분의 수학자는 이런 성향이 전혀 없습니다. 이들은 자신이 연구하는 수학 분야를 구성 논리와 유형론의 관점에서 새롭게 바라볼 동기가 없어요. 구성 논리를 선호하는 많은 이론 컴퓨터 과학자와, 호모토피 유형론[homotopy type theory, HoTT]에 관심 있는 수학자는 저런 성향이 있겠지만요.

Mario Carneiro said:

위의 인용문에서 DTT는 의존 유형론[dependent type theory]을 가리킵니다.