수학의 모든 증명에
모순이 없다는 사실도
증명할 수 있을까?

작은 체계에서 모순이 없음을 어떻게 보일까?

4. 작은 증명 체계의 무모순성을 직접 확인해 봅시다

세 개의 기호 명제 p, q, r을 사용하는 아주 작은 장난감 체계를 만들어 보겠습니다. p는 “가람은 연습을 마쳤다”, q는 “가람은 수료증을 받는다”, r은 “가람은 수료 명단에 오른다”라는 뜻으로 생각할 수 있습니다. 이 뜻은 예시를 이해하도록 돕는 역할을 하고, 실제 검사에서는 세 기호의 참·거짓만 사용합니다.

출발점으로 다음 세 식을 허용합니다.

① p

② p → q

③ q → r

추론 규칙은 한 가지만 사용합니다. 이미 확보한 A와 A → B가 있으면 B를 새 줄에 써도 됩니다. 허용된 출발 식과 이 규칙을 유한 번 적용하여 얻은 식들을 증명 가능한 식이라고 부르겠습니다. 우리가 만든 체계는 아직 산술도, 수학 전체도 아닙니다. 의도적으로 작게 만든 예시입니다.

이제 ①과 ②에서 q가 나오고, q와 ③에서 r이 나옵니다. 그래서 체계에서는 p, q, r을 차례로 증명할 수 있습니다. 다음으로 모순이 나오지 않는지 확인해 보겠습니다. 가능한 증명을 몇 개만 손으로 써 보고 “지금까지 모순이 없네”라고 말하면 부족합니다. 증명은 한 줄도 될 수 있고 천 줄도 될 수 있으므로, 우리가 만든 규칙으로 나올 수 있는 모든 길이의 증명을 함께 생각해야 합니다.

여기에는 작은 비결이 있습니다. p, q, r을 전부 참으로 정해 보세요. 그러면 세 출발 식이 모두 참이 됩니다. p는 참입니다. p → q 역시 앞과 뒤가 모두 참이므로 참입니다. q → r도 참입니다. 우리가 허용한 추론 규칙은 참인 A와 참인 A → B에서 참인 B를 얻으므로, 참인 식들에서 거짓인 식을 새로 만들지 않습니다.

첫 줄의 출발 식은 모두 참이고, 참인 줄에서 다음 줄로 갈 때마다 참을 보존하므로, 규칙을 열 번 적용하든 백만 번 적용하든 증명된 식은 모두 참입니다. 그런데 같은 참·거짓 배정에서 어떤 식 P와 그 부정 ¬P가 둘 다 참일 수는 없습니다. 따라서 우리의 작은 체계로는 P와 ¬P를 동시에 증명할 수 없습니다. 이것이 무모순성을 한꺼번에 보이는 논증입니다.

이 논증의 핵심을 놓치지 마세요. “가능한 증명을 모두 실제로 출력했다”는 주장이 아닙니다. 시작의 안전성과 각 단계에서 안전성이 보존된다는 사실을 합쳐, 길이에 관계없이 모든 증명에 같은 결론을 적용한 것입니다. 물론 체계의 모든 공리와 모든 추론 규칙을 빠짐없이 확인했다는 조건이 필요합니다. 작은 예시이기 때문에 우리가 규칙 전체를 손에 잡히게 열거할 수 있었습니다.

5. 방금 성공한 방법을 수학 전체로 옮기면 될까요?

작은 체계에서는 p, q, r에 참을 배정하는 일이 쉬웠습니다. 하지만 자연수와 덧셈, 곱셈을 다루고, 실수의 성질이나 무한 집합까지 사용하는 큰 이론은 다릅니다. 우리가 하는 계산과 설명이 수많은 정의와 규칙에 얽혀 있습니다. 특히 “무한히 많은 자연수 모두에 대해 …”라는 주장은 표에 있는 몇 개의 숫자를 검사하는 것으로 끝나지 않습니다.

