증명할 수 있는 모든 사실을 컴퓨터로 알아낼 수 있을까?

형식체계에 대해 정리를 말할 수 있나요?

5. 어떤 형식체계에 대해 정리를 말할 수 있나요?

괴델의 불완전성 정리를 모든 공리 체계에 무조건 적용할 수는 없습니다. 통상적으로 F는 공리와 증명을 기계적인 절차로 열거하거나 검사할 수 있도록 효과적으로 공리화되어야 합니다. 또한 기본적인 자연수 산술을 표현할 만큼 충분히 강해야 하고, 필요한 무모순성 조건을 충족해야 합니다.

예를 들어 로빈슨 산술 Q를 포함하는 일관된 효과적으로 공리화된 1차 이론은 중요한 대상입니다. Q는 매우 약하지만 덧셈과 곱셈을 다루는 기본 산술입니다. 이 정도의 산술적 표현 능력이 있어야 증명 기록을 자연수로 바꾸고 그 성질을 다시 산술 언어 안에서 다룰 수 있습니다. 제11회에서 설명한 괴델 부호화가 이 연결의 기술입니다.

반대로 유한한 명제논리의 진리표만을 다루는 판정 가능한 체계나 너무 약한 이론을 대상으로 '무조건 불완전하다'고 말할 근거는 없습니다. 적용 조건을 밝힌 뒤 정리의 결론을 말해야 합니다.

6. 증명 기록도 하나의 숫자로 바꿀 수 있습니다

문자, 논리 기호, 괄호, 수식, 증명 줄은 모두 유한한 기호열입니다. 기호 종류마다 자연수를 하나씩 대응시키고, 열 전체에 다시 자연수를 배정할 수 있습니다. 이를 괴델 부호화라고 부릅니다. 세부적인 부호화 방법에는 여러 가지가 있지만, 중요한 점은 코드가 주어졌을 때 해당 코드가 올바른 수식 또는 증명 기록인지 효과적으로 검사하도록 설계할 수 있다는 사실입니다.

Prf_F(p,a)를 '자연수 p는 번호 a를 가진 명제의 올바른 F-증명을 부호화한다'라는 관계로 정하겠습니다. 그러면 A의 증명 가능성은 다음과 같이 표현할 수 있습니다.

Prov_F(⌜A⌝) ≡ ∃p Prf_F(p,⌜A⌝)

⌜A⌝는 명제 A의 괴델 번호입니다. 앞의 ∃p는 올바른 증명 코드가 적어도 하나 있다는 뜻입니다. 이 기호 자체는 어떤 A의 증명을 이미 찾아냈다는 뜻이 아닙니다. 그런 코드가 존재한다는 성질을 산술 언어 안에 기록해 놓은 것입니다.

7. 가능한 모든 증명을 차례로 검사하면 어떤 일이 생길까요?

증명 기록 후보를 길이가 짧은 것부터 차례로 조사할 수 있습니다. F의 공리와 규칙을 열거하는 효과적 절차를 이용하면 모든 올바른 증명을 결국 만나도록 검색을 조직할 수 있습니다. 목표 A의 증명이 실제로 존재하면 어느 단계에서 그 증명을 찾을 수 있습니다.

ProofSearch_F(A): 후보 증명들을 차례로 검사하고 A의 증명을 찾으면 종료

하지만 A의 증명이 존재하지 않는다면 검색은 계속될 수 있습니다. 이 절차 자체에는 '증명이 영원히 나오지 않는다'고 말해 줄 종료 시점이 없습니다. 이미 주어진 유한한 증명을 검증하는 일은 가능하지만, 증명이 없다는 사실을 모든 경우에 대해 판정하는 문제는 다를 수 있습니다.

이런 절차의 성질을 반결정 가능이라고 부릅니다. 증명 가능한 사례에서는 언젠가 증거를 찾지만, 증명이 없는 사례에서는 검색이 끝난다는 보장이 없습니다. 이것을 F의 모든 정리가 판정 불가능하다는 주장으로 무조건 확대하지는 않습니다. 특정 이론 F의 정리 집합이 결정 가능한지는 그 이론의 표현 능력과 조건에 달려 있습니다.

