Incompleteness

(본 포스트는 불완전성 정리의 쉬운 설명입니다. 불완전성 정리의 엄밀한 정의: 불완전성 정리의 엄밀한 정의, 두번째 불완전성 정리의 엄밀한 정의)

배경✔

힐베르트는 수학자들이 수학을 발전시켜온 과정을 쭉 보니까 수학이란 공리에 몇 개의 추론 규칙을 반복적으로 적용하는 것이 전부 다 인 것 같다는 생각을 했다. 그리고 그러한 추론 규칙만 찾아낸다면 수학자가 더 이상 고생할 필요가 없어질 것이라고 생각했다.

20세기 초 수학계는 수학에서 자연 언어를 제거하고 수학을 완전히 형식적인 연역 체계로 구성하려고 노력했다. 수학적 사고를 순수한 기호 조작의 규칙에 의해 포착할 수 있다고 믿었기 때문이다. 이 노력은 러셀과 화이트헤드의 『수학 원리』로 절정을 이루었다. 다음은 러셀이 수학을 완전한 형식적인 연역 체계로 구성한 『수학원리』에서 1+1=2 의 증명을 보인 것이다.

용어✔

이제 앞으로 사용할 용어들을 다음과 같이 정리해보자.

예시: 명제 논리✔

하지만 아직 용어의 의미가 알쏭달쏭하다. 그래서 『수학 원리』의 작은 한 부분을 차지하는 명제 논리(Propositional Calculus)라는 형식적 연역 체계를 예를 들어서 용어에 대한 이해를 해보자.

다음의 과정으로 명제 논리는 완전히 형식화 된 형식적 연역 체계가 된다.

• 변항 기호(문장 변항)는 형식문이 대입될 수 있는 변항으로써 알파벳 소문자 \(p,q,r\) 등으로 나타낸다.

• 상항 기호는 다음과 같이 구성된다.

  상항기호	의미
  \(\ssim\)	아닌
  \(\lor\)	또는
  \(\land\)	그리고
  \(\to\)	만일 ~이면 ~이다

• 위 네 가지 공리를 쉽게 말하면 다음과 같다.

  \((p\lor{}p)\to{}p\): p 이거나 p 이면 p 이다. 가령, 임진왜란이 일어났거나 임진왜란이 일어났다면 임진왜란은 일어났다.

  \(p\to(p\lor{}q)\): p 이면 p 이거나 q 이다. 가령, 임진왜란이 일어났다면 임진왜란이 일어났거나 알파고가 이세돌을 이겼다.

  \((p\lor{}q)\to(q\lor{}p)\): p 이거나 q 이면 q 이거나 p 이다. 가령, 임진왜란이 일어났거나 알파고가 이세돌을 이겼다면 알파고가 이세돌을 이겼거나 임진왜란이 일어났다.

  \((p\to{}q)\to((r\lor{}p)\to(r\lor{}q))\): "p 이면 q 이다" 이면 "(r 또는 p) 이면 (r 또는 q) 이다" 이다. 가령, "도박을 하면 돈을 잃는다" 라면 "고향집에 내려가거나 도박을 하면 고향집에 내려가거나 돈을 잃는 것이다" 이다.

이로써 명제 논리는 무한히 많은 형식문들을 연역해낼 수 있다. 가령 너무나도 자명해보이는 추론 규칙과 공리로부터 전혀 자명하지 않은 다음과 같은 형식문을 연역해낼 수 있다.

이제 이 연역체계가 정합적 체계인지 부정합 체계인지, 그리고 완전체계인지 불완전체계인지 조사하기 위하여 다음의 논증을 펼쳐보자.

1. 위 네 가지 공리로부터 정리 \(p\to{}(\ssim{}p\to{}q)\) 를 연역할 수 있다.

2. 이 공리 체계에 정합성이 없다고 가정하면, 즉 이 체계가 모순을 도출한다고 가정하면 이 공리 체계로부터 형식문 \(S\) 와 부정문 \(\ssim{}S\) 가 동시에 연역된다.

3. 그렇다면 형식문 \(p\to{}(\ssim{}p\to{}q)\) 의 변항 \(p\) 에 \(S\) 를 대입하여 \(S\to{}(\ssim{}S\to{}q)\) 를 연역(대입규칙)할 수 있다.

4. 이때 \(S\) 가 증명될 수 있으므로 분리규칙에 의하여 \(\ssim{}S\to{}q\) 가 연역된다.

5. 그런데 \(\ssim{}S\) 도 증명될 수 있으므로 최종적으로 문장변항 \(q\) 가 연역(증명)된다.

6. 이 변항에는 존재하는 모든 형식문이 대입될 수 있으므로 존재하는 모든 형식문이 증명가능한 정리가 된다. 심지어 공리도 정리가 된다.

7. 이것은 부정합 체계에서는 모든 형식문이 증명 가능하다는 것이다.

8. 그러므로 공리 체계의 정합성의 증명은 공리로부터 연역되지 않는 형식문이 있다는 것을 보이는 것이다.

이렇게 정합성이 없는 체계에서는 "나는 한동대생이다" 와 "나는 한동대생이 아니다" 라는 명제가 동시에 올바르면서 증명가능한 주장이 되는 것이다. 뿐만 아니라 구성규칙과 추론규칙으로 잘 구성되기만 했다면 모든 문장이 증명가능한 명제가 되는 것이다.

따라서 명제 논리의 정합성의 증명은 그 체계로부터 연역될 수 없는 형식문이 적어도 하나 있다는 것을 보이는 것이 된다. 이것은 네 가지 공리가 공유하는 유전적 특성을 갖지 않는 형식문을 찾는 것으로 이루어진다.

만약 우리가 유전적 특성을 갖지 않는 형식문을 발견한다면 공리로부터 연역된 형식문이 아니라는 말이 된다. 따라서 그 체계의 정합성을 확립한 것이 된다. 여기에서는 네 공리가 공유하는 유전적 속성으로써 항진식(tautology)를 택하자.

• 실제로 다음과 같은 네 가지 공리는 구성성분 \(p,q,r\) 에 관계없이 항상 참이므로 항진식이다.

  \[(p\lor{}p)\to{}p,p\to(p\lor{}q),(p\lor{}q)\to(q\lor{}p),(p\to{}q)\to((r\lor{}p)\to(r\lor{}q))\]

이 항진식는 명제 논리의 네 가지 공리가 모두 공유하며 추론 규칙에 의하여 공리에서 정리가 연역될 때 항상 따라오는 성질이다.

