어느 히키코모리의 블로그

 Compactness Theorem이라고 부르는 이 정리는 모형론의 근본적인 정리 중에 하나입니다. 어떤 집합의 만족가능성을 따지기 위해서 집합 전체를 따질 필요가 없이 유한한 부분집합들이 모두 만족가능한지만 확인하면 되기 때문입니다. 이에 대한 증명을 봅시다.

 우선, $\Gamma$가 만족가능하면 그에 대한 모형(=해석)이 존재할 것이고 그 모형이 $\Gamma$의 부분집합들을 참으로 만들 겁니다. $\Gamma$가 모형 하에서 참이기 때문에 그 임의의 부분집합도 당연히 참이 되겠죠.

 역으로, $\Gamma$의 임의의 유한한 부분집합들이 모두 만족가능하다고 합시다. 그런데 $\Gamma$가 만족가능하지 않다고 합시다. 그러면 완전성 정리에 의해 $\Gamma$는 비일관적이고, 따라서 어떤 $\alpha$가 있어서 $\Gamma\vdash\alpha\wedge\neg\alpha$입니다. $\beta = \alpha\wedge\neg\alpha$라고 합시다. 그러면 도출가능성의 정의에 의해서 어떤 문장들의 나열 $<\beta_1, ..., =\beta_n>$이 있어서 정의를 만족하고 $\beta_n = \beta$가 됩니다. 증명이란 건 근본적으로 유한한 문장들에 추론규칙을 유한번 적용하여 얻어지는 유한한 절차입니다. 즉, $\Gamma$가 아무리 큰 무한집합이라고 할지라도 $\beta$를 이끌어내는데는 위와 같이 유한한 문장들만 사용합니다. 우리는 $\Gamma$에서 $\beta$를 증명하는데 사용된  $\beta_1, ..., \beta_n$ 중에서 $\Gamma$의 원소들을 뽑아서 $\Gamma_0$라고 합시다. 이는 당연히 유한집합입니다. $\Gamma$에서 실질적으로 $\beta$를 이끌어내는데 사용된 원소들을 뽑아내겠다는 거죠. 즉, 불필요한 원소들을 제외하는 건데, 증명에 쓰였던 원소들만 뽑아냈기 때문에 $\Gamma_0$만으로도 $\beta$가 증명이 되는 건 당연한 일입니다. 즉, $\Gamma_0\vdash\beta$입니다. 이에 완전성 정리를 사용하면 $\Gamma_0\models\beta$가 됩니다. 가정에 의해서 $\Gamma_0$가 유한하기 때문에 만족가능합니다. 이에 대한 해석을 $\mathcal{I}$라고 합시다. $\Gamma_0\models\beta$에 의해 $\mathcal{I}\models\beta$가 될 것인데, $\beta$는 $\alpha\wedge\neg\alpha$입니다. 해석은 어떤 문장과 그 문장의 부정을 동시에 만족시킬 수 없기 때문에 모순이 생깁니다. 따라서 처음에 가정한 $\Gamma$가 만족가능하지 않다는 것이 틀렸습니다. 귀류법에 의해 원하는 것을 우리가 원하는 것을 얻게 됩니다.

 조밀성 정리는 자연수체계에 대한 비표준적인 모형/해석을 제공하는데 쓰일 수 있습니다. 가령 어떤 자연수보다 더 큰 자연수라는 개념을 정의할 수 있게 만듭니다. 아래는 자연수공리계인 페아노 공리계(Peano axioms)입니다. 모형론이 발달하기 전까지는 아래의 공리들을 만족하는 집합은 우리가 아는 $\mathbb{N}=\{0,1,2,3,...\}$밖에 없다고 생각했습니다. 제가 지금까지 0을 자연수에 포함시키지 않아왔는데, 교양~전공입문 수준의 논리학을 배우시는 분들은 0을 자연수에 넣는 것에 익숙하지 않기 때문이었습니다. 수학분과마다 정의가 다르긴 하지만, 공리계적인 접근에서는 0을 자연수로 넣는 게 관례입니다. 이에 대한 이유를 설명하는 건 복잡하기 때문에 건너 뜁시다.. 여튼, 아래를 만족하는 모형은 우리가 아는 표준적인 자연수집합에 대한 모형밖에 없다고 생각했었습니다. 그런데 조밀성 정리를 사용하면 재밌는 발견을 할 수 있습니다.

위의 문장들의 집합을 PA라고 합시다. 페아노 공리계의 언어 $\mathcal{L_{PA}}$의 비논리상항에는 $0, 1, +, \cdot, <$가 있습니다. $x\leq y$는 $x<y \vee x=y$의 줄임말입니다.

그리고 언어에 개체상항 $c$를 추가해서 $\{c>1+1+...+1 \text{(1이 n개)} | n\in\mathbb{N}\}$라는 집합을 $\Gamma$로 둡시다. $1+1+...+1$이 n개의 1로 구성되어있을 때 n이라고 구분하지 않고 씁시다. $PA$의 언어에는 각각의 자연수에 대한 개체상항은 없기 때문에 자연수를 나타내려면 1과 덧셈을 사용해야 합니다. 그래서 실제 자연수 n과 이를 논리기호로 표현하는 1+1+...+1는 다르기 때문에 n' 등으로 다르게 써야하지만 굳이 그럴 필요는 없어 보이기에 구분하지 않고 쓰겠습니다.

