괴델의 완전성 정리

3. 전제

1차 논리에는 자연 연역 체계 및 힐베르트식 체계를 포함하여 수많은 연역 체계가 존재한다. 모든 연역 체계에 공통적으로 적용되는 것은 ''형식적 연역''의 개념이다. 이는 특별히 지정된 ''결론''을 가진 일련의 공식(또는 경우에 따라 유한 트리)이다. 연역의 정의는 유한하며, 주어진 일련의 공식(또는 트리)이 실제로 연역인지 알고리즘적으로(예: 컴퓨터 또는 손으로) 확인할 수 있다.

일차 공식은 해당 공식의 언어에 대한 모든 구조에서 참인 경우(즉, 공식의 변수에 값을 할당하는 경우) ''논리적으로 타당''하다고 한다. 완전성 정리를 공식적으로 진술하고 증명하기 위해 연역 체계도 정의해야 한다. 연역 체계는 모든 논리적으로 타당한 공식이 어떤 형식적 연역의 결론인 경우 ''완전하다''고 하며, 특정 연역 체계에 대한 완전성 정리는 이러한 의미에서 완전하다는 정리이다. 따라서 어떤 의미에서 각 연역 체계마다 다른 완전성 정리가 존재한다. 완전성의 반대 개념은 연역 체계에서 논리적으로 타당한 공식만 증명 가능하다는 사실인 ''건전성''이다.

4. 역사

이 정리는 쿠르트 괴델이 1929년에 증명하였다. 이는 괴델의 1930년 박사학위 강연에 포함되었고, 1931년에 출판되었다.^[11] 괴델의 불완전성 정리와 함께 괴델의 가장 중요한 초기 업적으로 꼽힌다.

1928년에 다비트 힐베르트와 빌헬름 아커만의 공저인 『기호 논리학의 기초』^[6] 초판이 출판되었는데, 이 책에서 일계 술어 논리의 완전성은 해결되지 않은 문제였다.^[7] 쿠르트 괴델은 이 문제를 해결하기 위해 1929년 가을에 학위 논문으로 그 결과를 발표했는데, 이것이 바로 괴델의 완전성 정리이다.^[8]

5. 정리가 함의하는 바

괴델의 완전성 정리에 따르면, 어떤 논리식이 논리적으로 유효하면 그 논리식에 대한 유한한 연역(형식적 증명)이 존재한다.^[10][11] 따라서 연역 체계는 모든 논리적으로 유효한 식을 증명하기 위해 추가적인 추론 규칙이 필요하지 않다는 의미에서 "완전"하다. 견고성과 함께 이 정리는 논리식이 형식적 연역의 결론이 되는 필요충분 조건이라는 것을 의미한다.

더 일반적인 형태로 표현하면, 모든 1차 이론 ''T''와 ''T''의 언어에 있는 모든 문장 ''s''에 대해, $T\backslash models\; s$이면 $T\backslash vdash\; s$이다. 역(무모순성) 또한 성립하므로, $T\backslash models\; s$와 $T\backslash vdash\; s$는 동치이다. 이는 1차 논리에서 구문적 결과와 의미적 결과가 동치임을 의미한다.

완전성 정리는 헨킨의 모델 존재 정리의 결과로서, 모순성의 관점에서 이해될 수 있다. 모델 존재 정리는 잘 정렬 가능한 언어를 가진 모든 일차 논리 이론 ''T''에 대해 다음과 같이 말한다.

뢰벤하임-스콜렘 정리와 관련 있는 또 다른 버전은 다음과 같다.

헨킨의 정리가 주어지면, 완전성 정리는 다음과 같이 증명될 수 있다. 만약 $T\; \backslash models\; s$라면, $T\backslash cup\backslash lnot\; s$는 모델을 가지지 않는다. 헨킨의 정리의 대우에 의해, $T\backslash cup\backslash lnot\; s$는 구문론적으로 모순적이다. 따라서 모순($\backslash bot$)은 연역 시스템에서 $T\backslash cup\backslash lnot\; s$로부터 증명 가능하다. 즉, $(T\backslash cup\backslash lnot\; s)\; \backslash vdash\; \backslash bot$이고, 연역 시스템의 성질에 의해 $T\backslash vdash\; s$이다.

