중간 정리 없이도
같은 결론을 증명할 수 있을까?

증명의 언어

전제·결론·추론 규칙의 자리를 정의합니다.

5. 시퀀트 계산법의 가장 작은 출발점

우선 'p를 전제로 갖고 있으면 p를 결론으로 쓸 수 있다'는 데서 시작합시다. 다음 표기는 더 앞선 전제를 필요로 하지 않는 기본 시퀀트입니다.

p ⇒ p

이를 항등 공리 또는 초기 시퀀트라고 부릅니다. '공리'라는 말이 현실에 관한 새로운 사실을 선포한다는 뜻은 아닙니다. 증명 나무에서 더 위의 추론 없이 사용할 수 있는 형식적인 시작 규칙이라는 뜻입니다. 같은 방식으로 r⇒r도 시작할 수 있습니다.

이어 왼쪽에 추가 전제를 넣는 약화 규칙을 생각합니다. p⇒p에서 p,q⇒p를 얻을 수 있습니다. p라는 결론을 이미 얻은 상황에서 q라는 전제가 함께 주어졌다고 해서 p를 잃는 것은 아닙니다. 반대로 p,q⇒p에서 q를 마음대로 삭제해도 된다고 주장하는 것은 다른 규칙을 요구합니다. 전제를 넣는 일과 빼는 일은 구별해야 합니다.

수축 규칙은 동일한 전제 두 개를 하나로 합칩니다. p,p,Γ⇒C에서 p,Γ⇒C로 이동할 수 있습니다. 교환 규칙은 전제의 순서를 바꿉니다. 고전과 직관주의의 표준 시퀀트 계산법에서는 이 구조 규칙들이 허용되며, 각 규칙이 정확히 어떤 자리에 작용하는지 표시해야 증명 변환을 검산할 수 있습니다.

6. 논리 기호를 사용하는 규칙: 왼쪽과 오른쪽

'그리고'를 뜻하는 ∧를 오른쪽 결론에 새로 도입하려면 A도 얻고 B도 얻어야 합니다. Γ⇒A와 Γ⇒B라는 두 증명이 있으면 Γ⇒A∧B를 얻습니다. 이것을 오른쪽 ∧ 규칙이라고 부릅니다. Γ는 이미 확보한 전제들을 나타냅니다.

'그리고'가 왼쪽 전제로 있다면 상황이 다릅니다. Γ,A,B⇒C의 증명이 있으면 Γ,A∧B⇒C로 묶을 수 있습니다. A∧B라는 한 전제를 받으면 A와 B를 모두 사용할 수 있기 때문입니다. 이것은 왼쪽 ∧ 규칙입니다. 같은 논리 기호가 어느 쪽에 놓이는지에 따라 증명 규칙이 달라지는 셈입니다.

'이면'을 뜻하는 →의 왼쪽 규칙은 한 단계 더 풍부합니다. Γ⇒A와 Δ,B⇒C라는 두 증명이 있으면 Γ,Δ,A→B⇒C를 얻습니다. 먼저 Γ에서 A를 확보하고, A→B를 통해 B를 사용할 수 있으며, 마지막으로 Δ와 B에서 C를 얻습니다. 우리 사례에서 A는 p, B와 C는 r입니다. 따라서 p⇒p와 r⇒r을 이용하면 p,p→r⇒r을 만들 수 있습니다.

이처럼 규칙은 논리식의 뜻에 맞춰 왼쪽과 오른쪽을 연결합니다. 그래서 시퀀트 계산법의 각 단계는 어떤 결론을 사용했고 어떤 전제를 추가했는지 추적할 수 있는 장점을 지닙니다.

7. 컷은 왜 편리한 규칙인가요?

수업 시간에는 '이제 보조정리 A를 얻었다. 다음 증명에서 A를 사용하자'라는 연결이 자연스럽습니다. 시퀀트 계산법에서는 다음 규칙이 바로 그 역할을 합니다.

Γ ⇒ A 그리고 A, Δ ⇒ C 이면 Γ, Δ ⇒ C

이것이 컷(Cut, 중간 논리식을 통한 두 증명의 연결) 규칙입니다. 앞 증명에서 A를 결론으로 얻고, 뒤 증명에서 A를 전제로 사용하여 C를 얻었다면, 양쪽의 다른 전제 Γ와 Δ만으로 C를 얻는 큰 증명을 만듭니다. 중간 논리식 A는 큰 증명의 마지막 시퀀트에서 보이지 않습니다.