즉, $c$는 어떤 1+1+1+...+1로도 표현될 수 없는 매우 큰 수(무한히 큰 수)이기를 바라는 것입니다. 조밀성 정리에 의해서 $\Gamma$의 임의의 유한한 부분집합이 만족가능하다는 걸 보이면 $PA$를 만족하면서 어떤 유한한 자연수보다도 더 큰 '비표준적인 자연수'가 있는 모형이 존재한다는 걸 증명하게 됩니다.

 이는 간단합니다. $\mathbb{N}$이 유한한 부분집합들의 모형이 되기 때문입니다. $\Gamma_0$를 $PA\cup\Gamma$의 임의의 유한한 부분집합이라고 합시다. 그러면 $\Gamma$의 원소 중에 택해진 유한한 원소들, 가령 $c>n_1, c>n_2, ..., c>n_i$가 있다고 합시다. $n$을 $n_1, ..., n_i$ 중에서 가장 큰 것에 1을 더한 수라고 합시다. 우리는 지금 표준적 자연수모형 $\mathbb{N}$을 사용하고 있습니다. 그러면, $c$의 해석에 $n$을 부여하면 택해진 유한한 문장들은 참이 됩니다. $\mathbb{N}$는 당연히 PA를 참으로 만들기 때문에 $\Gamma_0$는 $\mathbb{N}$에 의해 만족됩니다. 또한 $\Gamma_0$는 임의였기 때문에 조밀성 정리에 의해서 $PA\cup\Gamma$는 만족가능합니다. 즉, 자연수공리계를 참으로 만들면서 무한한 크기를 가지는 원소를 지닌 '비표준적 자연수 모형'이 존재합니다. 이제 추가된 개체상항 $c$을 언어에서 제외하고 다시 $PA$의 언어로 돌아가더라도, 무한히 큰 원소에 대한 개체상항을 표현하는 언어가 빠지느냐 아니냐의 문제일 뿐 모형의 원소와 구조 자체는 변하지 않기 때문에 아무 문제 없습니다. 따라서 $PA$의 언어에서 비표준적인 자연수모형이 존재합니다.

 모형론에서 흥미로운 것은 표준적 모형과 구조가 다른, 서로 다른 구조의 비표준적 모형들이 얼마나 많이 있는가를 밝힐 수 있다는 점입니다. 집합론을 배우신 분은 실수집합의 크기에 대해 아실 것입니다. 비표준적 모형들의 서로 다른 구조들의 개수는 실수크기만큼 있습니다. 또한 $PA$의 언어에서 표준적 자연수 모형에서 참인 문장과 비표준적 자연수모형에서 참인 문장들은 서로 같기 때문에 비표준적인 자연수모형을 토대로 무언가 참으로 만든 문장이 있다면 표준적 자연수모형에서도 참이게 됩니다. 

 논리학의 추론규칙체계는 다양합니다. 공리체계, 자연연역체계, 시퀀트체계가 대표적으로 많이 쓰이고 트리체계나 다른 여러 방식이 쓰이기도 합니다. 모두 소개하기엔 체계들도 많고 그에 대한 변형도 존재하고, 또한 하나를 소개하는 것도 제대로 설명하려면 상당히 복잡하기 때문에 현재로서는 어떤 추론체계를 설명하지는 않겠습니다. 나중에 시간이 되면 자연연역 같은 체계를 간단히 소개해 볼 것입니다. 여기서는 어느 체계에서나 통용되는 개념적으로 중요한 사실에 대해서만 언급하겠습니다.

 항상 아래와 같은 건 아니지만 보통 아래와 같이 증명가능성을 정의할 수 있습니다. 공리란 자명한 것으로 받아들여지는 문장이나 그것들의 집합을 뜻합니다. 이를 사용하여 '증명가능성' '도출가능성'을 아래와 같이 정의할 수 있습니다. 자연연역이나 다른 방식에서는 공리가 아에 없는 경우도 있기 때문에, 아래에서 공리라는 단어가 체계에 따라 빠질 수 있습니다. 

 $\Gamma\vdash\alpha$는 $\alpha$는 $\Gamma$로부터 증명가능하다, 도출가능하다고 말합니다. 혹은, $\alpha$는 $\Gamma$의 정리(theorem)라고 합니다. 수학에서 정리라고 하는 말이 이 말입니다. 현대 수학은 $\in$이라는 원소기호와 몇 가지 수학적 공리들을 사용해서 얻어지는데 $\Gamma$를 수학공리들의 집합이라고 하고 수학의 언어가 논리상항 + $\in$라고 생각한다면 우리가 말하는 수학의 정리는 모두 $\Gamma$로부터 증명가능한 문장들이고 따라서 일반적으로 $\Gamma\vdash\alpha$에서 $\alpha$를 $\Gamma$의 정리라고 부르는 데에 큰 문제가 없을 겁니다.

 이와 대비해서 메타정리라는 게 있습니다. 메타정리는 논리학 자체에 대한 결과입니다. 즉, $\Gamma\vdash\alpha$ 형태로 나타나는 문장들이 아니라 논리학의 기호에 대한 정의들에 대해 생산해낼 수 있는 결과물입니다. 앞에서 만족가능성과 논리적 함축 개념이 서로 상호교환가능하다는 것도, 우리가 다루는 술어논리학 자체가 가지는 성질에 관한 것입니다. 이와 관련하여 매우 중요한 정리가 논리학에 대한 건전성과 완전성 정리입니다.

 건전성 정리(soundness theorem)는 $\Gamma\vdash\alpha\Longrightarrow\Gamma\models\alpha$입니다. 말하자면, $\Gamma$에서 증명가능한 문장은, $\Gamma$에서 참입니다. 달리 말하면, 추론규칙을 포함한 추론체계에서 생산되는 문장들이 진리라는 개념을 보존한다고 보시면 됩니다. 어떤 논리학의 체계가 이런 성질을 만족할 때, 논리학의 체계가 건전하다고 말합니다. 다시 말해 공리와 추론규칙으로 삼은 것들이 진리(참)의 관점에서 문제가 없다는 것이고, 추론체계는 항상 참을 생산해내기 때문에 건전한 체계라는 것이죠.

 만약 건전하지 않은 체계라면 그 논리학의 체계는 쓸모가 없을 겁니다. 추론규칙을 통해서 얻어낸 문장이 진리를 보존하지 않는다면(즉 참이 아니라면) 아무리 좋은 결과를 추론해낸다해도 거짓이 될 수 있으므로 불안정한 체계일 수밖에 없겠죠. 그런 체계는 누구도 가지고 싶지 않을 겁니다.

 반대의 경우도 남아있습니다. 건전한 체계이면서 동시에 건전성의 역도 증명이 가능하다면 그 체계는, 진리와 증명의 관점이 서로 상호교환가능한 매우 완전한 체계일 겁니다. 그래서, 건전성이 성립할때 $\Gamma\models\alpha\Longrightarrow\Gamma\vdash\alpha$가 성립하는 논리학 체계를 완전한 체계라고 합니다. 건전성과 완전성이 성립하면 $\models$와 $\vdash$를 상호교환해서 언제든 쓰고 싶을 때 쓸 수 있습니다. 그래서 논리학에서는 $\models$만 사용하는 분야와 $\vdash$만 사용하는 분야가 나뉘어 있습니다. 전자를 모형론이라고 하고, 후자를 증명론이라고 합니다. 모형이란 개념은 철학에서는 거의 언급되지 않고 수학에서 주로 언급되는데, 우리가 다루었던 해석 $\mathcal{I}$를 수학에서는 구조(Structure) 또는 모형(model)으로 부릅니다. 다른 말로는 의미론과 구문론이라고도 부릅니다. $\models$는 무언가 진리, 참이라는 개념에 의존해있는 것 같고, $\vdash$는 구문론 즉, 어떤 글자들로부터 글자를 추론해내는 구문규칙에 의존해있는 것 같기 때문입니다.

