증명 보조기와 유형론 알아보기

논리학
1

증명 보조기와 유형론 알아보기

소개

형식화[formalization]는 어떤 이론을 증명 보조기의 언어로 서술하는 일을 뜻합니다. 원래는 '형식 증명'이나 '형식화'가 이보다 더 넓은 의미로 쓰이는 용어예요. 형식 증명은 특정한 형식 체계를 바탕으로 작성한 증명이고, 형식화는 그런 형식 체계로 어떤 이론을 서술하는 일입니다. 즉, 증명 보조기 없이도 형식 증명을 작성하고 어떤 이론을 형식화할 수 있죠.

프로그래밍 언어론 연구자들은 주로 코크(Coq)나 아그다(Agda)를 이용하는 것 같습니다. 이것들과 이저벨(Isabelle)은 소프트웨어의 정확성을 검증하는 데도 쓰입니다.

린(Lean)은 수학 기초론 밖의 분야를 연구하는 수학자들이 특히 많이 이용하고 있습니다. 그리고 린의 핵심 라이브러리에 있는 몇몇 전략[tactic]은 고전 논리 공리를 이용자의 지시 없이도 기본적으로 이용합니다. 그래서 비고전 논리를 바탕으로 한 프로젝트를 린으로 개발하려면 새로운 전략을 이용자가 직접 만들어야 돼요.

증명 보조기의 구조

안드레이 바우에르(Andrej Bauer) 교수님의 위 강연 내용(11:10~16:47)을 다음과 같이 요약해 봤습니다.

  • 커널: 증명 검증기 역할을 맡는 핵심 부분.
  • 사투리[vernacular]: 사람이 증명 보조기를 편리하게 다루기 위한 언어.
  • 부연[elaboration]: 사람이 증명 보조기의 사투리로 작성한 내용을 커널의 언어로 바꾸는 일.

간단한 린 코드와 유형론에 대한 긴 설명

이 절은 "호모토피 유형론: 수학의 한값 기초론"의 1.1~1.2절을 참고해 작성했습니다.

전건 긍정 논법[modus ponens]은 린의 언어로 다음과 같이 서술할 수 있습니다.

theorem mp (p q : Prop) (maj : p → q) (min : p) : q :=
  maj min

a : A라는 판단[judgment]은 항 a의 유형이 A임을 뜻합니다. 그리고 린의 유형론에서, 각 명제는 유형입니다. 유형 A가 명제를 나타낸다면, a는 A가 증명 가능하다는 증언[witness] 또는 A가 참이라는 증거[evidence]가 됩니다. 그냥 a가 명제 A의 증명이라고 말하는 편이 더 간결하다고 저는 생각해요.

각 유형이 속하는 유형은 따로 있습니다. Prop은 명제들의 유형 세계[type universe]입니다. 위의 린 코드에서, p와 q는 유형 세계 Prop에 속하므로 명제입니다. 그런데 각 명제는 유형이므로 p와 q는 유형입니다. 긍정 논법의 소전제 min의 유형은 명제 p이므로, 위의 정리 mp에는 p가 참이라는 증거 min이 가정으로 주어져 있습니다.

판단은 명제와 달리 유형론의 메타이론에 속하는, 다시 말해 유형론의 외부에 있는 진술입니다. 명제는 유형론 그 자체의 진술, 즉 유형론의 내부에 속하는 진술입니다. 그래서 a : A 자체가 명제라고 말하지는 않습니다. a나 A는 명제가 될 수 있지만요.

린의 유형론에서는 증명 무관성[proof irrelevance] 때문에 한 명제의 두 증명이 정의상 같습니다[definitionally equal].

두 유형 A와 B가 주어져 있을 때, A → B는 정의역 A에서 공역 B로의 함수의 유형입니다. 집합론에서와 달리, 유형론에서 함수는 원시 개념입니다. 두 유형 A와 B가 명제를 나타낸다면, A → B는 "A이면 B이다."라는 조건문이 됩니다. f의 유형이 그런 조건문이라면, f는 명제 A의 증명을 바탕으로 명제 B의 증명을 산출하는 함수입니다. 또한 f는 그 조건문의 증명이죠. 여기서 a가 유형 A의 항이라면, f(a)의 유형은 B입니다. 린에서는 f(a)를 간단히 f a로 표시할 수 있습니다.

위의 린 코드에서, 긍정 논법의 대전제 maj의 유형은 p → q이므로, 이 조건문의 증명이자 정의역 p에서 공역 q로의 함수입니다. min은 명제 p의 증명이므로, maj min은 min에서의 함수 maj의 함숫값입니다. 그래서 maj min의 유형은 q입니다.

정리 mp의 유형은 (p q : Prop) → (p → q) → p → q입니다. 여기서 화살표 기호 →는 오른쪽으로 결합합니다[right-associative]. 그래서 mp의 유형은 (p q : Prop) → ((p → q) → (p → q))와 같이 나타낼 수도 있습니다. 이는 린의 #check 명령어를 이용해 다음과 같이 확인할 수 있습니다.

#check (mp : (p q : Prop) → (maj : p → q) → (min : p) → q)

위의 정리 mp는 유형론의 관점에서 다음과 같이 설명할 수 있습니다.

p, q가 명제이고, 대전제 maj가 조건문 p → q의 증명이고, 소전제 min이 p의 증명일 때, 함숫값 mp p q maj min의 유형은 q이다. 다시 말해, 이 함숫값은 q의 증명이다.

린의 커널에서는 정리와 정의 사이의 본질적인 차이가 없습니다. 어떤 정리를 증명하는 일은 결국 그 정리의 증명 항을 정의하는 일이기 때문입니다. 그래서 함숫값 mp p q maj min은 증명 항 maj min과 정의상 같습니다.

증명 보조기를 철학 연구에 어떻게 활용할 수 있는지는 나중에 다른 글로 설명하겠습니다. 이 글의 길이가 제 예상보다 훨씬 길어졌네요.

참고 문헌

12개의 좋아요