디멘의 블로그 이데아를 여행하는 히치하이커

정신은 기계로 환원될 수 있는가: 괴델의 조건문과 펜로즈-루카스 논증

수학
철학
논리학

이 글은 Peter Koellner, On the question of whether the mind can be mechanized (2018)을 정리한 것이다.

초록. 처치-튜링 논제와 괴델의 불완전성 정리는 기계로 증명할 수 없는 수학적 참의 존재를 시사한다. 그러나 만약 이상적인 인간 정신은 모든 수학적 참을 증명할 수 있다면, 이상적인 인간 정신은 기계와 같지 않다는 결론이 얻어진다. 이 글에서는 이같은 방식으로 반기계주의를 입증하려는 루카스와 펜로즈의 논증을 검토하고, 이 논증을 반박하는 형식 증명을 소개한다.

서론

다음은 논리학에서 잘 알려진 결과들이다.

  • 처치-튜링 논제. 이상적인 기계에 의해 계산 가능하다computable는 것은 튜링 기계로 구현 가능하다는 것이다.

  • 괴델의 불완전성 정리. $F$가 특정 조건을 만족하는 형식 체계라면, 참이지만 $F$로 증명 불가능한 문장이 존재한다.

  • 형식 체계-튜링 기계 대응. $F$가 특정 조건을 만족하는 형식 체계라면, $F$로 증명 가능한 명제들을 열거하는 튜링 기계가 존재한다.

위 세 가지 논제에 더해, 우리 인간은 형식 체계가 포착하지 못하는 수학적 참 — 이를테면 산술의 무모순성 — 또한 포착할 수 있는 것으로 보인다는 사실을 종합해 보면, 불완전성 정리는 이상적인 인간 정신이 도출할 수 있는 수학적 결과들의 외연이 이상적인 유한 기계로 도출할 수 있는 결과들의 외연을 초과함을 시사하는 것으로 보인다. 즉, 불완전성 정리는 정신이 기계로 환원될 수 없다는 반기계주의를 시사하는 것으로 보인다.

이 글에서는 과연 이 시사 관계가 얼마나 정당화될 수 있는지 검토한다. 그 결과, 불완전성 정리는 반기계주의 또는 플라톤주의를 시사하긴 하지만 반기계주의를 직접적으로 시사하지는 않음을 보일 것이다.

1. 괴델 조건문

괴델은 불완전성 정리로부터, 다음 두 입장 중 적어도 하나가 참이라는 결론이 따라 나온다고 주장했다. 이것을 괴델 조건문Gödel’s Disjunction이라고 부르자.

  1. 반기계주의: 이상적인 인간 정신이 도출할 수 있는 수학적 결과들은 언제나 이상적인 유한 기계가 도출하는 수학적 결과들을 초과한다. 따라서 인간 정신은 기계로 환원될 수 없다.

  2. 플라톤주의: 이상적인 인간 정신이 포착할 수 없는 수학적 참이 존재한다. 따라서 수학적 참은 인간 정신과 독립적으로 존재한다.

두 입장 모두 유물론적 철학에 반한다는 점이 주목할 만하다. 괴델은 평소 철학적 논증에 유보적이었지만, 해당 논증에 관해서만큼은 “수학적으로 입증된 사실”이라고 강하게 주장했다. 우리의 첫 번째 과제는, 과연 이 논증이 “수학적으로 입증된 사실”인지를 검증하는 것이다.

1.1. 괴델의 세 가지 주장

몇 가지 기호를 도입하자.

  1. $F$는 형식 체계 $F$가 증명할 수 있는 모든 문장들의 집합이다.

  2. $K$는 이상적인 인간 정신이 증명할 수 있는 모든 문장들의 집합이다.

  3. $T$는 참인 문장들의 집합이다.

이 글에 걸쳐 $K \subseteq T$를 가정할 것이다. 또한 $F$는 괴델의 불완전성 정리가 적용되는 형식 체계 — 즉, 페아노 산술(사실 이 조건은 로빈슨 산술로 약화시킬 수 있다)을 포함하는 무모순적인 체계 — 임을 전제한다.

본론에 들어가기 앞서 괴델의 불완전성 정리를 복습해 보자.

괴델의 불완전성 정리. $F$가 산술을 포함하는 무모순적인 수학 체계일 때, 다음이 성립한다.

  • 제1정리. 참이지만 $F$로 증명 불가능한 명제가 존재한다.
  • 제2정리. $F$의 무모순성이 제1정리의 실례에 해당한다.

첨언하자면 전통적으로 불완전성 정리가 대상으로 하는 산술은 페아노 산술이지만, 로빈슨 산술을 비롯한 더 약한 산술 체계에서도 불완전성 정리가 성립한다.