* 건전성과 완전성을 구분해서 쓰기도 하지만, 많은 경우 건전성+완전성 = 완전성으로 표기하는 경우가 많으니 유의하시길 바랍니다.

 술어논리의 건전성, 완전성을 보이는 건 쉽지 않은 일입니다. 엄밀히 개념정의를 하고 증명하려면 수학적으로도 복잡하고 수학과 학부 3-4학년 수준이기 때문에 우리가 이걸 직접 증명할 수는 없습니다. 그러나 위에서 사용되는 건전성, 완전성 형태와 동치인, 좀더 간단한 형태들이 있다는 걸 보일 겁니다. 이를 위해선 아래의 성질들이 필요합니다. 

증명가능성과 관련하여 얻어낼 수 있는 몇 가지 성질들과 필요한 정의들이 있습니다. $\Gamma$는 임의의 문장들의 집합 $\alpha$, $\beta$는 임의의 문장이라고 합시다.

3,4는 정의이고 나머지는 모든 추론체계에서 증명가능한 것들입니다. 증명이란 개념만을 개괄적으로 가지고 증명의 개요를 봅시다.

(0) 문장들의 집합에 속하는 문장은 문장들의 집합으로부터 도출가능하다는 말입니다. 당연한 말이죠. 이미 주어진 것으로부터 주어진 것을 산출해내는 것은 그저 집합에 있는 글자를 써내려가는 것에 불과하기 때문입니다. 우리가 앞에서 내린 증명의 정의를 따라가면, 그냥 $<\alpha>$를 쓰면 끝납니다. $\alpha$가 $\Gamma$의 원소이기 때문에.. 

