증명 속 중간정리를 모두 걷어내도, 같은 결론에 도달할 수 있을까요?

원문은 왼쪽의 식들을 모두 전제로, 오른쪽의 식들 가운데 적어도 하나가 성립한다고 읽습니다. 따라서 A, B → C, D는 ‘A와 B이면 C 또는 D’입니다. 왼쪽이나 오른쪽, 심지어 양쪽이 비어 있어도 시퀀트입니다.

A, B →는 A와 B가 함께 모순을 이룬다는 표시이고, →는 빈 시퀀트입니다. 다케우치는 이 빈 시퀀트가 증명되지 않을 때 논리 체계를 무모순이라고 정의합니다.

아래 버튼은 같은 화살표의 좌우를 비워 원문의 세 가지 읽기를 비교합니다. 식을 없앴다고 곧바로 증명이 생기는 것은 아닙니다. 화면은 시퀀트의 문법과 읽는 법만 보여 줍니다.

추론 하나는 위쪽 시퀀트들에서 아래쪽 시퀀트 하나로 내려옵니다. 여러 추론을 유한하게 배열하되, 마지막 결론인 끝 시퀀트를 제외한 모든 시퀀트는 다른 추론의 윗부분이 되어야 합니다.

또한 아래로 내려가다 처음 자리로 돌아오는 원이 없어야 합니다. 원문은 이 조건을 ‘시퀀트들이 나무를 이룬다’고 설명합니다. 증명은 순환을 감춘 도식이 아니라, 시작 시퀀트에서 끝 시퀀트로 이어지는 유한한 나무입니다.

두 증명이 같은 식 C를 경계에서 공유한다고 합시다. 첫째는 Γ → Δ, C, 둘째는 C, Π → Λ입니다. 컷은 두 증명을 합쳐 Γ, Π → Δ, Λ를 얻습니다. C는 위쪽 두 전제에는 있지만 아래 결론에는 없습니다.

따라서 컷은 문장을 지우는 임의의 편집이 아닙니다. 왼쪽 증명이 C를 공급하고 오른쪽 증명이 C를 사용하는 정확한 두 경계를 맞춘 뒤, 그 중간식을 결론에서 숨기는 추론 규칙입니다.

컷은 이미 얻은 중간정리를 재사용하므로 증명을 짧고 모듈식으로 만듭니다. 그러나 결론에 보이지 않는 식 C가 증명 깊숙이 들어올 수 있어, 끝 시퀀트가 어떤 규칙과 식에 의존하는지 추적하기 어려워집니다.

컷 없는 증명이 존재한다는 정리는 같은 결론을 중간식 없이 다시 조직할 수 있음을 보장합니다. 겐첸은 LK에서 이 성질을 자연수 이론의 무모순성 증명에 활용했습니다. 다케우치가 묻는 것은 이 분석력이 높은 형의 언어에서도 유지되는가입니다.

보통의 개체 변수 x만이 아니라, 인수를 받는 변수와 함수 자체를 형에 따라 구분합니다. 예를 들어 형 (n₁,…,nᵢ)은 i개의 논항 자리를 가지며 각 자리에 요구되는 높이를 기록합니다. 원문은 자유·속박·특수 변수와 함수도 각각 나눕니다.

GLC는 이런 변수와 함수에 대한 보편·존재 양화 규칙을 LK에 더합니다. 다만 아무 식이나 넣는 것이 아니라, 요구된 형의 variety나 functional을 넣고 새 고유변수가 아래 시퀀트에 나타나지 않는다는 조건을 지켜야 합니다.

‘컷이 보이는 증명’을 선택하면 공통 중간식 C가 두 전제를 잇습니다. ‘컷 없는 목표’는 같은 끝 시퀀트를 C가 경계에 나타나지 않는 다른 전개로 얻고 싶다는 메타정리의 목표를 표시합니다.

버튼이 실제 컷 제거 알고리즘을 실행하는 것은 아닙니다. 특히 1953년 논문은 GLC 전체의 컷 제거를 증명하지 않았습니다. 이 실험은 규칙의 입력과 목표의 차이를 시각적으로 읽게 하는 장난감 모형입니다.

