Godel Imcompleteness: 두 판 사이의 차이

DoMath
 
(차이 없음)

2008년 4월 13일 (일) 23:38 기준 최신판

  • 한글 제목 : 괴델의 증명
  • 원제 : Godel's Proof (1983)
  • 지은이 : Ernest Nagel (Columbia Univ)
  • 번역 : 강주헌
  • 출판사 : 경문사 (2003)


서문

1931년 독일의 과학 저널에 Uber formal unentscheidbare Satze der Principia Mathematica und verwander Systeme (프린키피아 마떼마찌까와 관련 체계에서 형식적으로 결정할 수 없는 명제에 대하여 ) 발표. 25세 빈 대학 Kurt Godel (1906 - 1978).

기하학의 axiomatic method 는 시대마다 사색가들에게 영향 : 적은 공리로 끊없이 많은 정리를 만들어 내기 때문. 공리가 참이라면 정리도 참이고 그 적합성도 보장 된다. 과학적 지식이 지닐 수 있는 최적의 모델이었다. 기하학에서 발달한 이 방법은 다른 학문도 확실한 공리적 기초 위에 세울 수 있는가라는 질문 던졌을 것이다. 그래서 참된 명제를 계속 끌어내기에 충분한 몇 개의 공리 체계를 만들 수 있을 것이라는 암묵적 믿음.

괴델은 이런 믿음이 잘못된 것임을 증명해 보였다. 공리적 방법이 일정한 내재적 한계를 가지기 때문에 정수 세계 조차 순수하게 공리화 할 수 없다. 연역 체계 자체의 무모순성 마저 증명할 수 없다. 또한 수학적 사고에서 커다란 위치를 차지하는 많은 분야가 내적 모순에서 완전히 벗어날 수 있다는 절대적인 보장도 있을 수 없다. : 이를 위해 그는 데카르트가 기하학에 도입했던 대수적 방법에 견줄만한 새로운 분석법을 적용했다.

무모순성의 문제

수학사에서 19세기는 양과 질에서 놀라운 발전 이뤄 냄. 요지부동이던 근본적인 문제들이 해결, 새로운 연구 분야들 줄줄이 탄생. 고전 3 대 문제, 5차 이상의 방정식 해 문제, ... 소중한 부산물도 함께 얻었다. 어떤 방정식을 만족하는 근(root) 의 종류를 결정하는 것에 따라 해결책이 달라지기 때문에, 자연히 수의 성격과 수의 연속체의 구조를 심도 있게 연구하는 자극제가 되었다. 그 결과로 음수, 복소수, 무리수를 엄격하게 정의할 수 있었고 실수 체계에 대한 논리적 기초가 마련되었으며 새로운 분야로 무한수 이론 을 제안하게 되었다.

평행선 공준에 대한 문제도 풀린다. 가우스, 보야이, 로바체프스키, 리만의 연구. 고대 그리스에서도 이 공리는 자명한 것으로 받아들여질 수 없었다.  : 그 공리가 무한히 계속되는 공간을 전제로 사실에 바탕한 것 같다. 유클리드는 평행선을 '양 방향으로 무한히 이어지더라도' 서로 만나지 않는 평면 위의 직선으로 정의 했다. 그런데 옛사람들은 두 직선이 유한한 평면에서는 서로 교차하지 않더라도 '무한점'에서는 틀림없이 만나는 직선에 익숙해 있었다. 소위 '점근선'이라는 것이다. 예를들면 쌍곡선은 그 축을 중심으로 점근선이 된다. (메모 : 지은이가 이렇게 쓴 근거가 뭐지?)

공리는 자명함이라는 믿음이 뿌리째 흔들렸다. 그래서 수학의 진정한 목표는 공리화된 가정에서 정리를 유도하는 것 이란 의식이 뚜렷해지기 시작했다. 또 수학의 다른 분야에도 공리 재검토하고 완비하는 촉매 역할을 했다.

이처럼 비판적인 안목에서 수학의 기초를 연구한 결과, 수학을 "science of quantity" 라고 생각하던 과거의 관념이 부적절하다고 깨달았다. 몇개의 공리에서 논리적으로 함축된 결론을 끌어내는 진정한 의미에서의 학문이라는 생각이 분명해지게 되었다.