1.1.1. 첫 번째 주장

괴델은 먼저 다음을 주장한다.

주장 1. $F \subseteq T \implies F \subsetneq T$

증명은 다음과 같다. $F \subseteq T$라면 $\mathrm{Con}(F) \in T$이다. 그런데 제2불완전성 정리에 의해 $\mathrm{Con}(F) \notin F$이다. 따라서 $F \subsetneq T$이다.

1.1.2. 두 번째 주장

괴델의 두 번째 주장은 다음과 같다.

주장 2. $K(F \subseteq T) \implies F \subsetneq K$

증명은 다음과 같다. $K(F \subseteq T)$라면 $\mathrm{Con}(F) \in K$이다. 하지만 앞서 보았듯이 $F \subseteq T \implies \mathrm{Con}(F) \notin F$이므로 $F \subsetneq K$이다.

그런데 만약 $F \subsetneq K$가 참이라면, 이것을 어떤 식으로 이해해야 할까? 한 가지 방식은 형식 체계의 위계를 생각하는 것이다.

괴델은 불완전성 정리가 시사하는 증명 불가능한 문장들이, 절대적으로 증명 불가능할 필요는 없다고 강조한다. 형식 체계 $F$에서 증명 불가능한 문장이 $F$보다 고차적인 체계에서는 증명 가능해질 수 있기 때문이다. 예를 들어 $\mathsf{PA}$가 무모순적이라면 $\mathsf{PA}$는 $\mathrm{Con}(\mathsf{PA})$를 증명하지 못하지만, 2차 페아노 산술 $\mathsf{PA}_2$는 $\mathrm{Con}(\mathsf{PA})$를 증명할 수 있음이 알려져 있다. 물론 $\mathsf{PA}_2$는 $\mathrm{Con}(\mathsf{PA}_2)$를 증명하지는 못하지만, 이것은 3차 페아노 산술에서 증명 가능하며, 이런 식의 위계가 이어진다.

그리고 이 위계 전체는 $K$에 포섭되는 것으로 보인다. 이 관점으로 보았을 때 각각의 형식 체계는 집합과 같고, $K$는 모든 집합을 모은 것과 같다. 그리고 모든 집합의 모임이 집합일 수 없듯이, $K$는 형식 체계일 수 없다는 유비가 성립한다.

1.1.3. 세 번째 주장

그런데 이런 의문이 든다. ”주장 2“를 조건문으로 적는 대신, $K(F \subsetneq T)$가 참이라고 주장함으로써 $F \subsetneq K$를 주장할 수는 없을까?

괴델은 불완전성 정리만으로 그런 주장에 도착할 수는 없다고 지적한다. 왜냐하면 $K$와 일치하는 형식 체계 $F^\ast$의 존재 가능성을 완전히 배제할 수는 없기 때문이다 (앞선 고차 페아노 산술과 관련된 논의는 어디까지나 유비였음에 유의하라).

이에 대해 괴델은 다음과 같이 말한다.

[만약 그러한 형식 체계가 존재한다면] 인간 이성은 — 적어도 수학적인 측면에서는 — 유한한 기계와 동등하다. 그러나 그 기계는 자기 자신의 동작을 [스스로의 무모순성을 증명할 수 없다는 점에서] 완전히 이해할 수는 없다. 이 불능은 인간에게 있어 정신의 무한한 확장성으로 오인될 것이다.

대신 괴델의 세 번째 주장은 다음과 같다. 이 주장이 괴델의 조건문이다.

주장 3. $\forall F (F \subsetneq K) \; \lor \; K \subsetneq T$

증명은 다음과 같다. $F^\ast = K$인 형식 체계 $F^\ast$가 있다고 가정하자. $K \subset T$를 가정했으므로 $F^\ast \subset T$이며, 주장 1에 의해 $F^\ast \subsetneq T$이다.

전자는 반기계주의를, 후자는 플라톤주의를 의미한다.

1.2. 괴델 조건문의 형식화

지금까지 우리는 괴델의 세 가지 주장을 제시하고, 그에 대한 간략한 증명을 소개했다. 하지만 이 증명들은 사실 정확하지 않았다. 왜냐하면 $F, K, T$의 엄밀한 정의를 도입하지 않았을 뿐더러, 어디까지가 형식 체계 내에서 증명 가능한 내용이고 어디까지가 형식 체계 외에서만 증명 가능한 내용인지 구분하지 않았기 때문이다. 이 한계를 극복하기 위해, $F, K, T$ 및 괴델의 세 가지 주장에 대한 증명을 엄밀하게 형식화해 보도록 한다.