그러므로 이 항진식이 없는 형식문을 찾으면 명제 논리는 모순을 도출하지 않는 정합적인 체계가 된다. 그런데 항진식이 없는 형식문을 찾는 일은 쉽다.

• 증명

  형식문 \(p\lor{}q\) 는 명제 논리의 구성규칙에 의해 형성된 올바른 형식문이다. 그런데 구성성분 \(p\) 와 \(q\) 가 거짓이면 거짓이 되므로 형식문 \(p\lor{}q\) 는 항진식이 아니다. 그러므로 형식문 \(p\lor{}q\) 은 네 가지 공리로부터 연역된 정리가 아니다. 그러므로 명제 논리는 모순을 일으키지 않는 정합적 체계이다. ■

이제 이 연역 체계의 모든 정리는 항진식이고, 명제 논리의 공리들은 존재하는 모든 항진식을 만들어내기에 충분한 완전 체계라는 것이 증명되었다. 수학자들은 유클리드가 『원론』 에서 모든 정리들을 공리로부터 연역한 것처럼 모든 수학 분야를 완전 체계로 만들 수 있을 것이라고 수천년동안 믿어왔고, 이제 실제로 모든 수학 체계를 정합적인 완전 체계로 구성하려고 시도 한 것이다.

하지만 명제 논리는 기초 산술학을 전개하기에도 충분하지 못했다. 힐베르트는 수론 전체를 포괄할 수 있는 체계에 대한 정합성과 완전성을 확립하길 원했다. 왜냐하면 자연수 위에서 정수와 유리수와 무리수를 정의해하고, 그 위에 실수와 복소수를 정의해야 하고, 그 위에 기하학과 해석학을 건설해야 하기 때문이다.

수학의 역사 요약✔

이제 괴델의 불완전성 정리를 구체적으로 알아볼 것인데, 그 전에 지금까지의 내용을 다시 정리해보자.

1. (기원전 3000년 ~ 기원전 320년) 유클리드가 『원론』 을 집필하며 "수학이란 공리로부터 정리를 연역하는 연역 체계이다"라는 인식을 전수함.

2. (기원전 27년 ~ 476년) 로마가 유럽을 지배하며 기독교를 국교로 제정하였고 이로써 수많은 그리스 책들이 불태워졌음.

3. (200년 ~ 1200년) 인도와 아라비아 인들이 그리스 수학을 잘 물려받았다가 유럽에게 물려줌.

4. (400년 ~ 1100년) 로마가 멸망하기 전에 유럽에 기독교를 전파했고 십자군 전쟁으로 유럽인들이 아라비아 땅으로 가서 그곳에 보존되어 있던 그리스 학문을 배우게 됨.

5. (1400년 ~ 1600년) 수학자들(케플러, 뉴턴, 데카르트, 라이프니츠 등)이 하나님이 온 우주를 수학적으로 창조했다고 믿고 그분의 영광을 드러내기 위해 수학 연구를 진행하였고, 이로써 수학이 자연의 불변의 법칙을 연구하는 학문이라는 인식이 널리 퍼짐.

6. (1700년대) 이후 수학이란 자연을 추상화시킨 학문이고 하나님이 자연을 수학적으로 창조했다는 인식 때문에 수학자들이 엄밀하지 못한 논리적 토대 속에서도 열정만으로 수학을 발전시킴.

7. (~ 1700년대) 수학자들은 유클리드의 기하학이 물리 공간을 올바르게 추상화한 체계라고 믿었지만 제 5 공리인 평행선 공리에는 다른 공리들이 갖고 있는 간결함이 없어서 평행선 공리를 다른 공리로부터 연역하려고 노력함.

8. (1800년대) 가우스와 로바체프스키, 보여이가 평행선 공리와 대치되는 공리를 택함으로써 유클리드 기하학과 전혀 다른 비유클리드 기하학을 창시함. 이로써 유클리드 기하학이 신이 창조한 유일하고도 불변하는 진리가 아니라 인간의 창조물이라는 것이 밝혀짐. 수학이 인간의 인위적인 창조물이라면 수학에 모순이 있을 수도 있다는 문제가 제기됨. 가우스는 유클리드 기하학이 물리 세계의 진리가 아닐 수도 있다는 것을 깨닫고 수학의 진리를 산술, 즉 수론 체계에서 찾으려 했음.¹

9. (1800년 ~) 수학자들은 가우스처럼 산술만큼은 참되다고 믿었기에 해석학의 논리적 토대로써 산술을 채택함.

   해석학 ← 산술(정수 체계)

10. (1843년) 해밀턴이 사원수를 발견함. 이로써 불변하는 신의 창조물이라고 여겨졌던 유일한 수 체계인 실수와 복소수 말고도 또 다른 수 체계가 존재한다는 것이 밝혀졌고, 수 체계도 신이 만든 진리가 아니라 인간이 만든 인위적인 창조물이라는 것이 밝혀짐.

11. (1850년 ~) 수학자들은 믿었던 수 체계의 기초도 마련해야 한다는 것을 깨닫고 실수 체계의 기초를 위하여 무리수의 기초를 마련하려 함. 칸토어와 데데킨트가 유리수를 기반으로 무리수 체계를 확립함. 칸토어가 집합론을 창시하고 실수집합 구조의 이해를 위하여 무한집합 개념을 도입함. 바이어슈트라스가 자연수를 기반으로 유리수 체계를 확립함. 페아노도 공리적 방식으로 자연수 체계를 확립함. 이로써 실수 체계의 기초가 산술에 의해 확립됨.

    실수 체계 ← 무리수 체계 ← 유리수 체계 ← 정수 체계(산술)

12. (1900년) 힐베르트는 비유클리드 기하학의 정합성을 유클리드 기하학의 정합성으로 환원시키고 유클리드 기하학의 정합성을 대수학의 정합성으로 환원시킴.

    수학적 대상	비유클리드 기하학	유클리드 기하학	대수학
    직선			\(y=x\)
    삼각형
    원			\(x^{2}+y^{2}=1\)

    그러므로 만약 대수학이 정합적 체계라면 유클리드 기하학도 모순을 내뱉지 않는 정합적 체계이고, 이에따라 비유클리드 기하학도 정합적인 체계가 되는 것임. 대수학은 산술의 확장체이므로 힐베르트는 "기하학과 물리학의 무모순성(정합성)의 증명은 산술의 무모순성으로 귀결시킴으로써 성취된다"고 말함. 즉 산술에 모순이 없다면 산술의 확장체인 기하학의 대수적인 구성에도 모순이 없게되기 때문에 이제 초미의 관심사는 산술의 정합성이 되었음.

    비유클리드 기하학 ← 유클리드 기하학 ← 대수학 ← 산술(정수 체계)