완전성 정리의 중요한 귀결 중 하나는, 임의의 일계 이론에 대해, 그 이론의 공리를 사용한 올바른 연역을 모두 나열함으로써, 논리적 귀결을 나열하는 것이 가능하다는 것이다. 즉 완전성 정리는 논리적 귀결 관계 $\backslash Gamma\; \backslash models\; \backslash varphi$와 증명 가능성 관계 $\backslash Gamma\; \backslash vdash\; \backslash varphi$가 일치함을 말하고 있는데, 후자는 귀납적 가산이므로 전자도 귀납적 가산이라는 것이다.

괴델의 '''불'''완전성 정리(이 경우의 "완전성"의 의미는 다름)는 어느 정도의 초등 산술을 포함하는 귀납적 가산 이론이 무모순이라면, 그 이론 체계 내에서 증명도 반증도 할 수 없는 닫힌 논리식이 존재함을 보였다. 그 경우에도, 그러한 이론 체계에 완전성 정리를 적용할 수 있으며, 그 이론 체계에서의 임의의 논리적 귀결은 그 이론 체계 내에서 증명 가능하다.

6. 증명

괴델의 완전성 정리는 콤팩트성 정리로부터 유도할 수 있다. 1차 논리에서 콤팩트성 정리는 다음과 같다.

# $T\backslash models\backslash phi$이면, $T\_0\backslash models\backslash phi$인 유한 부분 집합 $T\_0\backslash subset\; T$가 존재한다.

# $T$의 모든 유한 부분집합이 충족 가능하면, $T$ 역시 충족 가능하다.

첫 번째 정리의 증명은 다음과 같다.^[11] $T\backslash vdash\backslash phi$가 $T\backslash models\backslash phi$를 함의한다는 것은 건전성 정리이다. 반대로, $T\backslash vdash\backslash phi$를 가정하면, 연역 과정은 유한하므로, $T\_0\backslash vdash\backslash phi$인 유한 부분 집합 $T\_0\backslash subset\; T$가 존재한다. 건전성 정리에 의해, 이는 $T\_0\backslash models\backslash phi$를 함의하고, 콤팩트성 정리에 의하여 $T\backslash models\backslash phi$이다.

두 번째 정리는 첫 번째 정리의 따름정리이다.^[11] $T$의 모든 유한 부분집합이 만족 가능하면, 건전성 정리에 의해 모든 유한 부분 집합이 무모순이다. 그런데 연역 과정은 유한하므로, $T$ 또한 첫 번째 명제에 의해 무모순이면 충족가능하다.

모델 존재 정리를 통해 완전성 정리를 증명할 수도 있다. (헨킨의 증명)

6. 1. 모델 존재 정리

6. 2. 산술 정리

7. 귀결

완전성 정리의 중요한 귀결 중 하나는 모든 재귀적으로 열거 가능한 의미론적 결과는 이론의 공리에서 가능한 모든 형식적 추론을 열거하고 이를 사용하여 결론의 열거를 생성함으로써 효과적인 일차 논리 이론을 재귀적으로 열거하는 것이 가능하다는 것이다.

이는 "증명 가능성"의 개념, 따라서 "정리"의 개념을 이론의 선택된 공리 시스템에만 의존하고 증명 시스템의 선택에는 의존하지 않는 명확한 개념으로 만든다.^[6]

8. 불완전성 정리와의 관계

괴델의 불완전성 정리는 수학의 주어진 일차 논리 이론 내에서 증명할 수 있는 것에 내재된 한계가 있음을 보여준다. 여기서 "불완전성"은 모형 이론에서 말하는 '완전'과는 다른 의미이다. 이론 $T$가 완전(또는 결정 가능)하다는 것은 $T$의 언어에 있는 모든 문장 $S$에 대해 $T\backslash vdash\; S$ (증명 가능)이거나 $T\backslash vdash\; \backslash neg\; S$ (반증 가능)인 경우를 말한다.