어떤 이론 T에서 참이라고 인정하는 출발 문장들을 공리라고 하고, 문장에서 새 문장을 만드는 허용된 방법들을 추론 규칙이라고 하겠습니다. 무모순성을 표시할 때는 보통 Con(T)라는 기호를 씁니다. 여기서 Con은 콘시스턴시(consistency, 무모순성)의 줄임말입니다. T는 지금 검사할 이론의 이름입니다. Con(T)는 T의 공리와 규칙을 이용해서 지정된 모순을 증명하는 유한한 증명은 존재하지 않는다는 뜻으로 이해하면 됩니다.

산술을 충분히 표현하는 표준적인 형식 이론에서는 0 = 1을 모순의 대표 식으로 사용할 수 있습니다. 자연수 체계는 0과 1이 다르다는 사실을 다루므로, 0 = 1의 증명이 존재한다면 이론에서 모순이 생기기 때문입니다. 다만 0 = 1을 아무 체계에서나 모순의 표식으로 삼아도 되는 것은 아닙니다. 이 식이 체계 안에서 부정될 수 있고 표준적인 고전 논리 규칙을 갖춘 상황을 전제합니다.

형식적으로는 다음처럼 씁니다.

Con(T) ≡ ¬∃n Proof_T(n, ⌜0 = 1⌝)

기호를 한 부분씩 읽어 봅시다. Proof_T(n, ⌜0 = 1⌝)는 자연수 n이 “T의 공리와 규칙으로 0 = 1을 증명했다”는 기록을 일정한 부호화 방법으로 나타내는 숫자이며, 그 부호가 실제로 맞는 증명인지 검사하는 관계를 뜻합니다. ∃n은 그런 번호 n이 하나라도 존재한다는 뜻입니다. 맨 앞의 ¬는 그런 번호가 존재하지 않는다는 뜻입니다. 이 식은 “우리가 아직 모순을 발견하지 못했다”는 말보다 강합니다. 아무리 긴 증명을 찾더라도 모순을 끝줄로 갖는 적법한 증명은 존재하지 않는다고 말하기 때문입니다.

그렇다면 우리가 작은 체계에서 한 것처럼, 큰 이론에도 모든 공리를 참으로 만드는 해석을 찾아서 해결하면 어떨까요? 이 방법은 어떤 이론에서는 실제로 유용합니다. 그러나 자연수 전체를 그대로 사용하거나 더 강한 수학을 동원해 큰 이론의 모델을 만들면, 그 모델이 존재한다고 믿는 근거가 문제의 핵심으로 돌아옵니다. 증명하려는 이론보다 더 강하거나 비슷하게 논쟁적인 가정에 기대고 있지는 않은가? 힐베르트는 바로 그 점을 피하는 무모순성 증명의 근거를 요구했습니다.

무한을 다루는 수학을 어떤 근거로 믿을까?

6. 힐베르트는 어떤 방법을 특별히 믿을 만하다고 보았을까요?

1920년대 초 힐베르트는 자신이 구상한 토대 연구를 분명히 설명하기 시작했습니다. 중요한 문헌으로 1922년의 강연 『수학의 새 기초』와 1926년 논문 『무한에 대하여』가 있습니다. 그는 기호를 쓰고 지우고, 구체적으로 주어진 유한한 배열을 비교하고, 정확한 규칙에 따라 계산하는 방법에 특별한 확실성이 있다고 여겼습니다. 이를 유한주의(finitism, 유한한 기호 조작에 토대를 두는 관점)라고 부릅니다.

예를 들어 종이에 ⅠⅠⅠ라는 획 세 개를 적었다고 합시다. 바로 옆에 ⅠⅠ라는 획 두 개를 이어 붙이면 다섯 개가 됩니다. 우리가 실제로 적은 유한한 획을 세고 비교하는 데에는 “무한히 많은 숫자가 이미 완성된 하나의 물건으로 주어졌다”는 가정을 끌어들일 필요가 없습니다. 힐베르트는 이런 구체적인 기호 조작에서 출발해, 수학 전체의 형식적 증명이 모순에 빠지지 않는다는 근거를 세우려 했습니다.

