자연연역에 대해 몇 자 적어 봅니다. 특히 "피치 자연연역이 더 직관적인데 왜 겐첸-프라위츠 자연연역을 사용하나요?"라는 물음에 답변해 드립니다. 

보통 학술 영역에서 '자연연역'이라고 하면 게르하르트 겐첸(Gerhard Gentzen)과 스타니스와프 야스코브스키(Stanisław Jaśkowski)의 체계를 고려합니다. 둘 다 1934년 1935년 경에 발표되어 시기도 유사합니다. 프레데릭 피치(Frederic Fitch)는 야스코브스키의 체계를 가져다 썼다고 볼 수 있고요. 이 포스팅에서는 겐첸을 중심으로 자연연역을 설명해 볼께요. 

20세기 초 유럽 및 독일에서 가장 영향력이 있었던 수학자 중의 한 명인 다비드 힐베르트(David Hilbert)는 수학자들이 풀어야 할 여러 문제를 공시한 바가 있는데요. 그 중 두 번째 문제가 수학의 일관성을 유한한 방식으로 증명하는 것이었습니다. 

게르하르트 겐첸은 이 문제에 그야말로 미친 듯이 빠져 들었었는데요. 스승인 파울 베르나이스(Paul Bernays)의 지도 하에 독일 괴팅겐 대학에서 수학의 일관성 정리 증명을 여러 번 시도했습니다. 1930년대 수리논리학과 수학기초론 역사에 있어 천재를 딱 세 명만 뽑으라고 한다면 저는 쿠르트 괴델(Kurt Goedel), 게르하르트 겐첸(Gerhard Gentzen), 그리고 앨런 튜링(Alan Turing)을 꼽고 싶은데요. 물론 알론조 처치(Alonzo Church), 폰 노이만(Von Neuman), 알프레드 탈스키(Alfred Tarski), 프랭크 램지(Frank Ramsey) 등과 같은 괴물 같은 천재들도 있지만 괴델, 겐첸, 튜링 이 세 사람은 몇 안되는 저작에도 불구하고 모형론, 증명론, 재귀이론의 핵심 개념을 정의함으로써 수리논리의 세상을 열었다는 데서 단연 돋보인다고 생각됩니다. 딴 소리가 길었내요. 논문도 아니고 대강 기억나는 대로 적는 거니 딴지는 거부한다...

겐첸은 수학의 일관성을 증명하는데 있어서 "수학에서 사용되는 추론의 자연스러운 방식"(the natural method of reasoning in mathematics)을 먼저 형식화하고 이를 통해 수학을 형식화함으로써 수학의 핵심 공리로 부터 모순이 도출되지 않음을 보이려고 하는데요. 그 과정에서 창시한 것이 "자연연역"(natural deduction)입니다. 

1935년 겐첸은 "Investigations into logical deduction"에서 '자연연역'이라는 개념을 최초로 사용하고 관련 규칙을 제시합니다. 그리고 이 규칙들을 사용해서 제시되는 어떠한 증명(도출, 연역)도 불필요한 우회를 지니지 않는다는 핵심 정리(Hauptsatz, the main theorem)를 보입니다. 거칠게 말하자면, 수학적 증명들은 생략하거나 반복되거나하는 증명들이 많이 있는데요. (자연연역을 통해 형식화된) 어떠한 증명이든지 이러한 불필요한 반복 없이 증명의 모든 과정이 명시적으로 제시될 수 있음을 보인 것이죠. 거칠게 설명한거니 정확하지 않다고 뭐라하기 없기!! 

참고. https://logic-teaching.github.io/prop/texts/Gentzen%201969%20-%20Investigations%20into%20Logical%20Deduction.pdf

산수의 일관성 증명에 대한 시도는 1936년 논문부터 시작됩니다. 이 얘기를 하자면 길어지니 넘어가고요. 

1935년 "Investigations"에서 겐첸이 제시한 방식은 현재 프라위츠-겐첸 자연연역 방식이라고 하는 것과 동일한 그래픽 형식과 정식열 연산(sequent calculus)를 모두 제시했었는데요. Hauptsatz에 대한 증명은 정식열 연산 방식으로 증명했었습니다.

