[황제의 새 마음 p173-182]
- "공리들과 추론 규칙들로 이루어진 형식 수학 체계"
- 수학 문장들을 표현하기 위한 기호와 알파벳
- 명제함수(propositional funciton): 하나 이상의 변수에 의존하는 명제
- 공리: 일반적인 명제들의 유한 리스트. 자명하게 '참'으로 간주
- 공리들로부터 출발하여 추론 규칙들을 되풀이 적용하여 명제들로 이루어진 리스트 작성
- 정리(定理, theorem): 적절한 방법에 의하여 조합된 명제들의 리스트 /176
- 어떤 명제 P를 증명 - 이 규칙에 맞게 조합된 리스트들 중에서 P로 끝나는 것을 찾으면 됨. 이 리스트는 P에 대한 증명이 되고, P는 정리가 됨
- 그러한 공리들과 절차 규칙들로 이루어진 체계가완전하길 바람: 그 체계 내에서 표현할 수 있는어떠한수학 문장에 대해서도 그것이 참인가 혹은 거짓인가를 결정 가능
- 구문론적으로 올바른 문자열 P가 나타내는 명제에 대해, P 혹은 ~P 를 증명
- 참 또는 거짓으로 증명: 완전성(completeness)뿐만 아니라 일관성(consistency)도 요구. P와 ~P가 동시에 정리가 될 수 있는 문자열 P가 존재하면 안됨.
- 형식주의적관점: 수학 명제들을 단지 어떤 형식 수학 체계에서 기호들의 스트링으로 간주함으로써 수학 문장들로부터 의미를 제거할 수 있다는 관점 - 괴델에 의해 치명적인 타격 /178
- n 번째 등장하는 것으로서 w에 적용되는 명제 함수를 다음과 같이 표기: Pn(w)
- m 번째 증명을: ㅈm
- 다음과 같은 명제 함수: ~ㄷx[ㅈxproves Pw(w)]
- ㄷ: 존재양화사 [existential quantifier]: '~한 것이 존재한다'
- 즉, 위 명제 함수는 "Pw(w)에 대한 증명 ㅈx는 존재하지 않는다" - 자연수 w에 대한 산술문장(하나의 변수 w에만 의존)
- 한 개의 변수를 갖는 모든 명제 함수들에 번호가 매겨져 있으므로 위 명제함수에도 번호가 있음 - 그 번호를 k 라 가정하면
Pk(w) = ~ㄷx[ㅈxproves Pw(w)]
- 특별한 w값(w=k)에 대하여 이 함수는
Pk(k) = ~ㄷx[ㅈxproves Pk(k)] - 특정 명제 Pk(k)는 완전히 잘 정의된(문법적으로 올바른) 산술 문장
- 이 형식 체계 내에서 Pk(k)는 증명을 가질 것인가? 아니면 ~Pk(k)는 증명을 갖는가? - 두 가지 질문 모두에 대한 답은 '아니오'이어야 함
- Pk(k) 에 대한 증명이 있다 가정하면 - Pk(k)가 실제로 주장하는 내용, 즉 증명이 없다는 것은 거짓이 됨 - 따라서 증명이 없어야 함 - 그러나 이것은 정확히 Pk(k)가 말하고자 하는 것 - 따라서 Pk(k)는 참
- 결국,체계 내에서 증명을 갖지 못하는 참명제
- ~Pk(k) 은 Pk(k)가 참이기 때문에 거짓 - 따라서 증명 존재하지 않음
- 결국 Pk(k), ~Pk(k) 는 모두 이 체계에서 증명할 수 없음