여기서 중요한 미묘함이 있습니다. 힐베르트가 요구한 방법을 단순히 “숫자 하나씩 몇 개만 확인하기”로 이해하면 그의 계획이 지나치게 작아집니다. 유한한 기호에 대해 일반적인 규칙이 성립함을 설명하는 추론도 핵심입니다. 다만 정확히 어디까지를 유한주의의 정당한 추론으로 인정할 것인지는 이후 연구자들 사이에서 논쟁이 이어졌습니다. 따라서 유한주의와 오늘날 특정 형식 체계 한 개가 완전히 같은 것이라고 선언하기는 어렵습니다.

그가 이처럼 엄격한 기초 방법을 강조한 이유도 살펴봐야 합니다. 당시에는 집합론의 역설과 무한을 둘러싼 철학적 논쟁이 활발했습니다. 힐베르트는 미적분학과 무한에 관한 고전 수학의 강력한 성과를 보존하고 싶었습니다. 무한을 마음껏 다루는 수학이 무모순적이라는 사실을, 더 확실하다고 여기는 유한한 방법으로 뒷받침한다. 이것이 그의 계획에 담긴 두 목표 사이의 관계입니다.

7. ‘이상적 수학’과 ‘기초적인 계산’은 어떤 관계일까요?

예를 들어 어느 수학자가 “모든 실수 중 어떤 조건을 만족하는 수가 존재한다”는 것을 증명한다고 합시다. 그런 실수를 손으로 정확하게 적어 내기는 어려울 수 있습니다. 그래도 존재를 주장하는 증명은 다른 문제들을 해결하는 강력한 도구가 될 수 있습니다. 힐베르트는 이런 고전적인 증명과 무한한 대상을 활용하는 이론을 이상적 요소를 포함한 수학으로 다루었습니다.

반면 우리가 종이에 적어 확인할 수 있는 유한한 숫자의 관계는 보다 직접적인 성격을 갖습니다. 힐베르트의 구상에서는 후자의 확실성을 바탕으로 전자의 사용을 정당화하려 했습니다. 이때 “이상적”이라는 말을 “거짓”이나 “쓸모없는 상상”이라는 뜻으로 읽으면 흐름을 놓칩니다. 복소수를 도입해 실수 문제를 해결하는 것처럼, 기호와 이상적 대상을 다루는 확장된 체계는 수학을 한층 풍부하게 만들 수 있습니다. 힐베르트는 그 확장이 기초적인 숫자의 명백한 사실과 충돌하지 않음을 보이고 싶었습니다.

현대 증명론에서는 이 생각의 한 부분을 보존성(conservativity, 강한 이론이 기초 언어의 새로운 결론을 더 만들어 내지 않음)으로 자세히 연구합니다. 가령 T라는 기초 이론과 그것보다 많은 추론 도구를 가진 S라는 이론이 있다고 합시다. 관심을 정한 문장 종류에 관하여 S에서 증명할 수 있는 모든 문장이 이미 T에서도 증명된다면, 그 문장 종류에 대해 S는 T 위에서 보존적이라고 합니다. 여기에서 ‘모든 수학에 대해 언제나 보존적이다’라고 확대하면 잘못입니다. 비교하는 이론과 문장의 범위를 명확히 적어야 합니다.

따라서 힐베르트의 큰 꿈에는 무모순성 확인과 확장된 수학의 사용을 기초적인 방법에 비추어 정당화하는 목표가 함께 놓여 있었습니다. 둘은 연결되지만 같은 내용은 아닙니다. 하나의 무모순성 증명만으로 모든 보존성 문제가 저절로 해결되는 것은 아닙니다.