위와 같은 형식의 규칙을 보통 "겐첸-프라위츠 자연연역"이라고 부릅니다. 물론, 현대적으로는 더 깔끔하게 제시되죠. 

대그 프라위츠(Dag Prawitz)는 1965년 그의 학위논문 Natural Deduction: A Proof-Theoretical Study에서 겐첸-프라위츠 자연연역 방식으로 Hauptsaz에 대한 증명을 제시하는데 이것이 증명론에서 매우 중요하게 여겨지는 정형화 정리(Normalization theorem)입니다. 물론 이후에 폰 플라토(Von Plato)라는 철학자가 겐첸의 미출판 기록을 발견하면서 프라위츠 방식의 증명을 겐첸이 이미 알고 있었다는 것도 밝혀지고요. 그래서 보통 증명론이나 전산학 영역에서 '자연연역'하면 겐첸-프라위츠 자연연역을 말합니다. 

그럼 이쯤에서 위의 질문으로 돌아가 볼께요.

프레데릭 피치(Frederic Fitch)의 자연연역은 1952년 그의 저작 Symbolic logic에서 제시된 것으로 스타니스와프 야스코브스키(Stanisław Jaśkowski)의 체계를 소개한 것이라고 볼 수 있습니다. 피치가 창시한게 아니에요. 차이가 있다면 야스코브스키는 박스 형식으로 가정을 다뤘다면 피치는 조금 더 단순화 했고 더 현대적으로 제시했다는 거겠죠. 

참고. https://plato.stanford.edu/entries/natural-deduction/#GentJask

실제로 가정을 사용하는 몇 가지 테크닉을 제외하고는 겐첸-프라위츠 자연연역과 피치 자연연역이 서로 동치임을 어느 정도 예상할 수 있습니다. 웬만한 교수님들은 그냥 동치라고 말하실텐데 저는 가정의 사용과 관련해서 애매한 부분이 있어서 약간 조심할랍니다. 

결론부터 말해서 피치의 자연연역과 겐첸-프라위츠 자연연역은 학술 영역에서 광범위하게 사용됩니다. 개인 간의 선호의 차이도 있겠지만 피치 자연연역이 더 "직관적"이라는 말에는 동의하기가 어려운 것이 예를 들어, 피치 자연연역은 증명의 구조를 설명하는데 있어 '극대식'(maximum formula) 혹은 '절단식'(cut formula)을 표현하는데 어려움이 있다고 생각합니다. 표현을 못 하는 것은 아니지만 찾기가 어렵달까요? 특히 자연연역의 길이를 고려할 때, 각 가지의 길이를 귀납법의 형식으로 제시하는데 있어 각 가지가 분화되는 지점을 특정하기가 어려운 점이 있어서 피치 방식은 학부 교양 수업에서 학생들에게 가르치는 용도로만 사용하고 있습니다. 또한 대다수의 증명론과 전산학에 적용하는 영역에서는 겐첸-프라위츠 방식 이외에 정식열 연산이나 람다 연산과의 관계를 따져서 연구를 진행하는데요. 제가 익숙치 않아서 그런지는 모르겠지만 피치 방식은 각 체계 간의 번역을 제시하는데 있어서도 어려움이 많습니다. 

하지만 피치의 책이 출판되고 많은 학자들이 겐첸의 자연연역 만큼이나 피치 방식을 사용해 왔습니다. 최근에도 철학 영역에서는 피치 방식을 자주 사용하는 것 같고요. 하지만 증명론, 전산학 영역을 고려한다면 피치 방식은 잘 사용되지 않고 있고요. 그렇다고 피치 방식이 잘못된 것은 아닌 것이 겐첸-프라위츠 자연연역으로 서로 번역이 되는 것이 통상적인 입장입니다. 그래서 대~강 결론을 얘기해 보자면, 연구자 개개인의 선호가 아닌가 합니다.