1.2.1. $F$

$F$는 가장 형식화하기 쉬운 개념이다. 특히 다음 사실들이 알려져 있다.

형식 체계-튜링 기계 대응. $F$가 재귀적으로 공리화 가능한recursively axiomatisable 형식 체계일 때, $F$로부터 증명 가능한 명제들을 재귀적으로 열거recursively enumerate하는 튜링 기계가 존재한다.

덧붙이자면, 우리가 관심을 가질 만한 형식 체계는 재귀적으로 공리화 가능하다.

클레이니 술어의 재귀성. 튜링 기계의 작동은 페아노 산술 내에서 형식화될 수 있다. 구체적으로, 괴델 수가 $x$인 튜링 기계가 자연수 $y$를 입력받았을 때 괴델 수가 $z$인 작동 기록computation record으로 끝나는지를 판단하는 1차 논리 술어 $K(x, y, z)$가 존재한다.

위 두 정리의 따름정리로 다음을 얻는다.

따름정리. 형식 체계는 재귀적으로 열거 가능하다. 즉, ”$e$번째 형식 체계“ $F_e$를 페아노 산술에서 정의할 수 있다.

예를 들어 $F_{123}$은 로빈슨 산술, $F_{456}$은 ZFC 등과 같은 식이다. $F_{123}(\ulcorner 1 + 1 = 2 \urcorner)$은 $1 + 1 = 2$가 로빈슨 산술에서 증명 가능하다는 것이다. 그리고 $\mathsf{PA} \vdash F_{123}(\ulcorner 1 + 1 = 2 \urcorner)$이다.

1.2.2. $T$

$T$의 형식적 정의로는 타르스키의 유형적 참 정의Tarski’s typed truth definition가 가장 유망하다. 타르스키의 유형적 참 정의는 의미론적 정의가 아니라 형태론적 정의이지만, 현 논의의 목적으로는 적합하다. 타르스키의 정의는 다음을 비롯한 공리들로 이루어져 있다.

  • $\forall x : \mathrm{Sent}(x) \rightarrow (T(\hat{\lnot} x) \leftrightarrow \lnot T(x))$

  • $\forall x, y : [\mathrm{Sent}(x) \land \mathrm{Sent}(y)] \rightarrow [T(x\; \hat{\lor} \;y) \leftrightarrow T(x) \lor T(y)]$

여기서 $\mathrm{Sent}$는 주어진 문장(의 괴델 수)가 적형식인지를 판단한다. 한편 $\hat{\quad}$은 언어와 메타언어를 구분하기 위해 도입되는데, 자세한 설명은 크게 중요하지 않기 때문에 이 정도로 줄인다.

1.2.3. $K$

$K$는 세 개념 중 가장 까다로운 개념이다. 완전한 의미론적 정의를 제시할 수 없음은 물론, 형태론적 정의를 제시하기에도 의문스러운 구석이 많다. 그러나 이 글의 목표는 불완전성 정리로부터 $F \subsetneq K$를 직접적으로 보일 수 없음을 논증하는 것이므로, 자비의 원칙에 따라 $K$의 외연을 최대한으로 보장하는 다음의 형태론적 정의를 제시하도록 하겠다.

$K$의 형태론적 정의.

  1. $\phi$가 논리적으로 참일 때, $K\phi$이다.
  2. 임의의 문장 $\phi, \psi$에 대해 $(K(\phi \rightarrow \psi) \land K\phi) \rightarrow K\psi$이다.
  3. 임의의 문장 $\phi$에 대해 $K\phi \rightarrow \phi$이다.
  4. 임의의 문장 $\phi$에 대해 $K\phi \rightarrow KK\phi$이다.

여기서 $K$는 논리 연산자이다. 때문에 $K(\phi)$ 또는 $K(\ulcorner \phi \urcorner)$가 아닌 $K\phi$와 같이 적었다. $K$가 술어가 아닌 논리 연산자로 간주되어야 하는 이유는 본 논문의 주석 29를 참고하라.

1.2.4. $\mathsf{EA}$와 $\mathsf{EA}_T$

$F, K, T$에 대해 추론할 수 있는 형식 체계를 구성해 보자. 먼저 1.2.1에서 보았듯이 $F$는 이미 $\mathsf{PA}$에서 형식화 가능하므로 별다른 조치가 필요하지 않다.