A가 단순한 p일 수도 있고, 수십 개의 기호가 들어간 복합 논리식일 수도 있습니다. 연구자가 다른 사람이 증명한 정리 A를 빌려서 새로운 결론을 얻는 방식과 닮았습니다. 컷이 허용되면 증명은 짧고 읽기 쉬워질 수 있습니다. 그러므로 컷 제거 정리는 보조정리를 쓰는 수학적 글쓰기 자체가 잘못되었다는 선언이 아닙니다. 그러한 보조정리를 거치는 증명도 일정한 규칙으로 직접적인 증명으로 재구성할 수 있다는 정리입니다.

한 증명의 두 가지 경로

컷을 사용한 도출과 컷을 없앤 도출을 실제로 비교합니다.

8. 실제로 컷을 한 번 써 봅시다

아까의 목표를 다시 적습니다. p∧q, p→r ⇒ r. 첫 증명은 p∧q⇒p입니다. 항등 공리 p⇒p에서 시작해 q를 전제로 추가하면 p,q⇒p가 되고, 왼쪽 ∧ 규칙을 적용하면 p∧q⇒p를 얻습니다.

두 번째 증명은 p,p→r⇒r입니다. p⇒p와 r⇒r이라는 두 초기 시퀀트를 '이면'의 왼쪽 규칙으로 결합하면 됩니다. 이 계산을 할 때 어떤 전제도 몰래 추가하거나 제거하지 않았습니다.

이제 중간 결론 p를 서로 연결해 보겠습니다. 앞 증명은 Γ=p∧q에서 A=p를 얻었습니다. 뒤 증명은 A=p와 Δ=p→r에서 C=r을 얻었습니다. 컷을 적용하면 p∧q, p→r⇒r이 나옵니다. 목표와 같습니다. 논리적으로 올바르고, 중간 논리식 p를 두 증명의 접합점으로 사용한 증명입니다.

그런데 목표 시퀀트에 필요한 것은 p∧q와 p→r에서 r을 얻는 사실이지, 반드시 p를 별도의 중간 결론으로 한 차례 적는 일이 아닙니다. 여기에서 컷을 제거할 방법을 찾아볼 수 있습니다.

9. 같은 결론을 컷 없이 만들어 봅시다

이번에는 p를 중간 결론으로 받는 컷 규칙을 쓰지 않겠습니다. 다음 순서는 순수한 시퀀트 규칙만 이용합니다. ① p⇒p와 r⇒r에서 시작합니다. ② 왼쪽 → 규칙으로 p,p→r⇒r을 만듭니다. ③ q를 왼쪽에 추가하여 p,q,p→r⇒r을 얻습니다. ④ 왼쪽 ∧ 규칙을 적용하여 p∧q,p→r⇒r을 얻습니다.

두 증명의 최종 시퀀트는 정확히 같습니다. 처음에는 p∧q⇒p와 p,p→r⇒r을 컷으로 연결했습니다. 새 증명은 p∧q에 들어 있는 p와 q를 전제 사용 자리에서 직접 처리했습니다. 중간에 p를 결론으로 한 번 완성했다가 다른 증명에 넘기는 일이 사라졌습니다.

이 예에서 컷을 지운 뒤 추론 단계가 눈에 띄게 짧아 보일 수도 있습니다. 그러나 정리의 일반적인 결론은 컷을 쓰지 않는 증명의 존재와 구성 가능성입니다. 컷이 사라진 결과가 언제나 더 짧고 더 읽기 쉬운 것은 아닙니다. 복잡한 증명을 펼치면서 여러 단계가 반복되면 결과가 훨씬 길어질 수도 있습니다.

여기서 잠깐 검산해 보겠습니다. 첫 방식의 컷 규칙에는 두 증명이 정확히 p로 이어져야 합니다. 'p∧q⇒p'와 'q,p→r⇒r'을 아무 이유 없이 연결하면 컷 전제의 자리가 맞지 않습니다. 두 번째 방식의 마지막 ∧ 규칙을 적용할 때도 p,q가 모두 왼쪽 전제로 놓여 있어야 합니다. 필요한 자리가 맞는지 살펴보면 변환의 정확성을 눈으로도 확인할 수 있습니다.

