증명, 명제 그리고 명제들의 유형

논리학
10

이런 용례는 제가 처음 만든 게 아니라는 점을 강조하고 싶습니다. 제가 쓴 글 '증명 보조기와 유
형론'에서 언급된 "호모토피 유형론: 수학의 한값 기초론"의 18쪽에 다음 문구가 있습니다.

The basic judgment of type theory, analogous to “A has a proof”, is written “a : A” and pronounced as “the term a has type A”, or more loosely “a is an element of A” (or, in homotopy type theory, “a is a point of A”). When A is a type representing a proposition, then a may be called a witness to the provability of A, or evidence of the truth of A (or even a proof of A, but we will try to avoid this confusing terminology).

그런데 "린 4로 하는 정리 증명"의 3장 '명제와 증명'에서는 오히려 저자가 '증거' 말고 '증명'이라는 용어만 씁니다.

"기존에 '증명'이라고 불러온 개념을 뭐라고 부를지 알 수 없게 되어 버립니다."라는 @car_nap 님의 말씀에서, 그 '증명'은 무엇을 가리키나요? 유형론을 거의 모르지만 그 밖의 논리학은 이미 배운 철학 또는 수학 전공자들이 이해하는 개념으로서의 '증명'인가요? "린 4로 하는 정리 증명" 교재에서와 같이 "증명"이라는 용어를 쓴다면, 이 교재에 나온 '증명'이 우리가 이미 알고 있는 개념 '증명'과 그리 다른지 저는 모르겠어요. 호모토피 유형론 교재에서는 '증거'가 어떤 명제의 증명 가능성을 보이는 개념이라고 설명했으니, 이 용어를 '증명'으로 바꿀 때 혼동이 생길 수 있죠.

"린 4로 하는 정리 증명" 3장의 위 인용문과 '커리-하워드 대응' 위키백과 항목이 이해에 도움이 될 거예요.

이 대응 때문에 린의 유형론에서는 theorem 명령이 본질적으로 def 명령의 한 버전에 불과해요.

Note that the theorem command is really a version of the def command: under the propositions and types correspondence, proving the theorem p → q → p is really the same as defining an element of the associated type. To the kernel type checker, there is no difference between the two. (Avigad et al. n.d.)

그래도 의문점이 남는다면 제 능력이 닿는 데까지 커리-하워드 대응을 설명해 드릴게요.

참고 문헌