'자신이 증명되지 않는다'는 명제는 어떻게 만들까요?

8. '자신이 증명되지 않는다'는 명제는 어떻게 만들까요?

우리는 '이 명제는 F에서 증명되지 않는다'라고 말하고 싶어 합니다. 그런데 자연어로 그 표현을 적는 것과 F의 산술 언어 안에 자기 번호를 정확하게 넣는 것은 다릅니다. 괴델은 번호 부호화와 대각화라는 기술을 사용했습니다.

현대적으로는 어떤 산술 공식 A(x)에 대해서도 적절한 자기 대입 문장 G를 만들어 다음 관계가 F에서 증명되도록 할 수 있다는 대각화 보조정리를 사용합니다.

F ⊢ G ↔ A(⌜G⌝)

A(x)를 '번호가 x인 문장은 F에서 증명되지 않는다'라는 성질로 선택하면, G와 'G는 F에서 증명되지 않는다' 사이의 형식적 연결을 얻습니다. 이때 G가 문자 그대로 자신과 완전히 동일한 문장으로 바뀌는 마술이 있는 것은 아닙니다. 정해진 코딩에 따라 두 명제가 F에서 동치로 증명된다는 뜻입니다.

9. 괴델 문장을 증명한다고 가정해 봅시다

G가 F에서 증명될 수 있다고 가정합니다. 그러면 실제로 G의 유한한 증명 코드 p가 존재합니다. F는 해당 코드가 G의 증명이라는 사실을 충분히 표현할 수 있으므로 Prov_F(⌜G⌝)를 증명하는 방향으로 나아갈 수 있습니다. 그런데 G는 자신의 비증명 가능성을 나타내도록 구성되어 있으므로 G의 증명과 연결하면 충돌을 일으킵니다.

F ⊢ G 라고 가정 → G의 증명 코드 존재 → F에서 Prov_F(⌜G⌝)와 그 부정 사이 충돌

F가 무모순이라는 조건을 두면 이런 충돌은 허용되지 않습니다. 따라서 원래 가정인 F⊢G를 버립니다. 이 단계가 보여 주는 것은 G가 F에서 증명될 수 없다는 주장입니다. 모든 수학 체계에서 영원히 증명할 수 없다는 말이 아닙니다. 선택한 F가 기준입니다.

10. G의 부정도 증명할 수 없다고 말하려면

한 걸음 더 나아가 F에서 ¬G 역시 증명할 수 없다고 말하려면 증명 방식과 무모순성 조건을 신중하게 확인해야 합니다. 괴델의 1931년 원래 논증에서는 일반적인 무모순성보다 강한 오메가 무모순성(ω-무모순성)이 중요한 역할을 합니다. 그 조건은 모든 개별 자연수에 대한 부정을 증명하면서 동시에 어떤 자연수에는 해당 성질이 있다고 증명하는 형태의 충돌을 금지합니다.

1936년 로서(J. Barkley Rosser)는 자기 언급과 증명 번호의 순서 비교를 정교하게 수정하여 단순 무모순성을 가정하는 방식으로 제1불완전성 정리를 강화했습니다. 따라서 오늘날 정리의 보편적 표현에서는 무모순이고 효과적으로 공리화되었으며 충분한 산술을 표현하는 이론이 불완전하다고 설명할 수 있습니다. 그러나 이때 사용되는 로서 문장과 괴델의 최초 문장을 동일한 기호열로 취급하지 않아야 합니다.

이 구분을 하지 않으면 '괴델이 1931년에 단순 무모순성만으로 원래 모든 결론을 증명했다'는 잘못된 역사적 설명이 생깁니다.

증명할 수 없는 문장이 참이라는 말은 언제 성립할까요?

11. 증명할 수 없는 문장이 참이라는 말은 언제 성립할까요?

괴델식 G가 표준 자연수 구조에서 참이라고 말할 때도 조건을 밝혀야 합니다. G는 정해진 F에서 자신의 비증명 가능성을 나타냅니다. 우리가 메타수학적 관점에서 F가 무모순임을 가정하여 G에 대한 F-증명이 존재하지 않는다고 판단하면, 표준 자연수에서 '그런 증명 코드는 없다'는 서술이 참이라고 설명할 수 있습니다.