10. 전제가 실제로 참일 때도 확인할 수 있습니다

형식 규칙으로 만든 증명이 참을 보존하는지는 간단한 진리표로 따로 검사할 수 있습니다. p, q, r이 모두 참·거짓 중 하나를 갖는 여덟 배정에서 p∧q와 p→r이 모두 참인 경우를 골라 보겠습니다. p∧q가 참인 배정은 p=참, q=참인 두 경우뿐입니다. 두 경우에서 r=거짓이면 p→r이 거짓이므로 전제가 모두 참인 상황에 해당하지 않습니다. 결국 전제가 모두 참인 경우는 p=q=r=참인 배정 하나이고, 이때 결론 r도 참입니다.

(p∧q) ∧ (p→r) → r

이 명제논리식은 여덟 배정 모두에서 참입니다. 앞에서 만든 두 증명 방식이 모두 같은 타당한 결론을 나타낸다는 추가 확인입니다. 그렇다고 이 여덟 줄의 진리표가 겐첸의 일반 정리를 증명하는 것은 아닙니다. 겐첸의 정리는 p·q·r 세 기호로 쓰인 한 사례를 넘어 임의로 긴 1차 논리 증명에 적용되어야 합니다.

정확히 말하면 규칙에 따라 구성된 모든 유한한 증명을 대상으로 컷을 없애는 변환을 보여야 합니다. 개별 진리배정 계산만으로는 그 변환이 언제나 끝나는지 알 수 없습니다. 따라서 진리표는 사례 검산으로, 다음 절의 구조 분석은 일반 정리의 이유로 역할을 나누어 읽어야 합니다.

복합 논리식의 컷

큰 식을 작은 식으로 바꾸고 규칙 사이를 이동합니다.

11. 컷이 있으면 어디에 낯선 논리식이 등장하나요?

보통의 오른쪽·왼쪽 논리 규칙을 적용하면 위쪽에 있던 논리식은 아래쪽의 논리식 안에 그대로 남거나 그 부분으로 나타납니다. 예를 들어 p,q⇒p에서 p∧q⇒p로 가면 위의 p와 q는 아래의 p∧q를 이루는 부분입니다. 논리식 'p'와 'q'는 아래의 'p∧q'보다 구성 요소 수가 적습니다.

그런데 컷은 상황이 다릅니다. Γ⇒A와 A,Δ⇒C에서 Γ,Δ⇒C로 이동하면 중간 논리식 A가 마지막 줄에서 완전히 사라집니다. A가 마지막 결론과 전제들 어디에도 없는 새로운 기호를 포함할 수도 있습니다. 예를 들어 원래 목표에는 p와 r만 있는데, 증명 도중 별도의 복잡한 식 A를 보조정리로 끌어올 수도 있습니다.

겐첸의 성과는 마지막 목표에 없는 논리식이 증명 중간에 쓰여야만 하는 것은 아니다라는 사실을 증명한 데 있습니다. 컷이 없는 증명에서는 각 단계의 논리식이 끝에 적힌 식들의 부분식과 이어집니다. 다만 양화사가 있을 때는 변수에 구체적인 항을 넣는 치환이 끼어들기 때문에, 부분식이라는 말을 문자 그대로의 글자 조각이라고만 이해하면 곤란합니다. 논리식의 구성 관계와 적절한 치환을 함께 고려해야 합니다.

12. 컷의 양쪽에서 같은 논리 기호를 다룰 때

앞의 사례에서 컷에 들어간 A가 단순한 p였습니다. 이제 A가 A₁∧A₂ 같은 복합 논리식이라고 생각해 봅시다. 왼쪽 증명에서는 A₁도 얻고 A₂도 얻어서 결론 A₁∧A₂를 만들었고, 오른쪽 증명에서는 A₁∧A₂를 전제로 받아 두 구성 요소를 사용했다고 하겠습니다.

이때 큰 논리식 A₁∧A₂를 통째로 연결하는 컷 하나를, 구성 요소 A₁과 A₂를 각각 연결하는 더 작은 컷으로 바꿀 수 있습니다. 원래 컷 논리식은 연결 기호 ∧가 하나 더 붙은 A₁∧A₂였지만, 새로 사용하는 논리식 A₁과 A₂는 모두 그 안의 부분식입니다. '증명하려는 중간 식의 복잡성'이 감소하는 변환입니다.