힐버트는 point, line, lie on , between 같은 용어를 정의 없이 썼다. primitive term 으로. 러셀은 "순수 수학은 우리가 지금 무엇에 대해 말하고 있는지도 모르는 학문이다. 또한 우리가 말하는 있는 것이 참인지도 모르는 학문이다. " 수학을 형식화 함으로써, 익숙했던 이정표를 없애고 추상으로 가득한 땅에 있게 된 셈이다. 돌아다니기는 쉽지 않지만 자유롭고 새롭게 세상을 바라볼 수 있게 되었다. 직관이 과학적 탐구엣 진실 판단이나 성과의 기준이 되서는 안된다. 직관이 뒤집어지는 경우도 많고, 예전엔 직관적이지 않던 것이 세대가 지나면서 '뻔한' 것이 되기도 할 만큼 '직관'은 낭창낭창하다.

하지만 추상화 정도가 심해지면서 심각한 문제를 제기했다. 공준의 집합체가 모순이 없는가? 그 문제 해결을 위해 '모델'을 찾아내는 방법이 고안되었다. 유클리드 기하학의 경우 일상적인 공간이 모델이었다.
파일:Triangle Model.svg

K, L 이라는 두 class 가 있고 그것에 대한 공리가 있다고 하자.

  • (ax 1) K 에서 임의의 도 원소는 L 의 단 하나 원소에 포함된다.
  • (ax 2) K 의 어떤 원소도 L 의 도 원소 이상에 포함되지 않는다.
  • (ax 3) K 의 원소 모두가 L 의 단 하나의 원소에 포함되는 것은 아니다.
  • (ax 4) L 에서 임의의 두 원소는 K 에서 하나의 원소만을 포함한다.
  • (ax 5) L 의 어떤 원소도 K 의 두 원소 이상을 포함하지 않는다.

이로부터 정리를 뽑아낼 수 있다. 예 : "K는 세 개의 원소만을 포함한다"

이것은 무모순일까? 모델을 세워서 모순이 아니라는 것을 보일 수 있다. K 를 삼각형의 꼭지점들의 class, L 을 변의 class 로 하고, '포함'의 개념을 '선 위에 놓인다.' 로 하면 된다. 비유클리드 기하학의 모델도 이와 같은 방법이다. 하지만, 문제는 아직 남았다. 유클리드 기하학이 무모순이어야만 한다. 수천년 동안 그렇게 해왔으니 그냥 믿을 만 하다고 여기거나 우리가 사는 실제 경험과 일치하기 때문에 괜찮다는 식의 논거는 취약하다.

힐버트는 Cartesian coordinate geometry 의 도움을 받아, 유클리드 공리를 대수적 참값으로 변환하였다. 예를들어 점을 수의 쌍으로, 직선을 1차 방정식으로. 표현할 수 있는 수 사이의 관계(1차적 관계) . 다른 두 점을 지나는 직선은 하나다. 라는 공리는 " 서로 다른 두 쌍의 수는 오로지 하나의 1차 관계식을 만들어낸다" 로 바꿀 수 있다. 하나의 직선과 원의 교점은 최대한 두 개다라는 정리는 " 이 둘을 나타내는 방정식을 모두 만족하는 해는 최대 두쌍이다. " 로 바뀐다. 유클리드 공리를 대수 모델로 보였고, 따라서 유클리드 기하학의 무모순성이 입증 되었다. 그러나 대수의 무모순성은?

이런 시도는 언제나 어려움이 도사리고 있다. 즉, 공리는 끝없이 많은 원소로 이루어진 모델로 해석되어야 한다는 점이다. 무한번 관찰해서 모델을 검토한다는 것은 사실상 불가능하다. 따라서 공리 차제의 진위는 언제나 의혹의 대상일 수 밖에 없다. 앞의 삼각형 모델은 원소가 유한 개라 서로 모순이 안되는 것을 판별하기란 쉽니다. 꼭지점을 하나씩 보면서 변 에 있다는 것을 확인할 수 있다. 하지만, 대부분의 수학 분야는 유한 모델로 안된다. " 모든 정수는 바로 다음에 오는 정수가 있고 그 정수는 앞에서 사용된 어떤 정수와도 다르다" 는 산술의 공리를 보자. 일일이 원소를 비교해서 볼 수 없다. 그래서 "명백하고 뚜렷한 개념" 으로 충분히 믿을만 하고, 그래서 모순이 없다고 말할 수 있지만, 그것도 여전히 취약하다. 칸토르 무한수 이론 (메모 : set theory 와 cardinal number 에 대한 것이었군...) 에 대한 러셀의 antinomy를 보라. 그 자신을 포함하지 않은 집합을 좋은 집합으로, 그 자신을 포함하는 집합 (예를들어 "생각할 수 있는 모든 것" 의 집합)을 나쁜 집합으로 보고, 모든 좋은 집합들의 집합은 좋은 집합인가 나쁜 집합인가?

