논리학, 그 열다섯 번째 이야기 | 1차 논리에서의 건전성 정리 ( Soundness Theorem for First Order Logic )
이번 글에서는 1차 논리에서의 건전성 정리에 대하여 설명할 것이다. 건전성이란, 명제논리를 다룰 때 설명했던 것과 같이, 구문론적 함의관계 $\vdash$가 의미론적 함의관계 $\models$를 함의한다는 것이다. 즉, "$\Gamma \vdash \varphi$이면, $\Gamma \models \varphi$이다"라는 성질을 건전성이라고 한다. 1차 논리에서의 건전성 정리란, 1차 논리는 건전하다는 정리이다. 그럼 바로 본론으로 들어가자.
Theorem 1. 1차 논리에서의 건전성 정리 ( Soundness Theorem for First Order Logic )
| 1차 논리 언어가 주어졌고, 주어진 언어의 wff의 집합 $\Gamma$와 wff $\varphi$가 주어졌을 때, $\Gamma \vdash \varphi$가 성립한다면, $\Gamma \models \varphi$ 역시 성립한다. |
Proof.
$\varphi$에 대한 귀납법을 통해 증명하자.
만약, $\Gamma \vdash \varphi$라면, wff $\varphi$는 다음의 3가지로 분류할 수 있다.
1) $\varphi \in \Gamma$
2) $\varphi$가 1차 논리의 공리이다.
3) $\varphi$는 $\Gamma \vdash \psi$, $\Gamma \vdash \theta$를 만족하는 두 wff $\psi$, $\theta$에 MP를 적용한 결과이다.
이 중 1)의 경우는 $\Gamma \models \varphi$임이 자명하며, 3)의 경우 역시 귀납가정과 $\Gamma \models \varphi$의 정의에 의해 $\Gamma \models \varphi$임이 자명하다.
따라서 $\varphi$가 1차 논리의 공리인 경우만 생각하면 충분하다.
먼저, (A1), (A2), (A3)에 대해 살펴보자.
$\models_\mathfrak{A} \alpha [s]$일 때와 그렇지 않을 때, $\models_\mathfrak{A} \beta [s]$일 때와 그렇지 않을 때, $\models_\mathfrak{A} \alpha [s]$일 때와 그렇지 않을 때의 총 8가지 경우를 모두 따져 보면, 다음이 항상 성립한다는 것을 알 수 있다.
$$\models_\mathfrak{A} \left( \alpha \Rightarrow \left( \beta \Rightarrow \alpha \right) \right) [s] \\ \models_\mathfrak{A} \left( \left( \alpha \Rightarrow \left( \beta \Rightarrow \gamma \right) \right) \Rightarrow \left( \left( \alpha \Rightarrow \beta \right) \Rightarrow \left( \alpha \Rightarrow \gamma \right) \right) \right) [s] \\ \models_\mathfrak{A} \left( \left( \left( \neg \beta \right) \Rightarrow \left( \neg \alpha \right) \right) \Rightarrow \left( \left( \left( \neg \beta \right) \Rightarrow \alpha \right) \Rightarrow \beta \right) \right) [s]$$
따라서, $\varphi$가 (A1), (A2), (A3) 중 하나인 경우에는 $\models \varphi$가 성립하므로, $\Gamma \models \varphi$임은 자명하다.
먼저, $\varphi$가 (Q1)의 꼴인 경우를 생각해보자.
즉, $\varphi = \left( \forall x \alpha \Rightarrow \alpha^x_t \right)$이고, $t$가 $\alpha$에서 $x$에 대해 substitutable하다고 하자.
이때, $\models_\mathfrak{A} \forall x \alpha [s]$이면 $\models_\mathfrak{A} \alpha^x_t [s]$가 성립함을 증명하면, $\models \varphi$인 것이 증명되므로, $\Gamma \models \varphi$가 자명한 귀결이 된다.
따라서 $\models_\mathfrak{A} \forall x \alpha [s]$가 $\models_\mathfrak{A} \alpha^x_t [s]$를 함의함을 증명하면 충분하다.
이때, 만약 $\models_\mathfrak{A} \alpha^x_t [s]$인 것이 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것과 동치라면, $\models_\mathfrak{A} \forall x \alpha [s]$가 $\models_\mathfrak{A} \alpha^x_t [s]$를 함의함은 자명하다. 왜냐하면, $\models_\mathfrak{A} \forall x \alpha [s]$는 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \alpha [s(x|d)]$가 성립하는 것으로 정의되므로 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$가 당연히 성립하게 될 것이기 때문이다.
이에 대해 논의하기에 앞서, term $u$, $t$, 변수 $x$에 대하여 $u$의 모든 $x$를 $t$로 치환한 term을 $u^x_t$라고 할 때, $\bar{s}(u^x_t) = \overline{s(x|\bar{s}(t))}(u)$임을 보이자.
이를 보이기 위해 $u$에 대한 귀납법을 사용할 것이다.
만약 $u$가 $x$가 아닌 변수라면, $u^x_t = u$이므로 위 등식은 $\bar{s}(u) = \bar{s}(u)$로 환원되므로 성립한다.
만약 $u=x$라면, $u^x_t = t$이므로 위 등식은 $\bar{s}(t) = \bar{s}(t)$로 환원되므로 성립한다.
만약 term $t_1, t_2, \cdots, t_k$에 대하여 위 등식이 성립하고 $k$항 function symbol $f$에 대하여 $u = ft_1t_2\cdots t_k$라면, $u^x_t = f(t_1)^x_t(t_2)^x_t\cdots(t_k)^x_t$이므로 귀납가정에 의해 위 등식은 $f^\mathfrak{A}\left(\overline{s(x|\bar{s}(t))}(t_1), \overline{s(x|\bar{s}(t))}(t_2), \cdots, \overline{s(x|\bar{s}(t))}(t_k)\right)=f^\mathfrak{A}\left(\overline{s(x|\bar{s}(t))}(t_1), \overline{s(x|\bar{s}(t))}(t_2), \cdots, \overline{s(x|\bar{s}(t))}(t_k)\right)$로 환원되므로 성립한다.
즉, 모든 term $u$, $t$, 변수 $x$에 대하여 $\bar{s}(u^x_t) = \overline{s(x|\bar{s}(t))}(u)$이다.
이제 원래 논의로 돌아와서 $\models_\mathfrak{A} \alpha^x_t [s]$인 것과 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것이 동치임을 보이자.
이번엔 $\alpha$에 대한 귀납법을 통해 증명할 것이다.
먼저, $\alpha$가 원자명제인 경우를 생각하자. $\alpha$가 원자명제라면, 어떤 자연수 $k$가 존재하여, 어떤 $k$항 predicate symbol $P$에 대하여 $\alpha = Pu_1u_2\cdots u_k$이다.
그런데, $\models_\mathfrak{A} \alpha^x_t [s]$인 것은 $\models_\mathfrak{A} P(u_1)^x_t(u_2)^x_t\cdots(u_k)^x_t [s]$인 것과 동치이고, 이는 곧 $\left( \bar{s}((u_1)^x_t), \bar{s}((u_2)^x_t), \cdots, \bar{s}((u_k)^x_t) \right) \in P^\mathfrak{A}$인 것과 동치이며, 이는 곧 $\left( \overline{s(x|\bar{s}(t))}(u_1), \overline{s(x|\bar{s}(t))}(u_2), \cdots, \overline{s(x|\bar{s}(t))}(u_k) \right) \in P^\mathfrak{A}$인 것과 동치이며, 이는 곧 $\models_\mathfrak{A} Pu_1u_2\cdots u_k [s(x|\bar{s}(t))]$인 것과 동치이며, 이는 곧 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$와 동치이므로, $\alpha$가 원자명제인 경우에는 $\models_\mathfrak{A} \alpha^x_t [s]$인 것과 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것이 동치이다.
이번엔 $\alpha$가 $\left( \neg \beta \right)$꼴이거나 $\left( \beta \Rightarrow \gamma \right)$꼴인 경우를 생각하자. 이 경우에는 귀납가정에 의해 $\models_\mathfrak{A} \alpha^x_t [s]$인 것과 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것과 동치이다.
이번엔 $\alpha$가 $\forall y \beta$이고 $x$가 $\alpha$의 자유변수가 아닌 경우를 생각하자. 이 경우에는 두 함수 $\bar{s}$와 $\overline{s(x|\bar{s}(t))}$의 $\alpha$의 자유변수에 대한 함숫값이 일치함이 자명하며, $\alpha^x_t$와 $\alpha$가 같은 wff가 되므로 $\models_\mathfrak{A} \alpha^x_t [s]$와 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$는 동치이다.
이번엔 $\alpha$가 $\forall y \beta$이고 $x$가 $\alpha$의 자유변수인 경우를 생각하자. 이 경우에는 $t$가 $\alpha$에서 $x$에 대해 substitutable하다는 조건으로부터 $y$가 $t$의 변수가 아니며 동시에 $t$가 $\beta$에서 $x$에 대해 substitutable하다는 사실을 알 수 있다.
따라서 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\bar{s}(t) = \overline{s(y|d)}(t)$가 성립함을 알 수 있다. $x$가 $\alpha$의 자유변수이므로 $x \neq y$임이 자명하며, 따라서 $\alpha^x_t = \forall y \beta^x_t$임을 알 수 있다.
그러므로, $\models_\mathfrak{A} \alpha^x_t [s]$인 것은 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \beta^x_t [s(y|d)]$인 것과 동치이며, 이는 귀납가정과 $\bar{s}(t) = \overline{s(y|d)}(t)$라는 사실로부터 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \beta [s(y|d)(x|\bar{s}(t))]$인 것과 동치임을 알 수 있다. 이때, $x \neq y$이므로 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \beta [s(y|d)(x|\bar{s}(t))]$인 것은 $\models_\mathfrak{A} \forall y \beta [s(x|\bar{s}(t))]$인 것과 동치이다. 따라서 $\models_\mathfrak{A} \alpha^x_t [s]$인 것은 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것과 동치이다.
따라서 귀납법에 의해 임의의 wff $\alpha$에 대하여 $\models_\mathfrak{A} \alpha^x_t [s]$인 것은 $\models_\mathfrak{A} \alpha [s(x|\bar{s}(t))]$인 것과 동치이다.
그러므로 $\varphi$가 (Q1)꼴의 wff라면, $\models \varphi$이므로 $\Gamma \models \varphi$가 성립한다.
이제 $\varphi$가 (Q2)의 꼴인 경우를 생각해보자.
즉, $\varphi = \left( \alpha \Rightarrow \forall x \alpha \right)$이고 $x$가 $\alpha$의 자유변수가 아니라고 하자.
이때, $\models_\mathfrak{A} \alpha [s]$가 $\models_\mathfrak{A} \forall x \alpha [s]$를 함의함을 증명한다면, $\models \varphi$가 증명되며, 이로 인해 $\Gamma \models \varphi$는 자명한 귀결이 된다.
그런데, $\models_\mathfrak{A} \forall x \alpha [s]$는 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \alpha [s(x|d)]$인 것과 동치이며, $x$가 $\alpha$의 자유변수가 아니므로 $\alpha$의 모든 자유변수에 대하여 $\bar{s}$와 $\overline{s(x|d)}$의 함숫값이 일치한다. 즉, $\models_\mathfrak{A} \alpha [s]$인 것과 $\models_\mathfrak{A} \alpha [s(x|d)]$인 것은 동치이다. 따라서 $\models_\mathfrak{A} \alpha [s]$인 것과 $\models_\mathfrak{A} \forall x \alpha [s]$인 것이 동치임을 알 수 있으며, 이로 인해 $\varphi$가 (Q2)꼴의 wff인 경우, $\Gamma \models \varphi$가 성립함을 알 수 있다.
이제 $\varphi$가 (Q3)의 꼴인 경우를 생각해보자.
즉, $\varphi = \left( \forall x \left( \alpha \Rightarrow \beta \right) \Rightarrow \left( \forall x \alpha \Rightarrow \forall x \beta \right) \right)$라고 하자.
이때, $\models_\mathfrak{A} \forall x \left( \alpha \Rightarrow \beta \right) [s]$가 $\models_\mathfrak{A} \left( \forall x \alpha \Rightarrow \forall x \beta \right) [s]$를 함의함을 증명한다면, $\models \varphi$가 증명되며, 이로 인해 $\Gamma \models \varphi$는 자명한 귀결이 된다.
그런데, $\models_\mathfrak{A} \forall x \left( \alpha \Rightarrow \beta \right) [s]$는 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \left( \alpha \Rightarrow \beta \right) [s(x|d)]$인 것과 동치이며, 이는 곧 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\not \models_\mathfrak{A} \alpha [s(x|d)]$이거나 $\models_\mathfrak{A} \beta [s(x|d)]$인 것과 동치이다.
따라서 만약 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \alpha [s(x|d)]$라면, 자동적으로 임의의 $d \in \lvert \mathfrak{A} \rvert$에 대하여 $\models_\mathfrak{A} \beta [s(x|d)]$일 수밖에 없다. 동치인 다른 명제로 말하자면, $\models_\mathfrak{A} \forall x \alpha [s]$가 $\models_\mathfrak{A} \forall x \beta [s]$를 함의하게 된다. 따라서 $\models_\mathfrak{A} \forall x \left( \alpha \Rightarrow \beta \right) [s]$는 $\models_\mathfrak{A} \left( \forall x \alpha \Rightarrow \forall x \beta \right) [s]$를 함의한다.
따라서 $\varphi$가 (Q3) 꼴의 wff인 경우, $\models \varphi$가 성립하며, 이로 인해 $\Gamma \models \varphi$ 역시 성립함을 알 수 있다.
먼저, $\varphi$가 (E1)의 꼴인 경우를 생각해보자.
즉, $\varphi = \left( x = x \right)$라고 하자.
그런데, 임의의 구조 $\mathfrak{A}$와 임의의 함수 $s : V \to \lvert \mathfrak{A} \rvert$에 대하여, $\bar{s}(x) = \bar{s}(x)$임은 자명하므로 $\models_\mathfrak{A} =xx [s]$임은 자명하다.
따라서 $\models x=x [s]$이며, 이는 곧 $\Gamma \models \varphi$를 함의한다.
이제 $\varphi$가 (E2)의 꼴인 경우를 생각해보자.
즉, $\varphi = \left( x=y \Rightarrow \left( \alpha \Rightarrow \alpha' \right) \right)$이고 $\alpha'$을 $\alpha$에 등장하는 $x$의 전부 또는 일부를 $y$로 치환한 wff라고 하자.
만약, $\alpha'$이 $\alpha$라면, $\varphi$는 공리 (A1), (A2)와 MP를 통해 얻을 수 있는 wff가 되므로 $\models \varphi$임은 자명하다.
따라서 이제 수학적 귀납법에 의해 $\alpha'$이 $\alpha$에 등장하는 $x$ 중 단 하나만을 $y$로 치환한 wff인 경우만 따져도 충분하다.
그런데, $\models_\mathfrak{A} x=y [s]$가 성립한다면, 임의의 자연수 $k$와 $k+1$항 function symbol $f$, $k$개의 term $t_1, t_2, \cdots, t_k$에 대하여 $f^\mathfrak{A}(\bar{s}(x), \bar{s}(t_1), \bar{s}(t_2), \cdots, \bar{s}(t_k)) = f^\mathfrak{A}(\bar{s}(y), \bar{s}(t_1), \bar{s}(t_2), \cdots, \bar{s}(t_k))$가 성립함은 자명하다.
따라서 귀납법에 의해 $\alpha'$이 $\alpha$에 등장하는 $x$ 중 단 하나만을 $y$로 치환한 wff인 경우에는 $\models_\mathfrak{A} \left( x=y \Rightarrow \left( \alpha \Rightarrow \alpha' \right) \right) [s]$가 임의의 구조 $\mathfrak{A}$와 임의의 함수 $s : V \to \lvert \mathfrak{A} \rvert$에 대하여 성립한다.
즉, $\models \left( x = y \Rightarrow \left( \alpha \Rightarrow \alpha' \right) \right)$가 성립하며, 수학적 귀납법에 의해 $\models \varphi$가 성립함을 알 수 있다.
따라서 $\varphi$가 (E2) 꼴의 wff인 경우, $\Gamma \models \varphi$가 성립한다.
따라서 $\varphi$가 공리일 때, $\Gamma \models \varphi$가 성립하며, 이로 인해 증명이 완성된다.
$\blacksquare$
건전성 정리에는 한 가지 매우 유명한 동치 명제가 존재한다. 해당 명제를 소개하기 전에 정의해야 할 것들이 있다. 다음 정의를 보자.
| 1차 논리 언어가 주어졌고, 주어진 언어의 wff의 집합 $\Gamma$가 주어졌다고 하자. 그러면 $\Gamma$가 Satisfiable하다는 것은 어떤 구조 $\mathfrak{A}$와 어떤 함수 $s : V \to \lvert \mathfrak{A} \rvert$가 존재해서 $\Gamma$의 모든 원소 $\varphi$에 대하여 $\models_\mathfrak{A} \varphi [s]$가 성립한다는 것을 말한다. |
| 1차 논리 언어가 주어졌고, 주어진 언어의 wff의 집합 $\Gamma$가 주어졌다고 하자. 그러면 $\Gamma$가 Consistent하다는 것은 $\Gamma \vdash \varphi$이면서 동시에 $\Gamma \vdash \neg \varphi$인 wff $\varphi$가 존재하지 않는다는 것을 말한다. |
이제 건전성 정리의 동치 명제에 대해 알아보자. 다음 정리를 보라.
Theorem 2. 건전성 정리와 그의 동치 명제 ( Soundness Theorem and Its Equivalence )
| 1차 논리 언어가 주어졌다고 하자. 그러면 다음 두 명제는 동치이다. (a) $\Gamma \vdash \varphi$이면 $\Gamma \models \varphi$이다. (b) $\Gamma$가 satisfiable하면 $\Gamma$는 consistent하다. |
Proof.
Part (a) -> (b)
귀류법을 이용한 증명을 하기 위해 (a)가 성립하고 $\Gamma$가 satisfiable하지만, $\Gamma \vdash \varphi$이고 $\Gamma \vdash \neg \varphi$인 wff $\varphi$가 존재한다고 가정해보자.
$\Gamma$가 satisfiable하므로 어떤 구조 $\mathfrak{A}$와 어떤 함수 $s : V \to \lvert \mathfrak{A} \rvert$가 존재하여 임의의 $\psi \in \Gamma$에 대하여 $\models_\mathfrak{A} \psi [s]$가 성립한다.
그런데, $\Gamma \vdash \varphi$라는 사실과 (a)로부터 $\Gamma \models \varphi$임을 알 수 있으므로 $\models_\mathfrak{A} \varphi [s]$가 성립함을 알 수 있다.
또한, 같은 방식으로 $\models_\mathfrak{A} \neg \varphi [s]$ 역시 성립함을 알 수 있다.
그런데, $\models_\mathfrak{A} \neg \varphi [s]$인 것은 $\not \models_\mathfrak{A} \varphi [s]$인 것과 동치이므로 $\models_\mathfrak{A} \varphi [s]$인 것과 모순이다.
따라서 (a)가 성립하면, (b)가 성립한다.
Part (b) -> (a)
귀류법을 이용한 증명을 하기 위해 (b)가 성립하고 $\Gamma \vdash \varphi$가 성립하지만, $\Gamma \not \models \varphi$라고 가정하자.
그러면 $\Gamma \vdash \varphi$로부터 $\Gamma \cup \{ \neg \varphi \}$는 inconsistent함을 알 수 있다.
따라서 (b)에 의해 $\Gamma \cup \{ \neg \varphi \}$는 unsatisfiable하며, 이는 곧 임의의 구조 $\mathfrak{A}$, 함수 $s : V \to \lvert \mathfrak{A} \rvert$에 대하여 $\not \models_\mathfrak{A} \neg \varphi [s]$이거나 어떤 $\psi \in \Gamma$에 대해 $\not \models_\mathfrak{A} \psi [s]$임을 의미한다.
이제 $\Gamma \not \models \varphi$라는 사실에 주목해보자. 이는 곧 임의의 $\psi \in \Gamma$에 대하여 $\models_\mathfrak{A} \psi [s]$가 성립하면서 동시에 $\not \models_\mathfrak{A} \varphi [s]$인 구조 $\mathfrak{A}$와 함수 $s$가 존재함을 의미한다.
그런데, 임의의 $\psi \in \Gamma$에 대하여 $\models_\mathfrak{A} \psi [s]$가 성립하면, 위에서 보인 사실에 의해 $\not \models_\mathfrak{A} \neg \varphi [s]$가 성립하며, 이는 $\models_\mathfrak{A} \varphi [s]$와 동치이다. 따라서 임의의 $\psi \in \Gamma$에 대하여 $\models_\mathfrak{A} \psi [s]$가 성립하면, $\models_\mathfrak{A} \varphi [s]$가 성립함을 알 수 있으며, 이는 곧 정의에 의해 $\Gamma \models \varphi$가 성립함을 의미한다.
하지만, 이는 처음의 가정인 $\Gamma \not \models \varphi$라는 사실과 모순이며, 이로 인해 (b)가 (a)를 함의함이 증명된다.
$\blacksquare$
'수학 > 논리학 | Mathematical Logic' 카테고리의 다른 글