이 변환이 왜 가능한지도 살펴봅시다. A₁∧A₂를 오른쪽 결론으로 만들었다는 것은 이미 A₁의 증명과 A₂의 증명을 갖고 있다는 뜻입니다. 반대로 A₁∧A₂를 왼쪽 전제로 사용했다는 것은 A₁과 A₂를 각각 사용할 수 있다는 뜻입니다. 그러므로 두 증명 사이에서 A₁∧A₂ 한 덩어리를 전달할 필요가 없습니다. 각 구성 요소에 대한 증명과 사용 위치를 직접 연결할 수 있습니다.

이 설명은 양쪽 끝에서 컷 논리식이 바로 마지막 규칙에 의해 만들어지거나 분해된 경우의 전형적인 변환입니다. 증명 안의 모든 컷이 처음부터 이런 모양으로 놓이지는 않습니다. 중간에 약화나 교환, 수축이 있고, 컷 논리식과 무관한 규칙이 마지막에 놓일 수도 있습니다. 그런 경우에는 컷을 추론 나무의 위쪽으로 옮기는 별도의 재배열이 필요합니다.

13. 컷을 다른 규칙 위로 옮기는 이유

두 증명 중 어느 한쪽의 마지막 규칙이 컷 논리식 A를 직접 다루지 않는다면, 그 규칙보다 앞선 자리로 컷을 옮겨 볼 수 있습니다. 이를 '컷의 순열적 변환'이라고 부를 수 있습니다. 컷이 특정 규칙과 만나는 순서를 바꾸면서 컷 위에 놓인 증명의 높이를 줄여 나가는 것입니다.

예를 들어 오른쪽 증명의 마지막 규칙이 전제 q를 하나 더 넣는 약화 규칙이라면, 처음부터 그 약화 규칙을 컷 뒤에 적용하도록 순서를 조정할 수 있습니다. 컷에서 정말 필요한 증명의 부분을 먼저 연결한 뒤, 결과에 q를 다시 넣으면 됩니다. 컷 논리식의 복잡성은 그대로라도 그 컷이 만나는 증명의 한쪽 높이가 낮아집니다.

그러나 수축 규칙을 만나면 문제가 복잡해집니다. 하나의 전제로 합쳐진 A가 그 직전 단계에서는 두 번 등장했다면, 컷을 위쪽으로 올릴 때 서로 다른 두 사용 자리를 각각 처리해야 할 수 있습니다. 따라서 컷이 하나였던 증명에서 새로운 컷이 여러 개 생길 수도 있습니다. '컷을 위로 한 칸 올리면 무조건 컷 개수가 하나씩 줄어든다'는 설명은 옳지 않습니다.

겐첸의 증명은 바로 이 어려움을 포함해 변환이 결국 마무리됨을 보여 줍니다. 단순히 단계 수만 줄어든다고 주장하면 수축이 가져오는 반복을 설명할 수 없습니다. 컷 논리식의 구조와 관련 증명들의 높이를 함께 따지는 이유가 여기에 있습니다.

양화사와 종료

변수의 조건과 증명 변환이 끝나는 이유를 설명합니다.

14. 양화사가 등장하면 변수 조건까지 확인합니다

1차 논리에서는 p와 q 같은 명제 기호뿐 아니라 모든 대상과 어떤 대상에 대해 이야기하는 ∀, ∃도 사용합니다. 예를 들어 P(x)를 'x가 등록했다'라고 정하면 ∀xP(x)는 '모든 대상이 등록했다'는 뜻입니다. 여기에서 P(c)는 이름이 c인 특정 대상이 등록했다는 뜻입니다.

모든 대상이 등록했다는 전제가 있다면 특정 대상 c도 등록했다는 결론을 얻습니다. 시퀀트로는 ∀xP(x) ⇒ P(c)입니다. 이 증명도 컷이 없어도 만들 수 있습니다. P(c)⇒P(c)라는 초기 시퀀트에서 시작하고, 왼쪽의 P(c)를 ∀xP(x)로 바꾸는 왼쪽 전칭 규칙을 적용하면 됩니다.