13. (1901년) 러셀이 칸토어가 창시한 집합론에 역설이 존재함을 보임. 이제 수학의 기초를 마련해야 하는 문제가 가장 급한 문제가 되어 수학의 기초를 마련하려는 논리주의 학파, 형식주의 학파, 직관주의 학파가 생겨남.²

14. (1910년) 러셀의 논리주의 학파는 논리학 공리로부터 산술을 연역하고 자연수 위에 실수, 복소수, 함수, 해석학, 기하학 전체를 연역해낼 수 있다는 내용을 『수학 원리』 에 담아 출판함. 이후 러셀은 1937년판 『수학 원리』 에서 논리학 공리가 진리라는 견해를 버림.

    산술(정수 체계) ← 논리학 체계

15. (1920년) 힐베르트와 형식주의 학파가 모든 수학이 공리와 일련의 추론규칙으로 연역되는 완전한 형식적 체계로 환원시킬 수 있다는 힐베르트 프로그램을 발표함.

    산술(정수 체계) ← 형식적 체계

16. (1931년) 괴델이 불완전성 정리를 발표하여 유클리드가 수천년전부터 전수해온 "수학이란 공리로부터 정리를 연역하는 연역 체계이다"라는 믿음을 박살내고, 수학을 『수학원리』에서 말하는 논리적 연역 체계나 힐베르트 프로그램이 말하는 형식적 연역체계로 설명할 수 없다는 것을 밝힘.

자동적으로(기계적으로) 수학의 모든 사실들을 만들 수 없다!✔

러셀은 『수학원리』로 논리학 공리 위에 수학을 건설함으로써 수학을 순수한 논리 체계로 환원시킬 수 있다고 믿었다. 힐베르트는 수학을 적절한 공리와 추론규칙을 설정한 다음 그것의 형식적인 조작을 통하여 연역되는 정리들의 집합체(형식적 연역체계)로 구성하려 했다. 즉, 힐베르트는 "수학자들이 지금까지 해온 연구과정을 보아하니, 유한한 공리와 몇가지 추론규칙을 통하여 수학의 모든 사실을 도출해내는 것을 자동으로 해낼 수 있을 것 같다" 라고 생각했다. 그래서 힐베르트가 이끄는 형식주의 학파는 이러한 자동기계를 만들기만 하면 근의 공식이나 도함수 구하는 공식같은 수학적 사실들이 모두 자동으로 만들어질 수 있을 것이라고 생각했다. 폰 노이만도 힐베르트의 제자로써 형식주의 학파였다. 이 생각들은 수학적 사고를 순수한 기호 조작의 규칙으로 규명할 수 있다는 믿음에 근거하고 있었다. 그리고 이로써 수학자들은 수학의 기초를 확립하려 했다.

하지만 이 상황에서 괴델이 불완전성 정리를 설명한 논문《Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I》(『수학원리』 및 그와 연관된 체계들 속에서 형식적으로 결정될 수 없는 명제에 관하여) 을 발표한다. 괴델은 이 논문을 통하여 "자동적으로(기계적으로) 수학의 모든 사실들을 만들 수 없다"는 것을 증명했다.

이 괴델의 불완전성 정리가 어찌나 중요한지 모든 수학의 역사 속에서 가장 중요한 정리라고 부르는 사람도 있다. 그리고 컴퓨터를 탄생시킨 튜링에게 직접적인 아이디어를 제공한 정리이기도 하니까 프로그래머들에게도 그 중요성이 얼마나 큰지 짐작할 수 있을 것 같다.

《Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I》✔

이제부터 괴델의 증명과정을 간단하게 알아보자. 실제 괴델의 불완전성 정리는 다음과 같다.

괴델은 『수학 원리』를 연구하면서 형식화된 기호 패턴이 수 패턴과 똑같다고 생각했고 실제로 모든 기호를 수로 대체할 수 있다는 것을 깨달았다. 즉, 괴델은 수가 모든 종류의 패턴을 표현할 수 있는 보편적인 매개 수단이라는 것을 깨달았고, 심지어 다른 모든 영역의 명제도 순수한 수로 환원할 수 있다는 것을 깨달았다.

한편, 이로써 다른 영역의 명제(은행 거래, 대화 나누기, FPS 게임, 뇌 세포와 뉴런의 동작 등)도 수학 명제로 사상시킨 다음 프로그램으로 자동화시킬 수 있다.

이는 『수학 원리』 의 주제가 "수" 인데, 『수학 원리』 자체도 "수" 로 환원시킬 수 있으므로 『수학 원리』 는 자기 자신에 관하여 언급하고 있다는 것을 의미했다. 그런데 괴델은 이것을 깨달은 시점에서 옛날부터 내려오던 자기 언급의 역설, 특히 "이 명제는 거짓이다." 라는 역설을 검토하지 않을 수 없었다.

"이 명제는 거짓이다" 가 참이라면 이 명제가 거짓이라고 한 것이 참이므로 이 명제는 거짓이 된다. 이것은 모순이다. 반면 "이 명제는 거짓이다" 가 거짓이라면 이 명제가 참이 되므로 역시 모순이다.

여기에서 수학명제와 상위 수학명제(메타 수학명제)의 차이를 짚고 넘어가야 한다. 힐베르트는 형식적 연역체계 속의 형식문은 수학명제이지만 그것에 관하여 언급하는 언어는 상위수학이라고 구별했다.

• 예시

  \(2+3=5\)

• 예시

  "\(2+3=5\)" 는 산술학적 형식문이다.

  "\(2+3=5\)" 의 두번째 기호는 + 이다.

수학의 모든 공리체계를 대표할 수 있는 PM✔

괴델은 먼저 『수학 원리』의 기호 체계를 약간 고쳐서 모든 산술학을 포괄할 수 있는 연산 체계 PM을 만들었다. 이로써 PM이 『수학원리』와 관련 체계를 대표할 수 있게 되었다. 그리고 괴델은 "PM 은 정합적 체계이다" 라는 상위 수학명제를 PM 속의 수학 명제로 사상(mapping)시켜서 논증을 진행했다.