그러나 이는 F 내부가 스스로 그 참을 모두 증명했다는 뜻이 아닙니다. 표준 구조에서의 진리와 F 내부 증명 가능성을 구분한 설명입니다. 산술의 임의 명제에 대해 '참이지만 증명할 수 없다'고 말하려면 어떤 표준 해석과 어떤 형식체계를 기준으로 했는지 확인해야 합니다.

이 점은 모든 자연언어 문장이나 일상적 주장에 불완전성 정리를 바로 적용할 수 없다는 뜻이기도 합니다. 교사의 설명에 빠진 내용이 있다고 해서 곧바로 괴델 정리의 사례가 되는 것은 아닙니다.

12. 제2불완전성 정리는 무엇을 더 말하나요?

형식체계 F의 무모순성을 '0=1의 F-증명이 존재하지 않는다'는 식으로 산술화할 수 있습니다. 이를 통상 Con(F)라고 나타냅니다. 제2불완전성 정리는 표준적인 증명 가능성 술어 조건을 충족하는 충분히 강한 효과적으로 공리화된 일관된 이론 F는 자신의 이러한 무모순성 진술을 F 안에서 증명할 수 없다는 결과입니다.

Con(F) ≡ ¬Prov_F(⌜0=1⌝)

F가 적절한 조건을 만족하며 무모순이면 F ⊬ Con(F)

이 조건을 붙이지 않고 모든 형식체계가 스스로 무모순성을 절대 증명할 수 없다고 말하면 부정확합니다. 매우 약한 체계나 증명 가능성을 특별히 바꿔 정의한 사례에서는 사정이 다릅니다. 힐베르트의 무모순성 계획과 겐첸의 후속 증명은 바로 어떤 방법과 어떤 강한 원리가 필요한지 보여 주는 역사적 맥락입니다.

13. 튜링의 프로그램은 어느 지점에서 부딪힐까요?

이번에는 공리와 증명 대신 프로그램과 실행 결과를 다룹니다. 컴퓨터로 작성한 프로그램 P와 입력 x를 주면 P가 x에서 언젠가 멈추는지를 정확하게 예측하는 범용 알고리즘 H가 있다고 가정하겠습니다. H는 모든 입력에 대해 반드시 끝나야 하고, 참인 답만 내놓아야 합니다.

H(P,x)=1 ⇔ P(x)가 멈춘다

H(P,x)=0 ⇔ P(x)가 멈추지 않는다

새 프로그램 D를 만들어 H(P,P)의 답이 1이면 일부러 영원히 반복하고, 0이면 즉시 멈추게 합니다. D 자신의 코드를 입력한 D(D)에 대해 H가 1을 답하면 실제 D는 멈추지 않으며, H가 0을 답하면 실제 D는 멈춥니다. 두 경우 모두 H의 완전 정확성 가정과 충돌합니다. 따라서 H는 존재할 수 없습니다.

이 논증은 프로그램의 동작에 관한 한계이며, 모든 산술 명제가 어느 체계에서 증명되는지에 관한 괴델의 결과와 직접 동일하지 않습니다.

서로 다른 두 불가능성이 만나는 지점

14. 서로 다른 두 불가능성이 만나는 지점

괴델은 형식체계 내부의 증명 기록을 자연수로 부호화하고, 그 체계에서 자기 증명 가능성을 가리키는 명제를 만들었습니다. 튜링은 프로그램 코드를 데이터로 입력할 수 있다는 사실을 이용해, 가정된 범용 판정기의 대답을 역행하는 프로그램을 만들었습니다.

두 경우 모두 유한한 기호열을 번호나 입력 데이터로 취급할 수 있다는 사실이 중요합니다. 그리고 어떤 절차가 '모든 경우'에 통한다고 가정하면 그 절차가 자기 자신과 연결되는 특별한 경우를 구성해 한계를 드러냅니다. 제19회가 설명한 대각선 구성의 공통 구조입니다.