치명적인 모순은 집합이란 명백한 개념을 무비판적으로 사용한 데서 왔다. 수학자 들이 패러독스에서 깨달은 것이 있다면, 모순 없는 체계를 발전시키는 데 친숙성이나 직관은 의존하기엔 너무 허약한 갈대라는 것.

무모순성의 절대적 증명

수학적 표준 공식이 모두 내적인 모순을 가지고 있을지도 모른다는 깨달음이 커지면서 앞에서 한 것 같은 '상대적' 증명을 하지 않고 '절대적 absolute ' 증명을 시도한다. 힐버트는 그 첫 단계로 연역 체계를 complete formaization 로. (메모 : 말은 많은데 결국 logic - calculus 에 대한 말이다.) 그는 meta-mathematics 라 불렀다. 의미없는 부호들의 체계로 formula 를 짜들어가고...

math 와 meta-math의 구별이 중요하다. 그 둘을 분명하게 구분하지 못해서 패러독스와 혼돈이 있었던 것이다. 이 둘을 구분하여 인식함으로써 수학적 추론의 논리적 구조를 분명히 했다. 이는 체스 게임 시작 전 말들의 위치는 공리고, 체스가 진행되어가면서 있는 말들의 위치는 정리 . 게임의 규칙은 (메모 : Modus Ponens 같은) 추론 법칙. meta-chess 적 진술은 '백군의 경우 이동의 가능성이 몇가지다', '세 수가 지나면 외통수 일 것이다' 들이다.

형식 논리학의 체계적인 코드화 작업

아리스토텔레스의 전통 논리학은 견고했다. 하지만 불완전하기 그지 없다. 5는 3보다 크다. 그래서 5의 제곱은 3의 제곱보다 크다라는 추론에 관계하는 원리도 설명할 수 없다. 그러나 1847년 G. Boole 이 The mathematical analysis of Logic 출간되면서 현대적 시각에서 논리학 연구 부활. 전통 논리학에서보다 일반적이고 다양한 유형의 추론을 설명할 정확한 표기법을 제시. '대수적으로' 논리 문제를 풀어갈 수 있다.

1910년 Whitehead 와 Russell 의 '프린키피아 마떼마찌까(Principia Matematica)' 에서 수학의 다양한 개념들이 정수와 그 연산으로 정의할 수 있다는 것을 보여주었다. 예를들어 허수 i 를 신비로운 '실재물'로 받아들이기 보다 덧셈과 곱셈의 연산이 행해지는 정수 (0,1) 의 순서쌍으로 정의하고 는 제곱값이 2 보다 작은 유리수 집합으로 정의. 프레게, 러셀은 arithmetic 의 개념을 순수하게 논리적 개념으로 정의하고, 그 정리들을 순수하게 논리적 참값인 소수의 기본 명제에서 추론될 수 있다는 것을 보이려 했다. 그 책은 무모순의 연구에 큰 영향을 끼치기만 한 것이 아니라, 엄청난 표기 체계를 제시했다. 따라서 그것을 코드화 할 수 있는 기초가 되었다.


무모순의 절대적 증명의 성공 사례

formalization 의 네 단계 : formula 를 위해 필요한 부호들 지정. vocabulary , 문장 결합의 원칙 결정, primitive formula 에서 어떻게 변형할 것인지 규칙 결정. 이것으로 추론을 할 수 있고 정리를 이끌어 낼 수 있다. 마지막으로 공리를 선택한다.(메모: 이렇게 해서 Propositional Logic, First order logic (Predicate Logic ) 이 생긴다. 그 위에 쌓아 올릴 수 있다.) 이제 공리로 부터 정리들을 이끌어낸다. 무모순의 '절대적 증명' 이란, 그런 과정에서 어떤 문장 를 동시에 유도할 수 없음을 증명하는 것을 말한다.