사상(mapping)은 우리가 일상에서도 많이 사용하는 개념이다. 우리는 실제 지구의 표면을 지구본에 사상시켰다. 그리고 비유클리드 기하학의 대원을 유클리드 기하학의 직선으로 사상시켰고 직선을 대수학의 관계(\(y=x\))로 사상시켰다. 그리고 애정을 뜻하는 마음 속 생각을 자연어 "사랑해"로 사상시켰고 다시 "사랑해"를 문자로 전달하기 위하여 유니코드 "\xc0ac\xb791\xd574" 로 사상시켰다. 책도 누군가의 마음 속 생각을 언어로 사상시킨 것이다.

괴델의 증명 과정✔

괴델은 다음과 같은 논증으로 불완전성 정리를 증명했다.

1. 괴델 수 붙이기(수학명제를 수로 사상시키기)

2. 상위 수학명제를 수학명제로 사상시키기

3. 핵심 논증

   1. "형식문 \(G\) 는 PM 으로 증명할 수 없다"는 상위 수학명제를 PM 속의 수학명제로 사상시킨 형식문 \(G\) 를 만들 수 있다.

   2. 형식문 \(G\) 는 그 부정문 \(\ssim{}G\) 이 증명될 수 있을 때에만 증명될 수 있다.

   3. 형식문 \(G\) 는 증명될 수 없지만 올바른 형식문이다.

   4. (제 1 불완전성 정리 증명) 형식문 \(G\) 가 옳으면서도 증명될 수 없으므로 PM 은 불완전 체계이다.

   5. (제 2 불완전성 정리 증명) "PM 은 정합적 체계이다." 라는 상위 수학명제를 PM 의 형식문 \(A\) 로 사상시키고 형식문 \(A\to{}G\) (\(A\) 이면 \(G\) 이다) 가 PM 속에서 증명될 수 있다는 것을 보인다. 그런데 \(A\) 가 증명되면 이로써 \(G\) 도 연역(증명)되는 셈이다. 그러므로 형식문 \(A\) 는 PM 속에서 증명될 수 없다.

1. 괴델 수 붙이기 (수학명제를 수로 변환하기)✔

모든 패턴과 구조를 수로 환원할 수 있다는 것을 깨달은 괴델은 『수학 원리』의 기호 체계를 약간 고쳐서 만든 형식적 연산 체계 PM의 모든 형식문을 수로 사상(수학명제를 수로 사상) 시킬 수 있는 방법을 보였다. 괴델은 (1) 기본 기호, (2) 기호의 모음인 형식문, (3) 형식문의 모음인 증명에 고유의 수를 부여할 수 있는 방법을 보여주었다.

기본 기호에 괴델수 붙이기✔

다음의 12개의 상항 기호를 상정하고 각각 1 에서 12 의 수를 부여하자.

가령 "\(0+s0=s0\)" 은 일상적인 의미로 0+1=1 을 뜻한다.

또한 숫자변항, 문장변항, 술어변항으로 구성되는 변항기호에도 괴델수를 부여할 수 있다. 다음과 같이 숫자변항에는 12 보다 큰 소수를 차례로 부여한다.

다음과 같이 문장변항에는 12 보다 큰 소수의 제곱수를 부여한다.

다음과 같이 술어변항에는 12 보다 큰 소수의 세제곱수를 부여한다.

형식문에 괴델수 붙이기✔

형식문에 괴델수를 붙이는 것은 매우 간단하다. 가령 \(y\) 바로 다음 수 \(x\) 가 있다는 의미의 형식문 "\((\exists{}x)(x=sy)\)" 의 기본 기호는 각각 괴델수

를 갖는데 일련의 소수에 이 괴델수의 거듭제곱을 취하여 곱한 수

를 이 형식문에 부여하면 된다. 이 방식으로 PM 의 모든 형식문에 고유의 괴델수를 부여할 수 있다.

증명에 괴델수 붙이기✔

형식문이 기호의 모임이듯, 수학에서의 증명 또한 형식문의 모임이다. 한편, 놀랍게도 형식문은 프로그램의 코드 한 줄에 대응되고, 프로그램은 수학에서의 논리적 증명에 완벽히 대응된다.

증명에 괴델수를 붙이는 것은 매우 쉽다. 가령 다음과 같은 증명이 있다고 하자. 이 논증은 매우 쉬운데 "어떤 수에는 다음 수가 존재하므로 0 다음 수도 존재한다" 는 논증이다. 즉, "1 이 존재한다" 에 대한 증명이다.

1. \((\exists{}x)(x=sy)\)

2. \((\exists{}x)(x=s0)\)

이 증명은 두 개의 형식문으로 구성되어 있으므로 각각의 형식문에 괴델수를 부여할 수 있다. 첫번째 형식문의 괴델수는 앞서 \(m\) 으로 이미 부여했으니 두번째 형식문에는 \(n\) 이라는 괴델수를 부여하겠다. 그러면 이 일련의 소수에 형식문들의 괴델수로 거듭제곱을 취하여 얻은 수 \(k=2^{m}\times{}3^{n}\) 를 이 증명의 괴델수로 부여하면 된다.

이로써 형식적 연산 체계 전체를 완벽하게 수로 사상시킬 수 있게 되었다. 즉, 모든 수학명제를 완벽하게 순수한 수로 환원시킬 수 있게 된 것이다. 또 거꾸로 어떤 수가 주어지면 그 수가 괴델수인지 결정할 수 있고, 괴델수라면 어떤 수학명제에 대응되는지 정확하게 알 수 있게 되었다.

2. 상위 수학명제를 수학 명제로 사상시키기✔

그런데 괴델은 수학명제에 관하여 언급하는 상위 수학명제란 형식적 표현과 그것들의 관계에 대하여 언급하는 명제라는 것을 깨닫고, 상위 수학명제를 그것에 대응하는 괴델수와 괴델수 간의 관계에 관하여 언급하는 수학명제로 사상시켰다. 이 방식으로 괴델은 상위 수학까지도 완전하게 산술로 환원시켰다.

가령 "영은 영과 같지 않다" 고 말하는 수학명제 "\(\ssim(0=0)\)" 와 그것에 관하여 언급하는 상위 수학명제 "형식문 \(\ssim(0=0)\) 의 첫번째 기호는 틸드(~)이다"를 예로 들어보겠다. 먼저 형식문(수학명제)의 괴델수는

