게르하르트 겐첸(Gerhard Gentzen)

게르하르트 겐첸은 1909년 독일 북동부의 그라이프스발트에서 태어났습니다. 그가 공부를 시작한 1920년대 말, 괴팅겐의 힐베르트는 수학 전체를 기호 규칙으로 적고 그 규칙이 모순을 낳지 않는다는 것을 유한한 방법으로 증명하려는 계획을 이끌고 있었습니다. 그런데 프레게와 러셀, 힐베르트가 쓴 형식 체계⁠(formal system)⁠의 증명은 공리⁠(axiom)⁠ 몇 개와 추론 규칙 한두 개로 이루어져서, 수학자가 실제로 쓰는 증명과는 모양이 많이 달랐습니다. 겐첸은 증명 자체를 수학의 대상으로 삼으려면 먼저 증명을 사람이 추론하는 방식에 가깝게 적어야 한다고 보았습니다.

나이 세 ·

그는 1929년 괴팅겐으로 옮겨 힐베르트의 동료 파울 베르나이스에게 배웠습니다. 1933년 나치 정권이 유대계 학자들을 공직에서 몰아낼 때 베르나이스도 자리를 잃었고, 겐첸은 헤르만 바일의 이름으로 박사 논문을 냈습니다. 그 논문이 1934–35년 「논리적 추론에 관한 연구」로 출판되었습니다. 여기서 그는 두 가지 증명 체계를 만들었습니다. 하나는 자연 연역입니다. "A라고 가정하자. …그러면 B이다. 그러니 A이면 B이다"처럼, 가정을 세웠다가 거두는 방식으로 추론합니다. 논리 기호마다 그것을 만드는 규칙(도입)과 쓰는 규칙(제거)이 짝을 이루는 것이 특징입니다.

다른 하나는 시퀀트 계산입니다. "가정들 Γ로부터 C가 따라 나온다"를 $\Gamma \vdash C$라는 한 덩어리로 적고, 이런 덩어리를 규칙으로 바꿔 나갑니다. 위의 식이 이 체계의 '절단⁠(cut)⁠' 규칙입니다. 중간 결론 A를 먼저 증명하고, A를 가정으로 써서 C를 증명하는 것, 곧 수학자들이 보조정리⁠(lemma)⁠를 쓰는 방식입니다. 겐첸의 핵심 정리는 이 규칙을 쓰는 증명은 언제나 절단 없는 증명으로 바꿀 수 있다는 것입니다(절단 제거). 절단 없는 증명에는 결론에 나오지 않는 식이 끼어들지 않으므로, 증명이 결론의 부분식만으로 이루어집니다. 이 성질 덕분에 증명을 기계적으로 찾거나, 어떤 식이 증명될 수 없음을 보이는 일이 쉬워집니다. 같은 사실을 자연 연역에서는 증명의 군더더기(도입했다가 곧바로 제거하는 돌아가기)를 모두 없앨 수 있다는 정규화로 말하고, 1965년 다그 프라비츠가 이것을 증명했습니다.

1936년 겐첸은 힐베르트 계획의 한가운데로 들어갔습니다. 자연수의 산술에 모순이 없다는 것을 증명한 것입니다. 그러나 1931년 괴델의 불완전성 정리⁠(incompleteness theorem)⁠는 산술이 자기의 무모순성을 산술 안에서 증명할 수 없음을 보인 뒤였습니다. 겐첸은 산술보다 강한 원리 하나, 곧 서수⁠(ordinal)⁠ $\varepsilon_0$까지의 초한 귀납법⁠(transfinite induction)⁠을 더해 증명했습니다. 이 증명은 힐베르트가 바란 '유한한 방법'만의 증명은 아니었지만, 어떤 체계의 무모순성을 증명하려면 정확히 어디까지의 무한이 필요한지를 재는 증명론⁠(proof theory)⁠의 출발점이 되었습니다.

그의 삶은 시대에 휩쓸렸습니다. 1933년 나치 돌격대에 들어갔고 뒤에 나치당원이 되었습니다. 1939년 징집되어 통신 부대에서 일하다 병으로 제대했고, 1943년 프라하의 독일 대학으로 옮겼습니다. 1945년 5월 프라하 시민들이 독일 점령군에 맞서 봉기했을 때 다른 독일 대학 교직원들과 함께 붙잡혀 수용소에 갇혔고, 석 달 뒤인 8월 4일 굶주림으로 세상을 떠났습니다. 서른다섯 살이었습니다.

자연 연역은 그 뒤 논리학 교과서의 표준이 되었고, 1969년 윌리엄 하워드는 그 규칙이 타입⁠(type)⁠ 붙은 람다 계산⁠(lambda calculus)⁠의 규칙과 하나하나 짝을 이룬다는 것을 보였습니다. 증명의 군더더기를 없애는 일이 곧 프로그램을 실행하는 일이라는 커리–하워드 대응⁠(Curry–Howard correspondence)⁠의 한쪽 절반이 겐첸의 체계입니다. 오늘날의 증명 보조기⁠(proof assistant)⁠도 대부분 이 규칙들 위에 서 있습니다.

이어지는 곳. 자연 연역의 규칙이 프로그램의 규칙과 어떻게 짝을 이루는지는 커리–하워드 대응과 직관주의 논리⁠(intuitionistic logic)⁠에서, 그가 목표로 삼은 힐베르트의 계획과 그것을 가로막은 정리는 수학 기초론 논쟁⁠(debate on the foundations of mathematics)⁠과 불완전성 정리에서 볼 수 있습니다. 증명을 기계가 검사하는 오늘의 모습은 증명 보조기에 있습니다.

관계.

• 영향을 받음 다비트 힐베르트 — 1934년부터 힐베르트의 조수로 일했고, 수학에 모순이 없음을 유한한 방법으로 증명하려던 힐베르트의 계획을 자기 연구의 목표로 삼았습니다.
• 영향을 받음 쿠르트 괴델 — 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠ 때문에 산술의 무모순성은 산술 안에서 증명할 수 없었고, 겐첸은 그 너머의 원리 하나(ε₀까지의 초한 귀납법)만 더해 증명하는 길을 찾았습니다.
• 영향을 줌 윌리엄 하워드 — 하워드는 겐첸의 자연 연역의 규칙 하나하나가 타입 붙은 람다 계산의 규칙과 짝을 이룬다는 것을 보여 커리–하워드 대응을 세웠습니다.

연표.

• 1909년 그라이프스발트에서 태어나다
• 1928년 그라이프스발트 대학에 들어가다
• 1929년 괴팅겐 대학으로 옮겨 베르나이스에게 배우다
• 1933년 베르나이스가 해직된 뒤 바일의 이름으로 괴팅겐에서 박사 학위를 받다
• 1934년 「논리적 추론에 관한 연구」에서 자연 연역과 시퀀트 계산을 내놓다
• 1934년 힐베르트의 조수가 되다
• 1936년 ε₀까지의 초한 귀납법으로 자연수 산술의 무모순성을 증명하다
• 1939년 징집되어 통신 부대에서 복무하다가 병으로 제대하다
• 1943년 프라하의 독일 대학으로 옮기다
• 1945년 5월 프라하 봉기 때 붙잡혀, 8월 4일 수용소에서 굶주림으로 세상을 떠나다