증명 기록을 연구 대상으로 삼는 방법

8. 증명도 숫자로 표현할 수 있을까요?

이제 연구 방법을 조금 더 정확하게 살펴봅시다. 형식적인 증명은 한 줄 한 줄 유한한 기호로 적혀 있습니다. 각 기호와 문장, 증명의 줄을 약속한 방식으로 숫자에 대응시킬 수 있습니다. 이를 부호화라고 합니다. 예를 들어 ‘p’에는 1, ‘→’에는 2, ‘q’에는 3 같은 임시 번호를 붙일 수 있습니다. 물론 실제 연구에서는 서로 다른 기호 배열과 증명에 서로 다른 번호가 매겨지도록 더 정교한 약속을 씁니다.

이렇게 번호를 붙이면 메타수학의 문제를 자연수에 관한 질문으로 바꾸어 쓸 수 있습니다. “n이라는 번호가 가리키는 문자열이 공리에서 시작해 올바른 규칙으로 이어지는 증명인가?”를 판정하는 절차를 설계할 수 있습니다. 공리의 집합이 효과적으로 확인 가능하도록 제시된 체계라면, 우리는 후보 증명의 각 줄이 적법한지 검토할 길을 마련할 수 있습니다. 다만 공리가 단순히 무한히 열거 가능하기만 한 일반 체계에서는 ‘주어진 줄이 공리인가?’라는 검사가 곧바로 단순한 결정 절차가 되지 않을 수 있습니다. 여기서는 공리를 효과적으로 검사할 수 있는 표준적인 형식화를 예로 생각하겠습니다.

적법한 증명인지 검사하는 일이 가능하다는 사실과, 모든 가능한 증명을 검사하여 모순이 없음을 끝내 확인하는 일은 다릅니다. 앞의 일은 주어진 유한한 증명 한 개를 다룹니다. 뒤의 일은 가능한 모든 유한한 길이의 증명을 한꺼번에 고려합니다. 이 구분이 힐베르트 계획의 기술적인 무게를 보여 줍니다.

9. 힐베르트의 연구진은 실제로 어떤 증명 방법을 개발했을까요?

힐베르트의 연구는 혼자서만 진행된 일이 아닙니다. 파울 베르나이스(Paul Bernays), 빌헬름 아커만(Wilhelm Ackermann), 존 폰 노이만(John von Neumann) 등 여러 연구자가 공리 체계와 무모순성 증명 방법을 연구했습니다. 그 가운데 중요한 기술이 엡실론 계산(ε-calculus, 선택 기호를 이용하는 논리 계산)과 엡실론 치환법(ε-substitution method, 선택 기호에 주어진 값을 단계적으로 고치는 방법)입니다.

먼저 선택 기호를 아주 간단히 살펴봅시다. 조건 A(x)를 만족하는 대상이 있다면, εx A(x)를 그 조건을 만족하는 대상 하나를 고르는 기호처럼 사용할 수 있습니다. 이를 “조건 A를 만족하는 대상 중 하나를 나타내는 선택항”이라고 읽으면 됩니다. 그 조건을 만족하는 대상이 실제로 존재하지 않는 상황까지 포괄하려면 형식적 규칙을 더 세밀히 정해야 합니다. 여기에서는 존재하는 경우의 작동 원리만 설명하겠습니다.

우리가 어떤 계산에 ε항을 임시 숫자로 넣었는데 조건과 맞지 않는 결과가 생겼다면, 다른 값을 넣어 잘못된 부분을 바로잡아 볼 수 있습니다. 이때 무한을 사용하는 복잡한 증명에서 나온 선택항들을 유한한 절차로 고쳐, 결국 문제가 없는 형태로 돌려놓는다면 무모순성을 보일 수 있을 것처럼 보입니다.