이다. 그런데 상위 수학명제가 틸드(\(\ssim\))를 언급하므로 상위 수학명제가 \(a\) 의 가장 작은 소수의 거듭제곱 \(2^1\) 와 관계되어 있다는 것을 알 수 있다. 이것에 착안하여 상위 수학명제 "형식문 \(\ssim(0=0)\) 의 첫번째 기호는 틸드(\(\ssim\))이다"를 수학명제 "형식문 \(\ssim(0=0)\) 의 괴델수 \(a\) 의 첫번째 소수 \(2\) 의 지수는 \(1\) 이다"로 사상시킬 수 있다. 이 수학명제는 다시 "\(2\) 는 \(a\) 의 인수이고 \(2^{2}\) 는 \(a\) 의 인수가 아니다"라는 수학명제와 동치이다.

그런데 수학명제 "\(x\) 는 \(y\) 의 인수이다" 는 수학명제 "\(x\) 를 곱하면 \(y\) 가 되는 수 \(z\) 가 있다" 와 같으므로 형식문 \((\exists{}z)(y=z{}\times{}x)\) 와 같다. 그러므로 결론적으로 수학명제 "\(2\) 는 \(a\) 의 인수이고 \(2^{2}\) 는 \(a\) 의 인수가 아니다"에서 "\(2\) 는 \(a\) 의 인수이다"는 형식문

으로 사상되고 "\(2^{2}\) 는 \(a\) 의 인수가 아니다"는

로 사상된다. 이에 따라 최종적으로 상위 수학명제 "형식문 \(\ssim(0=0)\) 의 첫번째 기호는 틸드(\(\ssim\))이다"를 수학명제 "\(2\) 는 \(a\) 의 인수이고 \(2^{2}\) 는 \(a\) 의 인수가 아니다"로 사상시킨 형식문

을 얻는다. 또 이 형식문의 괴델수는 매우 크겠지만 지금까지의 방식으로 쉽게 구할 수 있다.

한편, \(\land\) 는 "그리고" 를 뜻하는데 처음에 상정한 상항기호에는 "그리고" 가 없다. 그러나 이것을 기본 기호의 축약이라고 보면 된다. 가령 \(p\land{}q\) 는 \(\ssim(\ssim{}p\lor{}q)\) 의 축약인 것이다. 마찬가지로 \(2\) 도 \(ss0\) 의 축약이다.

이로써 수학에 관하여 언급하는 상위 수학까지도 완전하게 순수한 수학 명제로, 그리고 괴델수로 사상시킬 수 있게 되었다. 그러므로 우리는 PM에 관하여 언급하는 상위 수학이 PM 속에서 형식적 체계로 구성될 수 있다는 결론에 도달하게 된다.

이제 매우 간단한 두 가지 함수를 정의하자.

증명함수✔

"증명에 괴델수를 붙이기" 에서 괴델수 \(n\) 을 갖는 형식문의 증명의 괴델수 \(k=2^{m}\times{}3^{n}\) 를 살펴보았다. 이렇게 어떤 증명에 해당하는 괴델수 \(k\) 는 그 증명의 결론에 해당하는 형식문의 괴델수 \(n\) 과 산술학적 관계를 갖는다.

우리는 형식문 \(n\) 을 증명하는 형식문 모임의 괴델수 \(k\) 의 산술학적 관계(\(k=2^{m}\times{}3^{n})\) 를 \(\text{dem}(k,n)\) 으로 표현할 수 있다. 이 \(\text{dem}(k,n)\) 은 단순히 "\(k\) 가 \(n\) 의 증명이다" 라고 말하고 있는 것이다.

그러면 이것을 일반화해서 "괴델수 \(x\) 를 가지는 형식문 모임은 괴델수 \(z\) 를 가진 형식문의 증명이다" 라는 상위 수학명제에서 \(x\) 와 \(z\) 의 관계를 \(\text{dem}(x,z)\) 로 정의하자.

• 그냥 \(x\) 가 \(z\) 의 증명이다 라고 생각하면 된다.

• 증명(demonstration) 의 줄임말이다.

그리고 이 수론적 관계 \(\text{dem}(x,z)\) 를 형식문으로 사상시킨 것을 \(\text{Dem}(x,z)\) 라고 하겠다.

• \(\text{dem}(x,z)\) 가 형식문 \(\text{Dem}(x,z)\) 으로 사상된 것은 \(3=1+2\) 가 형식문 \(sss0=s0+ss0\) 로 사상된 것과 비슷한다. 그래서 사실은 \(\text{Dem}(x,z)\) 도 다음과 같이 써야 하지만 편의상 축약하여 쓰는 것이다.

  \[\text{Dem}(\overbrace{sss\dots{}sss0}^{x},\overbrace{sss\dots{}sss0}^{z})\]

대입함수✔

형식문에 괴델수 붙이기에서 형식문 "\((\exists{}x)(x=sy)\)" 이 괴델수 \(m\) 을 갖는다고 가정했었다. 이 형식문의 숫자변항 \(y\) 에 \(2\) 를 대입하면 "\(2\) 다음 수 \(x\) 가 존재한다" 고, 즉 "3 이 존재한다" 고 주장하는 형식문

을 얻을 수 있다. 이 형식문에도 괴델수를 붙힐 수 있으므로 그 괴델수를 \(t\) 라고 하자. 똑같은 방식으로 형식문 "\((\exists{}x)(x=sy)\)" 의 \(y\) 에 괴델수 \(m\) 을 대입하여 형식문

을 만들어보자. 그러면 이 형식문은 단순히 "\(m\) 다음 수 \(x\) 가 존재한다" 고, 즉 "\(m+1\) 이 존재한다" 고 주장한다. 이 형식문에도 괴델수를 붙힐 수 있으므로 그 괴델수를 \(r\) 이라고 하자.

이처럼 괴델수 \(m\) 을 갖는 형식문에 등장하는 모든 \(y\) 에 \(2\) 를 대입하여 얻은 형식문의 괴델수 \(t\) 와 \(m\) 를 대입하여 얻은 형식문의 괴델수 \(r\) 을 계산하는 함수를 각각

라는 대입함수로 표현할 수 있다. \(y\) 에 해당하는 괴델수가 17 이므로 두번째 인자가 17 인 것이다.

• 대입(substitution)의 줄임말이다.

이 대입함수 \(\text{sub}(x,17,x)\) 또한 수들의 산술학적 관계를 표현하므로 형식문으로 사상될 수 있다. 그 형식문을 \(\text{Sub}(x,17,x)\) 이라고 하자.