양화사 규칙 중에는 임의의 대상을 대표하는 새 변수에 관한 제한이 있습니다. 예를 들어 Γ⇒P(a)를 근거로 Γ⇒∀xP(x)를 도출하려면 a가 아직 Γ에 특별한 대상처럼 등장하지 않아야 합니다. 그렇지 않으면 '한 명에게 성립한다'는 사실을 '모든 사람에게 성립한다'로 잘못 넓힐 수 있습니다. 이를 고유변수 조건이라고 부릅니다.

컷을 옮기거나 없애는 과정에서는 서로 다른 증명에 우연히 같은 이름의 변수가 등장할 수 있습니다. 이런 경우 증명 규칙에 맞는 새 이름으로 변수를 바꾸어야 합니다. 겐첸의 정리가 1차 논리 전체에 적용된다고 할 때는 이와 같은 변수 치환과 고유변수 조건의 보존도 함께 포함됩니다. 명제논리의 작은 예제만 검사하고 일반적인 양화사 증명까지 검증했다고 말할 수 없는 이유입니다.

15. 어떤 기준으로 '반드시 끝난다'를 증명할까요?

변환 절차를 반복하는 동안 무엇이 감소하는지 살펴야 합니다. 한 가지 기준은 컷 논리식의 복잡성, 곧 컷 등급입니다. 원자식 p보다 p∧q가 복잡하고, p∧(q→r)은 더 복잡합니다. A₁∧A₂가 주된 논리식으로 등장하는 양쪽 규칙을 만났을 때 더 작은 부분식으로 컷을 바꾸면 이 등급이 감소합니다.

다른 기준은 해당 컷을 둘러싼 증명들의 높이입니다. 컷이 논리식 A와 관계없는 규칙을 지날 때는 컷 등급이 그대로일 수 있지만, 대상이 되는 증명 부분의 높이를 감소시키는 변환을 사용할 수 있습니다. 이런 기준을 조합하여 더 이상 무한히 내려갈 수 없는 순서를 만들고, 그 순서에 대한 귀납법으로 변환의 종료를 증명합니다.

수축으로 인해 하나의 컷이 여러 개의 컷으로 바뀌는 상황도 다룹니다. 새로 생긴 컷들의 논리식 등급과 그것들을 만드는 증명의 높이를 각각 관리해야 합니다. 중요한 것은 변환 과정의 어떤 숫자 하나가 매번 1씩 줄어드는 단순한 알고리즘이라는 뜻이 아닙니다. 전체 증명의 복잡성을 잘 조직하여 모든 유한한 증명에서 컷을 제거하는 유한한 변환이 존재한다는 것을 수학적으로 확립하는 일입니다.

이 절은 실제 원증명의 모든 분기와 규칙을 재현한 형식 증명이 아니라 표준적인 증명 전략의 설명입니다. 정확한 규칙별 변환, 귀납 가정의 적용 순서, 수축과 양화사 처리는 전문적인 증명론 교재와 겐첸의 연구에서 자세히 다루어집니다.

주요 정리의 결론

컷 제거·부분식 성질을 정리하고 결정 문제와 구별합니다.

16. 주요 정리: 컷을 포함한 증명은 어떻게 바뀌나요?

이제 정리의 핵심을 정확히 적을 수 있습니다. 고전 1차 논리의 표준 시퀀트 계산법 LK와 직관주의 1차 논리의 표준 시퀀트 계산법 LJ에서 어떤 시퀀트가 증명 가능하다면, 그 시퀀트는 컷 규칙을 한 번도 사용하지 않고도 증명 가능합니다. 이를 컷 제거 정리, 또는 겐첸의 주요 정리라고 부릅니다. 기호의 의미와 전제·결론을 바꾸지 않은 채 증명 기록을 변환하는 정리입니다.

Γ ⇒ Δ를 컷을 사용하여 증명할 수 있다면, 같은 Γ ⇒ Δ를 컷 없이 증명할 수 있다.

여기서 Δ가 여러 논리식의 열일 때는 고전 체계 LK를 뜻합니다. LJ를 사용할 때는 Δ 자리에 하나의 결론을 놓습니다. 두 체계의 구별은 단순한 표기 취향이 아닙니다. 직관주의 논리는 배중률과 이중 부정 제거를 고전 논리와 동일한 일반 규칙으로 받아들이지 않으므로, 증명 가능한 시퀀트의 범위도 다릅니다. 컷 제거 정리는 각 체계에서 이미 증명되는 시퀀트를 같은 체계 안에서 컷 없이 다시 증명할 수 있다는 주장입니다.

