쇼팽아저씨말 재미있네요. predicate logic (한국말로 이게 뭡니까?) 같은 경우는 Theorem Prover라고 시중에 팔고있는 소프트웨어가 있는데 주어진 스테이트먼트가 참인지 거짓인지 증명하는것인데 참인지 증명하는건 무척 쉽습니다. search tree를 만들어 가면서 만약 참이면 명제에서 연역이 되니까 그런데 문제는 이 스테이트먼트가 거짓인지를 증명하는 문제인데 이건 모순을 보여서뿐이 증명이 가능합니다. 현재 가장많이 연구되어진게 유클리드 공리계를 가지고 기하학적 증명을 하는 페케지인데 Geometric Theorem Prover 라는게 있는데 유클리드 공리계에서의 왼만한 증명은 다 해줍니다. 현재 유클리드 기하학은 완전히 바닥이 난 학문이지만 종종 기발한 발견을 하는경우가 있습니다. 얼마전에 미국의 고등학생이 geometer's sketch pad 라는 기하학 프로그램을 가지고 뭘 끄짓거리다가 무척 재미있는 정리를 발견한적이 있습니다. (이 프로그램 웹 에서 찾아보세요. 상당히 재미있는 프로그램 이더군요. ) 그런데 이미 수학에서는 이러한 종류들의 한계에 대해 이차세계대전쯤에 거의 완전히 증명되어졌습니다. 러셀이나 화이트헤드가 수학자체를 거대한 공리계로 환원시킬려다가 실패했습니다. 이들의 노력은 가히 아인쉬타인의 통일장이론에 비견되는데 말하자면 수학의 통일장 이론이라 생각하면 됩니다. 이런 종류의 프로그램들의 한계가 뭐냐면 주어진 공리체계안에서의 참과거짓뿐이 증명할수없습니다. (이것도 대단한거지만 ) 더더욱 그 공리체계안에서 참인데도 참임을 증명할숭없는 명제의 존재에 대한 속수무책입니다. (이게 괴델정리의 핵심) 괴델정리에 대해서는 펜로즈같은사람들이 AI와 관련되서 많이 울거먹었는데 보통 수학자들의 입장은 이 정리의 임플리케이션을 그렇게 중요시하지않습니다. (수학이외의것에 대해서는) 이건 어다까지나 철학의 영역으로 넘어갑니다. 괴델은 정말 20세기 최고의 수학자중 한명입니다. 괴델을 논리학자라고만 보는데 이사람이 타임머신에 관련된 블랙홀 어쩌구에대한 논문까지 썼습니다. 프린스턴대학의 어드벤스드 연구소에서 아인쉬타인, 폰노이만등과 옆방을 썼다고 하더군요. 세계에서 가장 똑똑한 사람 3명이서 몇미터 떨어져서 옆방에 살았다니... 어..이건 잡담이군요. iLUSiON 환상 �� Department of Mathematics, University of Toronto, Canada chung@math.toronto.edu / Fluid Dynamics, P.D.E., Non-linear System & Dynamics httpd://www.math.toronto.edu/~chung