이제 괴델의 증명을 이해할 준비가 모두 끝났다.

3. 핵심 논증✔

괴델의 핵심 논증은 다음의 5 가지 단계로 요약된다.

1. "형식문 \(G\) 는 PM 으로 증명할 수 없다" 는 상위 수학명제를 PM 속의 수학명제로 사상시킨 형식문 \(G\) 가 있다.

2. 형식문 \(G\) 는 그 부정문 \(\ssim G\) 이 증명될 수 있을 때에만 증명될 수 있다.

3. 형식문 \(G\) 는 증명될 수 없지만 올바른 형식문이다.

4. (제 1 불완전성 정리 증명) 형식문 \(G\) 가 옳으면서도 증명될 수 없으므로 PM 은 불완전 체계이다.

5. (제 2 불완전성 정리 증명) "PM 은 정합적 체계이다" 라는 상위 수학명제를 PM 의 형식문 \(A\) 로 사상시키고 형식문 \(A\to{}G\) 가 PM 속에서 증명될 수 있다는 것을 보인다. 이로써 형식문 \(A\) 가 PM 속에서 연역될 수 없다는 것을 보인다.

   • \(A\) 가 증명될 수 있다면 분리규칙에 의하여 \(G\) 도 증명되버리는데, \(G\) 가 증명된다면 PM 은 모순을 도출하는 체계가 된다. 그러므로 PM 의 정합성은 PM 자신의 형식적 추론으로 확립될 수 없다는 것이다.

자기 자신이 증명될 수 없다고 주장하는 형식문 G✔

상위 수학명제 "괴델수 \(z\) 를 가진 형식문은 증명할 수 있다"를 생각하자. 이 상위 수학명제는 "괴델수 \(z\) 를 가진 형식문을 증명하는 괴델수 \(x\) 를 가진 형식문 모임(증명)이 존재한다" 와 같다. 그러므로 "\(z\) 를 증명할 수 있다" 라는 상위 수학명제를 "\(z\) 에 대한 증명 \(x\) 가 존재한다" 고 주장하는 형식문

으로 사상시킬 수 있다. 그렇다면 "\(z\) 를 증명할 수 없다" 라는 상위 수학명제는 "\(z\) 를 증명하는 형식문 모임 \(x\) 가 존재하지 않는다" 고 주장하는 형식문

으로 사상시킬 수 있다. 그러면 숫자변항 \(z\) 에 괴델수 \(\text{sub}(y,17,y)\) 를 가진 형식문을 대입하여

를 만들 수 있다. 이 형식문을 \(S\) 라고 하자. 형식문 \(S\) 는 단순히 "괴델수 \(\text{sub}(y,17,y)\) 를 가진 형식문은 증명될 수 없다" 라고 주장한다. 형식문 \(S\) 에 대응하는 괴델수를 \(n\) 이라고 하겠다. "\(S(n):\)" 은 단순히 형식문과 그 괴델수를 의미하며 실질적인 형식문에 포함되지 않다. 가독성을 높히기 위하여 편의상 추가한 것이다. 콜론(:) 오른쪽 부분부터 실질적인 형식문이다.

그렇다면 형식문 \(S\) 의 숫자변항 \(y\) 에 괴델수 \(n\) 을 대입하여 형식문

을 만들 수 있다. 이 형식문을 \(G\) 라고 하자. 그리고 형식문 \(G\) 의 괴델수를 \(g\) 라고 하자.

그런데 이 형식문 \(G\) 는 괴델수 \(n\) 을 가진 형식문의 모든 변항 \(y\) 에 \(n\) 을 대입하여 만들어졌기 때문에 대입함수 \(\text{sub}\) 의 정의에 따라 괴델수 \(\text{sub}(n,17,n)\) 를 가진다. 그러므로

이다. 그렇다면 놀랍게도 형식문 \(G\) 는

가 되므로 "괴델수 \(g\) 를 가진 형식문은 증명될 수 없다", 즉 쉽게 말해 "이 명제는 증명될 수 없다" 라고 주장하고 있는 것이다. 형식문 \(G\) 는 자기 자신이 증명될 수 없는 형식문이라고 말하고 있는 것이다.

PM 이 정합적 체계라면 형식문 G 는 PM 에 의하여 증명될 수 없다✔

이제 우리는 PM 이 정합적 체계라면 형식문 \(G\) 는 증명될 수 없다는 논증에 도착했는데, 이 논증은 쉽다. 형식문 \(G\) 와 그 부정문이 다음과 같은 의미를 가진다는 것만 기억하면 된다.

• 만약 형식문 \(G\) 가 증명된다면 "\(G\) 는 증명된다"고 말한 부정문 \(\ssim{}G\) 이 증명된다.
• 반대로 "\(G\) 는 증명된다"고 말한 부정문 \(\ssim{}G\) 이 증명된다면 \(G\) 가 증명되는 것이다.

그러므로 우리는 형식문 \(G\) 가 그 부정문 \(\ssim{}G\) 이 증명될 경우에만 증명된다는 결론을 얻는다. 그런데 어떤 형식문과 그 부정문이 동시에 연역되면 그 형식 체계는 부정합 체계이다. 따라서 우리는 PM 이 정합적 체계라면 형식문 \(G\) 와 \(\ssim{}G\) 가 둘 다 PM 에 의하여 증명될 수 없다는 결론에 도달한다.

형식문 G 는 증명될 수 없지만 참이다✔

하지만 "나는 남자이다" 와 그 부정문 "나는 남자가 아니다" 중에서 단 하나만 올바른 명제가 되어야 하듯이 형식문 \(G\) 와 부정문 \(\ssim{}G\) 은 둘 중 하나만 옳아야 한다.³

그런데 \(G\) 와 \(\ssim{}G\) 가 둘 다 PM 에 의하여 증명될 수 없으므로 둘 중 무엇이 올바른지 알 수 없을 것만 같다. 하지만 이것을 밝히는 일은 생각보다 간단하며 다음과 같이 수학명제에 관하여 언급하는 상위 수학명제들에 의하여 증명될 수 있다.

• 형식문 \(G\) 의 상위 수학명제로써의 의미는 "PM 속에 \(G\) 의 증명이 없다." 이다.