다음 정리를 명제논리에서 유도할 수 있는 정리다.
따라서 우리가 만약 를 동시에 유도한다면 '치환 규칙'(substitution rule)에 따라, 항상, 어떤 문장이든 상관 없이 를 얻을 수 있다. 따라서 어떤 공리체계가 모순이면 거기서는 어떤 문장이든 이끌어 낼 수 있다는 말이 되버린다.

이를 뒤집어 보면, 모든 정리가 다 유도될 수 없다면 그 공리체계는 모순이 없다는 것을 뜻한다. 즉 절대적 증명은 공리에서 유도될 수 없는 공식이 적어도 하나가 있다는 것을 보여주는 것이 핵심이다. 이 과정을 요약해서 쓰면 이렇다.

- 체계의 모든 공리는 tautology(항상 참인 문장) 다. (메모 : 가 공리라면,)
- tautology 는 hereditary 하다. (메모 : 가 모두 tautology 면 T 도 그렇다. )
- 정리(공리에서 추론 규칙에 따라 나온 formula)도 tautology다.
- 메모 :  : soundness or consistency
- 다시 말해, tautology 가 아닌 formula은 정리가 아니다.
- tautology 아닌 formula 를 찾는다. 이것은 정리가 아니다. 이것이 공리체계가 무모순하다는 것을 말하는 것과 같다.

무모순과 함께 complete도 중요하다. 참인 모든 명제를 공리 체계에서 유도(증명)할 수 있을까? Arithmetic 의 공리는 완전하거나 아니면 몇개를 덧붙이면 complete 해질 것이라 믿었다. 하지만 괴델은 그런 생각을 잘못이라고 밝힌 것이다.

(메모 :유클리드가 공리 체계를 세울 때, 참이 되는 모든 기하하작적 문장을 유도할 수 있도록 공리를 정하려고 노력했을까? 어쨌든 ) 유클리드는 놀랍게도 평행성 공리가 다른 공리들과 대등하게 독립적인 가설로 다루었다. (메모 : 그리고 그 숱한 논리적으로 같은 명제를 선택하지 않고 바로 이런 '두 직선의 관계와 교점의 관계'로 된 문장을 선택했다. ) 이 공리는 다른 공리들로 증명할 수 없다. 따라서 이 공리를 공리 체계에 넣지 않았다면 유클리드 공리 체계(메모 : absoulte geometry)는 불완전한 것이 자명하다.

사상 개념과 수학에의 응용

sentence calculus 는 힐버트의 증명이론이 목표로 했던 것을 실현한 수학 체계의 예다. 그런데 그것이 절대적 무모순을 증명하기에 충분히 설득력이 있나? 그 대답을 구하기 위해 애썼지만, 번번히 실패했고, 괴델이 최종적으로 '불가능'을 보인 것이다. 게다가 힐버트 계획에 제시한 엄격한 제한 범위 안에서는 어떤 노력도 실패할 수 밖에 없다는 것을 말한다.

참인 것이 분명해보이지만, 증명하지 못하는 사례들은 많다. 그 중 골드바흐 정리 가 대표적인 것이다.

1905년 프. 쥘 리샤르 Jules Richard 가 제창해서 '리샤르 패러독스' 란 이름으로 알려진 논리적 이율 배반에 대한 추론법을 어느 정도 모방하고 있다.

  • 산술에 대한 모든 성질을 한국말로 '원칙을 정해서' 유일한 방법으로 표현한다고 하자. 끝없이 많지만 셀 수 있을 게 분명하다.
  • 이런 표현을 어떤 numbering 으로 정수로 바꿀 수 있을 것이다. 하나의 성질은 하나의 수로 바뀐다.
  • 예1 : "어떤 수의 제곱이 되는 수" 는 49에 대응시킨다.
  • 예2 : "1과 그 자신 이외의 어떤 정수로 나뉠 수 없는 수" 는 15에 대응시킨다.
  • 예3 : " 유일한 방법으로 소수로 분해된다." 는 3882 에 대응 되었다고 하자.