하지만 몇 번 고치면 잘 되는 예가 있다는 것과 어떤 적법한 증명이 들어와도 이 교정 과정이 반드시 끝난다는 것은 전혀 다른 주장입니다. 힐베르트의 계획에서 가장 어려운 기술적 문제 가운데 하나는 바로 이 종료 보증이었습니다. 아커만은 1924년에 복잡한 체계에 대한 무모순성 증명을 시도했지만, 그 주장은 이후 검토에서 문제가 드러났습니다. 폰 노이만도 더 제한된 체계에 대한 성과를 제시했습니다. 이 사실을 “1920년대에 산술과 해석의 무모순성이 완전히 증명되었다”라고 요약하면 연구의 성공 범위를 부풀리게 됩니다.

괴델 정리는 정확히 무엇을 막았을까?

10. 괴델은 무엇을 증명했기에 계획이 흔들렸을까요?

1931년 쿠르트 괴델의 불완전성 정리가 발표되었습니다. 앞선 제09회에서 다룬 1차 논리의 완전성 정리는 모든 해석에서 따라오는 결론을 형식적 증명으로 얻을 수 있다는 성과입니다. 이번에 등장하는 제2불완전성 정리는 일정한 산술 이론이 자기 자신의 무모순성을 증명할 수 있는가라는 전혀 다른 질문에 관한 결과입니다.

어떤 이론 T가 자연수의 기본적인 산술을 충분히 표현할 수 있고, 공리들을 효과적으로 나열할 수 있으며, 표준적인 증명 개념에 필요한 조건을 만족한다고 합시다. 이런 종류의 무모순적인 T는 자기 자신의 무모순성을 표현한 표준적인 식 Con(T)를 T 내부에서 증명할 수 없습니다. 간략히 T ⊬ Con(T)라고 적습니다. 여기서 ⊬는 “해당 이론의 공리와 규칙으로 그 식을 증명할 수 없다”는 뜻입니다.

말의 순서가 중요합니다. 이론 T가 실제로 무모순적이라는 가정이 들어가야 합니다. T가 충분한 산술을 표현한다는 조건도 필요합니다. 공리들이 효과적으로 주어진 형식 이론이어야 하고, 무모순성을 표현한 식이 표준적인 증명 관계에 맞게 구성되어 있어야 합니다. 그러므로 이 정리를 “어떤 사소한 규칙도 스스로 점검할 수 없다”라고 확대하면 곤란합니다. 우리가 만든 p·q·r 예시 같은 아주 작은 체계는 괴델 정리의 적용 조건을 갖추지 않았습니다.

또한 “자기 이론 안에서는 증명할 수 없다”는 말과 “어떠한 방법으로도 무모순성을 증명할 수 없다”는 말은 다릅니다. 뒤의 주장은 괴델의 정리가 말하는 내용이 아닙니다. 오히려 더 강한 이론, 서로 다른 정당화 방법, 새로운 증명 방법으로 특정 이론의 무모순성을 살필 수 있습니다. 다만 그렇게 했을 때는 증명을 수행한 다른 방법의 타당성을 어떤 근거로 받아들일 것인가라는 새 질문이 남습니다.

11. 왜 자기 자신의 무모순성은 특별히 어려울까요?

우리가 만든 작은 체계를 떠올려 보면 답에 다가갈 수 있습니다. 그 체계 안에서는 p나 q를 증명했지만, 그 체계가 사용하는 규칙 전체를 조사하고 “모든 증명은 안전하다”라는 결론을 내리는 일은 바깥에서 수행했습니다. 구체적으로 세 공리가 특정한 참·거짓 배정에서 참이라는 사실과 추론 규칙이 참을 보존한다는 사실을 이용했습니다. 작은 체계 안에 자기 자신의 모든 증명에 대한 장치를 따로 넣지 않았습니다.