• 그런데 우리는 방금전에 "PM 이 정합적 체계라면 \(G\) 가 PM 에 의하여 증명될 수 없다" 는 것을 밝혔는데, 이것이 바로 \(G\) 가 주장하는 것이다.

• 그러므로 PM 이 정합적 체계라는 가정 하에서 형식문 \(G\) 는 참이다.

또한 이로써 어떤 명제들은 공리 체계의 공리와 추론 규칙에 의하여 증명될 수 없고 그것에 관하여 언급하는 상위 논증을 통하여 증명된다는 것을 알 수 있다.

(제 1 불완전성 정리) PM 이 정합적 체계라면 PM 은 불완전체계이다✔

드디어 우리는 괴델의 제 1 불완전성 정리의 증명에 도달했다.

• 어떤 체계가 완전 체계라는 것은 그 체계에 의하여 표현될 수 있는 올바른 명제들이 그 공리와 추론규칙에 의하여 형식적으로 연역될 수 있다는 것이다.

• 그런데 PM 이 정합적 체계라면 형식문 \(G\) 는 PM 속에서 형식적으로 연역될 수 없다.

• 그럼에도 불구하고 \(G\) 는 참인 명제이다.

• 그러므로 PM 이 정합적 체계라면 PM 은 불완전 체계이다.

이로써 제 1 불완전성 정리가 증명되었다.

