| [ PhilosophyThought ] in KIDS 글 쓴 이(By): guest (sptrkcz) 날 짜 (Date): 1996년07월16일(화) 09시40분38초 KDT 제 목(Title): Re: 괴델의 정리란... 괴델의 정리란, 임의의 충분히 강력한 형식화된 수학의 공리계가 주어지면, 그 안에서 참이지만 정리가 아닌(즉, *그 공리계 안에서* 증명이 불가능한) 명제가 존재한다는 내용의 정리입니다. '형식화된'이란 우리가 연구할 명제들을 자연언어로 쓴 것이 아니라 형식언어로 옮겨놓았다는 뜻이고, '충분히 강력한'이라는 단어의 의미는 좀 있다가 설명드리겠습니다. 간단하게 증명을 해 볼까요? 괴델이 증명한 방법은 아니고 튜링의 증명의 한 변형을 소개하죠. C언어는 모든 알고리즘을 기술할 수 있는 충분히 강력한 언어입니다. 임의의 충분히 파워풀한 언어도 상관없지만, 그냥 C언어를 이용하죠. 한 개의 입력을 받아서 계산하는 C언어 프로그램들의 집합을 생각합시다. 입력은 바이너리 파일로 받는다고 하죠. 뭐하는 프로그램들인지는 모릅니다. 입력을 받아서 무슨 계산을 할 때, 예를 들어 재수 없으면 무한루프에 빠지는 경우가 있겠죠. 이런 사태를 미리 소스코드만 보고 예측할 수 있는 프로그램을 작성할 수 있을까요? 즉, 우리의 슈퍼 디버거 D(P,I)는 검사할 프로그램의 소스코드 P와 입력 I를 받아서, P에 I를 초기 입력으로 하여 실행시킬 때 무한루프에 빠져서 영원히 종료하지 않을 지, 언젠가는 계산을 멈출지의 여부를 출력해 줍니다. 이러한 D()는 존재하지 않습니다. 왜냐하면, 만일 이러한 D가 존재한다면, P'()이라는 프로그램을 다음과 같이 작성합시다. P'()에 입력으로 I를 넣으면, P'는 내부에서 D(I,I)를 계산합니다. 다만 문제는 I가 올바른 C프로그램이 아닐 가능성이 있는데, 문법적인 문제는 기계적으로 체크할 수 있으므로 그런 경우 멈추는 것으로 해 버리면 상관없습니다. 그래서 결과가 '멈춘다'라고 D()가 출력하면 P'()는 무한루프를 돌기 시작하고, 결과가 '안멈춘다'이면 P'()는 즉시 계산을 종료합니다. 조금만 생각하면 D()의 소스코드를 살짝 수정하는 것 만으로 P'()를 짤 수 있다는 것은 분명합니다. 이제, P'(P')를 계산하면 무슨 일이 생길까요? P'은 멈출까요? 안 멈출까요? 만일 멈춘다면, P'의 정의에 의해 멈추기 위해서는 D(P', P')의 결과는 '안멈춘다'였어야 하고, 따라서 D()의 성질에 의해 P'(P')는 무한루프에 빠져야 합니다. 모순이죠? 만일 안 멈춘다면, 역시 같은 방법으로 모순을 일으킵니다. 결국 이러한 D()는 존재하지 않습니다. 이제 괴델의 정리를 증명할 수 있습니다. 만일 '충분히 강력한' 어떤 자연수에 대한 시스템이 있어서, 그 안에서 참인 임의의 명제가 항상 정리라고(그 공리계 안에서 증명이 가능하다고) 가정합시다. 그런데, 어떤 명제 P가 정말로 정리라면, 우리는 아주 무식한 방법으로 기계적으로 그 정리의 증명을 얻을 수 있습니다. 우리가 사용하기로 한 언어는 형식화되어 있기 때문에, 그 언어의 알파벳은 유한개에 불과하고(0,1,x,',(,),every,and,successsor의 9개의 심볼 정도면 충분할 것 같군요. 하여튼간에...) 따라서 우리는 '사전 순서로' 그 시스템의 모든 단어들을, 심지어 모든 문장들을 나열할 수 있습니다. 이제 기계적으로 나열된 문장들이 일단 문법적으로 옳은지, 다음으로 우리의 목표 P에 대한 증명인지를 확인합니다. 이렇게 가다 보면 우리가 가정하기를 P가 정리랬으니까(즉, 증명이 있기는 있댔으니까) 언젠가는 정말로 문제의 정리 P에 대한 증명을 얻을 수 있습니다. 근데, 임의의 참인 명제가 정리라면, 이제 우리는 임의의 명제 P에 대해 그 명제가 참인지 거짓인지의 여부를 기계적으로 결정할 수 있게 됩니다. 왜냐하면, P또는 not P는 항상 참이고, 따라서 P또는 not P는 항상 정리입니다. 따라서 위에서 설명한 무식한 알고리즘에 의해 차근차근 계속하면 P아니면 not P의 증명을 발견할 수 있고, 따라서 증명된 놈이 참이 되는 거죠. 따라서 이 시스템 안에서는 참/거짓의 여부를 유한스텝만에 기계적으로 결정할 수 있는 알고리즘이 있습니다. 재미없죠. 이제 앞에서 얘기한 D()의 불가능성과 이 재미없는 시스템을 연결합시다. C언어로 위에서 설명한 시스템을 구현합니다(더럽게 길겠지만 불가능한 작업은 아닙니다. 모든 것이 이미 심하게 formalize되어있으니까요). 즉, 예를 들어 우리는 O(P)라는 프로그램을 짤 수 있습니다. O()라는 프로그램은 형식화된 명제 P를 받아서, 출력으로 'P는 참이다', 또는 'P는 거짓이다'의 둘 중 하나를 내 놓습니다. 그렇다면 이제 이상하게도, 우리는 앞에서 기술했던 D()를 짤 수 있다는 결론에 도달합니다. D(P,I)를 어떻게 짜냐면요, 다음의 명제를 생각합시다. P(I)는 언젠가 멈춘다 이것은 비록 우리의 형식화된 공리계의 언어로 표시되어 있지는 않지만, 우리의 가정에 의하면 우리의 형식화된 시스템은 충분히 강력하기 때문에, 이 명제를 암호화해서 그 시스템에 밀어넣을 수 있습니다. 즉, 어떤 산수에 대한 명제 P*가 존재해서, P*가 참일 필요충분조건이 P(I)가 멈추게 되는 것입니다. 이런 암호화는 자연수의 소인수분해 등을 이용해서 이룩할 수 있는데, 우리의 공리계가 자연수 위에서의 산수를 모두 처리할 수 있는 정도면 됩니다. 이제, O(P*)을 생각하면, 그 결과를 읽어내면 D(P,I)를 계산할 수 있게 되고, 이 모든 일들은 유한스텝만에 끝나죠. 모순인데, 이 모순은 처음에 이런 시스템이 있다고 가정했기 때문에 생깁니다. 즉 이상하게도 어떤 참인 명제는 그 형식화된 공리계 안에서 도무지 증명히 불가능한 것입니다. 흠냐, 무척 슬로피한 증명이었습니다만 하여튼 주된 줄거리는 위와 같습니다. 괴델의 증명은 좀 다른데, 근본 정신은 비스므레합니다. 괴델 버전에서는 정말로 그러한 참인데 정리가 아닌 명제 G를 '구체적으로' 만들어냅니다. 철학적인 함의에 대해서는 좀 조심스러운데...예를 들어 기계에게 산수를 시키면 잘 하겠지만 완전하지는 않을 것이다라는 것은 대충 짐작이 되죠...하지만 괴델의 정리는 나름대로의 구체적인 전제조건이 있는 수학적인 정리입니다...아주 일반적이고...약방의 감초처럼 이거 하나 인용하면서 예를 들어 '인공지능은 그러니까 불가능해'라든가 다른 수많은 'implication'을 이야기 하는 것은 좀 신중해야 할 것 같습니다. |