$L_{\mathsf{EA}}$를 $\mathsf{PA}$에 함수 $K$를 추가한 것으로 정의하자. $\Sigma$를 $\mathsf{PA}$의 공리들과, $K$의 형태론적 정의의 공리들의 모임이라고 하자 (단, $\mathsf{PA}$의 귀납 공리꼴을 $L_{\mathsf{PA}}$가 아닌 $L_{\mathsf{EA}}$의 문장들에 대해 취한다). $\mathsf{EA}$의 공리는 $\Sigma \cup K\Sigma$이다.

$L_{\mathsf{EA}_T}$를 $\mathsf{EA}$에 술어 $T$를 추가한 것으로 정의하자. $\Sigma^\ast$를 $\Sigma$와, $T$의 형태론적 정의의 공리들의 모임이라고 하자 (단, $\mathsf{PA}$의 귀납 공리꼴을 $L_{\mathsf{EA}_T}$의 문장들에 대해 취한다. $\mathsf{EA}_T$의 공리는 $\Sigma^\ast \cup K\Sigma^\ast$이다.

1.3. 괴델 조건문의 형식적 증명

괴델의 세 가지 주장은 $\mathsf{EA}_T$에서 형식적으로 증명 가능함을 보인다.

1.3.1. 첫 번째 주장

주장 1. $F \subseteq T \implies F \subsetneq T$

이 주장은 $\mathsf{EA}_T$에서 쉽게 증명 가능하다. 괴델의 불완전성 정리의 직접적인 결과이기 때문이다.

1.3.2. 두 번째 주장

주장 2. $K(F \subseteq T) \implies F \subsetneq K$

이 주장 또한 $\mathsf{EA}_T$에서 증명 가능하다. 사실 다음의 더 강한 결과가 증명 가능하다.

라인하르트 제1정리. 임의의 문장 $\phi$에 대해

\[\mathsf{EA} \vdash K(F(\ulcorner \phi \urcorner) \rightarrow \phi)\]

라면, 어떤 문장 $\psi$가 존재하여

\[\mathsf{EA} \vdash K\psi \land K\lnot F(\ulcorner \psi \urcorner)\]

이다 (즉, $\mathsf{EA} \vdash F \subsetneq K$이다).

1.3.3. 세 번째 주장

주장 3. $\forall F (F \subsetneq K) \; \lor \; K \subsetneq T$

위 주장에서 $F \subsetneq K$를 풀어 쓰면 다음과 같다.

\[\forall e \; \exists x \;(\mathrm{Sent}_{L_{\mathsf{PA}}}(x) \land K(x) \land x \notin F_e )\]

그리고 $K \subsetneq T$를 풀어 쓰면 다음과 같다.

\[\exists x \;(\mathrm{Sent}_{L_{\mathsf{PA}}}(x) \land T(x) \land \lnot K(x) \land \lnot K(\lnot x))\]

그런데 여기에는 문제가 있다. 앞서 말했듯이 $K$는 술어가 아닌 논리 연산자이기 때문에 양화 맥락에 속할 수 없다. 이를테면 $\exists \phi : \lnot\phi$가 문법적으로 올바르지 않듯이 말이다. 이 문제를 회피하기 위해, $\exists x \; K(x)$라고 적는 대신 $\exists x\; T(\hat{K}x)$와 같이 적도록 한다. 따라서 주장 3의 올바른 형식화는 다음과 같다.

\[\begin{gather} \forall e \; \exists x \;(\mathrm{Sent}_{L_{\mathsf{PA}}}(x) \land T(\hat{K}x) \land x \notin F_e ) \\\\ \lor\\\\ \exists x \;(\mathrm{Sent}_{L_{\mathsf{PA}}}(x) \land T(x) \land \lnot T(\hat{K}x) \land \lnot T(\hat{K}\lnot x)) \end{gather}\]

위 논리식을 $\mathrm{GD}$라고 하자. 다음 정리가 알려져 있다.

라인하르트 제2정리. $\mathsf{EA}_T \vdash \mathrm{GD}$.

따라서 괴델 조건문은 적절한 형식 체계 하에서 증명 가능하다.

2. 루카스와 펜로즈

2.1. 무모순성 판별 문제

루카스와 펜로즈는 $K(F \subseteq T)$임을 주장함으로써 $F \subsetneq K$를 직접적으로 보이고자 한다. 즉, 루카스와 펜로즈는 이상적인 인간 정식은 주어진 임의의 형식 체계가 모순적인지 아닌지를 판별할 능력이 있으며, 이에 따라 $\forall F \subseteq T: F \subsetneq K$라고 주장한다.

그러나 과연 이상적인 인간 정신에게 임의의 형식 체계의 무모순성을 판별할 능력이 있는지는 매우 의문스럽다. 일례로 $R$이 리만 가설이라고 하자. $R$은 페아노 산술에서 $\Pi_1$ 명제로 형식화될 수 있다. 그리고 앞서 언급했듯이 $\mathsf{PA}$는 $\Sigma_1$-완전하기 때문에, $\mathsf{PA} + R$의 무모순성은 $R$과 동치이다. 이 예시는 형식 체계의 무모순성 판별 문제가 리만 가설 이상으로 어려운 문제인 경우도 있음을 보여준다.

2.2. 기계주의의 상대적 무모순성

이 사실만으로 루카스와 펜로즈의 기획은 난관에 봉착하겠으나, 여기서 나아가 우리는 더 강력한 사실을 보일 수 있다. 그 사실이란, $K(F\subseteq T)$는 형식적으로 증명 불가능하다는 것이다. 왜냐하면 기계주의적 논제들이 $\mathsf{EA}_T$와 무모순적이기 때문이다.

이것을 보이기에 앞서, 기계주의적 논제들을 그 강도에 따라 분류하는 것이 유용하다. 이 글에서 채택하는 라인하르트의 구분법은 다음과 같다.

  • 약한 기계주의Weak Mechanical Thesis, WMT: $\exists e \; ( K = F_e )$
  • 강한 기계주의Strong Mechanical Thesis, SMT: $K\exists e\; (K = F_e)$
  • 아주 강한 기계주의Super Strong Mechanical Thesis, SSMT: $\exists e \; K(K = F_e)$

각각 풀어 설명하자면,

  • WMT: 이상적인 인간 정신은 어떠한 튜링 기계와 동등하다.
  • SMT: 이상적인 인간 정신은, 자신이 어떠한 튜링 기계와 동등함을 안다.
  • SSMT: 이상적인 인간 정신은, 자신이 특정한 튜링 기계와 동등함을 안다.

다음이 알려져 있다.

라인하르트 제3정리. $\mathsf{EA}_T + \mathsf{SSMT}$는 모순적이다.

따라서 $\mathsf{EA}_T$의 공리를 가정하면 아주 강한 기계주의는 거짓이다. 요컨데 설령 이상적인 인간 정신과 동등한 컴퓨터가 주어지더라도, 우리는 그것이 정말로 인간 정신과 동등한지 알 수는 없다.

그러나 이 사실만으로 루카스와 펜로즈의 손을 들어주기는 어렵다. 기계주의의 핵심 논제는 우리와 동등한 능력을 가지는 기계의 판별법이 아닌 우리와 동등한 능력을 가지는 기계의 존재성이기 때문이다. 그리고 이에 관해서는 다음이 알려져 있다.

라인하르트 제4정리. $\mathsf{EA}_T + \mathsf{WMT}$는 무모순적이다.

더 나아가 다음이 알려져 있다.

칼슨의 정리. $\mathsf{EA}_T + \mathsf{SMT}$는 무모순적이다.

즉 $\mathsf{EA}_T$는 이상적인 인간 정신과 동등한 기계의 존재 가능성을 열어둘 뿐 아니라, 그 사실을 인간 정신이 스스로 입증하는 가능성 또한 열어둔다. 위 사실들은 불완전성 정리만으로 반기계주의를 입증하려는 시도가 수포로 돌아갈 수밖에 없음을 보여준다.

2.3. 괴델의 혜안

놀랍게도 괴델은 처음부터 이 모든 논의를 꿰고 있었던 것으로 보인다. 왕Wang이 남긴 괴델과의 대화 회고에 따르면,

불완전성 정리는 인간의 수학적 직관과 동등한 결과를 내놓는 컴퓨터의 가능성 [$\exists e\; (F_e = K)$]을 배제하지 않는다. 그러나 다음을 시사하기는 한다. 만약 그 가능성이 — 비록 다른 고려 사항으로 인해 확률은 지극히 낮지만 — 사실이라면, 우리는 그러한 컴퓨터의 설계를 알 수 없거나 [$\lnot K (F_e = K)$], 그 컴퓨터가 올바르게 작동한다는 사실을 알 수 없다 [$\lnot K (F_e \subseteq T)$].

괴델은 신이야

3. 결론

지금까지의 논의는 괴델의 조건문으로부터 반기계주의를 직접적으로 이끌어내려는 더이상의 시도를 방지하는 데 충분할 것이다. 그러나 논리학의 결과로부터 반기계주의를 논증하려는 또다른 접근 방식이 있다. 흔히 펜로즈의 새 논증이라고 불리는 이 논증은 타르스키의 유형적 참과는 구별되는, 유형 독립적 참type-free truth을 내세우는 논증이다. 해당 논증의 형식화와 그것이 시사하는 바는 본 논문의 2편에서 다루도록 한다.