그렇다면 모든 자연수는 '어떤 성질'을 나타내고 있다. 그런데 두 종류로 나눌 수 있다. 예1과 예3의 경우, 49나 3882 은 '성질을 나타내는 그 수'가 그 성질을 갖고, 15는 그가 지시하는 성질을 나타내지 않는다. 이렇게 어떤 수 n 이, 그 자신이 내포하는 성질을 갖고 있지 않을 때, 이 수를 리샤르적인 수라고 하자. 그렇다면 질문 : 리샤르적이다 라는 것을 뜻하는 수 n 은 리샤르적인가 아닌가?

  • n 이 리샤르적이라, '리샤르적이라는 말의 뜻에 따라, ' 그 자신이 나타내는 성질(리샤르적이다)을 가지지 않는다. 따라서, 리샤르 적이 아니다.
  • n 이 리샤르적이 아니라면, '그 자신이 지시하는 성질을 갖지 않는 수이므로, 리샤르적이다.

패러독스처럼 보이는 위의 문장에서 '속임수'는 어디에 있는가? 바로, '리샤르적이다' 라는 말은 math 의 영역이 아니라, meta-math 영역의 진술이다 ' 라는 데 있다. '리샤르적이다' 라는 말을 arithmetic 의 범위 안에 있는 문장을 numbering 한다고 해놓고, meta-arithmetic 한 성질에 대해 '부당하게' 특권을 준 것이다. 그럼에도 불구, 리샤르 패러독스는 아주 중요한 의미를 갖는다. 왜냐하면 모든 산술적, 또는 더 넘어 초산술 명제를 수로 mapping 할 수 있도록 생각을 텄다. 이와 같은 mapping 은 개념은 수학, 과학에서 매우 중요한 의미를 갖는다. 물리적 현상도 모델을 세워서 실험하고 결과를 수학적 모델로 설명하는 것도 그렇고 projetive geometry 에서 projection 도 그렇다, (메모 : mapping 은 function 의 다른 말이라 두 말하면 잔소리다. 모든 수학, 수학적 사고의 기초 중 기초라. )

괴델은 리샤르 패러독스의 추론법을 따르면서, 그 과정에서 가능한 모든 오류를 제거하기 위해 극도로 신중했다. 그리고하여 그는 형식화된 산술식에 대한 meta-math 적 명제가 산술 공식으로 표현할 수 있다는 것을 보였다. 더 나아가, 어떤 '무모순하다' 라는 말과 같은 meta-math적인 명제에 mapped 산술식 또는 그것의 '무모순이 아니다' 에 대응하는 산술식도 '공리화된 산술 체계'에서 증명할 수 없음을 보였다.

괴델의 증명

이 부분은 보충 필요. 스스로 써야 함.

  • Godel numbering  : 기본 부호에 유일하게 대응하는 Gödel number 부여
  • (예)
  • variables for number :
이런 식으로 하면 나중에 어떻게 문장으로 묶겠는가? 더 좋은 규칙 없을까?

그래서 이렇게 한다. 먼저, 모든 formula 는 Disjuctive Normal form 으로 바꿀 수 있기 때문에 이렇게 해서 부호를 최소화한다. 또는 Conjunctive Normal Form 그렇다면 앞의 numbering 에서 과 같은 기호는 없어지고 기본 부호는 1부터 10 까지로 부여할 수 있다.

  • variables for number 는 10보다 큰 소수들 을 준다. 이것도 와 같이 할 수 있기 때문에 사실 다른 numbering 도 가능할 수 있다.
  • variables for propositional sentence 는 10보다 큰 소수의 제곱 으로 나타낸다.
  • variables for predicate 는 10보다 큰 소수의 세제곱 으로 나타낸다.
  • formula 에 대해 등장하는 수들을 소수의 지수로 해서 곱 해서 나타낸다.
  • 예를들어 라는 문장은 'y 다음 수가 되는 x 가 있다'를 뜻하는 formula 다. 수로 차례대로 변환하면, 가 된다.
  • 따라서 앞의 문장은 가 된다.
  • 이제 어떤 문장들이 이어서 나온다고 해보자. 첫째 문장이 을 갖고, 둘째 문장이 를 마지막 문장이 으로 수를 부여받은 문장이 n 개 있다고 하자. 그런데 이것이 어떤 정리를 증명하는데 쓰인 문장들일 수 있지 않겠는가 ! 그렇다면 이 '증명'에 수를 또 부여할 수 있다.