컷 규칙 한 줄만 삭제하는 작업을 떠올리기 쉽지만, 실제 변환은 충분히 길 수 있습니다. 처음 증명에서는 독립적인 보조정리를 한 번 증명한 뒤 여러 곳에서 이용했더라도, 컷을 제거하면 해당 보조정리의 내용을 쓰는 위치마다 앞서 했던 추론이 펼쳐질 수 있습니다. 정리의 목표는 언제나 증명의 길이 최소화가 아니라 컷 없는 증명으로 변환할 수 있다는 사실입니다.

17. 마지막 결론에서 등장한 부분식이 중요한 이유

컷 없는 증명을 만들고 나면 매우 유용한 성질이 드러납니다. 순수 논리의 표준적인 규칙에서는 증명의 각 단계에 등장하는 식들이 마지막 시퀀트의 논리식에서 출발한 부분식과 이어집니다. 이를 부분식 성질이라고 합니다. 예를 들어 목표가 p∧q⇒p일 때 컷 없는 증명의 핵심에는 p, q, p∧q 같은 식이 나타납니다. 목표에 전혀 없던 복잡한 새 명제 s→(t∧u)를 증명 중간에 세워야 할 필요가 없습니다.

이 성질이 도움이 되는 이유를 구체적으로 살펴봅시다. 증명 검색 프로그램이 목표의 기호 구조를 분석할 때 가능한 다음 단계를 제한할 수 있습니다. p∧q가 전제라면 그 구성 부분 p와 q를 살펴보고, 결론이 p∨r이라면 양쪽 선택지 중 어떤 식을 증명할지 따질 수 있습니다. 어디에서 등장했는지 알 수 없는 임의의 보조정리를 무한정 발명하는 수고가 줄어듭니다.

다만 '부분식만 조사하면 모든 1차 논리 문제를 언제나 결정할 수 있다'고 결론 내리면 오류입니다. 양화사 규칙은 항을 반복하여 집어넣을 수 있고, 컷 없는 증명 찾기 과정이 모든 입력에서 끝난다는 보장은 없습니다. 제15회에서 살펴본 처치의 결정불가능성 정리와 컷 제거 정리는 서로 충돌하지 않습니다. 하나는 모든 입력을 판정하는 알고리즘의 존재를, 다른 하나는 이미 존재하는 증명을 컷 없이 바꿀 수 있는지를 묻기 때문입니다.

무모순성과 실제 의미

순수 논리·산술의 무모순성을 구별하고 연구 의의를 정리합니다.

18. 순수 논리의 무모순성과 산술의 무모순성을 구별합니다

컷 제거 정리에는 순수 논리의 무모순성에 관한 중요한 귀결이 있습니다. 고전 LK에서 왼쪽도 비어 있고 오른쪽도 비어 있는 시퀀트 ⇒를 생각해 봅시다. 전제 없이 어떤 결론도 없다는 뜻이며, 순수 논리 안에서 모순이 생기면 이런 빈 시퀀트의 증명을 문제 삼을 수 있습니다.

만약 빈 시퀀트에 증명이 있다면, 컷 제거 정리에 따라 컷 없는 증명도 있어야 합니다. 부분식 성질을 적용하면 그 증명 안에서 사용할 수 있는 논리식은 빈 시퀀트의 부분식뿐입니다. 그러나 마지막에 아무 논리식도 없으므로 그 위의 증명에 등장할 논리식도 없습니다. 동시에 증명 나무는 A⇒A 같은 초기 시퀀트에서 시작해야 하며, 그 초기 시퀀트에는 반드시 논리식 A가 있습니다. 따라서 그런 증명 나무는 존재할 수 없습니다. 이것이 순수 논리의 무모순성을 설명하는 한 방법입니다.

하지만 여기서 '모든 수학 이론의 무모순성이 증명되었다'고 말하면 범위를 넘게 됩니다. 페아노 산술이나 집합론은 순수 논리 규칙 외에 수학적 대상을 다루는 별도의 공리를 가지고 있습니다. 이 공리를 넣으면 컷 제거 변환이 그대로 적용되지 않거나, 공리의 형태에 맞는 제한된 컷 제거만 가능할 수 있습니다. 순수 논리에서의 컷 제거와 임의의 강한 수학 이론의 무모순성 증명을 같은 문제로 취급해서는 안 됩니다.