반면 충분히 강한 산술 이론 T는 숫자를 이용해 자기 자신의 증명 기록을 부호화할 수 있습니다. “이 숫자는 T의 증명이다”라는 성질을 이론 안에서 다루고, 그 안에서 “모순을 증명하는 번호가 없다”라는 주장도 만들 수 있습니다. 단순히 바깥에서만 말하던 검사를 수학의 내부 문제로 바꾸는 일이 가능해지는 것입니다.

괴델의 기술은 이 자기지시 능력과 증명 가능성 사이에 깊은 제약이 있음을 보여 주었습니다. 이론이 충분히 강하고 무모순적이라면, 그 안에서 자신의 무모순성을 표준적인 방식으로 증명했다는 결론까지 만들 수 없습니다. 1931년 당시 힐베르트가 꿈꾸던 전체 수학의 무모순성을 약한 유한적 수학만으로, 그리고 그 정당화를 의심할 여지를 최소화하면서 증명한다는 원래의 구상이 거센 도전에 직면했습니다.

그러나 여기에도 학술적인 주의가 필요합니다. 힐베르트가 말한 모든 유한적 추론이 정확히 어느 형식 체계와 일치하는지는 간단한 정의 하나로 확정되는 문제가 아닙니다. 따라서 제2불완전성 정리에서 힐베르트의 철학적 계획 전체가 어느 범위까지 불가능해졌는지 평가할 때에는 이 해석 문제를 함께 밝혀야 합니다. 일반적인 평가는 원래 계획이 큰 제약을 받았다는 것이지만, 정리 한 줄로 이후의 모든 기초 연구를 무의미하게 만드는 설명은 정확하지 않습니다.

그 뒤의 증명론은 무엇을 더 알아냈을까?

12. 수학자들은 그 뒤에도 무모순성을 증명했을까요?

그렇습니다. 괴델의 정리가 등장한 뒤에도 증명론의 연구는 활발하게 이어졌습니다. 특히 게르하르트 겐첸(Gerhard Gentzen)은 1936년 자연수의 산술 이론에 대한 무모순성 증명을 발표했습니다. 다만 그 증명은 힐베르트가 바라던 단순한 형태의 유한주의만으로 닫힌 최종 해답이라기보다, 추가적인 정당화 원리를 이용해 산술의 무모순성을 뒷받침한 연구로 이해해야 합니다.

겐첸은 증명의 복잡한 구조에 순서수를 부여하고, 증명 변환을 하면 그 순서수가 일정한 방식으로 내려가도록 논증했습니다. 여기서 사용한 중요한 경계는 엡실론 영(ε₀, 첫 무한 순서수 ω에서 지수 올림을 반복해 얻는 수열의 극한인 순서수)입니다. 순서수는 단순한 자연수 하나가 아니라 잘 정렬된 순서의 형식을 다루는 수학적 대상입니다. ε₀와 그 아래의 순서수들이 어떤 식으로 구성되는지 충분히 공부하기 전에는, 이를 큰 정수 한 개쯤으로 이해하면 안 됩니다.

이 방법의 직관은 어떤 문제 있는 증명에서 더 단순한 증명으로 계속 바꿔 간다고 가정할 때, 그 변환이 끝나지 않고 영원히 이어질 수 있는지를 따지는 데 있습니다. 순서수에 관한 초한 귀납법을 사용하면 특정한 하강 과정이 끝없이 계속될 수 없다는 근거를 마련할 수 있습니다. 이를 통해 산술에 모순 증명이 존재한다는 가정에서 불가능한 결론에 이르는 방향을 연구할 수 있습니다.

겐첸의 성과는 “괴델이 틀렸고 힐베르트가 완전히 옳았다”는 이야기가 아닙니다. 증명을 수행하는 바깥의 방법이 원래 산술 이론보다 어떤 점에서 더 강한지, 어디까지 받아들일지를 분명하게 보여 주었다는 점에 의미가 있습니다. 제16회에서 겐첸의 컷 제거와 증명 변환을 다룰 때 이 관계를 다시 살펴볼 수 있습니다.