명제는 간결합니다. GLC에서 증명 가능한 모든 시퀀트는 컷 없이도 증명 가능하다는 것입니다. 다케우치는 더 작은 부분체계 G¹LC에 대해서조차 당시 답할 수 없다고 적고, 이 주장을 ‘fundamental conjecture’라고 명명합니다.

부록은 높이가 i 이하인 변수와 i+1 이하인 함수를 쓰는 부분체계를 GᶦLC라고 정의하고, G⁰LC = LK라고 둡니다. 익숙한 LK에서 출발해 높은 형으로 올라갈수록 같은 컷 제거 성질을 유지할 수 있는지가 질문의 뼈대입니다.

제2장은 세 묶음의 메타정리를 증명합니다. 제한 정리는 변수와 함수가 특정 조건을 만족하도록 번역했을 때 무모순성이 보존될 충분조건을 줍니다. 형 올리기 정리는 낮은 형의 표현을 높은 형으로 옮기는 조작을 다룹니다. 제9장은 이 도구들로 집합과 함수를 도입하는 여러 공리 체계의 무모순성 보존을 보입니다.

이 결과들은 근본 추측을 대신하지 않습니다. 오히려 GLC가 왜 필요한지를 보여 주는 작업입니다. 다케우치는 ‘개념을 더해도 무모순성이 보존된다’는 직관을 제한된 조건과 증명으로 분해합니다.

세 문장을 차례로 분류해 보세요. 첫 문장은 논문의 완성된 메타정리, 둘째는 근본 추측, 셋째는 그 추측이 참일 때 따라오는 조건부 귀결입니다.

오래된 논문을 현재의 정리와 섞어 읽으면, 저자가 어디까지 도달했는지가 사라집니다. 이 분류는 제5회의 가장 중요한 검수 장치입니다.

서론은 근본 추측이 GLC 또는 G¹LC에서 성립하면 실수 이론의 무모순성이 곧 따라온다고 말합니다. 제9장의 마지막 정리들은 자연수 이론과 실수 이론의 공리들을 GLC 안에서 다루는 조건부 연결을 마련합니다.

여기서 순서를 지켜야 합니다. 논문은 실수 이론의 무모순성을 무조건 증명하지 않았습니다. GLC의 컷 제거가 성립한다는 아직 풀리지 않은 전제가 먼저 필요합니다. 높은 형의 컷 제거가 중요했던 까닭이 바로 이 조건부 통로에 있습니다.

이 논문에는 다음 해 여덟 쪽짜리 정오표가 따로 실렸습니다. 단순 철자뿐 아니라 변수의 아래첨자, 식의 순서, ‘0’과 ‘1’, 정리 번호, 일부 문장 전체가 고쳐집니다. 예를 들어 p. 53의 한 조건은 N이 1인 경우에서 N이 0인 경우로 수정됩니다.

따라서 스캔 OCR만으로 수식을 옮기면 잘못된 기호가 겹쳐집니다. 이 글은 논문의 큰 주장과 컷 도식은 원본 이미지로 확인했고, 세부 기호를 인용할 때 정오표의 해당 쪽·행을 함께 대조했습니다.

다케우치는 1955년부터 ‘On the Fundamental Conjecture of GLC’ 연작에서 부분체계의 컷 제거를 계속 밀고 나갔습니다. 제2편은 모든 증명 가능한 시퀀트에 컷 없는 증명이 있다는 명제를 다시 정확히 쓰고, 실수 이론의 무모순성과의 연결을 설명합니다.

둘째 계층 논리의 경우 테이트가 1966년에 비구성적 증명을 제시했고, 다카하시와 프라비츠도 1960년대 후반 높은 차수 논리의 컷 제거를 증명했습니다. 이 후대 결과를 1953년 논문에 소급해 넣지는 않습니다. 제6회는 이 가운데 별도의 핵심 후속 논문 한 편을 골라, 어떤 새 방법이 추측을 실제 정리로 바꾸었는지 읽습니다.