19. 1936년 겐첸의 무모순성 증명과는 어떻게 연결될까요?

제10회에서 다룬 힐베르트의 무모순성 계획은 수학적 증명 체계 안에서 모순을 도출할 수 없다는 사실을 신뢰할 만한 방법으로 확립하려 했습니다. 겐첸은 1936년에 페아노 산술의 무모순성 증명을 발표하여 이 연구에 새로운 방향을 제시했습니다. 그 논증은 순수 논리의 컷 제거만 반복한 결과가 아니었습니다. 증명에 복잡성을 나타내는 순서수 표기를 연결하고, 엡실론 제로(ε₀)까지의 초한귀납을 이용하는 방법이 핵심입니다.

ε₀은 보통 자연수에 대한 귀납법을 단순히 길게 반복한 숫자가 아닙니다. 무한히 이어지는 순서의 크기를 다루는 특정한 순서수이며, 증명 변환이 잘 정돈된 감소 과정을 가진다는 점을 기술하는 역할을 합니다. 전문적으로는 유한주의적 기반 F에 ε₀까지의 원시재귀적 술어에 대한 초한귀납을 추가하면 페아노 산술 PA의 무모순성을 증명할 수 있다는 식으로 정리할 수 있습니다. F + PR-TI(ε₀) ⊢ Con(PA)라는 현대적 표기가 그 뜻입니다.

1931년 괴델의 제2불완전성 정리와도 정확히 구별해야 합니다. 일정한 효과적 공리화·일관성 조건을 충족하는 충분히 강한 산술 이론은 자기 자신의 무모순성을 이론 내부에서 증명할 수 없습니다. 겐첸의 무모순성 증명은 무모순성 입증에 필요한 원리의 범위를 바꾸어, PA가 자체적으로 사용하는 귀납 원리보다 별도로 강한 초한귀납 원리를 사용했습니다. 따라서 겐첸의 결과를 괴델 정리의 단순한 반례로 소개할 수 없습니다.

이 회차의 중심인 1935년 컷 제거 정리는 순수 논리 안에서 증명의 구조를 바꾸는 일입니다. 1936년 산술 무모순성 증명은 그 증명론적 연구가 산술의 기초 문제와 만나는 중요한 후속 성과입니다. 시간과 연구 대상을 구분하면 두 성과가 어떻게 이어지는지 분명하게 보입니다.

20. 그러면 중간 정리는 쓸모없게 되나요?

그렇지 않습니다. 실제 수학자의 논문에서는 이미 증명된 정리를 다시 사용할 수 있기 때문에 긴 논증을 읽기 쉬운 단위로 나눌 수 있습니다. '보조정리 A가 성립한다'는 결과를 인용하면 새로운 논증의 핵심이 무엇인지 더 선명해질 때도 많습니다. 컷 제거 정리는 그 편리한 중간 단계를 없앤 형식적 증명이 존재한다고 보장할 뿐, 사람들이 글을 쓸 때 보조정리를 포기하라고 권하지 않습니다.

예를 들어 어떤 수학 정리가 천 쪽의 계산을 보조정리 하나로 정리해 주었다고 합시다. 후속 연구자가 보조정리를 직접 쓰는 것은 합리적입니다. 모든 사용 위치마다 보조정리의 증명 내용을 펼치면 논리적 연결은 더 직접적일 수 있지만, 독자는 전체 구조를 파악하기 어려워질 수도 있습니다. 형식적으로 컷이 없는 증명과 설명하기 좋은 증명은 같은 기준으로 평가하지 않습니다.

컷 제거 변환은 증명의 최소 분량을 구하는 알고리즘도 아닙니다. 일반적인 증명에서는 변환 과정에서 식이나 단계가 거듭 복제되어 증명의 크기가 커질 수 있습니다. 그럼에도 컷을 제거한 형태를 연구하면 어느 논리식이 어디에서 쓰였는지, 어떤 추론 규칙이 증명을 구성하는지, 어떤 수학 이론이 특별한 공리를 더 필요로 하는지를 더 정밀하게 조사할 수 있습니다.