괴델 정리는 ‘아무것도 증명할 수 없다’는 뜻일까?

그림에서 무엇을 볼까요?

개별 증명 기록 검사, 체계 F 내부의 증명 가능성, 더 강한 메타이론 M의 설명을 세 층으로 나누고 불완전성 정리의 적용 범위를 표시한 표.

가상 체계 F에는 자연수, 덧셈과 곱셈, 공리 목록과 추론 규칙이 있습니다. 2+3=5의 짧은 유도는 F 안에서 검사할 수 있습니다. 또 입력된 기호열이 규칙에 맞는 증명인지 판정하는 절차를 만들 수 있습니다. 이 사실은 F가 자기 일관성 전체를 F 안에서 증명한다는 주장과 다릅니다.

그림은 ‘개별 유도 검사’, ‘체계 F에서의 증명 가능성’, ‘메타이론 M의 설명’을 세 층으로 둡니다. F 안에서 문장 G가 결정되지 않는다면, 단지 컴퓨터가 느려서 아직 못 찾았다는 말보다 강합니다. 하지만 G를 일상 언어의 아무 문장과 동일시하거나 F가 쓸모없다고 결론 내려서는 안 됩니다.