자, 그럼 보자. 우리는 어떤 산술적 문장, 증명에 대해서도 정수를 부여할 수 있었다. 게다가 산술의 기본정리 에 따라 어떤 자연수에 대해 그것이 괴델수라면 무엇을 말하는지 decoding 할 수 있다. (물론 모든 자연수가 괴델수는 아니다.) 예를들어 이므로, 이것은 을 뜻하는 문장이다.
  • 위와 같이 해서 산술적 명제는 다 수를 부여했다고 하자. 이제 meta-arithmetic 문장들을 산술적 문장으로 바꾼다. (arithmatization)
  • 논리적 명제에 수를 부여해보자. 공리 하나를 예로 들어 본다.
  • 앞에서 문장들이 이어져 있을 때, 그것도 괴델수를 부여할 수 있었기 때문에 증명도 괴델수를 부여 받을 수 있다. 그뿐 아니라, 어떤 증명에 어떤 문장이 참여했다. 와 같은 meta-math 적인 문장도 괴델수는 부여받을 수 있다. 왜냐하면 이것은 '문장의 괴델수 z 는 증명의 괴델수 z 의 인수다' 로 바꿀 수 있고 그 문장은 벌써 '산술적 문장'이다. 따라서 이것은 고유의 괴델수가 있을 것이다. 하지만, 이것을 엄격하게 어떻게 할 것인가 나타내는 것은 매우 복잡한 산술적 관계라는 것을 짐작할 수 있다.
  • 마찬가지로, '어떤 산술 공식 는 증명할 수 없다' 라는 meta-math 적 formula 도 산술화 할 수 있다. '그것과 연관된 n 을 갖는 공식은 증명될 수 없다. '는 명제에 대응하도록 그 formula 이 만들어진다.
  • 괴델은 formula 의 부정인 가 증명되는 경우에만 formula F 가 증명된다는 것을 보인다. 아무리 잘 되었더라도 '공리화된 산술'이 무모순이려면 도 '증명'으로 유도될 수 없어야 한다. 다시말해 undecidable 한 문장이 존재한다.
  • 괴델은 formula 가 증명으로 유도될 수 없더라도 참이 되는 formula 다 라는 것을 보인다.
  • 따라서 공리체계는 불완전하다.
  • 게다가 Axiomatized Arithmetic is consistensy . 다시 말해 '공리화된 산술 체계는 모순이 없다.' 라는 meta-math 적 문장을 산술 공식 로 바꾸고, 는 증명할 수 없다는 것을 증명했다.
  • 마지막으로 앞의 도 증명할 수 없다는 것을 증명했다.
주의
- 괴델이 말하는 것은 공리화된 산술 체계가 '그 자신이 무모순하다'는 것을 증명할 수 없다는 것이지, 공리화된 산술체계가 무모순하다는 것을 증명할 수 없다는 것이 아니다. 이미 Gentzen (1936) 은 transfinite induction 이라는 추론 법칙을 적용하여 이를 증명했다. 하지만 이것은 힐버트가 제안한 대로 'finite' 한 증명이 아니다.
- 괴델은 또한 산술 체계 안에서 formula 로 나타낼 수 없는 엄격하게 finite 한 증명이 있을 수 있다는 것을 부정하지 않았다. 하지만, 그게 과연 무엇인가? 오늘날까지도 분명히 정의내리지 못하고 있다.

결론에 대신해서

  • 괴델의 결론이 미친 영향은 너무나 광범위해서, 지금도 완전하게 파악하기 힘들 정도다.
  • 수학적 또는 논리적 진리를 완전히 포괄할 수 있는 정의를 우리가 만들 수 있을까? (공리론적 방법은 한계가 있다.)
  • 아주 기본적인 수학적 개념은 '정의' 나 '작도'와 별개로 존재하는 .. 실질적으로 존재하는 대상으로 여겨질 수 있다. 그것은 물리적 물체에 대해 우리가 실재한다고 가정하는 만큼 '수학적 대상'도 실재하는 것으로 받아들여야 할 것이다. (플라톤의 실재론적 입장이고 괴델도 이런 입장)[1]


책을 읽고

다시 보게 되지는 않을테지만, 괴델의 불완전성은 언젠가 따로 정리를 할 수 밖에 없겠다. 여러 다른 증명이 나왔지만, axiomatization 방법을 적용해서 증명한, 다른 정리들까지 , 서서히 내게서 잊혀져 가는 '것'들을 '되살려' 야 겠다. 이것도 '실재론' ??


Note

  1. 괴델이 쓴 것을 모은 "러셀의 철학" (1944) 에서 '러셀의 수학적 논리' 부분.
괴델 1931년 논문 영문 번역판 : On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Martin Hirzel, November 27, 2000.