이뿐 아니라 PM 이 불완전 체계인 것은 우연히 그렇게 된 것이 아니고 본질적으로 불완전하기 때문에 불완전 체계가 된 것이다. 가령 형식문 \(G\) 를 증명하기 위하여 공리와 추론규칙을 추가한다고 하더라도 또 다시 참이면서 증명할 수 없는 또 다른 형식문 \(G'\) 가 탄생한다. 왜냐하면 또 다른 공리와 추론규칙이 추가된 체계에서의 증명 개념은 PM 보다 더 복잡할 것이지만, 그것으로 새로운 증명함수 \(\text{dem}'(x,z)\) 로 표현할 수 있고, PM 에서 참이면서 형식적으로 결정될 수 없는 형식문 \(G\) 를 만든 방식과 똑같은 방식으로 새로운 형식문 \(G'\) 를 만들 수 있기 때문이다. 이렇게 공리와 추론규칙을 끝없이 추가한다고 하더라도 끝없이 참이지만 증명할 수 없는 형식문 \(G'',G''',G'''',\dots\) 들이 탄생하게 된다. 이것이 PM 이 본질적으로 불완전 체계라는 의미이다.

이 사실은 수학자들에게 청천벽력이었다. 왜냐하면 이것은 PM 에만 적용되는 것이 아니라 러셀의 『수학 원리』 를 비롯하여 자연수의 덧셈과 곱셈같은 자연수의 기본속성을 포괄할 수 있는 모든 공리 체계에 적용되었기 때문이다.

이로써 수학을 완전한 연역 체계로 만들어서 완전 체계로 만들려는 꿈은 산산조각이 났고, 수천년전 고대 그리스로부터 내려오던 공리적 방식에 대한 믿음이 철저하게 배신당했다. 왜냐하면 모든 산술학적 진리를 PM 의 공리와 추론 규칙으로 연역할 수 없다는 것이 드러났기 때문이다. 그런데 모든 수학 분야(기하학, 해석학 등)가 산술에 기초를 두고 있으므로 결국 모든 수학의 사실들을 그 체계의 공리와 추론규칙으로 연역할 수 없다는 것이 드러난 것이다. 결론적으로 이것은 수학적 사고의 본질이 순수하게 형식화된 공리적인 추론이 아니었다는 것을 알려주었다. 이것은 마치 기계적으로 사고하고 생각해서는 수학을 발전시킬 수 없고, 프로그램을 코딩할 수 없다는 것을 뜻한다. 쉽게 말해서, 체계 안에서의 논리만 다루어서는 새로운 진리를 창조해낼 수 없고, 새로운 프로그램을 코딩해낼 수 없고, 체계에 관하여 생각하는 상위 체계, 그리고 또 다시 그 상위 체계에 관하여 생각하는 고차원적인 생각을 해야한다는 것이다.

(제 2 불완전성 정리) "PM 은 정합적 체계이다" 라는 주장은 PM 의 체계로는 증명할 수 없다✔

이제 우리는 "PM 이 정합적 체계이면 PM 은 불완전 체계이다"라는 상위 수학명제를 얻었다. 이 상위 수학명제를 \(B\) 라고 하자. 이때 \(B\) 의 조건절 "PM 은 정합적 체계이다"를 명제 \(A\) 로 표현하고, \(B\) 의 귀결절 "PM 은 불완전 체계이다"를 명제 \(X\) 로 표현하자. 그렇다면 \(B\) 는 \(A\to{}X\) 이다.

• \(B\) 의 조건절 명제 \(A\) "PM 은 정합적 체계이다" 를 형식문으로 사상시키기

  그런데 상위 수학명제 \(A\) 는 매우 쉽게 PM 속의 형식문으로 사상될 수 있다. 왜냐하면 PM 이 정합적 체계라는 것은 "PM 속에 증명될 수 없는(형식적으로 연역될 수 없는) 형식문이 적어도 하나 있다" 라는 상위 수학명제와 같기 때문이다.

  이 진술은 "어떤 \(x\) 와도 \(\text{dem}\) 함수 관계를 맺지 못하는 괴델수 \(y\) 가 적어도 하나 있다"라는 수학명제로 사상된다. 쉽게 말해서 증명에 해당하는 괴델수 \(x\) 가 없는 \(y\) 가 존재한다는 말이다.

  그렇다면 이 상위 수학명제 \(A\) 는 "괴델수 \(y\) 가 존재하는데, \(y\) 는 증명에 해당하는 괴델수 \(x\) 가 없는 괴델수야"라고 주장하는 수학명제

  \[A:(\exists y)\ssim(\exists x)\text{Dem}(x,y)\]

  으로 표현할 수 있다.

• \(B\) 의 귀결절 명제 \(X\) "PM 은 불완전 체계이다." 를 형식문으로 사상시키기

  상위 수학명제 \(X\) 도 쉽게 PM 속의 형식문으로 사상시킬 수 있다. 왜냐하면 "PM 은 불완전 체계이다"라는 것은 올바르지만 증명될 수 없는 형식문 \(T\) 에 대하여 "\(T\) 는 PM 의 정리가 아니다" 라고 말하는 것과 같기 때문이다.

  그런데 우리는 형식문 \(T\) 를 너무 잘 알고 있다. \(T\) 는 올바르지만 증명될 수 없는 형식문이기 때문에 지금까지 우리가 다뤄왔던 형식문 \(G\) 이다. 그러므로 "PM 은 불완전 체계이다" 라는 것은 "\(G\) 는 PM 의 정리가 아니다" 와 같다.

  그런데 놀랍게도 형식문 \(G\) 가 주장하는 것이 "\(G\) 는 증명될 수 없다" , 즉 \(G\) 는 PM 의 정리가 아니라는 것이기 때문에 상위 수학명제 \(X\) 는 곧 \(G\) 이다.

  정리란 공리로부터 연역된 형식문, 즉 공리와 추론규칙을 통해 증명된 형식문이다. 따라서 증명될 수 없는 형식문은 정리가 아니다.

그러므로 우리가 얻은 상위 수학명제 \(B\) "PM 이 정합적 체계이면 PM 은 불완전 체계이다"를 완벽하게 순수한 수학명제 \(A\to{}G\) 로 사상시킬 수 있다. 즉, 형식문

로 사상시킬 수 있는 것이다. 이제 제 2 불완전성 정리를 증명하는 일만 남았다.

• 만약 PM 속에서 \(A\) 가 증명될 수 있다면 분리규칙에 의하여 \(G\) 도 증명된다.

• 그런데 PM 이 정합적 체계라면 \(G\) 는 형식적으로 결정될 수 없어야 한다. 즉, \(G\) 는 PM 에 의하여 증명될 수 없어야 한다.

• 그러므로 PM 이 정합적 체계라면 \(A\) 는 PM 에 의하여 증명될 수 없다.

결론적으로 "PM 은 정합적 체계이다" 라고 말하는 \(A\) 는 PM 에 의하여 증명될 수 없는 것이다. 이로써 제 2 불완전성 정리가 증명되었다.

이로써 우리는 PM 이 정합적 체계라면 PM 의 정합성이 PM 에 사상될 수 있는 그 어떠한 상위 수학적 추론으로도 증명될 수 없다는 결론에 도달한다. 왜냐하면 PM 의 정합성에 대한 증명이 PM 의 수학명제로 환원된다면 그것은 \(A\) 를 증명하는 꼴이 되고 결국 \(G\) 도 증명하는 꼴이 되며 최종적으로 PM 에 정합성이 없다는 말이 되기 때문이다. 하지만 \(G\) 가 PM 에 의해서가 아니라 상위 수학적 추론에 의하여 참이라는 것이 증명된 것처럼 PM 의 정합성도 PM 으로 사상되지 않는 상위 수학적 추론에 의하여 증명될 수 있다.

실제로 PM 과 관련 체계들의 정합성을 확립하는 상위 수학적 증명은 1936년 겐첸에 의하여 이루어졌고, 이후 다른 수학자들에 의해서도 이루어졌다. 겐첸은 PM 의 모든 증명을 "단순성" 의 정도에 따라 선형 순서로 배열한 다음 이 선형 순서에 "초한 귀납 원리" 라는 추리 규칙을 적용하여 PM 의 정합성을 증명했다. 이 논증은 PM 속으로 사상될 수 없는 것이었다. 겐첸의 상위 수학적 증명은 수학에서 매우 중요한데, 그 증명이 새로운 형태의 상위 수학적 체계를 보여주었고, 그 상위 수학적 체계가 PM 과 관련 체계의 정합성을 확립하기 위하여 추론 규칙을 어떻게 확장해야 하는지 보여주었기 때문이다.

불완전성 정리의 의미✔

이로써 괴델은 공리와 추론규칙으로 형식적으로 연역될 수 없지만 올바른 산술학적 진리가 무수히 많다는 것을 보였다. 이 사실은 유클리드가 시작하였고 고대 그리스로부터 1900년대까지 내려오던 "공리적 방식" 으로 수학을 연구한다면 수학의 본질을 완전히 해명할 수 없다는 혁명적이고 충격적인 결론을 알려주었다.

모든 진리가 가장 저차원적인 존재로부터 기계적으로 생성된 것이 아니라면 모든 진리는 어디에서 생성되는 것인가?

또, 이 사실은 인간이 수학을 이해하는 방식이 형식화된 공리적 방법처럼 미리 정의된 명확한 공리와 변형규칙으로부터 결론에 도달하는 것과 일치하지 않는다는 인공지능 연구자들에게도 중요한 사실을 알려주었다. 인간의 지능은 완전히 형식화될 수 없을만큼 깊이 있는 것이다.

이 불완전성 정리에서 아이디어를 얻어서 튜링이 튜링기계를 만들고 그것이 결국 컴퓨터가 되었다. 컴퓨터와 프로그램은 유한개의 명령을 따라 작동하는 기계인데, 이 유한개의 명령은 형식화된 공리 체계에서 사용하는 한정된 수의 추론 규칙에 해당하고, 입력되는 데이터가 공리의 역할을 한다. 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 증명이 어떤 논리식을 연역해나가는 과정이라면, 프로그램은 어떤 데이터를 만들어내는 과정이다.

그런데 괴델의 불완전성 정리는 일정한 틀 속에서만 움직이는 공리적 방법으로는 해결할 수 없는 문제가 무수히 많다는 것을 알려주었고, 프로그램이란 PM 속에서 진행하는 형식적 논증이기 때문에 프로그램으로는 모든 문제를 해결하고 자동화할 수 없다는 것을 알 수 있다.

산술의 무모순성 증명✔

해석학, 기하학, 대수학 등의 무모순성이 산술(페아노 공리계, Peano Arithmetic, PA)의 무모순성으로 귀결된 이후 수학자들은 여러가지 방법으로 산술의 무모순성을 증명하려 했다. 괴델은 PA 를 포함할 수 있을만큼 강력한 공리체계의 무모순성은 그 공리체계로 증명할 수 없다는 괴델의 불완전성 정리를 보였다. 이에 따라 겐첸이 1936, 1938년에 PA 로 형식화 할 수 없는 초한귀납법으로 PA 의 무모순성을 증명했다. 이 내용을 \(\mathsf{PA}\) 의 서수 분석에서 엄밀하게 알아본다.

이후 1940년에 아커만이 또 다른 무모순성 증명을 보였고, 1951년에는 Schutte 도 산술의 무모순성 증명을 보였다. 이 내용은 공리적 집합론에서 초보적으로 간단하게 다룬다.