그러나 괴델의 제1정리는 '충분히 강한 특정 공리 체계 F에서 어떤 산술 명제와 그 부정을 모두 증명할 수 없다'는 결과이고, 튜링의 정지 문제는 '모든 프로그램·입력을 다루는 종료 보장 판정기가 없다'는 결과입니다. 증명 불가능성과 계산 불가능성의 연결은 깊지만, 용어를 하나로 뭉뚱그려서는 안 됩니다.

15. 전부 검사하면 되는 것처럼 보였던 이유

프로그램을 모두 번호 붙일 수 있고 증명 후보도 모두 번호 붙일 수 있습니다. 그래서 학생은 '하나씩 검사하면 언젠가 정답이 나오지 않을까?'라고 생각할 수 있습니다. 증명이 실제로 있는 경우에는 맞는 생각입니다. 목표 문장 A의 증명이 있다면 충분한 단계 뒤에 그 증명을 찾게 할 수 있습니다.

하지만 찾지 못한 상태가 '앞으로도 영원히 없다'는 사실을 보여 주지는 않습니다. 정지 여부를 기다리는 프로그램의 경우에도 마찬가지입니다. 멈추는 프로그램을 직접 실행하면 종료를 관찰할 수 있지만, 계속 실행되고 있다는 사실만으로 앞으로도 절대 멈추지 않는다고 판정할 수는 없습니다.

이 둘의 공통점은 증거가 나올 때는 확인 가능해도 부재를 모든 경우에 유한 시간 안에 판정할 수 없을 수 있다는 점입니다. 다만 어떤 명제 집합이 실제 결정 가능한지 판단하려면 그 집합의 정의와 표현 능력에 대한 추가 정리가 필요합니다.

16. 처치의 결정 불가능성과는 무엇이 같고 다른가요?

제15회에서 다룬 결정문제(Entscheidungsproblem)는 주어진 1차 논리식의 타당성을 모두 판정하는 일반 절차가 있는지 묻습니다. 괴델의 완전성 정리에 따라 타당한 식은 형식적 증명을 찾을 수 있습니다. 그러나 임의의 식이 타당하지 않다는 판정까지 모든 입력에서 유한 단계 안에 끝낸다는 뜻은 아닙니다.

처치와 튜링은 1936년 전후 이 일반적인 판정 문제가 풀릴 수 없다는 결과를 서로 다른 계산 모델과 논증을 통해 보였습니다. 이를 설명할 때 '완전한 형식적 증명체계가 있으니 반드시 완전한 결정 알고리즘도 있다'는 추론은 실패합니다. 어떤 참인 명제에 대해 언젠가 증명을 찾을 수 있다는 반결정성은 모든 입력의 참과 거짓을 종료 보장과 함께 분리하는 결정성과 다릅니다.

따라서 완전성, 불완전성, 결정 불가능성은 이름이 비슷하게 들리더라도 각각 무엇을 비교하는지 밝혀야 올바른 논증이 됩니다.

우리가 일상에서 쓰는 검증 프로그램에는 어떤 의미가 있을까요?

17. 우리가 일상에서 쓰는 검증 프로그램에는 어떤 의미가 있을까요?

코드를 실행하기 전에 문법 오류를 찾아주는 편집기나 정해진 유형의 프로그램을 검사하는 분석 도구는 실제로 많은 오류를 검출합니다. 정지 문제가 결정 불가능하다는 사실은 그러한 도구의 효용을 부정하지 않습니다. 검사 가능한 프로그램의 범위를 제한하거나, 시간이 지나도 결론을 내리지 못하는 사례를 허용하거나, 특정한 규칙 위반을 찾아내는 방식으로 강력한 도구를 만들 수 있습니다.

형식 증명 검사기도 마찬가지입니다. 이미 적힌 유한한 증명의 각 단계가 규칙에 맞는지를 확인하는 일과, 모든 수학 명제가 참인지 자동으로 판정하는 일 사이에는 큰 차이가 있습니다. 현대의 정리 증명 보조기는 사람이 만든 증명을 세밀하게 검사하거나 탐색을 도울 수 있지만, 그런 성과로 괴델과 튜링의 일반 정리가 사라지는 것은 아닙니다.

