한 이론의 증명이 닿지 않는 문장은 왜 생기나요?

여기서 T는 고전 일차논리의 공리와 추론 규칙을 갖춘 산술 이론입니다. 일관성, 효과적인 공리 열거, 로빈슨 산술 Q를 포함하는 충분한 산술 표현력을 가정합니다. 괴델–로서 제1불완전성 정리에 따르면 T가 G도 ¬G도 증명하지 못하는 닫힌 문장 G가 존재합니다.

셋 중 하나를 빠뜨리면 정리의 적용 범위가 달라집니다. 증명이 존재한다는 말과 표준 자연수에서 참이라는 말도 구별합니다.

로빈슨 산술 Q는 0, 후속 함수 S, 덧셈 +, 곱셈 ×에 대한 기본 공리를 갖습니다. x+0=x와 x+S(y)=S(x+y)가 예입니다. 유한한 계산과 기호열을 수로 다루는 표현력을 확보합니다.

페아노 산술 PA는 Q를 포함하며 귀납 공리 도식을 더합니다. Q나 PA와 무관한 모든 논리 게임에 정리를 적용하는 것은 정확하지 않습니다.

효과적 공리화는 공리들을 알고리즘으로 빠짐없이 열거할 수 있다는 뜻입니다. 공리가 무한해도 정해진 순서로 모두 내보내는 절차가 있으면 됩니다.

증명은 유한 기호열이므로 적절한 형식화에서는 증명 후보를 차례로 검사해 정리들을 열거할 수 있습니다. 아직 나타나지 않은 문장이 끝내 나타나지 않을지는 다른 문제입니다.

일관성은 T ⊬ ⊥입니다. 이론의 구문적 완전성은 모든 닫힌 문장 A에 대해 T ⊢ A 또는 T ⊢ ¬A가 성립한다는 뜻입니다.

11편의 일차논리 의미론적 완전성은 Γ ⊨ A ⇒ Γ ⊢ A입니다. 특정 이론이 모든 문장을 결정할 수 있다는 주장과는 다른 개념입니다.

괴델 번호화는 기호·식·유한 증명에 번호를 대응시키는 방법입니다. Proof_T(n,m)은 n번 기호열이 m번 문장의 정당한 T-증명이라는 산술 관계를 나타냅니다.

Prov_T(m) := ∃n Proof_T(n,m)는 ‘m번 문장에 T-증명이 있다’는 뜻입니다. 여기에는 T의 공리 열거와 기계적인 증명 검사 가능성이 쓰입니다. 진리 술어와 혼동하지 않습니다.

대각화 보조정리는 변수가 하나인 적절한 산술식 F(x)에 대해 T ⊢ G ↔ F(⌜G⌝)를 만족하는 문장 G를 만들어 줍니다. ⌜G⌝는 G의 괴델 번호를 가리킵니다.

F를 ¬Prov_T(x)로 택하면 G는 자기 T-증명이 존재하지 않는다는 산술적 내용을 갖습니다. 자연어 수수께끼를 공리로 넣는 대신 번호 부여와 대입 계산을 형식화합니다.

T가 G를 증명한다고 가정합시다. 실제 유한 증명의 번호가 있으므로 그 사실을 산술화해 Prov_T(⌜G⌝)를 도출할 수 있습니다. 동시에 G와 동치식에서 ¬Prov_T(⌜G⌝)를 얻어 모순입니다.

따라서 T가 일관적이면 T ⊬ G입니다. 여기서 G의 부정까지 증명되지 않음을 보여 주려면 별도 논증이 필요합니다. 괴델의 원래 논증과 로서의 개선은 가정이 정확히 다릅니다.

로서는 증명과 반증의 번호를 비교하는 방식으로 자기 지시 문장을 새로 만들었습니다. 적절한 로서 문장 R에 대해 일관성만으로 T ⊬ R과 T ⊬ ¬R을 보일 수 있습니다.

원래 괴델 논증에서는 반대 방향을 다루는 데 ω-일관성 같은 더 강한 가정을 사용했습니다. 현대 제1정리의 표준적인 로서 형식은 효과적 공리화·Q의 포함·일관성을 정확한 조건으로 씁니다.

일차논리의 의미론적 완전성은 Γ ⊨ A ⇒ Γ ⊢ A입니다. 제1불완전성은 특정 T에 독립인 G가 존재한다는 결론입니다. 질문의 층위가 다릅니다.

T에서 G와 ¬G가 모두 도출되지 않으면 T∪{G}, T∪{¬G}는 각각 무모순합니다. 일차논리 완전성으로 두 집합 모두 모형을 얻으며, 서로 다른 T-모형에서 G의 참값이 달라집니다.

참이라는 말에는 해석이 필요합니다. 표준 자연수 ℕ에서의 참, 특정 T-모형에서의 참, 모든 T-모형에서의 참을 구별합니다. 불완전성의 직접 결론은 T가 결정하지 못하는 문장의 존재입니다.

14편의 비표준 모형처럼 같은 공리들을 만족하는 여러 구조가 있을 수 있습니다. 한 T의 증명이 없다는 것은 모든 형태의 추론이 불가능하다는 뜻이 아닙니다.

적절한 형식의 자기 일관성 문장은 Con(T):=¬Prov_T(⌜⊥⌝)처럼 쓸 수 있습니다. 제2정리는 통상적인 산술화와 증명 가능성의 유도 조건을 갖춘 충분히 강한 효과적 이론 T가 일관적이면 T 안에서 Con(T)를 증명할 수 없다고 말합니다.

여기서는 PA와 같은 표준 형식화를 예로 듭니다. 제1정리와 제2정리의 세부 가정을 기계적으로 동일하게 놓지 않습니다. 외부의 더 강한 이론이 T의 일관성을 증명하는 일은 구별됩니다.

일관적이고 효과적으로 공리화된 Q의 확장 T가 있다고 합시다. 제1정리의 G에 대해 T는 G도 ¬G도 증명하지 않습니다. 동시에 건전성 T ⊢ A ⇒ T ⊨ A와 일차논리 완전성 T ⊨ A ⇒ T ⊢ A는 유지됩니다.

기호의 역할을 살펴봅니다. ⊢는 형식적 도출, ⊨는 모든 전제 모형에서의 귀결입니다. 제1정리는 T가 모든 산술 문장을 한쪽으로 증명할 수 있다는 기대에 경계를 그어 줍니다. 다음 편에서는 세계마다 참이 달라지는 양상논리를 배웁니다.