제1 불완전성 정리는 일관성이 있고, 효율적인 계산 가능하며, 로빈슨 산술("''Q''")을 포함하는 모든 $T$는 이 의미에서 불완전해야 하며, $T$ 내에서 증명하거나 반증할 수 없다는 것이 명백한 문장 $S\_T$를 명시적으로 구성한다.^[6] 제2 불완전성 정리는 $S\_T$가 $T$ 자체의 일관성을 표현하도록 선택될 수 있음을 보여줌으로써 이 결과를 확장한다.

$S\_T$는 $T$에서 증명될 수 없으므로 완전성 정리는 $S\_T$가 거짓인 $T$의 모형이 존재함을 의미한다. $S\_T$는 Π₁ 문장이며, 모든 자연수에 대해 어떤 유한론적 속성이 참이라고 말한다. 따라서 거짓이면 어떤 자연수가 반례이다. 이 반례가 표준 자연수 내에 존재한다면, 그 존재는 $T$ 내에서 $S\_T$를 반증할 것이다. 그러나 불완전성 정리는 이것이 불가능하다는 것을 보여주었으므로 반례는 표준 숫자가 아니어야 하며, 따라서 $S\_T$가 거짓인 $T$의 모든 모형은 비표준 숫자를 포함해야 한다.

산술 모형 존재 정리의 체계적인 구성을 통해 얻은 ''Q''를 포함하는 ''모든'' 이론의 모형은 ''항상'' 비표준이며, 비동등한 증명 가능성 술어와 자체 구성을 해석하는 비동등한 방식을 가지므로 이 구성은 비재귀적이다(재귀적 정의는 모호하지 않기 때문).

$T$가 ''Q''보다 약간 강하면(예: 경계된 존재적 공식에 대한 귀납법을 포함하는 경우), 테넨바움 정리는 재귀적 비표준 모형이 없음을 보여준다.

괴델의 '''불'''완전성 정리는 어느 정도의 초등 산술을 포함하는 귀납적 가산 이론이 무모순이라면, 그 이론 체계 내에서 증명도 반증도 할 수 없는 닫힌 논리식이 존재함을 보였다.^[7] 그러한 이론 체계에도 완전성 정리를 적용할 수 있으며, 그 이론 체계에서의 임의의 논리적 귀결은 그 이론 체계 내에서 증명 가능하다.^[8]

완전성 정리는 의미론과 통사론 사이를 연결함으로써 모델 이론과 증명론 두 분야의 기본적인 연관성을 확립한다. 그러나 완전성 정리는 이 두 개념의 차이를 없애는 것은 아니다. 괴델의 불완전성 정리에 따르면, 수학에서의 형식적 증명으로 달성할 수 있는 것에는 본질적인 한계가 있다. 불완전성 정리에서 말하는 "완전"은 다른 의미이다. 완전성 정리는 일차 이론의 논리적 귀결인 논리식을 다루고, 불완전성 정리는 특정 이론의 논리적 귀결이 되지 않는 논리식을 구성한다.

완전성 정리의 중요한 귀결 중 하나는 일차 이론에서의 논리적 귀결의 집합이 귀납적 가산 집합이라는 사실이다. 그러나 괴델의 불완전성 정리의 귀결에 따라, 논리적으로 타당한 논리식의 집합은 결정 가능하지 않다.

9. 콤팩트성 정리와의 관계

완전성 정리와 콤팩트성 정리는 일차 논리의 두 가지 기초이다. 이들 정리는 모두 실효적인 방법으로 증명할 수 없지만, 한쪽에서 다른 쪽을 실효적으로 얻는 것이 가능하다.

콤팩트성 정리는 논리식 φ가 일련의 논리식(무한일 수도 있음)의 집합 Γ의 논리적 귀결일 때, φ는 Γ의 유한한 부분 집합의 논리적 귀결이기도 하다는 것이다.^[11] φ의 형식적 추론에서 언급되는 Γ의 공리는 유한 개이므로, 이것은 완전성 정리로부터 직접 얻을 수 있는 귀결이다. 연역계의 건전성으로부터, φ가 이 유한 집합의 논리적 귀결이 된다. 이 콤팩트성 정리의 증명은 원래 쿠르트 괴델에게서 유래되었다.

반대로 많은 연역계에서는, 콤팩트성 정리의 실효적인 귀결로서 완전성 정리를 증명할 수 있다.