기계가 어느 영역에서 강력하고 어디에서 원리적 한계를 가지는지 구분하면 기술의 실제 능력을 더 정확하게 이해할 수 있습니다.

18. 충분히 긴 시간을 주면 모든 문제가 해결될까요?

아주 오랜 시간을 주면 답을 찾을 것이라는 주장은 문제가 어려운 경우와 아예 일반적인 판정 절차가 없는 경우를 구별하지 못합니다. 계산 복잡도 이론은 해결 가능한 문제를 대상으로 시간·공간 자원이 얼마나 필요한지 연구합니다. 결정 불가능성은 어떤 알고리즘도 모든 입력에 대해 반드시 정확한 예·아니요 결과를 내놓을 수 없다는 성질입니다.

예를 들어 100만 단계가 필요하지만 항상 끝나는 계산은 느린 알고리즘의 사례일 수 있습니다. 반면 어떤 프로그램이 자신의 정지 여부를 예측하는 완전한 범용 프로그램이 있다는 가정과 충돌하는 정지 문제의 논증은 단순히 느린 계산의 문제가 아닙니다.

'계산할 수 없는 것'을 '지금 컴퓨터가 너무 느려서 못 하는 것'으로 설명하면 이 차이가 사라집니다. 반대로 현재 알고리즘이 해결하지 못하는 문제가 모두 원리적으로 불가능하다고 단정해도 잘못입니다. 불가능성을 주장하려면 필요한 수학적 증명이 있어야 합니다.

19. 인간은 그러면 모든 수학적 진리를 알 수 있나요?

괴델의 정리를 듣고 '기계가 할 수 없는 것은 인간이 언제나 알 수 있다'라고 결론 내리는 경우가 있습니다. 그러나 정리의 결론은 특정 조건의 형식체계가 가진 증명 능력의 한계입니다. 인간의 직관이 모든 산술 진리를 확실하게 파악할 수 있다는 심리학적 또는 철학적 주장을 별도로 증명하지 않습니다.

형식체계 F 밖에서 F의 무모순성을 가정하고 어떤 괴델 문장을 평가할 수 있다는 사실이, 인간이 모든 가능한 형식체계를 한 번에 뛰어넘는다는 보장은 아닙니다. 새 공리를 도입하면 더 많은 문장을 증명할 수 있을 수 있지만, 그 새 이론이 적절한 조건을 충족하면 불완전성 문제를 다시 만나게 됩니다.

인간 지능과 인공지능을 논의할 때도 마찬가지입니다. 정리를 직접 인용하려면 각 대상이 어떤 형식체계 또는 계산 절차로 정의되는지부터 밝혀야 합니다.

겐첸의 컷 제거와 무모순성 증명이 해 주는 일

20. 겐첸의 컷 제거와 무모순성 증명이 해 주는 일

제16회에서 배운 컷 제거는 표준 시퀀트 계산법에서 컷을 사용한 증명을 컷 없이 재구성할 수 있다는 정리였습니다. 그 결과는 형식적 증명의 구조와 변환에 대한 매우 강력한 성질입니다. 그러나 컷 제거가 모든 산술 진리를 자동으로 판정한다는 뜻은 아닙니다.

1936년 겐첸의 산술 무모순성 증명은 적절한 초한귀납 원리를 도입하는 방법을 사용했습니다. 이는 힐베르트가 추진했던 무모순성 연구의 후속 성과입니다. 괴델의 제2불완전성 정리와 충돌하려면 더 강한 메타수학적 방법을 사용했다는 조건을 무시해야 합니다. 어느 체계 안에서 무엇을 증명하는지를 구분하면 두 성과는 함께 이해됩니다.

앞에서 읽은 칸토어의 집합론, 괴델의 산술, 튜링의 계산, 겐첸의 증명 변환은 연구 대상이 다르지만 모두 대상·규칙·적용 범위를 엄밀하게 정할 때 큰 힘을 발휘합니다.