괴델의 정리는 충분히 강력하고 무모순인 공리계에서는 참이면서도 정리가 아닌 명제가 있다는 정리입니다. 자체무모순을 증명할 수 없다는 것은 corollary로 딸려나오죠. 근데 둘은 동치입니다. 예를 들어, 자체무모순을 증명할 수 없다고 가정합시다. '이 시스템은 무모순이다'라는 명제(정확히는 이 명제를 그 시스템 안으로 암호화하여 밀어넣은 것)는 이제 증명이 불가능하죠. 이 명제는 거짓일까요? 만일 거짓이라면 이 시스템은 모순이 있고, 이제 모든 명제가 증명되지요(모순은 임의의 명제를 함의하니까요) --- 아까의 '이 시스템은 무모순이다'라는 명제 자체까지 포함해서. 즉 이 명제가 바로 참이면서 증명이 불가능한 명제입니다. 자동정리증명은 일반적으로 가능하지요. 단 증명하려는 명제가 정리라면. ^_^ 뭔가가 정리인지 아닌지 판별하는 것이 일반적으로는 불가능하죠. 왜 '페르마의 마지막 정리'를 집어넣지 않는가는 당연한데, 첫번째는 아직 그런 본격적인 정리를 다룰만한 자동정리증명 프로그램이 없는데다가(그렇겠죠? ^_^), 증명은 틀림없이 너무 길테고(Andrew Wiles가 1~2년 전에 증명을 완료했는데, 무척 길었죠), 설령 기계에 의해 증명이 찍혀나온다고 해도 그 결과가 의미있는 일일까요? Andrew Wiles는 대수기하적인 도구들을 사용해서 증명을 했습니다만, 예를 들어 그 도구들을 모두 정수론의 단순한 개념들로 환원하고(그 과정에서 증명은 더욱 길어지고 더욱 알아보기 어려운, 그래서 별로 이해에 도움을 주지 않는 무언가로 변하겠지요), 또 그 결과를 특정 formal system의 언어로 형식화한 결과물이 만일 10000페이지가 찍혀나온다면 그 기계에게 필즈상을 줘야 할까요? 또한 결과를 내기까지의 시간과 컴퓨팅 파워를 생각하면... 그런데 정수까지는 별로 어렵지 않은 것이 아니라 정수가 어렵습니다. Tarski가 증명한 정리가 있는데, 예를 들어 실수에 대한 first order system은 결정가능하다는군요. 놀랍죠?