(0') 작은 집합에서 증명되면 더 큰 집합에서도 증명된다는 말입니다. 당연한 말입니다. 가령, $\{A,B\}$에서 $D$가 증명됐다고 합시다. 그러면 $\{A,B,C\}$에서도 $D$가 증명될 겁니다. $A,B$만 가지고도 증명되던 게 갑자기 $C$를 추가한다고 증명이 안 된다는 건 이상하니까요. 그냥, $A,B$에서 $D$를 증명할 때 썼던 증명식들이 있다면 $A,B,C$에서도 그대로 쓰면 됩니다.

(1) $\alpha$와 $\beta$가 $\Gamma$로부터 증명가능하다고 합시다. 그러면 $\Gamma$에서 $\alpha$와 $\beta$가 증명된 것입니다. 즉, $\alpha$이고 $\beta$이다가 증명된 것이죠. 이 말은, $\alpha\wedge\beta$가 증명되었다는 말입니다. 좀더 앞에서 제시한 증명이란 개념에 맞추어서 보면, $\Gamma$에서 $\alpha$를 증명하는데 쓰인 문장들이 있을 겁니다. $\beta$에 대해서도 동일하겠죠. 가령, $\alpha_1, \alpha_2, ... \alpha_m$을 통해 $\alpha_m= \alpha$임을 추론해냈고, $\beta_1, \beta_2, ..., \beta_n$을 통해 $\beta_n = \beta$임을 추론해냈다고 합시다. 그러면, 그냥 두 문장을 증명하는데 쓰인 문장들의 나열을 그냥 이어주고, 마지막에 $\alpha\wedge\beta$를 쓰면 됩니다. 즉, $\alpha_1, ..., \alpha_m, \beta_1, ..., \beta_n, \alpha_m\wedge\beta_n$를 적으면 증명이 됩니다. 물론 추론체계에서 $\alpha$와 $\beta$가 문장들의 나열 속에 있으면 $\alpha\wedge\beta$를 허용하는 규칙이 있어야 하겠습니다만 이는 어느 체계에서든 직접적으로든, 간접적인 방식으로든 들어가 있습니다. 그러면 $\Gamma\vdash\alpha$와 $\Gamma\vdash\beta$로부터 $\Gamma\vdash\alpha\wedge\beta$를 증명할 수 있습니다. 역도 성립합니다. 어느 추론체계든 $\alpha\wedge\beta$에서 $\alpha$와 $\beta$를 각각 추론하게 허용합니다. 알파이고 베타이다가 증명되는데, 각각이 증명되도록 허락되지 않은 체계는 개념적으로 이상하겠죠.

(1') $\Gamma$에서 $\alpha$를 가정했을 때 모순이 생기면 가정한 $\alpha$가 틀렸다고 볼 수 있으므로 그의 부정인 $\neg\alpha$를 추론한다는 의미입니다. 귀류법의 전형적인 형태입니다.

(2) 이를 연역정리(deduction theorem)이라고 부릅니다. (2) 식의 의미는 간단합니다. $A\rightarrow B$같은 조건문이 의미론에서는 $A$가 참이면 $B$도 참이라는 것으로 이해되지만, 구문론에서는 $A$라는 글자가 주어지면 그에 추론규칙을 사용하여 $B$를 얻어낼 수 있다는 것으로 이해됩니다. 이는 후에 설명할 완전성 정리에 의해 같은 의미를 지님을 좀더 명확히 알 수 있습니다. 어쨌든, 이 개념을 사용해서 연역정리를 풀이해봅시다.

(2)식의 앞부분은 "$\Gamma$와 $\alpha$에 추론규칙을 사용하면 $\beta$를 얻어낼 수 있다"

(2)식의 뒷부분은 "$\Gamma$가 주어졌을 때, $\alpha$가 주어지면 $\beta$를 얻어낼 수 있다"

 가 됩니다. $\alpha$가 앞에 있느냐 뒤에 있느냐의 차이일 뿐이지 의미차이는 없습니다. 가령, 소크라테스에 대한 논증을 빌려옵니다. 사람은 죽는다, 소크라테스는 사람이다, 소크라테스는 죽는다는 문장들이 있습니다. 각각 $A,B,C$로 둡시다. $\Gamma=\{A\}$라고 합시다. 그러면 의미를 쉽게 파악할 수 있습니다. 사람은 죽기 마련이고 소크라테스는 사람이라면, 당연히 소크라테스는 죽을 겁니다. 이 말은 사람은 죽기 마련일 때, 소크라테스는 사람이라면 소크라테스는 죽을 것이다 라는 말과 같은 말입니다. 전제를 조건문을 사용해서 문장에 넣느냐, 아니면 집합 안에 넣어두느냐의 차이일 뿐입니다.

(3), (4)는 정의입니다. 비일관적인 집합은 어떤 문장과 그 문장의 부정을 동시에 증명합니다. 즉, 모순을 증명합니다. 일관적인 집합은 그런 경우가 생기지 않는다는 말입니다.

(5), (6) 예전에 $\models$와 만족가능성에 관해서 비슷한 형태의 증명을 했습니다. 이름이 단지 $\models$가 $\vdash$로 바뀌고 일관성/비일관성이 만족가능성/만족불가능성으로 바뀌었을 뿐입니다.

 증명형식은 같기 때문에 (6)만 봅시다.

$\Gamma\vdash\neg\alpha$라고 합시다. $\Gamma\cup\{\alpha\}$를 살펴봅시다. 우선 $\Gamma\subseteq\Gamma\cup\{\alpha\}$이기 때문에 우리는, $\Gamma\vdash\neg\alpha$와 (0')으로부터 $\Gamma\cup\{\alpha\}\vdash\neg\alpha$임을 알 수 있습니다. 그런데 이 집합에는 $\Gamma\cup\{\alpha\}$에는 $\alpha$가 있기 때문에, (0)으로부터 $\Gamma\cup\{\alpha\}\vdash\alpha$임을 알 수 있습니다. 즉, 우리는 $\Gamma\cup\{\alpha\}$가 비일관적인 집합이라는 것을 알 수 있습니다.

 반대를 가정합시다. 즉, $\Gamma\cup\{\alpha\}$가 비일관적이라고 합시다. 그렇다면, 어떤 문장 $\beta$가 있어서 우리는 해당 문장들의 집합에서 $\beta\wedge\neg\beta$를 증명할 수 있습니다. 이는 비일관성의 정의와 (1)을 사용한 것입니다. 즉, $\Gamma\cup\{\alpha\}\vdash\beta\wedge\neg\beta$를 얻어낼 수 있고, 여기에 연역정리(2)를 사용하면 $\Gamma\vdash\alpha\rightarrow (\beta\wedge\neg\beta)$를 얻을 수 있습니다. 귀류법(1')을 사용하면 $\Gamma\vdash\neg\alpha$를 얻을 수 있습니다.

 따라서 원하는 것이 모두 증명되었습니다.

(5),(6)을 사용하면 예전에 논리적 함축과 만족가능성의 개념이 상호교환하다는 것을 증명할 수 있었듯이, 도출가능성/증명가능성이 일관성과 개념적으로 상호교환가능하다는 걸 알 수 있습니다. 굳이 여기서 쓰진 않겠습니다만 증명의 형태는 논리적함축과 만족가능성에서 했던 양식을 따라간다는 것만 적어두겠습니다.

 이제, 건전성과 완전성을 다른 형태로 나타낼 수 있습니다. 논리적 함축은 만족가능성의 문제로, 도출가능성은 일관성의 문제로 환원시키는 겁니다. 건전성부터 봅시다.

 2는 1을 기호로 나타낸 것이고, 3는 2에 나타난 $\models$와 $\vdash$를 동치인 조건으로 바꾼 것입니다. 4는 3에 대우를 취한 것입니다(즉 $\neg B\rightarrow\neg A$이면 $A\rightarrow B$). 4의 형태를 더 단순히 바꿀 수 있느냐가 문제가 됩니다. 즉, 5로 바꾸는 게 문제가 됩니다. 4와 5가 동치임을 봅시다.

 가장 중요한 건 모든 $\Gamma$와 $\alpha$에 대해 4가 성립한다는 것이고, 5는 모든 $\Gamma$에 대해 성립한다는 것입니다.

 우선 4를 가정합시다. 우리는 1-4가 모두 동치임을 알기 때문에 사실 아무거나 사용하면 됩니다. 5의 대우를 대신 증명합시다. 즉, $\Gamma$가 비일관적이면, $\Gamma$가 만족가능하다는 걸 보입시다. $\Gamma$가 비일관적이면, 어떤 $\alpha$가 있어 $\Gamma\vdash\alpha$이고 $\Gamma\vdash\neg\alpha$입니다. 4은 2와 동치이므로 2를 사용하면, 우리는 $\Gamma\models\alpha$와 $\Gamma\models\neg\alpha$를 얻습니다. 이때 $\Gamma$를 만족가능하게 하는 해석이 존재한다고 합시다. 이를 $\mathcal{I}$라고 합시다. 그런데 $\Gamma\models\alpha$, $\Gamma\models\neg\alpha$와 $\mathcal{I}\models\Gamma$에 의해서 $\mathcal{I}$는 $\alpha$와 $\neg\alpha$를 모두 참으로 만들어야 하고 이는 모순입니다. 우리는 $\Gamma$가 만족가능하다는 가정에서 출발하여 모순을 낳았으므로 귀류법에 의해 $\Gamma$는 만족불가능합니다. 따라서 4로부터 5를 얻어냈습니다.

 마지막으로, 5에서 4를 증명하면 됩니다. 그런데 5에서 4는 자동적으로 증명됩니다. 5는 임의의 문장들의 집합에 대해 성립하기 때문에, 4를 증명하기 위해 임의의 어떤 $\Gamma\cup\{\alpha\}$를 택하더라도 여전히 이 집합은 문장들의 집합이기 때문에 5를 적용할 수 있습니다.

 따라서 모든 증명이 끝났습니다. 그런데 보통 2와 5만 직접 증명하기 때문에 추가적으로 증명을 쓰도록 하겠습니다. 2에서 5는 위에서 4에서 5로 쓴 것과 같습니다. 4를 가정해서 동치인 2를 이용해서 5를 이끌어냈기 때문입니다. 5에서 2만 보면 됩니다. 이도 간단합니다. 임의의 $\Gamma$와 $\alpha$에 대해 $\Gamma\vdash\alpha$라고 합시다. 도출가능성과 일관성의 관계에 의해서 $\Gamma\cup\{\neg\alpha\}$는 비일관적입니다. 이 집합은 문장들의 집합이므로 5를 사용할 수 있습니다. 5에 의해서ㅡ5의 대우를 사용하든, 혹은 MT rule($A\rightarrow B$와 $\neg B$로부터 $A$를 도출)을 사용하든ㅡ $\Gamma\cup\{\neg\alpha\}$는 만족불가능합니다. 다시 만족가능성과 논리적 함축의 관계에 의해서 $\Gamma\models\alpha$가 됩니다. 따라서 증명이 끝났습니다.

 건전성 정리를 했던 것처럼 바꾸고 바꾸고 바꾸어서 하면 이런 결론이 도출됩니다. 증명방식도 위와 크게 다르지 않습니다. 사실 건전성 정리는 위와 같이 바꾸어서 증명하는 건 어렵고, 실제로는 $\vdash\Longrightarrow\models$의 방식으로 증명합니다. 그런데 완전성 정리는 그런 방식으로 괴델이 증명하긴 했지만 매우 복잡하고 별로 중요한 증명방식이 아닙니다. 후에 헨킨은 특히 Henkin Construction이라는 방법을 만들어서 일관성으로부터 만족가능성을 이끌어내는 매우 중요한 해석/모형을 만들어냈고 이것이 모형론의 기반이 되었습니다.

 어쨌든, 건전성+완전성 혹은 완전성 정리(앞으론 건전성+완전성을 완전성으로 쓰겠습니다)로부터 우리가 알 수 있는 건 ㅑ와 ㅏ라는 개념이 일치한다는 것입니다. 또한 만족가능성과 일관성이라는 개념이 일치한다는 것입니다. 또한 $\alpha\models\beta$는 "$\alpha$가 참이면 $\beta$도 언제나 참이다"이고 $\alpha\vdash\beta$는 "$\alpha$에 추론규칙을 사용하여 $\beta$를 얻는다"가 되고, 서로 일치하기 때문에 조건문은 참이라는 개념을 사용해서 생각될수도, 추론규칙의 방식으로도 이해될 수 있습니다. 연역정리로 생각한다면, $\models\alpha\rightarrow\beta$ 그리고 $\vdash\alpha\rightarrow\beta$와 일치하기 때문에 "$\alpha\rightarrow\beta$"의 위와 같이 의미를 정할 수 있습니다.

https://m.blog.naver.com/PostView.nhn?blogId=pdw9024&logNo=80190456642&proxyReferer=https:%2F%2Fwww.google.co.kr%2F

Cranberries, Bad wolves, Daria Stavrovich의 버젼입니다.

 아일랜드는 북아일랜드와 아일랜드공화국으로 나뉘는데, 북아일랜드는 영국에 속한다.

중세시대 아일랜드는 여러 왕국들로 이루어진 지역이었는데, 12세기에 영국이 아일랜드를 침략하면서부터 700년간 영국에게 침략/식민/수탈 당해왔다. 1914년이 되어서야 아일랜드인들의 노력으로 영국 의회에서 아일랜드 자치법이 통과되었다. 그러나 문제는 있었는데, 아일랜드 북부 지방(얼스터지방, 현재 북아일랜드)은 잉글랜드와 스코틀랜드 출신의 이민자들이 상당수 차지하고 있었고 이들은 아일랜드 자치령에 속하게 되는 것을 매우 반대했다. 그리하여 아일랜드에서는 많은 봉기들이 일어났다. 대표적으로는 1916년 부활절봉기를 들 수 있다. 이 사건을 기점으로 아일랜드에서는 무장봉기가 많이 일어나게 되었다. 급기야 1910년대 말에는  아일랜드 공화국군(IRA, Irish Republican Army)이 형성되고 여러 독립운동이 일어나게 된다. 1921년에는 결국 영국과의 협상 끝에 북아일랜드를 제외한 아일랜드 지방을 영국 자치령으로 두게 되었다. 북아일랜드는 변동없이 영국에 그대로 속하게 되었다.

 이 조약은 문제가 있었는데 아일랜드가 남북으로 갈라졌고 아일랜드인들은 완전한 독립을 원했기 때문이다. 비록 영국 본토가 아니라 자치령으로 승격되긴 했지만, 아일랜드는 외교, 군사권이 없었고 영국 국왕에게 충성을 맹세해야하고 아일랜드에 영국본토의 총독을 두어야 했기 때문이다. 이에 아일랜드는 조약 찬성자들과 반대자들로 나뉘게 되었고 IRA도 똑같이 나뉘게 되었다. 찬성측은 아일랜드 국방군으로 이어지게 되었고, 나머지 IRA 인원들은 IRA를 탈퇴하여 PIRA(Provisional Irish Republican Army)를 세우고 영국과도 아일랜드와도 대립하며 투쟁을 지속하였다. 이들이 이 곡에 주요한 역할을 한다.

 영국령에 그대로 남은 북아일랜드는 영국본토에서 온 사람들과 아일랜드 본토인들이 모두 거주하고 있었는데, 이들은 여러 대립과 충돌을 겪었다.  가장 큰 사건이 1972년에 북아일랜드 데리에서 충돌이 일어났던 것인데, 이때 영국본토군이 북아일랜드에 상륙해 비무장 북아일랜드인들에게 발포했고 14명이 사망하고 13명이 부상을 입었다ㅡ이들은 영국계과 아일랜드계 주민들의 동등한 권리를 요구했다ㅡ. 1월 30일 일요일이었고, 이 사건은 피의 일요일로 불리운다.
 사실 PIRA는 영국과 아일랜드의 압박 속에 힘을 많이 잃어갔는데, 이 사건 때문에 북부 아일랜드에 PIRA가 크게 득세했고, 그 뒤로 PIRA는 30년 넘게 영국과 북아일랜드 영국계와 대립하게 된다(2005년에 이들은 결국 무장 해제를 선언했고 평화적인 방식으로 문제를 해결하기로 선언했다. 이른바 굿 프라이데이 조약).
 1993년 워링턴 폭탄 테러 사건도 이들에 의한 사건이었다. PIRA는 영국본토의 워링턴에 폭탄 테러를 하였고 그로 인해 3살이었던 조나단 볼과 12살의 팀 패리가 사망하게 되었다(조나단 볼은 폭탄으로 인해 사망하였고, 패리는 병원에 옮겨졌었는데 의사의 실수로 연명장치 스위치를 잘못눌러 사망). Zombie는 이런 아일랜드 지역의 분쟁으로 인한 슬픔을 나타내고 두 희생자를 기리기 위해서 쓰여졌다.
 

Another head hangs lowly,
Child is slowly taken.
And the violence caused such silence,
Who are we mistaken?
또 누군가 참수되고,
아이는 아무도 모르게 끌려가
그리고 그런 침묵을 만든 폭력들,
길을 잘못든 우리들은 도대체 누구야?

But you see, it's not me, it's not my family.
In your head, in your head they are fighting,
With their tanks and their bombs,
And their bombs and their guns.
In your head, in your head, they are crying...
그러나 알다시피 이렇게 만든 건 나도, 우리 가족도 아니야
네 이념 때문에, 네 머리 속에서 그들이 싸우고 있어
전차와 폭탄들로,
폭탄들과 총으로.
네 이념 때문에, 네 머리 속에서, 그들은 절규하고 있어..


(What's) in your head, in your head,
Zombie, zombie, zombie,
Hey, hey, hey. What's in your head, In your head,
Zombie, zombie, zombie?
Hey, hey, hey, hey, oh, dou, dou, dou, dou, dou...
네 머리 속엔 도대체 뭐가 있는거야, 바로 네 머리 속에 말이야
좀비야, 좀비, 좀비처럼 행동하고 있어
이봐, 이봐, 이봐, 네 머리 속엔 도대체 뭐가 있는거야
좀비야, 좀비, 이념에 물든 좀비
...

Another mother's breakin',
Heart is taking over.
When the violence causes silence,
We must be mistaken.
또 다른 엄마는 망가져서
슬픔으로 심장이 멈출 것만 같아
폭력이 그런 정적을 야기한다면
우리는 뭔가 잘못된거야

It's the same old theme since nineteen-sixteen.
In your head, in your head they're still fighting,
With their tanks and their bombs,
And their bombs and their guns.
In your head, in your head, they are dying...
1916년 이후로 우리는 바뀐게 하나도 없어(1916년 부활절 봉기)
네 이념 때문에, 네 머리 속에서 그들은 아직도 싸우고 있어
전차와 폭탄,
폭탄과 총으로.
네 이념 때문에, 네 머리 속에서, 그들은 죽고 있어..

(What's) In your head, in your head,
Zombie, zombie, zombie,
Hey, hey, hey. What's in your head, In your head,
Zombie, zombie, zombie?
Hey, hey, hey, hey, oh, oh, oh,
Oh, oh, oh, oh, hey, oh, ya, ya-a...
네 머리 속엔 도대체 뭐가 있는거야, 바로 네 머리 속에 말이야
좀비야, 좀비, 좀비처럼 행동하고 있어
이봐, 이봐, 이봐, 네 머리 속엔 도대체 뭐가 있는거야
좀비야, 좀비, 이념에 물든 좀비
...


 원곡도 충분히 좋은 곡입니다만, 저는 Bad Wolves버전을 가장 좋아하고 그 다음으로는 Daria버전을 좋아합니다.. 참고로 Bad Wolves는 돌로레스와 함께 노래를 하기로 했으나  올해 1월에 사망하였습니다.

---

2018년에 네이버에서 번역한 곡으로 2018년 1월에 돌로레스가 떠났습니다.

드림시어터는 가족의 죽음에 관한 곡이 꽤 있습니다. 기타리스트인 존 페트루치의 아버지가 암에 걸려 사망한 뒤에 쓰인 곡입니다.
가사는 같지만 시점이 바뀌고 3인칭 주어가 지시하는 대상이 조금씩 달라진다는 게 흥미로운 점입니다.

해석이 조금은 필요합니다. 우선 아버지의 시점에서 노래가 시작되고, 병마에 걸린 배우 진 켈리에 대한 언급이 나타납니다. 참고로 진 켈리는 페트루치의 아버지 사후 같은 년도에 세상을 떴습니다. 어쨌든, 그러면서 아버지는 '내 영웅들을 앗아가실 수 있습니다. 그러니 내 고통도 덜어주시겠습니까?'라고 하는데, 나이를 먹으며 같이 늙고 세상을 뜬 아버지의 어렸을 적, 젊을 적의 영웅들을 뜻하고, 또한 '내 고통'의 정체는 바로 아래에서 드러납니다. 임종이 얼마 남지 않은 병상에는 찬공기와 슬픔, 울음을 참는 가족들이 있습니다. 그래서 그것이 자신에게는 큰 고통이기에, 신에게 가족이 겪는, 겪을 고통을 거둬주라고 합니다.

그리고 페트루치의 아버지는 진 켈리가 무대에서 내려오듯 삶이라는 무대에서 내려옵니다. 이제 페트루치의 시점으로 바뀝니다. 아버지의 유해를 강가에서 보내고 물에 비치는 자신의 얼굴을 보는데, 아버지가 마지막 순간에 자신의 이름을 속삭였던 것이 떠오릅니다. 그리고 신이 자신에게서 자신의 영웅, 아버지를 앗아갔다면서 자신의 고통도 가져가달라고 말합니다. 이제 아버지가 완전히 떠났다는 걸 자각하고, 아버지에게 보여줄 수 없었던 자신의 슬픔을 받아들이고 눈물을 흘립니다. 아버지가 떠났기 때문에 더 이상 괜찮은 척 감정을 숨기지 않아도 되니까요. 그리고 마지막으로 당신이 자신을 찾아올 때까지 당신없이 사는 법을 배워나갈 것이라고 하며 곡이 끝납니다.

Take Away My Pain

I was sitting on the edge of his bed
나는 그의 침대 끝자락에 앉아있었어
Staring at the headlines on the paper
신문의 헤드라인을 보면서 그는 말했어
He said, "look at poor gene Kelly
I guess he won't be singing in the rain."
"진 켈리 좀 봐. 안타까워. 비가 내려서 노래를 못부를 것 같아"
You can take away my heroes
당신은 제게서 제 영웅들을 데려가실 수 있습니다
Can you take away my pain
그러니 부디 제 아픔도 거둬주실 수 있으신가요

Take away my pain
제 고통을 거둬주세요
Leave the cold outside
한기를 밖으로 보내고,
Please don't let it rain
비가 내리지 않도록 해주세요
Don't stumble on my pride
내 자랑스런 이들이 넘어지지 않게 해주세요

Take away my pain
내 고통을 가져가 주세요
I'm not frightened any more
전 더 이상 두렵지 않습니다
Just stay with me tonight
오늘밤 저와 함께 있어주세요
I'm tired of this fight
전 더 이상 힘을 낼 수가 없어요
Soon I'll be knocking at your door
곧 당신이 계신 곳의 문을 두드리겠습니다


She was standing by the edge of his bed
그녀(페트루치의 어머니)는 그의 침대 끝자락에 서 있었어
Staring at the message on their faces
그들의 얼굴에 써져있는 슬픔을 보면서 그는 말했어
He said, "what else can you do babe?
I guess I won't be coming home again."
"아가들아 너희들이 더 이상 할 수 있는 건 없단다.
나는 집으론 더 이상 갈 수 없을 것 같구나"

They just took away all my promises
그들[암 고통 등]은 내 모든 약속들(나아서 집에 가겠다는)을 가져가버렸어
Make them take away my pain
그러니 내 고통들도 가져가거라

Take away my pain
제 고통을 거둬주세요
Leave the cold outside
한기를 밖으로 보내고,
Please don't let it rain
비가 내리지 않도록 해주세요
Don't stumble on my pride
내 자랑스런 이들이 넘어지지 않게 해주세요

Take away my pain
내 고통을 가져가 주세요
I'm not frightened any more
전 더 이상 두렵지 않습니다
Just stay with me tonight
오늘밤 저와 함께 있어주세요
I'm tired of this fight
전 더 이상 힘을 낼 수가 없어요
Soon I'll be knocking at your door
곧 당신이 계신 곳의 문을 두드리겠습니다

His final scene
그의 마지막 씬
The actor bows
배우는 절하네
And all those years
그간의 모든 세월들,
Are gone somehow
어떻게든 지나갔었지
The crowd applauds
관객들은 박수를 치고
The curtain falls
커튼이 내려오네

I was standing by the edge of the water
난 물가의 끝자락에 서있었습니다
I noticed my reflection in the waves
물결 위에 비치는 내 모습을 보고 있었어요
Then I saw you looking back at me
그러다 당신께서 뒤돌아 날 보는 걸 봤습니다
And I knew that for a moment
그리고 전 깨달았어요
You were calling out my name
당신께서 내 이름을 부르고 있다는걸요

You took away my hero
당신께선 내게서 영웅을 앗아갔어요
Will you take away my pain
부디, 내 고통도 함께 가져가주세요

Take away my pain
날 해방시켜주세요
Let the cold inside
이젠 모든걸 받아들일 때에요
It's time to let it rain
슬픔을 받아들일게요
There's nothing left to hide
이젠 숨길 게 없어요

Take away my pain
내 고통을 가져가주세요
I'm not frightened any more
난 더 이상 두렵지 않아요
I'm learning to survive
Without you in my life
당신 없이 사는 법을 배워갈거에요
Til you come knocking at my door.......
당신이 나를 찾아올 때까지..



해석이 많이 갈릴 수 있습니다. 기타리스트인 페트루치의 아버지의 죽음을 바탕으로 쓰여진 노래입니다. 지시대명사를 어떻게 해석하느냐에 따라 내용이 많이 달라질 수 있겠습니다만 저는 이런 방식으로 해석했습니다.

 아버지의 병상에 가족들이 다들 모여있습니다. 아버지는 신문을 보며 "켈리가 비가 내려 노래를 못할 것 같아."라고 하는데 아버지는 켈리를 자신에게 투영한다고 생각할 수 있습니다. 그리곤 그가 독백합니다. "당신(신으로 생각)은 제게서 제 영웅들(가족)을 앗아갈 수 있습니다. 그러면 부디 제 슬픔도 앗아가주세요." 아버지 입장에서보면 죽음은 자신에게서 가족들을 뺏어가는 것으로 생각할 수 있고, 다시 볼 수 없는 슬픔을 느낄 수 있습니다.

 그리곤 아들의 독백이 이어집니다. '죽음의 한기, 차가움, 고통, 슬픔아 오지마라. 죽음아 내 자랑스러운 아버지 위에 올라타지 말거라.' 누구나 죽음의 다가옴과 죽음을 받아들이고 싶지 않습니다. 그렇기 때문에 슬픔과 고통이 내게서 사라졌으면..이라고 생각하고, 그들이 오지 않기를 바랍니다. 그래서 또한 그것들이 와도 무덤덤히 있는척을 하고 그렇게 노력합니다. 그래야 슬프지 않을것이라고 생각하니까요

그 다음엔 아버지의 독백입니다. 죽음을 목전에 두고 신께 말합니다. "저는 더 이상 두렵지 않습니다. 그러나 저는 더 이상 힘을 낼 수가 없습니다. 제가 당신이 계신 곳의 문(천국의 문=죽음을 상징)을 두드릴 때까지 오늘 밤 제곁에 있어주시길 바랍니다"

 임종이 다가오고, 그녀(어머니)를 비롯한 가족들이 아버지의 옆에 서있습니다. 아버지는 임종이 옮을 깨닫고 가족에게 작별인사를 합니다. 그리곤 독백하기를 "퇴원하여 같이 놀러가고 밥을 먹고 행복하게 살자는 약속을 죽음(과 그와 관련된 것들)이 빼앗아가버렸구나. 이것들아 그럼 내 이 슬픔(가족을 더 이상 볼 수 없는)도 가져가거라." 코러스가 반복됩니다.

 임종의 순간을 옵니다. 아버지의 죽음을 배우의 연극의 마지막 씬으로 비유하고, 연극의 끝이 오자 아버지와 함께했던 순간들을 떠올립니다. 거대한 연극이 끝나고 관객들(가족)은 박수갈채(열렬히 살아온 그의 연극과 삶에 박수와 존경을 보냄) 하고 드디어 커튼이 내려옵니다.

 아버지의 장례가 끝나고 그의 재를 강에 흘려보냅니다. 멍하니 강에 비친 모습을 보다 문득 아버지께서 강을 건너다 뒤돌아 자신을 부르는 것 같은 생각이 들었습니다. 아들은 신께서 아버지를 데려갔음을 알고 자신의 아픔, 상실감도 함께 가져가주시기를 바랍니다.

 임종 이후 아들은 깨닫습니다. 죽음은 받아들이는 수밖에 없다는걸요. 그래서 그는 상실감, 아픔, 슬픔, 고통 모든 걸 받아들입니다. 더 이상 자신의 슬픔을 숨길 필요가 없다는 걸 알았습니다.

 슬픔은 이겨낼 수 없고 이겨내려해도 할 수 없다는 걸 깨닫습니다. 슬픔은 받아들이는 수밖에 없습니다. 모든 걸 받아들이고 더 이상 숨길것도 없고, 어찌 살아야할지 모든 걸 알았기 때문에 이젠 두려울 게 없습니다. 이제  아버지의 빈자리를 있는 그대로 느끼면서 다시 만날 때까지 살아갈 것을 다짐합니다.