페아노 공리계가 포함된 어떠한 공리계가 무모순일 경우, 그 공리계로부터 그 공리계 자신의 무모순성을 도출할 수 없다. 는 말에 대해, 좀 더 알아 봅시다.
페아노 공리계라는 건, 사실상 자연수 집합을 정의하는 것입니다.
그리고 페아노 공리계가 포함된 공리계라는 것은, 페아노 공리계 자체를 명제로서 부분 집합으로 갖고 있다는 게 아니라,
해당 공리계가 모두 참이면, 언제나 자연수 집합이 존재한다는 의미입니다.
근데 사실 페아노 공리계를 포함한다는 것 자체가 모호한 말입니다. 모호하니 저처럼 해석할 수도 있고, 다르게 해석할 수도 있겠다만, 그렇게 더 제한 조건을 붙이고 싶으면 그런 조건을 추가적으로 서술되어야 할 것입니다.
다음과 같이 논리 체계를 설정하면, 페아노 공리계를 포함하면서 공리계 자신의 무모순성을 도출할 수 있습니다.
우선,
상수 0, 함수 기호 S, 등호 =, countably infinite 개수의 variable 등을 포함하는 1st order logic을 설정하죠.
그리고 명제나 formula는 주어진 논리 체계의 기호들을 유한하게 나열한 것들 중 특정 규칙을 만족하는 것들입니다.
그러므로 모든 명제와 formula들의 집합은 countable합니다.
(formual는 좀 더 명확한 의미 전달을 위해 보통 well-formed formula라고 표현됩니다. 근데, 기니까 그냥 formula라고 하면 wellformed formula를 지칭하는 걸로 사용하겠습니다.)
그리고 T={∀x(x=x)}U{ ∀x∀y(x = y->y = x)} U {∀x∀y∀z((x = y &y = x)->x =z))}
U{∀x~0=S(x)}
U{ ∀x∀y((((S(x)=S(y) -> x=y))}
U{ (P(0)&∀x(P(x) ->P(S(x)))) -> ∀xP(x)) | x는 variable, P(x)는 1항 술어.}
그러면, T를 만족하는 모델은 언제나 자연수 집합을 포함합니다.
명제 P가 T의 증명이라는 것은, 명제들의 유한 수열 (P1, P2, ..., Pn)이 존재하여, 각각의 Pi에 대해, Pi∈T인 것만을 증명으로 인정하는 증명 체계를 생각합시다.
그러면, T로부터 유도되는 명제들은 언제나 T의 원소입니다.
그리고 임의의 명제 P에 대해, P∈T이면, ~P는 T의 원소가 아닙니다. 애초에 T의 원소 중에 ~으로 시작하는 원소가 없습니다.
따라서, T라는 공리 체계는 해당 증명 체계에서 consistent, 즉, 무모순적입니다.
