증명은 결론에 들어 있는 개념만으로
다시 쓸 수 있을까요?

겐첸은 프레게·러셀·힐베르트 계열의 형식화가 기술적으로 강력하지만 실제 수학자가 쓰는 추론의 모습과 거리가 있다고 보았습니다. 소수의 공리에서 긴 식을 끌어내는 체계에서는 “어떤 가정을 세웠고, 언제 그 가정에서 벗어났는가”가 표면에 잘 드러나지 않습니다.

그의 첫 목표는 실제 추론에 가능한 한 가까운 계산을 세우는 일이었습니다. 여기서 자연연역 NJ와 NK가 나옵니다. 다음 목표는 증명 전체를 분석해 우회적인 중간 개념을 걷어낼 수 있는 계산을 만드는 일이었습니다. 이를 위해 시퀀트 계산 LJ와 LK가 등장합니다.

수학자는 대개 “A라고 가정하자”로 시작해 그 가정 아래에서 B를 얻은 뒤 “따라서 A이면 B이다”라고 정리합니다. 자연연역은 이 흐름을 그대로 규칙으로 만듭니다. 증명은 위에서 아래로 뻗는 나무이고, 맨 위에는 가정, 맨 아래에는 최종 결론이 놓입니다.

한 번 얻은 식을 여러 번 쓰는 실제 필기와 달리 나무에서는 각 사용을 가지로 따로 표시합니다. 겐첸은 이 차이가 편리한 형식화를 위한 선택이라고 설명합니다. 자연연역이 일상 필기를 사진처럼 복제한다는 뜻은 아닙니다.

A를 가정한 채 B를 얻었다면, 함의 도입 규칙은 그 가지의 가정 A에 대한 의존을 해제하고 A→B를 결론으로 만듭니다. 결론은 이제 그 임시 가정에 기대지 않습니다. 증명마다 어떤 식이 어느 가정에 의존하는지 기록해야 하는 이유입니다.

존재양화사와 전칭양화사의 규칙에는 고유변수 조건이 붙습니다. ‘아무 대상이나’ 택한 변수가 특정 가정에 숨어 있으면 전체 대상에 대한 결론으로 일반화할 수 없습니다. 형식은 자연스러운 말 속에 생략되기 쉬운 조건을 보이게 합니다.

각 논리 기호에는 그 기호를 결론에 만드는 도입 규칙과, 그 기호가 붙은 식에서 정보를 꺼내는 제거 규칙이 있습니다. 예를 들어 A와 B에서 A∧B를 만드는 것이 ∧-도입이고, A∧B에서 A를 꺼내는 것이 ∧-제거입니다. 함의도입은 A라는 가정에서 B를 얻은 가지를 A→B로 묶고, 함의제거는 A와 A→B에서 B를 얻습니다.

도입 직후 같은 기호를 제거하면 방금 포장한 내용을 곧바로 다시 풉니다. 겐첸은 제거 규칙이 도입 규칙이 부여한 의미를 따라야 한다는 생각을 제시했습니다. 이 대칭은 이후 증명 정규화와 증명론적 의미론의 출발점이 됩니다.

시퀀트 Γ ⊢ Δ는 왼쪽 문맥 Γ의 모든 전제가 성립할 때 오른쪽 문맥 Δ 가운데 적어도 하나가 성립한다는 형태를 나타냅니다. Γ와 Δ는 식 한 개가 아니라 식들의 유한한 목록입니다. 빈 쪽도 허용됩니다.

시퀀트는 진리표 한 줄이 아닙니다. 어떤 전제가 사용 가능한지, 어떤 결론 후보가 놓였는지, 규칙이 어느 쪽의 어떤 기호를 다루는지를 기록하는 증명 단위입니다. 원문의 화살표를 이 글에서는 현대적으로 널리 쓰이는 ⊢로 표시합니다.

그렇습니다. A가 왼쪽에 있으면 사용할 수 있는 전제이고, 오른쪽에 있으면 얻으려는 결론입니다. 같은 식도 자리에 따라 규칙의 역할이 달라집니다. A∧B를 왼쪽에서 쓰면 A와 B를 각각 이용할 수 있고, 오른쪽에서 만들려면 A와 B를 모두 증명해야 합니다.

이 좌우 구분 덕분에 논리 기호의 규칙을 대칭적으로 배열할 수 있습니다. 증명을 아래 결론에서 위 전제로 거꾸로 탐색할 때도 “왼쪽 규칙을 적용할지, 오른쪽 규칙을 적용할지”를 명확히 선택할 수 있습니다.

LJ는 직관주의 술어논리, LK는 고전 술어논리를 위한 시퀀트 계산입니다. 겐첸의 형식에서 LJ의 오른쪽 문맥에는 식이 최대 하나만 놓입니다. LK는 오른쪽에 여러 식을 허용합니다. 이 구조적 차이가 고전논리와 직관주의 논리의 차이를 드러냅니다.

자연연역에서는 배중률을 기본식으로 더해 NK를 만들었지만, 시퀀트 계산에서는 오른쪽 문맥의 허용 범위가 차이를 나타냅니다. 같은 논리 차이가 계산에 따라 서로 다른 위치에서 보인다는 점이 중요합니다.

A를 “신청서가 있다”, B를 “사진이 있다”, C를 “추천서가 있다”라고 합시다. A∧B에서 A∨C를 얻으려 합니다. 신청서와 사진이 있으면, 신청서 또는 추천서가 있다는 결론이 따라옵니다.