완전성 정리의 비실효성은 역수학의 관점에서 측정될 수 있다. 가산 언어에 대해 고려할 때, 완전성 정리와 콤팩트성 정리는 서로 동등하며, 약한 쾨니히의 보조정리로 알려진 선택 공리의 약한 형태와 동등하며, RCA₀ (Σ⁰₁ 공식에 대한 귀납법으로 제한된 페아노 산술의 2차 변형)에서 동등성이 증명 가능하다. 약한 쾨니히의 보조정리는 선택 공리가 없는 체르멜로-프렝켈 집합론 시스템인 ZF에서 증명 가능하므로, 가산 언어에 대한 완전성 정리와 콤팩트성 정리는 ZF에서 증명 가능하다. 그러나 언어가 임의의 큰 기수를 가질 때는 상황이 다르다. 완전성 정리와 콤팩트성 정리는 ZF에서 서로 증명 가능한 동등성을 유지하지만, 초여과기 보조정리로 알려진 선택 공리의 약한 형태와도 증명 가능한 동등성을 갖는다. 특히 ZF를 확장하는 어떤 이론도, 임의의 (아마도 비가산적인) 언어에 대해 초여과기 보조정리를 같은 기수의 집합에 대해 증명하지 않고서는 완전성 정리나 콤팩트성 정리를 증명할 수 없다.

10. 다른 논리에서의 완전성

완전성 정리는 모든 논리에 성립하는 것은 아닌 일차 논리의 핵심적인 속성이다. 예를 들어, 2차 논리는 표준 의미론에 대한 완전성 정리를 갖지 않으며(하지만 Henkin 의미론에 대해서는 완전성 속성을 갖는다), 2차 논리에서 논리적으로 유효한 공식들의 집합은 재귀적으로 열거될 수 없다. 이는 모든 고차 논리에서도 마찬가지이다. 고차 논리에 대한 건전한 연역 시스템을 만들 수 있지만, 그러한 시스템은 완전할 수 없다.

린스트룀의 정리는 일차 논리가 (특정 제약 조건에 따라) 압축성과 완전성을 모두 만족하는 가장 강력한 논리라고 명시한다.

크립키 의미론에 관하여, 양상 논리 또는 직관 논리에 대한 완전성 정리를 증명할 수 있다.

11. 증명 방법

괴델의 정리의 원본 증명은 문제를 특정 구문 형식의 공식에 대한 특수한 경우로 축소한 다음, 이 형식을 임시 변론으로 처리하는 방식으로 진행되었다.^[4]

현대 논리 교과서에서는 괴델의 완전성 정리가 괴델의 원본 증명보다는 헨킨의 증명으로 증명되는 경우가 많다. 헨킨의 증명은 임의의 일관적인 일차 논리 이론에 대한 항 모델을 직접 구성한다. 다른 증명들도 알려져 있다.

참조

_[1] arXiv Gödel's Incompleteness Theorem 2022-12-01
_[2] 저널 The completeness of the first-order functional calculus 1949-09
_[3] 저널 Eine Bemerkung zu Henkin's Beweis für die Vollständigkeit des Prädikatenkalküls der Ersten Stufe 1953-03
_[4] 보고서 Proving the Completeness Theorem within Isabelle/HOL http://afp.sourcefor[...] 2004-09
_[5] 문서 廣瀬,横田(1985) p.147、ヒルベルト、アッケルマン(第三版) p.107、ヒルベルト、アッケルマン(第六版) pp.139-145
_[6] 문서 国内では第三版と第六版の邦訳が出版されている。ヒルベルト、アッケルマン(第三版)、ヒルベルト、アッケルマン(第六版)
_[7] 문서 制限された形では証明されていた。さらにこの初版本は「この公理系が、すべての正しい論理式を導き出すことができるという意味で、完全であるか否かは依然として未解決の問題である。この公理系がどんな場合にも十分であるというのは、まったく経験的なものである」と述べていた。廣瀬,横田(1985) pp.5-6
_[8] 문서 廣瀬,横田(1985) pp.5-6
_[9] 문서 博士論文書誌データベース
_[10] 서적 Model theory: an introduction Springer 2002
_[11] 서적 A mathematical introduction to logic http://www.math.ucla[...] Academic Press 2014-11-25