먼저 A∧B에서 A를 얻는 증명과, A에서 A∨C를 얻는 증명을 따로 만듭니다. 두 증명을 중간식 A로 잇는 것이 이 예의 컷입니다. 컷을 없앤 쪽은 A∧B에서 A를 얻은 증명에 바로 ∨의 오른쪽 규칙을 적용합니다. 두 경우의 마지막 시퀀트는 같습니다.

아래의 ⊢는 왼쪽 전제에서 오른쪽 결론을 도출한다는 표시입니다. ∧L은 왼쪽의 연언을 쓰는 규칙, ∨R은 오른쪽의 선언을 만드는 규칙입니다. W는 사용하지 않는 전제를 더하는 약화입니다. 여기서는 겐첸의 LJ·LK에서 허용되는 규칙을 사용합니다.

LJ나 LK에서 어떤 끝시퀀트를 증명할 수 있다면, 같은 끝시퀀트를 컷 없이 증명할 수 있다는 정리입니다. 원문의 표현대로 모든 순수 논리적 증명은 일정한 정상형으로 환원될 수 있습니다. 정상형은 하나로 유일할 필요가 없습니다.

증명은 보통 짧아지기만 하지 않습니다. 컷으로 공유하던 보조정리를 펼치면 증명 나무가 커질 수 있습니다. 정리가 보장하는 핵심은 길이 절약이 아니라 분석 가능한 형식의 존재입니다.

컷 없는 LJ·LK의 논리 규칙에서 위쪽의 곁식은 아래쪽 주식의 부분식입니다. 증명 나무를 끝시퀀트에서 위로 따라가면 새롭고 더 복잡한 식이 임의로 끼어들 통로가 없습니다. 따라서 증명에 나타나는 모든 식은 끝시퀀트에 나타난 식의 부분식입니다.

이를 부분식 성질이라고 부릅니다. ‘개념’은 여기서 일상적인 생각 주제가 아니라 형식 안의 식과 그 구성 부분을 뜻합니다. 술어논리에서는 항 치환과 고유변수 조건까지 함께 살펴야 하므로 단순한 문자열 포함 검사로 끝나지 않습니다.

명제논리의 끝시퀀트가 주어지면 그 안의 부분식은 유한합니다. 겐첸은 같은 식의 중복 횟수를 제한한 ‘축약된 시퀀트’를 사용해 후보 시퀀트의 수도 유한하게 만듭니다. 기본 시퀀트에서 시작해 허용된 규칙으로 얻을 수 있는 후보를 차례로 표시하면, 목표에 도달하거나 더 이상 새 후보가 생기지 않는 순간이 옵니다.

그래서 고전 및 직관주의 명제논리에 대한 결정 절차가 원리적으로 생깁니다. 이는 효율적인 현대 증명기를 곧바로 제공한다는 뜻이 아닙니다. 유한성과 실용적 계산량은 서로 다른 질문입니다.

빈 시퀀트는 왼쪽에도 오른쪽에도 아무 식이 없는 형태입니다. 원문의 LJ·LK 규칙을 살펴보면 컷을 제외하고는 빈 시퀀트를 아래 결론으로 만드는 규칙이 없습니다. 주정리가 모든 증명을 컷 없는 증명으로 바꿀 수 있다고 말하므로, 빈 시퀀트의 증명이 있을 수 없습니다.

이 결과는 고전·직관주의 술어논리 계산 자체의 일관성에 관한 것입니다. 산술 전체의 일관성과 곧바로 같지 않습니다. 겐첸은 같은 논문의 제IV절에서 완전귀납법을 뺀 고전 산술에 별도의 응용을 제시합니다.

그렇게 넓게 말하면 지나칩니다. 부분식 성질은 특정 계산의 컷 없는 형식에서 등장하는 식의 종류를 제한합니다. 증명 나무의 선택, 가지의 수, 규칙 적용 순서, 항과 변수의 배치는 결론 문자열만 보아서는 알 수 없는 정보를 담습니다.

또한 보조정리는 수학적 이해와 공동 작업에서 매우 유용합니다. 컷 제거 가능성은 보조정리를 쓰지 말라는 조언이 아닙니다. 완성된 증명을 분석할 때 보조정리를 펼친 형식이 존재하고, 그 형식에서 어떤 구성 요소가 필수였는지 조사할 수 있다는 말입니다.

고전 및 직관주의 술어논리의 LJ·LK 증명은 같은 끝시퀀트를 가진 컷 없는 증명으로 바꿀 수 있습니다. 그 증명에 나타나는 식은 끝시퀀트 식들의 부분식으로 제한됩니다. 이 정확한 의미에서 증명은 결론에 들어 있는 개념만으로 다시 쓸 수 있습니다.

겐첸의 전환은 증명을 참을 운반하는 검은 상자에서 조사 가능한 수학적 대상으로 바꾸었습니다. 이후 연구는 정상형이 계산과 어떤 관계를 맺는지, 증명에서 수치·알고리즘 같은 정보를 어떻게 뽑는지 묻게 됩니다. 제12회는 겐첸의 1936년 산술 무모순성 연구를 읽습니다. 증명 변환이 끝난다는 사실을 순서수의 감소로 설명하는 과정을 살펴봅니다.