일차논리(First-order logic)

정의1

$n$항함수($n$-ary function) :

$n \in $ $\mathbb{Z}^+$에 대해 임의의 집합 $X$의 $n$항함수 또는 $n$항연산을 $f : $ $X^n$ $ \to X$인 함수로 정의한다.

임의의 $(x_1,x_2,\cdots, x_n) \in X^n$에 대해 $f(x_1,x_2,\cdots,x_n) = f(\,(x_1,x_2,\cdots, x_n) \,) $으로 표기할 수 있다.

$1$항연산을 단항연산 또는 일항연산이라 표기할 수 있고 $2$항연산을 이항연산이라 표기할 수 있다.

$n$항관계($n$-ary relation) : 

$n \in \mathbb{Z}^+$에 대해 임의의 집합 $X$의 $n$항관계 $R$을 $X$의 $n$-데카르트곱의 부분집합 $R \subseteq X^n$로 정의한다.

임의의 $x_1,x_2,\cdots, x_n \in X$이 $n$항관계 $R$을 만족하기 위한 필요충분조건은 $(x_1,x_2,\cdots, x_n) \in R$인 것이다.

$(x_1,x_2,\cdots, x_n) \in R$을 $R(x_1,x_2,\cdots, x_n)$로 표기할 수 있다.

$1$항관계를 단항관계 또는 일항관계라 표기할 수 있고 $2$항관계를 이항관계라 표기할 수 있다.

 

 

 

정의2

언어(language) : 

함수기호들의 집합이 $\mathcal{F}$이고 관계기호들의 집합이 $\mathcal{R}$이고 상수기호들의 집합이 $\mathcal{C}$일때

기호들의 임의의 집합 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$을 언어로 정의한다.

언어의 구조(structure) :

언어가 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$이고 공집합이 아닌 집합이 $M$일때

각각의 함수기호 $f \in \mathcal{F}$에 유일하게 대응되고 $n_f \in \mathbb{Z}^+$인 $n_f$항함수 $ f_{\mathcal{M}} : M^{n_f} \to M$와

각각의 관계기호 $R \in \mathcal{R}$에 유일하게 대응되고 $n_R \in \mathbb{Z}^+$인 $n_R$항관계 $ R_\mathcal{M} \subseteq M^{n_R}$과

각각의 상수기호 $c \in \mathcal{C}$에 유일하게 대응되는 상수 $c_\mathcal{M}\in M$에 대해

$\mathcal{M}(f) = f_{\mathcal{M}} $과 $\mathcal{M}(R) = R_\mathcal{M} $과 $\mathcal{M}(c) = c_\mathcal{M}$이 함수값이고 정의역이 $\mathcal{L}$인

함수 $\mathcal{M}$을 $\mathcal{L}$-구조로 정의하고 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$과 같이 순서쌍 형태로 표기한다.

기호 $f,R,c \in \mathcal{L}$에 대응되는 $f_\mathcal{M},R_\mathcal{M},c_\mathcal{M}$을 각각 $f,R,c$의 해석(interpretation)으로 정의하고

집합 $M$을 $\mathcal{L}$-구조 $\mathcal{M} $의 전체(universe)로 정의한다.

언어의 매장(embedding) :

언어가 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$이고 $\mathcal{L}$-구조가 $\mathcal{N} = (N,f_\mathcal{N},R_\mathcal{N},c_\mathcal{N})$과 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$일때

임의의 함수기호 $f \in \mathcal{F}$와 임의의 $a_1,\cdots,a_{n_f} \in N$에 대해

$\eta(f_\mathcal{N}(a_1,\cdots,a_{n_f})) = f_\mathcal{M}(\eta(a_1),\cdots, \eta(a_{n_f}))$이고

임의의 관계기호 $R \in \mathcal{R}$과 임의의 $a_1,\cdots,a_{n_R} \in N$에 대해

$R_\mathcal{N}(a_1,\cdots, a_{n_R} )$이기 위한 필요충분조건이 $R_\mathcal{M}(\eta(a_1),\cdots, \eta(a_{n_R}) )$인 것이고

임의의 상수기호 $c \in \mathcal{C}$에 대해 $\eta(c_\mathcal{N}) = c_\mathcal{M}$인 단사함수 $\eta : N \to M$를 $\mathcal{N}$에서 $\mathcal{M}$으로의 $\mathcal{L}$-매장으로 정의한다.

$\mathcal{L}$-매장 $\eta : N \to M$가 전단사이면 $\eta$를 $\mathcal{N}$에서 $\mathcal{M}$으로의 $\mathcal{L}$-동형사상이라 정의하고

$\mathcal{N}$에서 $\mathcal{M}$으로의 $\mathcal{L}$-동형사상이 존재하면 $\mathcal{N}$과 $\mathcal{M}$을 $\mathcal{L}$-동형이라 정의한다.

부분구조(substructure) : 

$\mathcal{L}$-구조 $\mathcal{N} = (N,f_\mathcal{N},R_\mathcal{N},c_\mathcal{N})$과 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$의 전체가 $N\subseteq M$일때

임의의 함수기호 $f \in \mathcal{F}$와 임의의 $a_1,\cdots,a_{n_f} \in N$에 대해 $f_\mathcal{N}(a_1,\cdots,a_{n_f}) = f_\mathcal{M}(a_1,\cdots, a_{n_f})\in N$이고

임의의 관계기호 $R \in \mathcal{R}$과 임의의 $a_1,\cdots,a_{n_R} \in N$에 대해 $R_\mathcal{N}(a_1,\cdots, a_{n_R} )$과 $R_\mathcal{M}(a_1,\cdots, a_{n_R} )$이 동치이고

임의의 상수기호 $c \in \mathcal{C}$에 대해 $c_\mathcal{N} = c_\mathcal{M} \in N$이면

$\mathcal{N}$을 $\mathcal{M}$의 부분구조라고 정의하고 $\mathcal{M}$은 $\mathcal{N}$의 확장(extension)이라 정의한다.

 

 

 

정의3(일차논리)

일차논리 :

아래에서 정의된 기호, 논리식, 공리, 추론규칙으로 이루어진 형식계를 일차논리로 정의한다.

일차논리의 기호집합에 포함되는 언어가 $\mathcal{L}$일때 언어가 $\mathcal{L}$인 일차논리 또는 $\mathcal{L}$-일차논리라고 정의한다.

언어를 명시하지 않으면 일차논리의 언어는 임의로 가정한다.

일차논리의 기호 :

임의의 언어 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$과 등호집합 $\{ =\}$과 가부번인 변수기호집합과

괄호집합 $\{ (,)\}$과 쉼표집합 $\{ , \}$과 결합자기호집합 $\{ \neg, \to\}$과 한정기호집합 $\{ \forall \}$의 합집합을

$\mathcal{L}$-일차논리의 기호집합으로 정의한다.

또 기호집합들은 모두 서로소라고 가정한다.

일차논리의 항(term) :

$\mathcal{L}$-일차논리의 항들을 $\mathcal{L}$-항이라 정의할때 다음 1, 2, 3번을 만족하는 모든 집합 $\mathcal{T}$에 대해

$T\subseteq \mathcal{T}$이고 1, 2, 3을 만족하는 집합 $T$를 $\mathcal{L}$-항집합으로 정의한다.

1. $x$가 변수기호로만 구성된 길이가 $1$인 문자열이면 $x \in \mathcal{T}$이다.

2. $c$가 상수기호 $c \in \mathcal{C}$로만 구성된 길이가 $1$인 문자열이면 $c \in \mathcal{T}$이다.

3. $f \in \mathcal{F}$가 $n_f$항함수에 대응되는 함수기호이고 길이가 유한인 문자열 $t_1, t_2,\cdots, t_{n_f}$가 $t_1, t_2,\cdots, t_{n_f} \in \mathcal{T}$이면

길이가 유한인 문자열 $f(t_1,t_2,\cdots, t_{n_f})$는 $f(t_1,t_2,\cdots, t_{n_f})\in \mathcal{T}$이다.

일차논리의 원자논리식(atomic formula) :

$\mathcal{L}$-일차논리의 원자논리식들을 $\mathcal{L}$-원자논리식이라 정의할때

다음 1, 2번을 만족하는 문자열을 $\mathcal{L}$-원자논리식으로 정의한다.

1. $R \in \mathcal{R}$이 $n_R$항관계에 대응되는 관계기호이고

길이가 유한인 문자열 $t_1, t_2,\cdots, t_{n_R}$이 모두 $\mathcal{L}$-항이면 길이가 유한인 문자열 $R(t_1,t_2,\cdots, t_{n_R})$은 $\mathcal{L}$-원자논리식이다.

2. 길이가 유한인 문자열 $t, u$가 모두 $\mathcal{L}$-항이면 길이가 유한인 문자열 $(t = u)$는 $\mathcal{L}$-원자논리식이다.

일차논리의 논리식 :

$\mathcal{L}$-일차논리의 논리식들을 $\mathcal{L}$-논리식이라 정의할때 다음 1, 2, 3번을 만족하는 모든 집합 $\mathcal{W}$에 대해

$W \subseteq \mathcal{W}$이고 1, 2, 3을 만족하는 집합 $W$를 $\mathcal{L}$-논리식집합으로 정의한다.

1. $p$가 $\mathcal{L}$-원자논리식이면 $p \in \mathcal{W}$이다.

2. 길이가 유한인 문자열 $\phi, \psi$가 $\phi, \psi\in \mathcal{W}$이면 길이가 유한인 문자열 $(\neg \phi),(\phi \to \psi)$는 $(\neg \phi),(\phi \to \psi)\in \mathcal{W}$이다.

3. 길이가 유한인 문자열 $\phi$가 $\phi \in \mathcal{W}$이고 $x$가 변수기호이면 길이가 유한인 문자열 $(\forall x)\phi$는 $(\forall x)\phi\in \mathcal{W}$이다.

$\land, \lor,\leftrightarrow,\exists$에 대한 논리식 :

$\phi,\psi$가 논리식이고 $x$가 변수기호일때 $(\phi \lor \psi) ,(\phi \land \psi), (\phi \leftrightarrow \psi),(\exists x) \phi$를 다음과 같은 논리식으로 정의한다.

1. $(\phi \lor \psi) = ((\neg \phi) \to \psi)$

2. $(\phi \land \psi) = (\neg (\phi \to (\neg \psi)))$

3. $(\phi \leftrightarrow \psi) = ((\phi \to \psi) \land (\psi \to \phi)) = (\neg ((\phi \to \psi) \to (\neg (\psi \to \phi))))$

4. $(\exists x) \phi = (\neg (\forall x) (\neg \phi))$

자유변수(free variables) :

논리식의 자유변수를 다음과 같이 정의한다.

1. 원자논리식 $\phi$에 변수기호 $x$가 포함되면 $x$는 $\phi$의 자유변수이다.

2. 변수기호 $x$가 논리식 $(\neg \phi)$의 자유변수이기 위한 필요충분조건은 $x$가 논리식 $\phi$의 자유변수인 것이다.

3. 변수기호 $x$가 논리식 $(\phi \to \psi)$의 자유변수이기 위한 필요충분조건은 $x$가 논리식 $\phi$ 또는 $\psi$의 자유변수인 것이다.

4. 변수기호 $x$가 논리식 $(\forall y) \phi$의 자유변수이기 위한 필요충분조건은 $x \ne y$이고 $x$가 논리식 $\phi$의 자유변수인 것이다. 

구속변수(bound variables) :

논리식 $\phi$에 포함되는 어떤 항이 변수기호 $x$를 포함할때 $x$가 $\phi$의 자유변수가 아니면 $x$를 $\phi$의 구속변수로 정의한다.

문장(sentence) :

자유변수가 없는 $\mathcal{L}$-논리식을 $\mathcal{L}$-문장으로 정의한다.

치환가능성(substitutability) :

논리식 $\phi$와 변수기호 $x$와 항 $t$에 대해 다음이 성립하면 $\phi$에서 $x$를 $t$로 치환가능하다고 정의한다.

1. $\phi$에 $x$가 포함되지 않으면 $\phi$에서 $x$를 $t$로 치환가능하다.

2. $\phi$에 $x$가 포함되고 $\phi$가 원자논리식이면 $\phi$에서 $x$를 $t$로 치환가능하다.

3. $\phi = (\neg \psi)$인 논리식 $\psi$에서 $x$를 $t$로 치환가능하면 $\phi$에서 $x$를 $t$로 치환가능하다.

4. $\phi = (\psi\to \theta)$인 논리식 $\psi,\theta$에서 $x$를 $t$로 치환가능하면 $\phi$에서 $x$를 $t$로 치환가능하다.

5. $\phi = (\forall y)\psi$인 변수기호 $y$와 논리식 $\psi$에 대해

$x =y$이거나 $x\ne y$일때 $t$에 $y$가 포함되지 않고 $\psi$에서 $x$를 $t$로 치환가능하면 $\phi$에서 $x$를 $t$로 치환가능하다.

치환한 논리식 :

논리식 $\phi$에서 변수기호 $x$를 항 $t$로 치환가능할때 $\phi$에서 $x$를 $t$로 치환한 논리식 $\phi[t/x]$를 다음과 같이 정의한다.

1. $\phi$에 $x$가 포함되지 않으면 $\phi[t/x] = \phi$이다.

2. $\phi$에 $x$가 포함되고 $\phi$가 원자논리식이면 $\phi[t/x]$는 $\phi$에서 $x$를 $t$로 치환한 논리식이다.

3. 논리식 $\psi$에 대해 $\phi = (\neg \psi)$일때 $\phi[t/x] = (\neg \psi[t/x])$이다.

4. 논리식 $\psi,\theta$에 대해 $\phi = (\psi\to \theta)$일때 $\phi[t/x] = (\psi[t/x]\to \theta[t/x])$이다.

5. 변수기호 $y$와 논리식 $\psi$에 대해 $\phi = (\forall y)\psi$일때

$x=y$이면 $\phi[t/x] = (\forall y)\psi$이고 $x\ne y$이면 $\phi[t/x] = (\forall y)\psi[t/x]$이다.

일차논리의 공리 :

$\phi, \psi,\theta$가 논리식이고 $t,u,v$가 항이고 $x,y$가 변수기호일때 다음은 공리이다.

1. $(\phi \to (\psi \to \phi))$

2. $((\phi \to (\psi \to \theta)) \to ((\phi \to \psi)\to(\phi \to \theta)))$

3. $(((\neg \phi) \to (\neg \psi)) \to (\psi \to \phi))$

4. $x$가 $\phi$의 자유변수가 아닐때 $((\forall x)\phi \to \phi)$ 

5. $x$가 $\phi$의 자유변수이고 $\phi$에서 $x$를 $t$로 치환가능할때 $((\forall x)\phi \to \phi[t/x])$

6. $x$가 $\phi$의 자유변수가 아닐때 $((\forall x)(\phi \to \psi) \to (\phi \to (\forall x) \psi))$

7. $(x = x)$

8. $x$가 $\phi$의 자유변수이고 $\phi$에서 $x$를 $t$와 $u$로 치환가능할때 $((t =u) \to (\phi[t/x] \to \phi[u/x]))$

일차논리의 추론규칙 :

다음 두 함수 $f,g_x$는 추론규칙이다.

임의의 논리식 $\phi, \psi$에 대해 $f(\phi, (\phi \to \psi)) = \psi$인 함수 $f$를 전건긍정(Modus Ponens)으로 정의한다.

임의의 변수기호 $x$와 임의의 논리식 $\phi$에 대해 $g_x(\phi) = (\forall x)\phi$인 함수 $g_x$를 일반화(Generalisation)로 정의한다.

 

 

 

정리1

명제논리의 논리식 $p$가 명제논리의 원자논리식 $p_1,p_2,\cdots,p_n$으로 구성되고 명제논리의 정리이면

$p_1,p_2,\cdots,p_n$을 임의의 일차논리의 논리식 $\phi_1, \phi_2,\cdots, \phi_n$으로 치환한 논리식 $\phi$는 일차논리의 정리이다.

증명

$p$는 명제논리의 정리이므로 명제논리의 공리 1,2,3과 전건긍정만 사용하여 증명된다.

어떤 $k \in \mathbb{N}$에 대해 $p$의 명제논리의 증명에서 나오는 원자논리식이 $p_1,p_2,\cdots,p_n,\cdots,p_{n+k}$일때

임의의 일차논리의 논리식 $\phi_1, \phi_2,\cdots, \phi_n,\cdots, \phi_{n+k}$에 대해 $p_i$를 $\phi_i$로 치환하면

일차논리의 공리 1,2,3과 전건긍정만 사용한 일차논리의 증명이므로 $\phi$는 일차논리의 정리이다.

 

 

 

정리2

일차논리의 논리식집합이 $W$일때 임의의 $\Sigma \subseteq W$와 임의의 $\phi,\psi \in W$에 대해 다음이 성립한다.

1. $\phi$가 $\Sigma \cup \{ \psi \}$의 정리이고

$\Sigma \cup \{ \psi \}$로부터 $\phi$의 증명에서 일반화를 적용한 모든 증명의 항 $(\forall x) \theta$에 대해 $x$가 $\psi$의 자유변수가 아니거나

$\psi$가 문장이면 논리식 $(\psi \to \phi)$는 $\Sigma$의 정리이다.

2. 어떤 $\theta \in W$에 대해 논리식 $\theta, (\neg \theta)$가 $\Sigma \cup \{ (\neg \phi) \}$의 정리이고

$\Sigma \cup \{ (\neg \phi) \}$로부터 $\theta, (\neg \theta)$의 증명에서 일반화를 적용한 모든 증명의 항 $(\forall x) \gamma$에 대해 $x$가 $\phi$의 자유변수가 아니거나

$\phi$가 문장이면 논리식 $\phi$는 $\Sigma$의 정리이다.

증명

1.

문장은 자유변수가 없으므로 일반화를 적용한 모든 $(\forall x) \theta$에 대해 $x$가 $\psi$의 자유변수가 아닐때만 증명한다.

$(\psi \to \phi)$가 $\Sigma$의 정리임을 $\Sigma \cup \{ \psi \}$로부터 $\phi$의 증명의 길이 $n \in \mathbb{Z}^+$에 대한 강귀납법을 사용하여 보인다.

$n = 1$일때

$\Sigma \cup \{ \psi \}$로부터 $\phi$의 증명의 정의와 합집합과 단일 원소집합의 정의로 $\phi$는 공리이거나 $\phi \in \Sigma$이거나 $\phi =\psi $이므로

$\phi$가 공리이거나 $\phi \in \Sigma$이면

$\begin{align*}  \Sigma \vdash & \; \phi \qquad \text{0번째 항 : } \text{공리이거나 } \phi \in \Sigma \\[0.5em]  \Sigma \vdash & \; (\phi \to (\psi \to \phi))  \qquad \text{1번째 항 : }  \phi,\psi \text{에 대한 일차논리의 공리1}  \\[0.5em]  \Sigma \vdash & \; (\psi \to \phi)  \qquad \text{2번째 항(정리) : } \text{0,1번째 항에 전건긍정을 적용} \end{align*} $    가 되어 $(\psi \to \phi)$는 $\Sigma$의 정리이다.

$\phi =\psi $이면 위 정리와 명제논리 정리로 $(\phi \to \phi) = (\psi \to \phi)$는 일차논리의 정리이므로 형식계 정리로 $\Sigma$의 정리이다.

모든 증명의 길이 $1,2,\cdots, k \in \mathbb{Z}^+$에 대해 가정이 성립할때

길이가 $k+1$인 $\Sigma \cup \{ \psi \}$로부터 $\phi$의 증명이 $\begin{align*} \Sigma \cup \{ \psi\} \vdash &\;  p_0  \\ &\; \vdots  \\ \Sigma \cup \{ \psi \} \vdash &\; p_{k-1}  \\ \Sigma \cup \{ \psi \}\vdash & \; \phi  \end{align*}$이면

$\phi$는 공리이거나 $\phi \in \Sigma \cup \{ \psi \}$이거나 이전 항들에 추론규칙을 적용하여 얻어진 논리식이므로

$\phi$는 공리이거나 $\phi \in \Sigma \cup \{ \psi \}$이면 $n = 1$일때처럼 $(\psi \to \phi)$는 $\Sigma$의 정리이다.

$\phi$가 이전 항들에 전건긍정 $f$를 적용하여 얻어졌다면

어떤 $\theta , (\theta \to \phi) \in \{ p_0, \cdots, p_{k-1} \}$에 대해 $f(\theta, (\theta \to \phi)) = \phi$이므로

$\theta, (\theta \to \phi) $는 증명의 길이가 $1$이상 $k$이하인 $\Sigma \cup \{ \psi \}$의 정리이고

$\theta$가 어떤 $\gamma \in \{ p_0, \cdots, p_{k-1} \}$에 대해 일반화를 적용한 $\theta = (\forall x) \gamma$일때 $x$는 $\psi$의 자유변수가 아니다.

따라서 귀납가정으로 $(\psi \to \theta), (\psi \to (\theta \to \phi))$는 $\Sigma$의 정리이므로

어떤 $m,r \in \mathbb{N}$에 대해 

$\begin{align*}  & \; \vdots \\  \Sigma \vdash & \; (\psi \to \theta) \qquad m \text{번째 항 : } \Sigma\text{의 정리} \\  & \; \vdots  \\  \Sigma \vdash & \; (\psi \to (\theta\to \phi)) \qquad m+r\text{번째 항 : }  \Sigma \text{의 정리} \\[0.5em]  \Sigma \vdash & \; ((\psi \to (\theta \to \phi)) \to ((\psi \to \theta) \to (\psi \to \phi))) \qquad m+r+1 \text{번째 항 : }\psi,\theta,\phi \text{에 대한 일차논리의 공리2}  \\[0.5em]  \Sigma \vdash &\; ((\psi \to \theta) \to (\psi \to \phi)) \qquad m+r+2\text{번째 항 : } m+r,m+r+1\text{번째 항에 전건긍정을 적용} \\[0.5em]  \Sigma \vdash & \; (\psi \to \phi)  \qquad m+r+3\text{번째 항(정리) : } m,m+r+2\text{번째 항에 전건긍정을 적용} \end{align*} \text{ 이다.} $

$\phi$가 어떤 변수기호 $x$와 이전 항에 대해 일반화를 적용하여 얻어졌다면

어떤 $\theta \in \{ p_0, \cdots, p_{k-1} \}$에 대해 $\phi = (\forall x) \theta$이므로 $\theta $는 증명의 길이가 $1$이상 $k$이하인 $\Sigma \cup \{ \psi \}$의 정리이고

$\theta$가 어떤 $\gamma \in \{ p_0, \cdots, p_{k-1} \}$에 대해 일반화를 적용한 $\theta = (\forall y) \gamma$일때 $y$는 $\psi$의 자유변수가 아니다.

따라서 귀납가정으로 $(\psi \to \theta)$는 $\Sigma$의 정리이고 $x$는 $\psi$의 자유변수가 아니므로

어떤 $m \in \mathbb{N}$에 대해 

$\begin{align*}  & \; \vdots \\  \Sigma \vdash & \; (\psi \to \theta) \qquad m \text{번째 항 : } \Sigma\text{의 정리}  \\[0.5em]  \Sigma \vdash & \; (\forall x)(\psi \to \theta) \qquad m+1 \text{번째 항 : }x,(\psi \to \theta) \text{에 대한 일반화}  \\[0.5em]  \Sigma \vdash &\; ((\forall x)(\psi \to \theta) \to (\psi \to (\forall x )\theta)) \qquad m+2\text{번째 항 : } \psi,\theta\text{에 대한 일차논리의 공리6} \\[0.5em]  \Sigma \vdash & \; (\psi \to (\forall x) \theta)   \qquad m+3\text{번째 항(정리) : } m+1,m+2\text{번째 항에 전건긍정을 적용} \end{align*} \text{ 이고} $

$(\psi \to \phi) = (\psi \to (\forall x) \theta)$는 $\Sigma$의 정리이다.

모든 $n \in \mathbb{Z}^+$에 대해 가정이 성립하므로 $(\psi \to \phi)$는 $\Sigma$의 정리이다.

2.

문장은 자유변수가 없으므로 일반화를 적용한 모든 $(\forall x) \gamma$에 대해 $x$가 $\phi$의 자유변수가 아닐때만 증명한다.

$\alpha \in W$가 임의의 일차논리의 공리일때

$\theta, (\neg \theta)$는 $\Sigma \cup \{ (\neg \phi) \}$의 정리이고 위 정리와 명제논리 정리로 $((\neg \theta) \to (\theta \to (\neg \alpha)))$는 일차논리의 정리이므로

형식계 정리로 $((\neg \theta) \to (\theta \to (\neg \alpha)))$는 $\Sigma \cup \{ (\neg \phi) \}$의 정리가 되어

어떤 $n,m,k \in \mathbb{N}$에 대해

$\begin{align*} & \; \vdots \\  \Sigma  \cup \{ (\neg \phi) \}\vdash &\; (\neg \theta) \qquad n \text{번째 항 : } \Sigma \cup \{ (\neg \phi) \}\text{의 정리} \\ & \; \vdots  \\  \Sigma \cup \{ (\neg \phi ) \} \vdash & \; \theta \qquad n+m\text{번째 항 : }  \Sigma \cup \{ (\neg \phi)\} \text{의 정리} \\ & \; \vdots  \\  \Sigma \cup \{ (\neg \phi ) \} \vdash &\; ((\neg \theta) \to (\theta \to (\neg \alpha))) \qquad n+m+k\text{번째 항 : }  \Sigma \cup \{ (\neg \phi)\} \text{의 정리} \\[0.5em]  \Sigma \cup \{ (\neg \phi ) \} \vdash &\; (\theta \to (\neg \alpha)) \qquad n+m+k+1 \text{번째 항 : } n,n+m+k\text{번째 항에 전건긍정을 적용}  \\[0.5em]  \Sigma \cup \{ (\neg \phi ) \} \vdash &\; (\neg \alpha) \qquad n+m+k+2 \text{번째 항(정리) : } n+m,n+m+k+1\text{번째 항에 전건긍정을 적용} \end{align*} \text{ 이고} $

$(\neg \alpha)$는 $\Sigma \cup \{ (\neg \phi) \}$의 정리이다.

또 $\Sigma \cup \{ (\neg \phi) \}$로부터 $\theta, (\neg \theta)$의 증명에서 일반화를 적용한 모든 $(\forall x) \gamma$에 대해 $x$가 $\phi$의 자유변수가 아니고

$\Sigma \cup \{ (\neg \phi) \}$로부터 $((\neg \theta) \to (\theta \to (\neg \alpha)))$의 증명에선 공리 1,2,3과 전건긍정만 사용하였으므로 

$\Sigma \cup \{ (\neg \phi) \}$로부터 $(\neg \alpha)$의 증명에서 일반화를 적용한 모든 $(\forall x) \gamma$에 대해 $x$가 $\phi$의 자유변수가 아니게 되어

1번으로 $((\neg \phi) \to (\neg \alpha))$는 $\Sigma$의 정리이다.

따라서 어떤 $r \in \mathbb{N}$에 대해

$\begin{align*} & \; \vdots \\  \Sigma \vdash &\; ((\neg \phi) \to (\neg \alpha)) \qquad r \text{번째 항 : } \Sigma\text{의 정리}  \\[0.5em]  \Sigma \vdash &\; (((\neg \phi) \to (\neg \alpha)) \to (\alpha \to \phi)) \qquad r+1 \text{번째 항 : } \phi,\alpha \text{에 대한 일차논리의 공리3}  \\[0.5em]  \Sigma \vdash & \; (\alpha \to \phi) \qquad r+2\text{번째 항 : } r,r+1\text{번째 항에 전건긍정을 적용} \\[0.5em]  \Sigma \vdash &\; \alpha \qquad r+3\text{번째 항 : } \text{임의의 일차논리의 공리} \\[0.5em] \Sigma \vdash & \; \phi  \qquad r+4\text{번째 항(정리) : } r+2,r+3\text{번째 항에 전건긍정을 적용} \end{align*}  $ 이므로

$\phi$는 $\Sigma$의 정리이다.

 

 

 

정리10

일차논리의 임의의 논리식 $\phi$가 $x$를 자유변수로 갖고 변수기호 $y$가 $\phi$에 포함되지 않으면

$((\forall x)\phi \to (\forall y) $$\phi[y / x]$$)$는 일차논리의 정리이다.

증명

$\begin{align*} \{ (\forall x) \phi \} \vdash & \; (\forall x)\phi \qquad \text{0번째 항 : 가정}  \\[0.5em]  \{ (\forall x) \phi \} \vdash & \; ((\forall x) \phi \to \phi[y/x])  \qquad \text{1번째 항 : 일차논리의 공리5} \\[0.5em]  \{ (\forall x) \phi\} \vdash & \; \phi[y/x]  \qquad \text{2번째 항 : } \text{0,1번째 항에 전건긍정을 적용} \\[0.5em] \{ (\forall x) \phi \} \vdash & \; (\forall y) \phi[y/x] \qquad \text{3번째 항(정리) : 2번째 항에 일반화를 적용} \end{align*} $   이고

$(\forall x) \phi$는 $y$를 자유변수로 갖지 않으므로 위 정리로 $((\forall x)\phi \to (\forall y)\phi[y/x])$는 일차논리의 정리이다.

 

 

 

정리19

언어가 $\mathcal{L}$인 일차논리의 논리식집합 $W$와 일차논리의 항집합 $T$에 대해 다음이 성립한다.

항집합의 구성 :

$T_0\subseteq T$이 변수기호 또는 $\mathcal{L}$의 상수기호로만 구성된 항들의 집합이고

모든 $n \in \mathbb{N}$에 대해 $T_0,T_1,\cdots,T_n \subseteq T$이 강귀납적으로 정의될때

모든 $n_f$항함수기호 $f \in \mathcal{L}$와 모든 $t_1,t_2,\cdots,t_{n_f} \in \displaystyle \bigcup_{i = 0}^nT_i$에 대해

$f(t_1,t_2,\cdots,t_{n_f}) \in T_{n+1}$로 $T_{n+1} \subseteq T$이 정의되면 $T = \displaystyle \bigcup_{i = 0}^\infty T_i$이다.

논리식집합의 구성 :

$W_0 \subseteq W$이 일차논리의 원자논리식들의 집합이고

모든 $n \in \mathbb{N}$에 대해 $W_0,W_1,\cdots,W_n \subseteq W$이 강귀납적으로 정의될때 

모든 변수기호 $x$와 모든 $\phi ,\psi \in \displaystyle \bigcup_{i = 0}^n W_n$에 대해

$(\neg \phi),(\phi \to \psi),(\forall x)\phi \in W_{n+1}$로 $W_{n+1} \subseteq W$이 정의되면 $W = \displaystyle \bigcup_{i = 0}^\infty W_i$이다.

증명

항집합의 구성

모든 $t \in \displaystyle \bigcup_{i = 0}^\infty T_i$에 대해 $t \in T_k$인 $k \in \mathbb{N}$가 존재하여 $t \in T$이므로 $  \displaystyle \bigcup_{i = 0}^\infty T_i \subseteq T$이고

모든 $t_1,\cdots, t_{n_f} \in \displaystyle \bigcup_{i = 1}^\infty T_i$는 $t_1,t_2,\cdots,t_{n_f} \in \displaystyle \bigcup_{i = 0}^kT_i$인 $k \in \mathbb{N}$가 존재하여

임의의 $n_f$항함수기호 $f \in \mathcal{L}$에 대해 $f(t_1,t_2,\cdots,t_{n_f}) \in T_{k+1} \subseteq \displaystyle \bigcup_{i = 0}^\infty T_i$이므로

$T$의 정의로 $T \subseteq \displaystyle \bigcup_{i = 1}^\infty T_i$이고 집합정리로 $T = \displaystyle \bigcup_{i = 1}^\infty T_i$이다.

논리식집합의 구성 

모든 $\phi \in \displaystyle \bigcup_{i = 0}^\infty W_i$에 대해 $\phi \in W_k$인 $k \in \mathbb{N}$가 존재하여 $\phi \in W$이므로 $\displaystyle \bigcup_{i= 0}^\infty W_i \subseteq W$이고

모든 $\phi,\psi \in \displaystyle \bigcup_{i = 0}^\infty W_i$는 $\phi, \psi \in \displaystyle \bigcup_{i = 0}^k W_i$인 $k \in \mathbb{N}$가 존재하여

임의의 변수기호 $x$에 대해 $(\neg \phi), (\phi \to \psi) ,(\forall x) \phi\in W_{k+1} \subseteq \displaystyle \bigcup_{i = 0}^\infty W_i$이므로

$W$의 정의로 $W \subseteq \displaystyle \bigcup_{i= 0}^\infty W_i $이고 집합정리로 $W = \displaystyle \bigcup_{i = 0}^\infty W_i$이다.

 

 

 

정의4(일차논리의 의미론)

일차논리 항의 해석(interpretation) :

언어가 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$인 일차논리의 항집합이 $T$이고 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$이 임의의 $\mathcal{L}$-구조일때 

위 정리의 집합 $T_0,T_1,\cdots \subseteq T$에 대해 모든 $t \in T_0$는 변수기호이거나 상수기호이므로

$t = x$가 변수기호이면 $M$의 임의의 원소 $s_0(t)=s_0(x) = x_\mathcal{M}\in M$으로

$t = c$가 상수기호이면 $c \in \mathcal{C}$에 대응되는 $\mathcal{M}$의 상수 $s_0(t)=s_0(c) = c_\mathcal{M}\in M$으로 함수 $s_0 : T_0 \to M$을 정의하고

모든 $n \in \mathbb{N}$에 대해 함수 $s_n : \displaystyle \bigcup_{i = 0}^n T_i \to M$이 귀납적으로 정의되면

모든 $t \in \displaystyle \bigcup_{i = 0}^{n+1} T_i $는 $t \in \displaystyle \bigcup_{i = 0}^{n} T_i $이거나 $t \in T_{n+1}$이므로 $t \in \displaystyle \bigcup_{i = 0}^{n} T_i $이면 $s_{n+1}(t) = s_n(t)$로 정의하고

$t \in T_{n+1}$이면 어떤 함수기호 $f \in \mathcal{F}$와 어떤 $t_1,t_2,\cdots,t_{n_f} \in \displaystyle \bigcup_{i = 0}^{n} T_i $에 대해 $t = f(t_1,t_2,\cdots,t_{n_f})$이므로

$f \in \mathcal{F}$에 대응되는 $\mathcal{M}$의 $n_f$항함수 $f_\mathcal{M}$에 대해

$s_{n+1}(t) = s_{n+1}(f(t_1,t_2,\cdots,t_{n_f})) = f_\mathcal{M}(s_n(t_1),s_n(t_2),\cdots,s_n(t_{n_f}))$로 함수 $s_{n+1} : \displaystyle \bigcup_{i = 0}^{n+1} T_i \to M$을 정의한다.

변수기호에 대해 임의로 $s_0 : T_0 \to M$이 정의될때 모든 $n \in \mathbb{N}$에 대해 $s_{n} : \displaystyle \bigcup_{i = 0}^{n} T_i \to M$은 유일하고

임의의 항 $t \in T = \displaystyle \bigcup_{i = 0}^\infty T_i$는 $t \in \displaystyle \bigcup_{i = 0}^{m} T_i $인 $m \in \mathbb{N}$이 존재하여 정렬성으로 최소인 $m$은 유일하므로

$s(t) = s_m(t)$인 함수 $s : T \to M$를 $\mathcal{M}$에 대한 항의 해석으로 정의한다.

치환한 항의 해석 :

언어가 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$인 일차논리의 항집합이 $T$이고

$\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$에 대한 항의 해석이 $s : T \to M$일때

항의 해석은 변수기호에 대한 함수값에 따라 함수가 결정되므로

임의의 $r \in M$과 임의의 변수기호 $x$에 대해 $s[r/x](x) = r$이고

$y \ne x$인 임의의 변수기호 $y$에 대해 $s[r/x](y) = s(y)$로 할당되는

항의 해석 $s[r/x] : T \to M$를 $s$에서 $x$를 $r$로 치환한 항의 해석으로 정의한다.

일차논리의 값매김 :

$\mathcal{L}$-일차논리의 논리식집합이 $W$이고 $(B,\lor,\land,\neg , \mathbf{F},\mathbf{T})$가 $\mathbf{F}\ne \mathbf{T}$인 불 대수일때

$\mathcal{L}$-구조 $\mathcal{M}$에 대한 임의의 항의 해석 $s : T \to M$와 위 정리의 집합 $W_0,W_1,\cdots \subseteq W$에 대해

모든 $\phi \in W_0$는 원자논리식이므로

$\phi \in W_0$가 어떤 관계기호 $R \in \mathcal{R}$과 어떤 항 $t_1,t_2,\cdots,t_{n_R} \in T$에 대해 $\phi = R(t_1,t_2,\cdots,t_{n_R})$이면

$R \in \mathcal{R}$에 대응되는 $\mathcal{M}$의 $n_R$항관계 $R_\mathcal{M}$에 대해

$v_{0,s}(\phi)=v_{0,s}(\,R(t_1,t_2,\cdots,t_{n_R})\,) =\mathbf{T}$이기 위한 필요충분조건이 $R_\mathcal{M}(s(t_1),s(t_2),\cdots,s(t_{n_R})) $인 것이고

$\phi \in W_0$가 등호 $=$와 어떤 항 $t,u \in T$에 대해 $\phi = (t = u)$이면

$v_{0,s}(\phi) = v_{0,s}(\,(t= u)\,) = \mathbf{T}$이기 위한 필요충분조건이 $s(t) = s(u)$인 함수 $v_{0,s} : W_0 \to \{\mathbf{F},\mathbf{T} \}$를 정의하고

$\mathcal{M}$에 대한 모든 항의 해석 $s:T\to M$와 모든 $n \in \mathbb{N}$에 대해 함수 $v_{n,s} : \displaystyle \bigcup_{i = 0}^nW_i \to \{\mathbf{F},\mathbf{T} \}$가 귀납적으로 정의되면

모든 $\theta \in \displaystyle \bigcup_{i = 0}^{n+1}W_i$는 $\theta \in \displaystyle \bigcup_{i = 0}^{n}W_i$이거나 $\theta \in W_{n+1}$이므로 $\theta \in \displaystyle \bigcup_{i = 0}^{n}W_i$이면 $v_{n+1,s}(\theta) = v_{n,s}(\theta)$로 정의하고

$\theta \in W_{n+1}$이면 어떤 변수기호 $x$와 어떤 $\phi,\psi \in \displaystyle \bigcup_{i = 0}^{n}W_i$에 대해 $\theta = (\neg \phi)$ 또는 $\theta = (\phi \to \psi)$ 또는 $\theta = (\forall x)\phi$이므로

$\theta = (\neg \phi)$ 또는 $\theta = (\phi \to \psi)$일때 $v_{n+1,s}(\,(\neg \phi)\,) = \neg v_{n,s}(\phi)$ 또는 $v_{n+1,s}(\,(\phi \to \psi)\,) = v_{n,s}(\phi) \to v_{n,s}(\psi)$로 

$\theta = (\forall x)\phi$일때 $s$에서 $x$를 임의의 $r \in M$로 치환한 항의 해석이 $s[r/x] : T \to M$이면

$v_{n+1,s}(\,(\forall x) \phi\,) = \mathbf{T}$이기 위한 필요충분조건이 모든 $r \in M$에 대해 $v_{n,s[r/x]}(\phi) =\mathbf{T}$인

함수 $v_{n+1,s} : \displaystyle \bigcup_{i = 0}^{n+1}W_i \to \{\mathbf{F},\mathbf{T} \}$를 정의한다.

임의의 항의 해석 $s : T \to M$에 대해 $v_{0,s} : W_0 \to \{ \mathbf{F},\mathbf{T} \}$이 정의될때

모든 $n \in \mathbb{N}$에 대해 $v_{n,s} : \displaystyle \bigcup_{i = 0}^nW_i \to \{ \mathbf{F},\mathbf{T}\} $은 유일하고

임의의 $\phi \in  W = \displaystyle \bigcup_{i = 0}^\infty W_i$는 $\phi \in  \displaystyle \bigcup_{i = 0}^m W_i$인 $m \in \mathbb{N}$이 존재하여 정렬성으로 최소인 $m$은 유일하므로

$v_s(\phi) = v_{m,s}(\phi)$인 함수 $v_s : W \to \{ \mathbf{F},\mathbf{T} \}$를 $s$에 대한 값매김으로 정의한다.

$\mathcal{L}$-구조 $\mathcal{M}$에 대한 항의 해석 $s$를 명시하지 않을땐 $s$에 대한 값매김 $v_s$를 $\mathcal{M}$의 값매김 $v_\mathcal{M}$으로 표기한다.

$\mathcal{M}$의 모든 값매김 $v_\mathcal{M}$은 $\mathcal{M}$에 대한 항의 해석 $s$가 존재하여 $s$에 대한 값매김 $v_s$에 대해 $v_\mathcal{M} = v_s$이다.

$\mathcal{L}$-구조 $\mathcal{M}$을 명시하지 않을땐 $\mathcal{M}$의 값매김 $v_\mathcal{M}$을 $\mathcal{L}$-일차논리의 값매김 $v$로 표기한다.

$\mathcal{L}$-일차논리의 모든 값매김 $v$는 $\mathcal{L}$-구조 $\mathcal{M}$이 존재하여 $\mathcal{M}$의 어떤 값매김 $v_\mathcal{M}$에 대해 $v = v_\mathcal{M}$이다.

만족가능성(satisfiability) :

$\mathcal{L}$-일차논리의 임의의 논리식 $\phi$에 대해 $\mathcal{L}$-구조 $\mathcal{M}$에 대한 항의 해석 $s$가 존재하여 

$s$에 대한 값매김 $v_s$에 대해 $v_s (\phi) = \mathbf{T}$이면 $\phi$가 $\mathcal{M}$에서 만족가능하다고 정의한다.

일차논리의 논리식집합 $W$의 임의의 부분집합이 $\Sigma \subseteq W$일때 어떤 $\mathcal{L}$-구조 $\mathcal{M}$이 존재하여

$\mathcal{M}$의 어떤 값매김 $v_\mathcal{M}$에 대해 모든 $\sigma \in \Sigma$가 $v_\mathcal{M}(\sigma) = \mathbf{T}$이면 $\Sigma$는 $\mathcal{L}$-일차논리에서 만족가능하다.

구조에서 참(true)인 논리식 :

$\mathcal{L}$-일차논리의 임의의 논리식이 $\phi$이고 $\mathcal{L}$-구조가 $\mathcal{M}$일때

$\mathcal{M}$의 모든 값매김 $v_\mathcal{M}$에 대해 $v_\mathcal{M}(\phi) = \mathbf{T}$이면 $\phi$가 $\mathcal{M}$에서 참이라고 정의하고 $\mathcal{M} \models \phi$로 표기한다.

모든 $\mathcal{M}$에 대해 $\mathcal{M} \models \phi$이면 논리식 $\phi$는 $\mathcal{L}$-일차논리의 논리적 귀결 $\models \phi$이다.

모델(model), 이론(theory) :

$\mathcal{L}$-일차논리의 임의의 문장이 $\psi$이고 $\mathcal{L}$-구조가 $\mathcal{M}$일때

$\mathcal{M} \models \psi$이면 $\mathcal{M}$을 $\psi$의 모델로 정의한다.

모든 $\psi\in T$가 $\mathcal{L}$-문장인 임의의 집합 $T$를 $\mathcal{L}$-이론으로 정의하고

모든 $\psi \in T$가 $\mathcal{M} \models \psi$이면 $\mathcal{M}$을 $T$의 모델로 정의하고 $\mathcal{M} \models T$로 표기한다.

$\mathcal{M} \models \psi$인 모든 $\mathcal{L}$-문장 $\psi$들의 집합을 $\mathcal{M}$의 이론으로 정의하고 $\operatorname{Th}(\mathcal{M})$으로 표기한다.

 

 

 

정리21

$\mathcal{L}$-일차논리의 논리식집합이 $W$이고 항집합이 $T$일때

$\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$에 대한 임의의 항의 해석 $s,h :T \to M$에 대해 다음이 성립한다.

1.

임의의 항 $t \in T$에 포함되는 모든 변수기호 $x$에 대해 $s(x) = h(x)$이면 $s(t) = h(t)$이다.

2.

임의의 논리식 $\phi \in W$에 포함되는 모든 자유변수 $x$에 대해 $s(x) = h(x)$이면

$s,h$에 대한 값매김 $v_s,v_h : W \to \{ \mathbf{F},\mathbf{T} \}$에 대해 $v_s(\phi) = v_h(\phi)$이다.

3.

임의의 논리식 $\phi \in W$가 문장이면 $s,h$에 대한 값매김 $v_s,v_h : W \to \{ \mathbf{F},\mathbf{T} \}$에 대해 $v_s(\phi) = v_h(\phi)$이다.

4.

항의 해석 $s$를 구성하는 함수열이 $s_0,s_1,\cdots$이고 집합열이 $T_0,T_1,\cdots \subseteq T$일때

$t \in T$에 대해 $t \in \displaystyle \bigcup_{i = 0}^mT_i$인 $m \in \mathbb{N}$이 최소이면 $m\le n$인 모든 $n \in \mathbb{N}$에 대해 $s_m(t) = s_n(t)$이다.

5.

$s$에 대한 값매김 $v_s : W \to \{ \mathbf{F},\mathbf{T} \}$를 구성하는 함수열이 $v_{0,s},v_{1,s},\cdots$이고 집합열이 $W_0,W_1,\cdots \subseteq W$일때

$\phi \in W$에 대해 $\phi \in  \displaystyle \bigcup_{i = 0}^m W_i$인 $m \in \mathbb{N}$이 최소이면 $m\le n$인 모든 $n \in \mathbb{N}$에 대해 $v_{m,s}(\phi) = v_{n,s}(\phi)$이다.

증명

1.

항의 해석 정의에 나온 $s,h$를 구성하는 함수열이 각각 $s_0,s_1,\cdots$과 $h_0,h_1,\cdots$이고 집합열이 $T_0,T_1,\cdots \subseteq T$일때

모든 $n \in \mathbb{N}$에 대해

$t\in \displaystyle \bigcup_{i = 0}^n T_i$에 포함되는 모든 변수기호 $x$가 $s(x) = h(x)$이면 $s_n(t) = h_n(t)$임을 귀납법으로 보인다.

$n = 0$일때 $t \in T_0$는 상수기호이거나 변수기호이므로

$t = c$가 상수기호이면

$c \in \mathcal{L}$에 대응하는 상수 $c_\mathcal{M}\in M$에 대해 항의 해석 정의로 $s_0(c)=c_\mathcal{M}= h_0(c)$이고

$t = x$가 변수기호이면

$0\in \mathbb{N}$보다 작은 자연수는 존재하지 않으므로 항의 해석 정의로 $s_0(x) = s(x) = h(x) = h_0(x)$이다.

모든 $k \in \mathbb{N}$에 대해 $t\in \displaystyle \bigcup_{i = 0}^k T_i$에 포함되는 모든 변수기호 $x$가 $s(x) = h(x)$이면 $s_{k}(t) = h_k(t)$일때

모든 $t \in  \displaystyle \bigcup_{i = 0}^{k+1}T_{i}$는 $t \in  \displaystyle \bigcup_{i = 0}^{k}T_{i}$이거나 $t \in T_{k+1}$이므로

$t \in  \displaystyle \bigcup_{i = 0}^{k}T_{i} $이면 항의 해석 정의와 귀납가정으로 $s_{k+1}(t) = s_{k}(t) = h_k(t) = h_{k+1}(t)$이고

$t \in T_{k+1}$이면 어떤 함수기호 $f\in \mathcal{L}$과 어떤 $ t_1,t_2,\cdots,t_{n_f} \in  \displaystyle \bigcup_{i = 0}^{k}T_{i} $에 대해 $t = f(t_1,t_2,\cdots,t_{n_f})$이고

$1\le j \le n_f$에 대해 $t_j$는 $t$에 포함되므로 귀납가정으로 $s_k(t_j) = h_k(t_j)$가 되어

$f$에 대응되는 $n_f$항함수 $f_\mathcal{M}$에 대해 항의 해석 정의와 함수의 정의로

$s_{k+1}(t) = f_\mathcal{M}(s_k(t_1),s_k(t_2),\cdots,s_k(t_{n_f})) = f_\mathcal{M}(h_k(t_1),h_k(t_2),\cdots,h_k(t_{n_f})) = h_{k+1}(t)$이다.

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고 $t \in T$에 포함되는 모든 변수기호 $x$에 대해 $s(x) = h(x)$일때

$t \in T = \displaystyle \bigcup_{i =0}^\infty T_i$는 정렬성으로 $t \in  \displaystyle \bigcup_{i = 0}^m T_i $가 되는 최소인 $m \in \mathbb{N}$이 존재하여

항의 해석 정의와 위에서 보인 것으로 $s(t) = s_m(t) = h_m(t) = h(t)$이다.

2.

$(B,\lor,\land,\neg ,\mathbf{F},\mathbf{T})$가 $\mathbf{F}\ne \mathbf{T}$인 불 대수일때 불 대수 정리로 $(\{ \mathbf{F}, \mathbf{T}\},\lor,\land,\neg ,\mathbf{F},\mathbf{T})$는 불 대수이고

값매김의 정의에 나온 $v_s,v_h$를 구성하는

함수열이 각각 $v_{0,s},v_{1,s},\cdots$와 $v_{0,h},v_{1,h},\cdots$이고 집합열이 $W_0,W_1,\cdots \subseteq W$일때

모든 $n \in \mathbb{N}$에 대해

$\phi \in \displaystyle \bigcup_{i = 0}^n W_i$에 포함되는 모든 자유변수 $x$가 $s(x) =h(x)$이면 $v_{n,s}(\phi) = v_{n,h}(\phi)$임을 귀납법으로 보인다.

$n = 0$일때 $\phi \in W_0$에 포함되는 모든 자유변수 $x$가 $s(x) = h(x)$일때 $\phi \in W_0$는 원자논리식이므로 

어떤 관계기호 $R \in \mathcal{L}$과 어떤 $ t_1,t_2,\cdots,t_{n_R} \in  T$에 대해 $\phi = R(t_1,t_2,\cdots,t_{n_R})$이면

$R$에 대응되는 $n_R$항관계 $R_\mathcal{M}$에 대해 값매김의 정의로 

$v_{0,s}(\phi) = \mathbf{T}$이기 위한 필요충분조건이 $R_\mathcal{M}(s(t_1),s(t_2),\cdots,s(t_{n_R}))$이고

$v_{0,h}(\phi) = \mathbf{T}$이기 위한 필요충분조건이 $R_\mathcal{M}(h(t_1),h(t_2),\cdots,h(t_{n_R}))$이고

1번으로 $1\le j \le n_f$에 대해 $s(t_j) = h(t_j)$이므로 $v_{0,s}(\phi) = v_{0,h}(\phi)$이다.

어떤 $t_1,t_2 \in  T$에 대해 $\phi = (t_1 = t_2)$이면 값매김의 정의로

$v_{0,s}(\phi) = \mathbf{T}$와 $s(t_1) = s(t_2)$가 동치이고 $v_{0,h}(\phi) = \mathbf{T}$와 $h(t_1) = h(t_2)$가 동치이고

1번으로 $s(t_1) = h(t_1)$과 $s(t_2) = h(t_2)$가 성립하므로 $v_{0,s}(\phi) = v_{0,h}(\phi)$이다.

모든 $k \in \mathbb{N}$에 대해

$\theta \in \displaystyle \bigcup_{i = 0}^k W_i$에 포함되는 모든 자유변수 $x$가 $s(x) = h(x)$일때 $v_{k,s}(\theta) = v_{k,h}(\theta)$라고 가정하면

$\theta \in \displaystyle \bigcup_{i = 0}^{k+1} W_i$에 포함되는 모든 자유변수 $x$가 $s(x) = h(x)$일때 $\theta $는 $\theta \in \displaystyle \bigcup_{i = 0}^k W_i$ 또는 $\theta \in W_{k+1}$이므로

$\theta \in \displaystyle \bigcup_{i = 0}^k W_i$이면 값매김의 정의와 귀납가정으로 $v_{k+1,s}(\theta)=v_{k,s}(\theta) = v_{k,h}(\theta) = v_{k+1,h}(\theta)$이고

$\theta \in W_{k+1}$이면 어떤 $\phi,\psi \in \displaystyle \bigcup_{i = 0}^k W_i$와 어떤 변수기호 $y$에 대해 $\theta = (\neg \phi)$ 또는 $\theta = (\phi \to \psi)$ 또는 $\theta = (\forall y)\phi$이므로

$\theta = (\neg \phi)$ 또는 $\theta = (\phi \to \psi)$이면 귀납가정으로 $v_{k,s}(\phi) = v_{k,h}(\phi)$이고 $v_{k,s}(\psi) = v_{k,h}(\psi)$이므로

불 대수 연산 $\neg : B\to B$와 $\to : B\times B \to B$에 대해

$v_{k+1,s}(\,(\neg \phi)\,)= \neg v_{k,s}(\phi) = \neg v_{k,h}(\phi) = v_{k+1,h}(\,(\neg \phi)\,)$이거나

$v_{k+1,s}(\,(\phi \to \psi)\,)= v_{k,s}(\phi) \to v_{k,s}(\psi) = v_{k,h}(\phi) \to v_{k,h}(\psi) = v_{k+1,h}(\,(\phi \to \psi)\,)$이다.

$\theta = (\forall y)\phi$일때 임의의 $r \in M$에 대해

$s$에서 $y$를 $r$로 치환한 항의 해석이 $s[r/y]:T\to M$이고

$h$에서 $y$를 $r$로 치환한 항의 해석이 $h[r/y] : T \to M$이면 값매김의 정의로

$v_{k+1,s}(\,(\forall y)\phi\,) =\mathbf{T}$이기 위한 필요충분조건이 모든 $r \in M$에 대해 $v_{k,s[r/y]}(\phi)=\mathbf{T}$이고

$v_{k+1,h}(\,(\forall y)\phi\,) =\mathbf{T}$이기 위한 필요충분조건이 모든 $r \in M$에 대해 $v_{k,h[r/y]}(\phi)=\mathbf{T}$이고

모든 $r \in M$에 대해 $\phi \in \displaystyle \bigcup_{i = 0}^k W_i$에 포함되는 모든 자유변수 $x$가

$x\ne y$이면 $s[r/y](x) = s(x) = h(x) = h[r/y](x)$이고 $x = y$이면 $s[r/y](y) = r = h[r/y](y)$이므로

귀납가정으로 $v_{k,s[r/y]}(\phi)= v_{k,h[r/y]}(\phi)$가 되어 $v_{k+1,s}(\,(\forall y)\phi\,) = v_{k+1,h}(\,(\forall y)\phi\,)$이다.

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고

모든 $\phi \in W = \displaystyle \bigcup_{i =0}^\infty W_i$는 정렬성으로 $\phi \in  \displaystyle \bigcup_{i = 0}^m W_i $가 되는 최소인 $m \in \mathbb{N}$이 존재하여

$\phi \in  \displaystyle \bigcup_{i = 0}^m W_i $에 포함되는 모든 자유변수 $x$가 $s(x) = h(x)$이면

값매김의 정의와 위에서 보인 것으로 $v_s(\phi) = v_{m,s}(\phi) = v_{m,h}(\phi) = v_h(\phi)$이다.

3.

$\phi \in W$가 문장이면 $\phi$에는 자유변수가 없으므로 공허하게 2번이 성립하여 $v_s(\phi) = v_h(\phi)$이다.

4.

$s_{m}(t) = s_{n}(t)$임을 $m\le n$인 $n \in \mathbb{N}$에 대한 귀납법으로 증명한다.

$n =m$일때는 자명하게 성립한다.

$m\le k$인 모든 $k \in \mathbb{N}$에 대해 $s_{m}(t) = s_{k}(t)$라고 가정하면

$t \in  \displaystyle \bigcup_{i = 0}^m T_i$인 $m \in \mathbb{N}$이 최소이므로 $t \in  \displaystyle \bigcup_{i = 0}^m T_i \subseteq \bigcup_{i = 0}^k T_i \subseteq \bigcup_{i = 0}^{k+1} T_i$가 되어

항의 해석 정의로 $s_{k+1}(t) = s_{k}(t)$이고 귀납가정으로 $s_{m}(t) = s_{k}(t) = s_{k+1}(t)$이다.

따라서 $t \in  \displaystyle \bigcup_{i = 0}^m T_i$인 $m \in \mathbb{N}$이 최소이면 $m\le n$인 모든 $n \in \mathbb{N}$에 대해 $s_{m}(t) = s_{n}(t)$이다.

5.

$v_{m,s}(\phi) = v_{n,s}(\phi)$임을 $m\le n$인 $n \in \mathbb{N}$에 대한 귀납법으로 증명한다.

$n =m$일때는 자명하게 성립한다.

$m\le k$인 모든 $k \in \mathbb{N}$에 대해 $v_{m,s}(\phi) = v_{k,s}(\phi)$라고 가정하면

$\phi \in  \displaystyle \bigcup_{i = 0}^m W_i$인 $m \in \mathbb{N}$이 최소이므로 $\phi \in  \displaystyle \bigcup_{i = 0}^m W_i \subseteq \bigcup_{i = 0}^k W_i \subseteq \bigcup_{i = 0}^{k+1} W_i$가 되어

값매김의 정의로 $v_{k+1,s}(\phi) = v_{k,s}(\phi)$이고 귀납가정으로 $v_{m,s}(\phi) = v_{k,s}(\phi) = v_{k+1,s}(\phi)$이다.

따라서 $\phi \in  \displaystyle \bigcup_{i = 0}^m W_i$인 $m \in \mathbb{N}$이 최소이면 $m\le n$인 모든 $n \in \mathbb{N}$에 대해 $v_{m,s}(\phi) = v_{n,s}(\phi)$이다.

 

 

 

정리20

$\mathcal{L}$-일차논리의 논리식집합이 $W$이고 항집합이 $T$일때 

$\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$에 대한 임의의 항의 해석 $s : T \to M$이고

$s$에서 임의의 변수기호 $x$를 임의의 $r \in M$로 치환한 항의 해석이 $s[r/x] : T \to M$이면

$s$에 대한 값매김 $v_s : W \to \{ \mathbf{F},\mathbf{T}\}$와 모든 항 $u,t \in T$와 모든 논리식 $\phi,\psi\in W$에 대해 다음이 성립한다.

1. $v_s(\,(\neg \phi )\,) = \neg v_s(\phi)$

2. $v_s(\,(\phi \to \psi )\,) = v_s(\phi) \to v_s(\psi)$

3. $v_s(\,(\phi \lor \psi )\,) = v_s(\phi) \lor v_s(\psi)$

4. $v_s(\,(\phi \land \psi )\,) = v_s(\phi) \land v_s(\psi)$

5. $v_s(\,(\phi \leftrightarrow \psi )\,) = v_s(\phi) \leftrightarrow v_s(\psi)$

6. $v_{s}(\,(\forall x) \phi\,) = \mathbf{T}$이기 위한 필요충분조건은 모든 $r \in M$에 대해 $v_{s[r/x]}(\phi) =\mathbf{T}$인 것이다.

7. $v_{s}(\,(\exists x) \phi\,) = \mathbf{T}$이기 위한 필요충분조건은 $v_{s[r/x]}(\phi) =\mathbf{T}$인 $r \in M$이 존재하는 것이다.

8. $x$가 $u$에 포함되지 않으면 모든 $r \in M$에 대해 $s[r/x](u) = s(u)$이다.

9. $x$가 $\phi$의 자유변수가 아니면 모든 $r \in M$에 대해 $v_{s}(\,(\forall x) \phi\,) = v_s(\phi) = v_{s[r/x]}(\phi)$이다.

10.

$x$가 $u$에 포함되면 $u[t/x] \in T$가 $u$에서 $x$를 $t$로 치환한 항이고

$x$가 $u$에 포함되지 않으면 $u[t/x] = u$로 정의되는 항에 대해 $s[s(t)/x](u) = s(u[t/x])$이다.

11.

$x$가 $\phi$의 자유변수이고 $\phi$에서 $x$를 $t$로 치환가능하면 $\phi[t/x] \in W$가 $x$를 $t$로 치환한 논리식이고

$x$가 $\phi$의 자유변수가 아니면 $\phi[t/x] = \phi$로 정의되는 논리식에 대해 $v_{s[s(t)/x]}(\phi) = v_s(\phi[t/x])$이다.

증명

$(B,\lor,\land,\neg ,\mathbf{F},\mathbf{T})$가 $\mathbf{F}\ne \mathbf{T}$인 불 대수일때 불 대수 정리로 $(\{ \mathbf{F}, \mathbf{T}\},\lor,\land,\neg ,\mathbf{F},\mathbf{T})$는 불 대수이고

값매김 정의에 나온 $v_s$를 구성하는 함수열이 $v_{0,s},v_{1,s},\cdots$이고 집합열이 $W_0,W_1,\cdots \subseteq W$일때

위 정리와 정렬성으로 $\phi ,\psi\in  \displaystyle \bigcup_{i = 0}^n W_i \subseteq W$가 되는 최소인 $n \in \mathbb{N}$이 존재하여 $(\neg \phi),(\phi \to \psi),(\forall x)\phi \in W_{n+1}$이다.

일반성을 잃지 않고 $\psi\in  \displaystyle \bigcup_{i = 0}^k W_i$가 되는 최소인 $k \in \mathbb{N}$가 $k\le n$이라고 가정하면 위 정리로 $v_{k,s}(\psi) = v_{n,s}(\psi)$이다.

1, 2

값매김의 정의로 $v_s(\,(\neg \phi )\,) = v_{n+1,s}(\,(\neg \phi)\,) = \neg v_{n,s}(\phi) = \neg v_s(\phi)$이고

$v_s(\,(\phi \to \psi )\,) = v_{n+1,s}(\,( \phi \to \psi )\,) = v_{n,s}(\phi) \to v_{n,s}(\psi) =v_{n,s}(\phi) \to v_{k,s}(\psi) = v_s(\phi) \to v_s(\psi)$이다.

3.

논리식 $(\phi \lor \psi)$는 $(\phi \lor \psi) = ((\neg \phi) \to \psi)$로 정의되므로 불 대수 정의와 1, 2번으로

$v_s(\,(\phi \lor \psi )\,)  = v_s(\,((\neg \phi) \to \psi)\,) = v_s(\,(\neg \phi)\,) \to v_s(\psi) = \neg v_s(\phi) \to v_s(\psi) = v_s(\phi) \lor v_s(\psi)$이다.

4.

논리식 $(\phi \land \psi)$는 $(\phi \land \psi) = (\neg (\phi \to (\neg \psi)))$로 정의되므로 불 대수 정의와 불 대수 정리와 1, 2번으로

$v_s(\,(\phi \land \psi )\,) = v_s(\, (\neg (\phi \to (\neg \psi)))\,) =\neg v_s(\,(\phi \to (\neg \psi))\,) = \neg (v_s(\phi) \to v_s(\,(\neg \psi)\,)) = \neg (v_s(\phi) \to \neg v_s(\psi)) = v_s(\phi) \land v_s(\psi) \text{ 이다.}$

5.

논리식 $(\phi \leftrightarrow \psi)$는 $(\phi \leftrightarrow \psi) = ((\phi \to \psi) \land (\psi \to \phi)) $로 정의되므로 불 대수 정의와 2, 4번으로

$v_s(\,(\phi \leftrightarrow \psi) \,) = v_s(\,((\phi \to \psi) \land (\psi \to \phi)) \,) = v_s(\,(\phi \to \psi)\,) \land v_s(\,(\psi \to \phi)\,) = (v_s(\phi) \to v_s(\psi)) \land (v_s(\psi) \to v_s(\phi)) = v_s(\phi) \leftrightarrow v_s(\psi) \text{ 이다.}$

6.

값매김의 정의로

$v_{n+1,s}(\,(\forall x)\phi\,) =\mathbf{T}$이기 위한 필요충분조건은 모든 $r \in M$에 대해 $v_{n,s[r/x]}(\phi)=\mathbf{T}$인 것이고

$v_{s}(\,(\forall x) \phi\,) = v_{n+1,s}(\,(\forall x)\phi\,)$와 $v_{s[r/x]}(\phi) =v_{n,s[r/x]}(\phi)$가 성립하므로

$v_{s}(\,(\forall x) \phi\,) = v_{n+1,s}(\,(\forall x)\phi\,) =\mathbf{T}$이기 위한 필요충분조건은

모든 $r \in M$에 대해 $v_{s[r/x]}(\phi) =v_{n,s[r/x]}(\phi)=\mathbf{T}$인 것이다.

7.

논리식 $(\exists x)\phi$는 $(\exists x)\phi = (\neg (\forall x)(\neg \phi))$로 정의되므로 $v_{s}(\,(\exists x) \phi\,) = v_s(\,(\neg (\forall x)(\neg \phi))\,) = \mathbf{T}$이면

1번과 불 대수 정리로 $\mathbf{F}=\neg \mathbf{T} =\neg v_s(\,(\neg (\forall x)(\neg \phi))\,) = \neg (\neg v_s(\,(\forall x)(\neg \phi)\,)) = v_s(\,(\forall x)(\neg \phi)\,)$이고

6번으로 모든 $r \in M$에 대해 $v_{s[r/x]}(\,(\neg \phi)\,)=\mathbf{T}$가 아니므로 $v_{s[r/x]}(\,(\neg \phi)\,)=\mathbf{F}$가 되는 $r \in M$이 존재하여

1번과 불 대수 정리로 $\mathbf{T} = \neg \mathbf{F} =\neg v_{s[r/x]}(\,(\neg \phi)\,)= \neg (\neg v_{s[r/x]}(\phi)) = v_{s[r/x]}(\phi)$이다.

역도 비슷하게 성립한다.

8.

$x$가 $u$에 포함되지 않으면 $u$에 포함되는 모든 변수기호 $y$는 $y \ne x$이므로

모든 $r \in M$에 대해 $s[r/x]$의 정의로 $s[r/x](y) = s(y)$가 되어 위 정리로 $s[r/x](u) = s(u)$이다.

9.

$x$는 $\phi$의 자유변수가 아니므로 $\phi$에 포함되는 모든 자유변수 $y$는 $y \ne x$가 되어

모든 $r \in M$에 대해 $s[r/x]$의 정의로 $s[r/x](y) = s(y)$이고 위 정리로 $v_s(\phi) = v_{s[r/x]}(\phi)$이다.

따라서 6번으로 $v_s(\,(\forall x)\phi \,) = \mathbf{T}$와 모든 $r \in M$에 대해 $v_s(\phi) =v_{s[r/x]}(\phi) = \mathbf{T} $임은 동치이고

6번의 대우로 $v_s(\,(\forall x)\phi \,) = \mathbf{F}$와 $v_s(\phi) =v_{s[r/x]}(\phi) = \mathbf{F}$인 $r \in M$이 존재함은 동치이므로

$v_s(\phi) =v_{s[r/x]}(\phi) = \mathbf{F}$인 $r \in M$이 존재하면 모든 $r \in M$에 대해 $v_s(\phi) =v_{s[r/x]}(\phi) = \mathbf{F}$가 되어

모든 $r \in M$에 대해 $v_{s}(\,(\forall x) \phi\,) = v_s(\phi) = v_{s[r/x]}(\phi)$이다.

10.

$x$가 $u$에 포함되지 않으면 $u[t/x] = u$이므로 $s(t) \in M$에 대해 8번으로 $s[s(t)/x](u) = s(u) =s (u[t/x])$이다.

위 정리의 집합열이 $T_0,T_1,\cdots \subseteq T$일때

모든 $n \in \mathbb{N}$에 대해 $u \in \displaystyle \bigcup_{i = 0}^n T_i$가 $s[s(t)/x](u) = s(u[t/x])$임을 귀납법으로 보인다.

$n = 0$일때 $u \in T_0$에 $x$가 포함되면

$u= x$이고 $u[t/x] = t$이므로 $s[s(t)/x]$의 정의로 $s[s(t)/x](u) = s[s(t)/x](x) = s(t) = s(u[t/x])$이다.

모든 $k \in \mathbb{N}$에 대해 $u \in \displaystyle \bigcup_{i = 0}^k T_i$가 $s[s(t)/x](u) = s(u[t/x])$라고 가정할때

$u \in \displaystyle \bigcup_{i = 0}^{k+1} T_i$가 $u \in \displaystyle \bigcup_{i = 0}^{k} T_i$이면 귀납가정으로 $s[s(t)/x](u) = s(u[t/x])$이다.

$u \in \displaystyle \bigcup_{i = 0}^{k+1} T_i$가 $u \in T_{k+1}$이면 어떤 함수기호 $f \in \mathcal{L}$와 어떤 $u_1,u_2,\cdots,u_{n_f} \in \displaystyle \bigcup_{i = 0}^{k} T_i$에 대해

$u = f(u_1,u_2,\cdots,u_{n_f})$이므로 $u[t/x] = f(u_1[t/x],u_2[t/x],\cdots,u_{n_f}[t/x])$이고

귀납가정으로 $1\le j \le n_f$에 대해 $s[s(t)/x](u_j) = s(u_j[t/x])$이므로

$f$에 대응되는 $n_f$항함수 $f_\mathcal{M}$에 대해 항의 해석 정의로

$\begin{align*}s[s(t)/x](u) & = s[s(t)/x](\,f(u_1,u_2,\cdots, u_{n_f})\,) \\[0.5em] & = f_\mathcal{M}(s[s(t)/x](u_1),s[s(t)/x](u_2),\cdots, s[s(t)/x](u_{n_f})) \\[0.5em] & = f_\mathcal{M}(s(u_1[t/x]),s(u_2[t/x]),\cdots, s(u_{n_f}[t/x])) \\[0.5em] & = s(\,f(u_1[t/x],u_2[t/x],\cdots,u_{n_f}[t/x])\,) \\[0.5em] &=s(u[t/x]) \text{ 이다.} \end{align*}$

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고 $T = \displaystyle \bigcup_{i = 0}^\infty T_i$이므로 모든 $u \in T$에 대해 $s[s(t)/x](u) = s(u[t/x])$이다.

11.

$x$가 $\phi$의 자유변수가 아니면 $\phi[t/x] = \phi$이므로 $s(t) \in M$에 대해 9번으로 $v_{s[s(t)/x]}(\phi) = v_s(\phi) = v_s(\phi[t/x])$이다.

위 정리의 집합열이 $W_0,W_1,\cdots \subseteq W$일때

모든 $n \in \mathbb{N}$에 대해 $\phi \in \displaystyle \bigcup_{i = 0}^n W_i$가 $v_{s[s(t)/x]}(\phi) = v_s(\phi[t/x])$임을 귀납법으로 보인다.

$n = 0$일때 $\phi \in W_0$는 원자논리식이므로

$\phi \in W_0$가 어떤 관계기호 $R \in \mathcal{L}$과 어떤 $u_1,\cdots,u_{n_R} \in T$에 대해 $\phi = R(u_1,\cdots,u_{n_R})$이면

10번과 같이 정의된 항 $u_1[t/x],\cdots,u_{n_R}[t/x]$에 대해 $\phi[t/x] = R(u_1[t/x],\cdots, u_{n_R}[t/x])$이므로

$R$에 대응되는 $n_R$항관계 $R_\mathcal{M}$에 대해 값매김의 정의로 

$v_{s[s(t)/x]}(\,R(u_1,\cdots, u_{n_R})\,) = \mathbf{T}$이기 위한 필요충분조건은 $R_\mathcal{M}(s[s(t)/x](u_1),\cdots,s[s(t)/x](u_{n_R}))$이고

$v_{s}(\,R(u_1[t/x],\cdots, u_{n_R}[t/x])\,) = \mathbf{T}$이기 위한 필요충분조건은 $R_\mathcal{M}(s(u_1[t/x]),\cdots,s(u_{n_R}[t/x]))$이고

$1\le j \le n_R$에 대해 10번으로 $s[s(t)/x](u_j) = s(u_j[t/x])$가 되어

$v_{s[s(t)/x]}(\phi) =v_{s[s(t)/x]}(\,R(u_1,\cdots, u_{n_R})\,) = v_s(\,R(u_1[t/x],\cdots,u_{n_R}[t/x])\,) = v_s(\phi[t/x])$이다.

$\phi \in W_0$가 어떤 $u_1,u_2 \in T$에 대해 $\phi = (u_1 = u_2)$이면

10번과 같이 정의된 항 $u_1[t/x],u_{2}[t/x]$에 대해 $\phi[t/x] = (u_1[t/x] = u_2[t/x])$이므로 값매김의 정의로

$v_{s[s(t)/x]}(\,(u_1 = u_2)\,) = \mathbf{T}$이기 위한 필요충분조건은 $s[s(t)/x](u_1) = s[s(t)/x](u_2)$이고

$v_s(\,(u_1[t/x] = u_2[t/x])\,)= \mathbf{T}$이기 위한 필요충분조건은 $s(u_1[t/x]) = s(u_2[t/x])$이고

10번으로 $s[s(t)/x](u_1) = s(u_1[t/x])$와 $s[s(t)/x](u_2) = s(u_2[t/x])$가 성립하여

$v_{s[s(t)/x]}(\phi) =v_{s[s(t)/x]}(\,(u_1= u_{2})\,) = v_s(\,(u_1[t/x] =u_{2}[t/x])\,) = v_s(\phi[t/x])$이다.

모든 $k \in \mathbb{N}$에 대해 $\theta \in \displaystyle \bigcup_{i = 0}^k W_i$가 $v_{s[s(t)/x]}(\theta) = v_s(\theta[t/x])$라고 가정할때

$\theta \in \displaystyle \bigcup_{i = 0}^{k+1} W_i$가 $\theta \in \displaystyle \bigcup_{i = 0}^{k} W_i$이면 귀납가정으로 $v_{s[s(t)/x]}(\theta) = v_s(\theta[t/x])$이다.

$\theta \in \displaystyle \bigcup_{i = 0}^{k+1} W_i$가 $\theta \in  W_{k+1}$일때

어떤 $\phi,\psi \in \displaystyle \bigcup_{i = 0}^k W_i$에 대해 $\theta = (\neg \phi)$ 또는 $\theta = (\phi \to \psi)$이면 1, 2번과 귀납가정으로

$v_{s[s(t)/x]}(\theta) = v_{s[s(t)/x]}(\,(\neg \phi)\,) = \neg v_{s[s(t)/x]}(\phi) = \neg v_s(\phi[t/x]) = v_s(\,(\neg \phi[t/x])\,)= v_s(\theta[t/x])$이거나

$v_{s[s(t)/x]}(\theta) = v_{s[s(t)/x]}(\,(\phi \to \psi)\,) = v_{s[s(t)/x]}(\phi) \to v_{s[s(t)/x]}(\psi) = v_s(\phi[t/x]) \to v_s(\psi[t/x]) = v_s(\,(\phi[t/x] \to \psi[t/x])\,)= v_s(\theta[t/x]) \text{ 이다.}$

$x$가 $\theta \in W_{k+1}$의 자유변수이고 $\theta$에서 $x$를 항 $t$로 치환가능할때

어떤 변수기호 $y$와 어떤 $\phi \in \displaystyle \bigcup_{i = 0}^k W_i$에 대해 $\theta = (\forall y)\phi$이면

$x$가 $(\forall y)\phi$의 자유변수이므로 $y \ne x$이고 $(\forall y)\phi$에서 $x$를 $t$로 치환가능하므로 $t$는 $y$를 포함할 수 없다.

$a =s[s(t)/x]$에서 $y$를 임의의 $r\in M$로 치환한 항의 해석 $a[r/y] : T \to M$와

$b = s[r/y]$에서 $x$를 $r$로 치환한 항의 해석 $b[r/x] : T \to M$에 대해 8번으로

$a[r/y](x) = a(x) = s[s(t)/x](x) = s(t) =s[r/y](t) = b(t) = b[b(t)/x](x)$와

$a[r/y](y) = r = s[r/y](y) = b(y)= b[b(t)/x](y)$가 성립하고

$z\ne x$이고 $z \ne y$인 $\phi$의 모든 자유변수 $z$에 대해

치환한 항의 해석의 정의로 $a[r/y](z) = a(z) = s[s(t)/x](z) = s(z) = s[r/y](z)= b(z) =b[b(t)/x](z)$이므로

모든 $r \in M$에 대해 위 정리로 $v_{a[r/y]}(\phi) =v_{b[b(t)/x]}(\phi)$이고

귀납가정으로 $v_{a[r/y]}(\phi) =v_{b[b(t)/x]}(\phi) = v_b(\phi[t/x]) = v_{s[r/y]}(\phi[t/x]) $이다.

6번으로 $v_{a}(\,(\forall y)\phi\,) = \mathbf{T}$와 모든 $r \in M$에 대해 $v_{a[r/y]}(\phi) = \mathbf{T}$임은 동치이고

$v_s(\,(\forall y)\phi[t/x]\,) = \mathbf{T}$와 모든 $r \in M$에 대해 $v_{s[r/y]}(\phi[t/x]) = \mathbf{T}$임은 동치이므로

$v_{s[s(t)/x]}(\theta)=v_{s[s(t)/x]}(\,(\forall y)\phi\,)=v_{a}(\,(\forall y)\phi\,) = v_s(\,(\forall y)\phi[t/x]\,) = v_s(\theta[t/x])$이다.

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고 $W = \displaystyle \bigcup_{i = 0}^\infty W_i$이므로 모든 $\phi \in W$에 대해 $v_{s[s(t)/x]}(\phi) = v_s(\phi[t/x])$이다.

 

 

 

정리3

명제논리의 논리식 $p$가 명제논리의 원자논리식 $p_1,p_2,\cdots,p_n$으로 구성되고 명제논리의 논리적 귀결이면

$p_1,p_2,\cdots,p_n$을 임의의 일차논리의 논리식 $\phi_1, \phi_2,\cdots, \phi_n$으로 치환한 논리식 $\phi$는 일차논리의 논리적 귀결이다.

증명

$p$가 명제논리의 논리적 귀결이면 명제논리의 모든 값매김 $w$에 대해 $w(p)=\mathbf{T}$이고

명제논리의 값매김 정리로 명제논리의 값매김의 함수값은 $p$에 포함되는 원자논리식에 따라 결정된다.

또 명제논리의 논리식 $p$에는 한정기호가 포함되지 않고 $\neg ,\to$만 포함되므로

명제논리의 값매김 정리와 일차논리의 값매김 정리로 $\neg, \to$에 대한 값매김의 함수값이 동일하게 구성됨에 따라

$p_i$를 $\phi_i$로 치환한 일차논리의 논리식 $\phi$는 일차논리의 모든 값매김 $v$에 대해 $v(\phi) = \mathbf{T}$이다.

 

 

 

정리4

일차논리의 모든 공리는 일차논리의 논리적 귀결이다.

증명

공리 1, 2, 3은 명제논리 정리와 위 정리로 일차논리의 논리적 귀결이다.

또 일차논리의 언어가 $\mathcal{L}$이고 항집합이 $T$이고 논리식집합이 $W$이고

$\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$에 대한 항의 해석이 $s : T \to M$이고 $s$에 대한 값매김이 $v_s : W \to \{\mathbf{F},\mathbf{T}\}$이고

$s$에서 임의의 변수기호 $x$를 임의의 $r \in M$로 치환한 항의 해석이 $s[r/x] : T \to M$일때

다음과 같이 공리 4, 5, 6, 7, 8은 일차논리의 논리적 귀결이므로 일차논리의 모든 공리는 일차논리의 논리적 귀결이다.

공리4

$x$가 $\phi \in W$의 자유변수가 아니면 위 정리와 불 대수 정의로

$v_s(\,((\forall x)\phi \to \phi)\,) = v_s(\,(\forall x)\phi\,) \to v_s(\phi) = v_s(\phi) \to v_s(\phi) = \neg v_s(\phi) \lor v_s(\phi)= \mathbf{T}$이다.

공리5

$x$가 $\phi \in W$의 자유변수이고 $\phi$에서 $x$를 $t \in T$로 치환가능할때

$v_s(\,(\forall x)\phi\,) = \mathbf{F}$이면 위 정리와 불 대수 정의와 불 대수 정리로

$v_s(\,((\forall x)\phi \to \phi[t/x]) \,)=v_s(\,(\forall x)\phi\,) \to v_s(\phi[t/x]) = \mathbf{F} \to v_s(\phi[t/x]) = \neg \mathbf{F} \lor v_s(\phi[t/x]) = \mathbf{T} \lor v_s(\phi[t/x]) = \mathbf{T} \text{ 이다.}$

$v_s(\,(\forall x)\phi\,) = \mathbf{T}$이면 위 정리로 모든 $r \in M$에 대해 $v_{s[r/x]}(\phi) = \mathbf{T}$가 성립하여

위 정리와 불 대수 정의와 불 대수 정리로

$v_s(\,((\forall x)\phi \to \phi[t/x])\,) = v_s(\,(\forall x)\phi\,) \to v_s(\phi[t/x]) = \mathbf{T} \to v_{s[s(t)/x]}(\phi) = \neg \mathbf{T} \lor \mathbf{T} = \mathbf{T}$이다.

공리6

$x$가 $\phi \in W$의 자유변수가 아닐때 

$v_s(\,(\forall x)(\phi \to \psi)  \,) = \mathbf{F}$이면 위 정리와 불 대수 정의와 불 대수 정리로

$\begin{align*}v_s(\,((\forall x)(\phi \to \psi) \to (\phi \to (\forall x)\psi)) \,) & =v_s(\,(\forall x)(\phi \to \psi)\,) \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \mathbf{F} \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \neg \mathbf{F} \lor v_s(\,(\phi \to (\forall x)\psi)\,) \\[0.5em] & = \mathbf{T} \lor v_s(\,(\phi \to (\forall x)\psi)\,) \\[0.5em] & = \mathbf{T} \text{ 이다.} \end{align*}$

$v_s(\,(\forall x)(\phi \to \psi)  \,) = \mathbf{T}$일때

$v_s(\phi) = \mathbf{F}$이면 위 정리와 불 대수 정의와 불 대수 정리로

$\begin{align*}v_s(\,((\forall x)(\phi \to \psi) \to (\phi \to (\forall x)\psi)) \,) & =v_s(\,(\forall x)(\phi \to \psi)\,) \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \mathbf{T} \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \neg \mathbf{T} \lor v_s(\,(\phi \to (\forall x)\psi)\,) \\[0.5em] & = \mathbf{F} \lor (v_s(\phi) \to v_s(\,(\forall x)\psi)\,)) \\[0.5em] & = v_s(\phi) \to v_s(\,(\forall x)\psi\,) \\[0.5em] & =\mathbf{F} \to v_s(\,(\forall x) \psi\,) \\[0.5em] & = \neg \mathbf{F} \lor v_s(\,(\forall x)\psi\,) \\[0.5em] & = \mathbf{T} \lor v_(\,(\forall x)\psi\,) \\[0.5em] & = \mathbf{T} \text{ 이고} \end{align*}$

$v_s(\phi) = \mathbf{T}$이면

위 정리로 모든 $r \in M$에 대해 $v_s(\phi) \to v_{s[r/x]}(\psi) =v_{s[r/x]}(\phi) \to v_{s[r/x]}(\psi) =v_{s[r/x]}(\,(\phi \to \psi)\,) = \mathbf{T}$이므로

모든 $r \in M$에 대해 $ v_{s[r/x]}(\psi) = \mathbf{T}$가 되어 위 정리로 $v_s(\,(\forall x) \psi  \,) = \mathbf{T}$이고 불 대수 정의와 불 대수 정리로

$\begin{align*}v_s(\,((\forall x)(\phi \to \psi) \to (\phi \to (\forall x)\psi)) \,) & =v_s(\,(\forall x)(\phi \to \psi)\,) \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \mathbf{T} \to v_s(\,(\phi \to (\forall x)\psi )\,) \\[0.5em] & = \neg \mathbf{T} \lor v_s(\,(\phi \to (\forall x)\psi)\,) \\[0.5em] & = \mathbf{F} \lor (v_s(\phi) \to v_s(\,(\forall x)\psi)\,)) \\[0.5em] & = v_s(\phi) \to v_s(\,(\forall x)\psi\,) \\[0.5em] & = \mathbf{T} \to v_s(\,(\forall x) \psi\,) \\[0.5em] & = \neg \mathbf{T} \lor v_s(\,(\forall x)\psi\,) \\[0.5em] & = \mathbf{F} \lor v_s(\,(\forall x)\psi\,) \\[0.5em] & = v_s(\,(\forall x)\psi\,) \\[0.5em] & = \mathbf{T} \text{ 이다.} \end{align*}$

공리7

$s(x) = s(x)$이므로 값매김의 정의로 $v_s(\,(x = x)\,) = \mathbf{T}$이다.

공리8

$x$가 $\phi \in W$의 자유변수이고 $\phi$에서 $x$를 $t ,u \in T$로 치환가능할때

$v_s(\,(t = u)\,) = \mathbf{F}$이면 위 정리와 불 대수 정의와 불 대수 정리로

$\begin{align*}v_s(\,((t = u) \to (\phi[t/x] \to \phi[u/x])) \,) & =v_s(\,(t = u)\,) \to v_s(\,(\phi[t/x] \to \phi[u/x])\,) \\[0.5em] & = \mathbf{F} \to v_s(\,(\phi[t/x]\to \phi[u/x])\,) \\[0.5em] & = \neg \mathbf{F} \lor v_s(\,(\phi[t/x]\to \phi[u/x]\,)) \\[0.5em] & = \mathbf{T} \lor v_s(\,(\phi[t/x]\to \phi[u/x])\,) \\[0.5em] & = \mathbf{T} \text{ 이다.} \end{align*}$

$v_s(\,(t = u)\,) = \mathbf{T}$이면

값매김의 정의로 $s(t) = s(u)$이므로 위 정리로 $v_s(\phi[t/x]) = v_{s[s(t)/x]}(\phi) = v_{s[s(u)/x]}(\phi) = v_s(\phi[u/x])$가 되어

위 정리와 불 대수 정의와 불 대수 정리로

$\begin{align*}v_s(\,((t = u) \to (\phi[t/x] \to \phi[u/x])) \,) & =v_s(\,(t = u)\,) \to v_s(\,(\phi[t/x] \to \phi[u/x])\,) \\[0.5em] & = \mathbf{T} \to v_s(\,(\phi[t/x]\to \phi[u/x])\,) \\[0.5em] & = \neg \mathbf{T} \lor v_s(\,(\phi[t/x]\to \phi[u/x]\,)) \\[0.5em] & = \mathbf{F} \lor v_s(\,(\phi[t/x]\to \phi[u/x])\,) \\[0.5em] & = v_s(\,(\phi[t/x] \to \phi[u/x])\,) \\[0.5em] & = v_s(\phi[t/x]) \to v_s(\phi[u/x]) \\[0.5em] & = \neg v_s(\phi[t/x]) \lor v_s(\phi[u/x]) \\[0.5em] & = \neg v_s(\phi[t/x]) \lor v_s(\phi[t/x]) \\[0.5em] & = \mathbf{T} \text{ 이다.} \end{align*}$

 

 

 

정리14

$\mathcal{L}$-일차논리의 $\mathcal{L}$-구조가 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$일때

$n \in \mathbb{Z}^+$개의 임의의 변수기호 $x_1,x_2,\cdots, x_n$과 임의의 논리식 $\phi$에 대해

$\mathcal{M} $ $\models$ $ \phi$이기 위한 필요충분조건은 $\mathcal{M} \models (\forall x_1) (\forall x_2) \cdots (\forall x_n) \phi$인 것이다.

증명

$\mathcal{M} \models \phi$와 $\mathcal{M} \models (\forall x_1) (\forall x_2) \cdots (\forall x_n) \phi$가 동치임을 $n \in \mathbb{Z}^+$에 대한 귀납법으로 보인다.

$n = 1$일때 $\mathcal{M} $ $\models$ $ \phi$이면 $\mathcal{M}$에 대한 모든 항의 해석 $s$와 $s$에 대한 값매김 $v_s$에 대해 $v_s(\phi) =\mathbf{T}$이므로

$s$에서 $x_1$을 임의의 $r \in M$로 치환한 항의 해석 $s[r/x_1]$에 대해 $v_{s[r/x_1]}(\phi) = \mathbf{T}$가 되어

모든 $s$에 대해 위 정리로 $v_s(\,(\forall x_1)\phi\,) = \mathbf{T}$이므로 $\mathcal{M}  \models (\forall x_1)\phi$이다.

역으로 $\mathcal{M}  \models (\forall x_1)\phi$이면

모든 $s$에 대해 $v_s(\,(\forall x_1)\phi\,)= \mathbf{T}$이므로 위 정리로 모든 $r \in M$에 대해 $v_{s[r/x_1]}(\phi) = \mathbf{T}$이고

위 정리로 $\phi[x_1/x_1] = \phi$와 $s(x_1) \in M$에 대해 $\mathbf{T} = v_{s[s(x_1)/x_1]}(\phi) = v_s(\phi[x_1/x_1]) = v_s(\phi)$가 되어 $\mathcal{M}  \models \phi$이다.

모든 $k \in \mathbb{Z}^+$에 대해 $\mathcal{M} \models \phi$와 $\mathcal{M} \models (\forall x_2) \cdots (\forall x_k) (\forall x_{k+1}) \phi$가 동치라고 가정할때

$n = 1$일때처럼 $\mathcal{M} \models (\forall x_2) \cdots (\forall x_k)(\forall x_{k+1}) \phi$와 $\mathcal{M} \models (\forall x_1) (\forall x_2) \cdots (\forall x_k)( \forall x_{k+1}) \phi$가 동치이므로

$\mathcal{M} \models \phi$와 $\mathcal{M} \models (\forall x_1) (\forall x_2) \cdots (\forall x_k)( \forall x_{k+1}) \phi$가 동치이다.

따라서 모든 $n \in \mathbb{Z}^+$에 대해 정리가 성립한다.

 

 

 

정리5(일차논리의 건전성[soundness])

일차논리의 논리식집합이 $W$이고 임의의 부분집합이 $\Sigma \subseteq W$일때 임의의 논리식 $\sigma \in W$에 대해

$\Sigma \vdash \sigma$이고

$\Sigma$로부터 $\sigma$의 증명에서 일반화를 적용한 모든 증명의 항 $(\forall x) \theta$에 대해 $x$가 모든 $\psi \in \Sigma$의 자유변수가 아니거나

$\Sigma$가 이론이면 $\Sigma \models \sigma$이다.

증명

문장은 자유변수가 없으므로 일반화를 적용한 모든 $(\forall x) \theta$에 대해 $x$가 모든 $\psi \in \Sigma$의 자유변수가 아닐때만 증명한다.

$\Sigma \vdash \sigma$이면 $\Sigma \models \sigma$임을 $\Sigma$로부터 $\sigma$의 증명의 길이 $n \in \mathbb{Z}^+$에 대한 강귀납법을 사용하여 보인다.

$n = 1$일때 $\sigma$는 공리이거나 $\sigma \in \Sigma$이므로

$\sigma$가 공리이면 위 정리로 $\models \sigma$가 되어 형식계 정리로 $\Sigma \models \sigma$이고 $\sigma \in \Sigma$이면 자명하게 $\Sigma \models \sigma$이다.

모든 증명의 길이 $1,2,\cdots , k \in \mathbb{Z}^+$에 대해 가정이 성립할때 길이가 $k+1$인 $\Sigma$로부터 $\sigma$의 증명이 $\begin{align*} \Sigma  \vdash &\;  p_0  \\ &\; \vdots  \\ \Sigma \vdash &\; p_{k-1}  \\ \Sigma \vdash & \; \sigma \end{align*}$이면

$\sigma$는 공리이거나 $\sigma \in \Sigma $이거나 이전 항들에 추론규칙을 적용하여 얻어진 논리식이므로

$\sigma$는 공리이거나 $\sigma \in \Sigma$이면 $n = 1$일때처럼 $\Sigma \models \sigma$이다.

$\sigma$가 이전 항들에 전건긍정 $f$를 적용하여 얻어졌다면

어떤 $\theta , (\theta \to \sigma) \in \{ p_0, \cdots, p_{k-1} \}$에 대해 $f(\theta, (\theta \to \sigma)) = \sigma$이고

$\theta$가 어떤 $\gamma \in \{ p_0, \cdots, p_{k-1} \}$에 대해 일반화를 적용한 $\theta = (\forall x) \gamma$일때 $x$는 모든 $\psi \in \Sigma$의 자유변수가 아니다.

따라서 귀납가정으로 모든 논리식 $\psi \in \Sigma$에 대해 $v(\psi) = \mathbf{T}$인 모든 값매김 $v$가 $v(\theta) = v(\, (\theta \to \sigma) \,) = \mathbf{T}$가 되어

위 정리로 $\mathbf{T} = v(\,(\theta \to \sigma)\,)=v(\theta) \to v(\sigma)$이므로 불 대수 정리로 $v(\sigma) = \mathbf{T}$이고 $\Sigma \models \sigma$이다.

$\sigma$가 이전 항들에 일반화를 적용하여 얻어졌다면

어떤 $\theta \in \{ p_0, \cdots, p_{k-1} \}$와 어떤 변수기호 $x$에 대해 $\sigma = (\forall x) \theta$이고

$\theta$가 어떤 $\gamma \in \{ p_0, \cdots, p_{k-1} \}$에 대해 일반화를 적용한 $\theta = (\forall y) \gamma$일때 $y$는 모든 $\psi \in \Sigma$의 자유변수가 아니므로

귀납가정으로 모든 논리식 $\psi \in \Sigma$에 대해 $v(\psi) = \mathbf{T}$인 모든 값매김 $v$가 $v(\theta) = \mathbf{T}$이다.

일차논리 언어의 구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$에 대한 항의 해석이 $s$이고 $s$에 대한 값매김이 $v_s$일때

$x$는 모든 $\psi \in \Sigma$의 자유변수가 아니므로 모든 $\psi \in \Sigma$가 $v_s(\psi) = \mathbf{T}$이면

위 정리로 모든 $r \in M$에 대해 $\mathbf{T} = v_s(\psi) = v_{s[r/x]}(\psi)$이고 귀납가정으로 $v_{s[r/x]}(\theta) = \mathbf{T}$가 되어

위 정리로 $\mathbf{T} =v_{s}(\,(\forall x) \theta\,) = v_s(\sigma)$이므로 $\Sigma \models \sigma$이다.

따라서 모든 $n \in \mathbb{Z}^+$에 대해 정리가 성립한다.

 

 

 

정리8

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$는 가부번이고 모든 문장들의 집합 $S$도 가부번이다.

또 변수기호를 갖지 않는 항들의 집합도 가산이다.

증명

$\mathcal{L}$이 가산인 일차논리의 기호집합은 가산집합들의 유한 합집합이므로 가산집합 정리로 가산이 되어

일차논리의 기호로 구성된 크기가 유한인 모든 문자열들의 집합 $\mathcal{S}$는 가산집합 정리로 가산이고

$S\subseteq W\subseteq \mathcal{S}$이므로 $S,W$는 가산집합 정리로 가산이다.

변수기호들의 집합 $\{x_0,x_1,x_2,\cdots\}$은 가부번으로 정의되므로 모든 $n \in \mathbb{N}$에 대해

원자논리식 $(x_n = x_0) \in W$에 한정기호 적용한 $(\forall x_n)(\forall x_0)(x_n = x_0) \in S$은 문장이 되어

무한집합 정리로 $S,W$는 무한이고 가부번 정리로 $S,W$는 가부번이다.

또 변수기호를 갖지 않는 항들의 집합도 $\mathcal{S}$에 포함되므로 가산집합 정리로 가산이다

 

 

 

정의5(무모순성[consistency])

일차논리의 논리식집합 $W$의 임의의 부분집합이 $\Sigma \subseteq W$일때

어떤 논리식 $\psi \in W$에 대해 $\psi, (\neg \psi)$가 모두 $\Sigma$의 정리이면 $\Sigma$에 모순이 있다(inconsistent)고 정의하고

모순이 없으면 $\Sigma$를 무모순(consistent)이라고 정의한다.

 

 

 

정리6

일차논리의 논리식집합 $W$의 임의의 부분집합 $\Sigma \subseteq W$가 무모순이면

임의의 문장 $\phi \in W$에 대해 $\Sigma \cup \{ \phi \}$ 또는 $\Sigma \cup \{ (\neg \phi) \}$가 무모순이다.

증명

귀류법으로 어떤 문장 $\phi \in W$에 대해 $\Sigma \cup \{ \phi \}$와 $\Sigma \cup \{ (\neg \phi) \}$에 모순이 있다고 가정하면

어떤 논리식 $\theta \in W$에 대해 $\theta, (\neg \theta)$가 $\Sigma \cup \{ (\neg \phi) \}$의 정리이므로 위 정리로 $\phi$는 $\Sigma$의 정리이고

어떤 논리식 $\psi \in W$에 대해 $\psi, (\neg \psi)$가 $\Sigma \cup \{ \phi \}$의 정리이므로 위 정리로 $(\phi \to \psi), (\phi \to (\neg \psi))$도 $\Sigma$의 정리이다.

따라서 전건긍정으로 $\psi,(\neg \psi)$가 $\Sigma$의 정리가 되어 $\Sigma$가 무모순이라는 가정에 모순이므로

$\Sigma$가 무모순이면 $\Sigma \cup \{ \phi \}$ 또는 $\Sigma \cup \{ (\neg \phi) \}$가 무모순이다.

 

 

 

정리9

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$의 임의의 부분집합 $\Sigma \subseteq W$가 무모순이면

모든 문장 $\phi \in W$에 대해 $\phi \in \Sigma^+$ 또는 $(\neg \phi) \in \Sigma^+$중 하나만 성립하고

$\Sigma \subseteq \Sigma^+$가 성립하는 무모순인 집합 $\Sigma^+$가 존재한다.

증명

위 정리로 모든 문장들의 집합 $S = \{ \phi_0,\phi_1,\cdots \}$는 가부번이고

위 정리로 문장과의 합집합 또는 문장의 부정과의 합집합 중 하나는 무모순이므로

$\Sigma\cup \{ \phi_0 \}$가 무모순이면 $\Sigma_0 = \Sigma\cup \{ \phi_0 \}$으로 $\Sigma \cup \{ \phi_0 \}$에 모순이 있으면 $\Sigma_0 = \Sigma \cup \{ (\neg \phi_0) \}$으로 정의하고

모든 $n \in \mathbb{N}$에 대해 $\Sigma_n$이 귀납적으로 정의될때

$\Sigma_n\cup \{ \phi_{n+1}\}$이 무모순이면 $\Sigma_{n+1} =\Sigma_n\cup \{ \phi_{n+1}\}$로 정의하고

$\Sigma_n\cup \{ \phi_{n+1}\}$에 모순이 있으면 $\Sigma_{n+1} =\Sigma_n\cup \{ (\neg \phi_{n+1} )\}$로 정의하여 $\displaystyle \Sigma^+ = \bigcup_{n = 0}^\infty \Sigma_{n}$를 정의하면

임의의 문장 $p \in S$는 $p =\phi_n$인 $n \in \mathbb{N}$이 존재하므로 $p \in \Sigma^+$ 또는 $(\neg p ) \in \Sigma^+$이다.

또 $\Sigma^+$에 모순이 있다고 가정하면 어떤 논리식 $\psi \in W $에 대해 $\psi, (\neg \psi)$가 $\Sigma^+$의 정리인데

$\Sigma^+$로부터 $\psi, (\neg \psi)$의 증명은 각각 크기가 유한인 배열이므로 증명에 사용된 $\psi,(\neg \psi)$의 가정도 유한 개가 되어

어떤 $n \in \mathbb{N}$에 대해 증명에 사용된 $\psi,(\neg \psi)$의 가정을 모두 포함하는 $\Sigma_n \subseteq \Sigma^+$이 존재하므로

$\psi, (\neg \psi)$는 $\Sigma_n$의 정리가 되고 $\Sigma_n$이 무모순이라는 가정에 모순이므로 $\Sigma^+$는 무모순이다.

임의의 문장 $\phi$가 $\phi \in \Sigma^+$이고 $(\neg \phi) \in \Sigma^+$라 가정하면

$\Sigma^+ \vdash \phi$이고 $ \Sigma^+\vdash (\neg \phi)$가 되어 $\Sigma^+$가 무모순임에 모순이므로 $\phi \in \Sigma^+$ 또는 $(\neg \phi) \in \Sigma^+$중 하나만 성립한다.

 

 

 

정리12

일차논리의 논리식집합 $W$에 대해 임의의 이론 $T\subseteq W$가 일차논리에서 만족가능하면 $T$는 무모순이다.

증명

언어가 $\mathcal{L}$인 일차논리에서 $T$가 만족가능할때

모든 문장 $\sigma \in T$에 대해 $v_\mathcal{M}(\sigma) = \mathbf{T}$인 $\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$과 $\mathcal{M}$의 값매김 $v_\mathcal{M}$이 존재하므로

$\mathcal{L}$-이론 $T$에 모순이 있다고 가정하면

어떤 논리식 $\psi \in W$에 대해 $T \vdash \psi$이고 $T \vdash (\neg \psi)$이므로 건전성으로 $T \models \psi$이고 $T \models (\neg \psi)$가 되어

모든 $\sigma \in T$에 대해 $v_\mathcal{M}(\sigma) =\mathbf{T}$인 $\mathcal{M}$의 모든 값매김 $v_\mathcal{M}$은 $v_\mathcal{M}(\psi) = \mathbf{T}$이고 $v_\mathcal{M}(\,(\neg \psi)\,) = \mathbf{T}$인데

위 정리와 불 대수 정리로 $ \mathbf{T} = v_\mathcal{M}(\,(\neg \psi)\,) = \neg v_\mathcal{M}(\psi) = \neg \mathbf{T} = \mathbf{F}$가 되어 불 대수 정의에 모순이므로

$T$는 무모순이다.

 

 

 

정리11

$\mathcal{L}$-일차논리의 논리식집합 $W$의 임의의 부분집합이 $\Sigma \subseteq W$이고

$\mathcal{L}$-일차논리의 항집합 $T$의 임의의 부분집합 $V \subseteq T$가 $V \ne \emptyset$일때 다음이 성립한다.

반사성 : 모든 $t \in V$에 대해 $\Sigma$ $\vdash$ $(t = t)$이다.

대칭성 : 임의의 $t,u \in V$가 $\Sigma \vdash (t =u)$이면 $\Sigma \vdash (u= t)$이다.

추이성 : 임의의 $t,u,v \in V$가 $\Sigma \vdash (t = u)$이고 $\Sigma \vdash (u = v)$이면 $\Sigma \vdash (t=v)$이다.

동치관계 :

임의의 $t,u \in V$에 대해

$E(t,u)$이기 위한 필요충분조건이 $\Sigma \vdash (t = u)$인 $V$의 동치관계가 $E$이고 $E$에 대한 $t$의 동치류가 $[t]_E$일때 

$n_f$항함수기호 $f \in \mathcal{L}$와 $n_R$항관계기호 $R \in \mathcal{L}$에 대해 다음이 성립한다.

1.

임의의 $t_1,\cdots,t_{n_f} \in V$와 임의의 $u_1\in [t_1]_E, \cdots, u_{n_f} \in [t_{n_f}]_E$에 대해

$\displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{n_f} \in [t_{n_f}]_E}[f(a_1,a_2,\cdots,a_{n_f})]_E = [f(u_1,u_2,\cdots,u_{n_f})]_E$이다.

2.

임의의 $t_1,\cdots,t_{n_R} \in V$에 대해 $\Sigma \vdash R(t_1,t_2,\cdots,t_{n_R})$이면

모든 $u_1\in [t_1]_E, \cdots, u_{n_R} \in [t_{n_R}]_E$에 대해 $\Sigma \vdash R(u_1,u_2,\cdots,u_{n_R})$이다.

증명

반사성

임의의 $t\in V$와 임의의 변수기호 $x$에 대해

$\begin{align*}  \Sigma \vdash &\; (x = x) \qquad 0 \text{번째 항 : 일차논리의 공리 7}  \\[0.5em]  \Sigma \vdash &\; (\forall x)(x=x) \qquad 1\text{번째 항 : } \text{0번째 항에 일반화를 적용} \\[0.5em]  \Sigma \vdash & \; ((\forall x)(x= x) \to (t= t)) \qquad 2\text{번째 항 : } \text{일차논리의 공리5} \\[0.5em]  \Sigma \vdash &\; (t= t) \qquad 3\text{번째 항 : } 1,2\text{번째 항에 전건긍정을 적용}  \end{align*}  $  이다.

대칭성

임의의 $t,u \in V$에 대해 $\Sigma \vdash (t = u)$이면

$t,u$에 포함되지 않고 $x\ne y$인 임의의 변수기호 $x,y$와 어떤 $n,k \in \mathbb{N}$에 대해

$\begin{align*} & \; \vdots \\ \Sigma \vdash &\; (t = u) \qquad n \text{번째 항 : } \Sigma\text{의 정리} \\[0.5em]  \Sigma \vdash &\; ((t = u) \to ((t = x) \to (u = x))) \qquad n+1 \text{번째 항 : }(y= x) \text{에서 } y\text{를 치환한 일차논리의 공리8} \\[0.5em]  \Sigma \vdash & \; ((t= x) \to (u = x)) \qquad n+2\text{번째 항 : } n,n+1\text{번째 항에 전건긍정을 적용} \\[0.5em]  \Sigma \vdash &\; (\forall x)((t= x) \to (u = x)) \qquad n+3\text{번째 항 : } n+2\text{번째 항에 일반화를 적용} \\[0.5em]  \Sigma \vdash &\; ((\forall x)((t= x) \to (u = x)) \to ((t =t) \to (u = t))) \qquad n+4\text{번째 항 : } \text{일차논리의 공리5} \\[0.5em]  \Sigma \vdash &\; ((t =t) \to (u = t)) \qquad n+5\text{번째 항 : } n+3,n+4\text{번째 항에 전건긍정을 적용} \\ &\; \vdots \\  \Sigma \vdash &\; (t =t) \qquad n+k\text{번째 항 : } t\text{에 대한 반사성}  \\[0.5em]  \Sigma \vdash &\; (u =t) \qquad n+k+1\text{번째 항(정리) : } n+5,n+k\text{번째 항에 전건긍정을 적용} \end{align*}  $이다.

추이성

임의의 $t,u ,v \in V$에 대해 $\Sigma \vdash (t = u)$이고 $\Sigma\vdash (u= v)$이면

$t,u,v$에 포함되지 않고 $x\ne y$인 임의의 변수기호 $x,y$와 어떤 $n,k \in \mathbb{N}$에 대해

$\begin{align*} & \; \vdots \\ \Sigma \vdash &\; (u = v) \qquad n \text{번째 항 : } \Sigma\text{의 정리} \\[0.5em]  \Sigma \vdash &\; ((u = v) \to ((x = u) \to (x = v))) \qquad n+1 \text{번째 항 : }(x= y) \text{에서 } y\text{를 치환한 일차논리의 공리8} \\[0.5em]  \Sigma \vdash & \; ((x= u) \to (x = v)) \qquad n+2\text{번째 항 : } n,n+1\text{번째 항에 전건긍정을 적용} \\[0.5em]  \Sigma \vdash &\; (\forall x)((x= u) \to (x = v)) \qquad n+3\text{번째 항 : } n+2\text{번째 항에 일반화를 적용} \\[0.5em]  \Sigma \vdash &\; ((\forall x)((x= u) \to (x = v)) \to ((t =u) \to (t = v))) \qquad n+4\text{번째 항 : } \text{일차논리의 공리5} \\[0.5em]  \Sigma \vdash &\; ((t =u) \to (t = v)) \qquad n+5\text{번째 항 : } n+3,n+4\text{번째 항에 전건긍정을 적용} \\ &\; \vdots\\ \Sigma \vdash &\; (t =u) \qquad n+k\text{번째 항 : } \Sigma\text{의 정리} \\[0.5em]  \Sigma \vdash &\; (t =v) \qquad n+k+1\text{번째 항(정리) : } n+5,n+k\text{번째 항에 전건긍정을 적용} \end{align*}$이다.

동치관계

반사성, 대칭성, 추이성으로 $V$의 이항관계 $E$는 동치관계이다.

1.

모든 $n \in \mathbb{Z}^+$에 대해 $n\le n_f$일때

$1\le i \le n\le n_f$인 임의의 $t_i \in V$와 임의의 $u_i \in [t_i]_E$와 $n < j \le n_f$인 임의의 변수기호 $x_j$에 대해

$\displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{n} \in [t_{n}]_E}[f(a_1,a_2,\cdots,a_{n}, x_{n+1},\cdots, x_{n_f})]_E = [f(u_1,u_2,\cdots,u_{n},x_{n+1},\cdots,x_{n_f})]_E$임을

$n \in \mathbb{Z}^+$에 대한 귀납법으로 보인다.

$n = 1$일때 $u_1 \in [t_1]_E$이므로 $ [f(u_1,x_{2},\cdots,x_{n_f})]_E \subseteq \displaystyle \bigcup_{a_1\in [t_1]_E}[f(a_1,x_2,\cdots,x_{n_f})]_E$이다.

임의의 $t \in \displaystyle \bigcup_{a_1 \in [t_1]_E}[f(a_1,x_2,\cdots,x_{n_f})]_E$는

$\Sigma \vdash (t = f(a_1,x_2,\cdots,x_{n_f}))$인 $a_1 \in [t_1]_E$이 존재하여 $\Sigma \vdash ( a_1 = t_1)$이고

임의의 $u_1 \in [t_1]_E$에 대해 $\Sigma \vdash ( t_1 = u_1)$이므로 추이성으로 $\Sigma \vdash ( a_1 = u_1)$이다.

$a_1,u_1$에 포함되지 않고 $x_2,\cdots,x_{n_f}$와 모두 다르고 $x\ne y$인 변수기호 $x,y$가 존재하므로

$(f(x,x_2,\cdots,x_{n_f}) = f(y,x_2,\cdots,x_{n_f}))$에 공리8을 적용하여 $y$를 $a_1,u_1$로 치환하면

$\Sigma \vdash ((a_1 = u_1) \to ((f(x,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(x,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f}))))$이고

전건긍정으로

$\Sigma \vdash ((f(x,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(x,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f})))$이다.

일반화로

$\Sigma \vdash (\forall x)((f(x,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(x,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f})))$이고

공리5로

$ \begin{align*}\Sigma \vdash & ((\forall x)((f(x,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(x,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f}))) \\[0.5em] & \to ((f(a_1,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(a_1,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f})))) \end{align*}$이므로

전건긍정으로

$\Sigma \vdash ((f(a_1,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f})) \to (f(a_1,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f})))$이다.

반사성으로 $\Sigma \vdash (f(a_1,x_2,\cdots,x_{n_f}) = f(a_1,x_2,\cdots,x_{n_f}))$이므로

전건긍정으로 $\Sigma \vdash  (f(a_1,x_2,\cdots,x_{n_f}) = f(u_1,x_2,\cdots,x_{n_f}))$가 되어

$\Sigma \vdash (t = f(a_1,x_2,\cdots,x_{n_f}))$에 추이성을 적용하면 $\Sigma \vdash (t = f(u_1,x_2,\cdots,x_{n_f}))$이다.

따라서 $t \in [f(u_1,x_2,\cdots,x_{n_f})]_E$이므로 $ \displaystyle \bigcup_{a_1\in [t_1]_E}[f(a_1,x_2,\cdots,x_{n_f})]_E \subseteq [f(u_1,x_2,\cdots,x_{n_f})]_E$가 되어

집합정리로 $\displaystyle \bigcup_{a_1\in [t_1]_E}[f(a_1,x_2,\cdots,x_{n_f})]_E = [f(u_1,x_2,\cdots,x_{n_f})]_E$이다.

모든 $k \in \mathbb{Z}^+$에 대해 $k\le n_f$일때

$\displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{k} \in [t_{k}]_E}[f(a_1,a_2,\cdots,a_{k}, x_{k+1},\cdots, x_{n_f})]_E = [f(u_1,u_2,\cdots,u_{k},x_{k+1},\cdots,x_{n_f})]_E$라고 가정하면

$k<k+1 \le n_f$일때 $1\le i \le k+1$에 대해 $u_i \in [t_i]_E $이므로

$[f(u_1,u_2,\cdots,u_k,u_{k+1},x_{k+2}\cdots,x_{n_f})]_E\subseteq \displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{k} \in [t_{k}]_E} \bigcup_{a_{k+1} \in [t_{k+1}]_E}[f(a_1,a_2,\cdots,a_{k}, a_{k+1},x_{k+2}\cdots, x_{n_f})]_E \text{ 이고}$

임의의 $t \in \displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{k} \in [t_{k}]_E}\bigcup_{a_{k+1}\in [t_{k+1}]_E} [f(a_1,a_2,\cdots,a_{k}, a_{k+1},x_{k+2},\cdots, x_{n_f})]_E $는

$\Sigma \vdash ( t= f(a_1,a_2,\cdots,a_k,a_{k+1},x_{k+2},\cdots,x_{n_f}))$인 $a_i \in [t_i]_E $가 존재하여 귀납가정으로

$\begin{align*}[f(a_1,a_2,\cdots,a_k,x_{k+1},x_{k+2}\cdots,x_{n_f})]_E & = \displaystyle \bigcup_{b_1 \in [t_1]_E}\bigcup_{b_2\in [t_2]_E}\cdots \bigcup_{b_{k} \in [t_{k}]_E}[f(b_1,b_2,\cdots,b_{k}, x_{k+1},x_{k+2},\cdots, x_{n_f})]_E\\[0.5em] & = [f(u_1,u_2,\cdots,u_{k},x_{k+1},x_{k+2},\cdots,x_{n_f})]_E \text{ 이므로} \end{align*}$

동치류 정리로 $\Sigma \vdash ( f(a_1,a_2,\cdots,a_k,x_{k+1},x_{k+2}\cdots,x_{n_f}) = f(u_1,u_2,\cdots,u_{k},x_{k+1},x_{k+2},\cdots,x_{n_f}))$이다.

$a_i,u_i \in [t_i]_E$에 포함되지 않고 $x_{k+2},\cdots,x_{n_f}$와 모두 다르고 $x\ne y$인 변수기호 $x,y$가 존재하므로

$( f(a_1,a_2,\cdots,a_k,x,x_{k+2}\cdots,x_{n_f}) = f(u_1,u_2,\cdots,u_{k},y,x_{k+2},\cdots,x_{n_f}))$에 대해 $n = 1$일때처럼

$\Sigma \vdash ( f(a_1,a_2,\cdots,a_k,a_{k+1},x_{k+2}\cdots,x_{n_f}) = f(u_1,u_2,\cdots,u_{k},u_{k+1},x_{k+2},\cdots,x_{n_f}))$이고

추이성으로 $\Sigma \vdash ( t = f(u_1,u_2,\cdots,u_{k},u_{k+1},x_{k+2},\cdots,x_{n_f}))$가 되어

$ \displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{k} \in [t_{k}]_E} \bigcup_{a_{k+1} \in [t_{k+1}]_E}[f(a_1,a_2,\cdots,a_{k}, a_{k+1},x_{k+2}\cdots, x_{n_f})]_E \subseteq [f(u_1,u_2,\cdots,u_k,u_{k+1},x_{k+2},\cdots,x_{n_f})] \text{ 이므로}$

집합정리로

$ \displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{k} \in [t_{k}]_E} \bigcup_{a_{k+1} \in [t_{k+1}]_E}[f(a_1,a_2,\cdots,a_{k}, a_{k+1},x_{k+2}\cdots, x_{n_f})]_E = [f(u_1,u_2,\cdots,u_k,u_{k+1},x_{k+2},\cdots,x_{n_f})] \text{ 이다.}$

따라서 모든 $n\in \mathbb{Z}^+$에 대해 $n\le n_f$일때

$\displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{n} \in [t_{n}]_E}[f(a_1,a_2,\cdots,a_{n}, x_{n+1},\cdots, x_{n_f})]_E = [f(u_1,u_2,\cdots,u_{n},x_{n+1},\cdots,x_{n_f})]_E$이므로

$n = n_f$일때 $ \displaystyle \bigcup_{a_1 \in [t_1]_E}\bigcup_{a_2\in [t_2]_E}\cdots \bigcup_{a_{n_f} \in [t_{n_f}]_E}[f(a_1,a_2,\cdots,a_{n_f})]_E = [f(u_1,u_2,\cdots,u_{n_f})]_E$이다.

2.

모든 $n \in \mathbb{Z}^+$에 대해 $n\le n_R$일때

$1\le i \le n\le n_R$인 임의의 $t_i \in V$와 임의의 $u_i \in [t_i]_E$와 $n < j \le n_R$인 임의의 $a_j\in V$에 대해

$\Sigma \vdash R(t_1,t_2,\cdots,t_{n},a_{n+1},\cdots,a_{n_R})$이면 $\Sigma \vdash R(u_1,u_2,\cdots,u_{n},a_{n+1},\cdots,a_{n_R})$임을

$n \in \mathbb{Z}^+$에 대한 귀납법으로 보인다.

$n = 1$일때 $\Sigma \vdash R(t_1,a_2,\cdots,a_{n_R})$이면 임의의 $u_1 \in [t_1]_E$에 대해 $\Sigma \vdash ( t_1 = u_1)$이므로

$a_2,\cdots,a_{n_f}$에 포함되지 않는 변수기호 $x$에 대해 $R(x,a_2,\cdots,a_{n_R})$에 공리5를 적용하여

$\Sigma \vdash ((t_1 = u_1) \to (R(t_1,a_2,\cdots,a_{n_R}) \to R(u_1,a_2,\cdots,a_{n_R})))$이므로 전건긍정으로 $\Sigma \vdash R(u_1,a_2,\cdots,a_{n_R})$이다.

모든 $k \in \mathbb{Z}^+$에 대해 $k \le n_R$일때

$\Sigma \vdash R(t_1,t_2,\cdots,t_{k},a_{k+1},\cdots,a_{n_R})$이면 $\Sigma \vdash R(u_1,u_2,\cdots,u_{k},a_{k+1},\cdots,a_{n_R})$임을 가정한다.

$k+1 \le n_R$일때 $\Sigma \vdash R(t_1,t_2,\cdots,t_{k},t_{k+1},a_{k+2}\cdots,a_{n_R})$이면

$1\le i \le k < n_R$인 $u_i\in [t_i]_E$에 대해 귀납가정으로 $\Sigma \vdash R(u_1,u_2,\cdots,u_{k},t_{k+1},a_{k+2}\cdots,a_{n_R})$이고

$u_{k+1}\in [t_{k+1}]_E$에 대해 $\Sigma \vdash (t_{k+1} = u_{k+1})$이므로

$u_1,u_2,\cdots,u_k$와 $a_{k+2},\cdots,a_{n_f}$에 포함되지 않는 변수기호 $x$에 대해

$ R(u_1,u_2,\cdots,u_{k},x,a_{k+2}\cdots,a_{n_R})$에 공리5를 적용하면

$\Sigma \vdash ((t_{k+1} = u_{k+1}) \to (R(u_1,u_2,\cdots,u_k,t_{k+1},a_{k+2}\cdots,a_{n_R}) \to R(u_1,u_2,\cdots,u_{k},u_{k+1},a_{k+2},\cdots,a_{n_R}))) \text{ 이 되어}$

전건긍정으로 $\Sigma \vdash R(u_1,u_2,\cdots,u_{k},u_{k+1},a_{k+2},\cdots,a_{n_R})$이다.

따라서 모든 $n \in \mathbb{Z}^+$에 대해 $n\le n_R$일때

$\Sigma \vdash R(t_1,t_2,\cdots,t_{n},a_{n+1},\cdots,a_{n_R})$이면 $\Sigma \vdash R(u_1,u_2,\cdots,u_{n},a_{n+1},\cdots,a_{n_R})$이므로

$n = n_{R}$일때 $\Sigma \vdash R(t_1,t_2,\cdots,t_{n_R})$이면 $\Sigma \vdash R(u_1,u_2,\cdots,u_{n_R})$이다.

 

 

 

정리7

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$에 대해

임의의 $\mathcal{L}$-이론 $T\subseteq W$가 무모순이면 $T$는 $\mathcal{L}$-일차논리에서 만족가능하다.

증명

임의의 기호는 집합이므로 $b_0 = \mathcal{L}$으로 정의하고 모든 $n \in \mathbb{N}$에 대해 $b_n$이 귀납적으로 정의될때

$b_{n+1} = \mathcal{L} \cup \{b_n \}$으로 정의되는 기호집합 $\{ b_0,b_1,\cdots\}$는 집합 정리로 가부번이고 모든 $n \in \mathbb{N}$에 대해 $b_n \notin \mathcal{L}$이다.

언어 $\mathcal{L} = \mathcal{F} \cup \mathcal{R} \cup \mathcal{C}$의 상수기호집합 $\mathcal{C}$는 가산이므로 가부번인 상수기호집합 $\{ b_0,b_1,\cdots\}$를 추가하여

$\mathcal{C}^+ = \mathcal{C} \cup \{ b_0,b_1,\cdots\}$로 확장하면 $\mathcal{L}$이 가산이므로 가산집합 정리로 $\mathcal{L}^+ = \mathcal{L} \cup \{ b_0,b_1,\cdots\}$는 가산이다.

일차논리에서 모든 변수기호들의 집합이 $\{ x_0,x_1,\cdots\}$일때

위 정리로 $W \subseteq W^+$인 $\mathcal{L}^+$-논리식집합 $W^+$는 가부번이므로

가산집합 정리로 하나의 자유변수를 가지는 $\mathcal{L}^+$-논리식들의 집합 $A = \{ \alpha_0,\alpha_1,\cdots\} \subseteq W^+$는 가산이고

모든 $n \in \mathbb{N}$에 대해 $(x_n = b_0) \in A$가 되어 무한집합 정리로 $A$는 무한이고 가부번 정리로 $A$는 가부번이다.

모든 논리식은 길이가 유한인 문자열이고 $\mathcal{C}^+\setminus \mathcal{C}$는 무한이므로

$\alpha_0\in A$에 포함되지 않는 $b_{n_0} \in \mathcal{C}^+\setminus \mathcal{C}$인 $n_0 \in \mathbb{N}$이 존재하고

정렬성으로 $b_{n_0}$에 대해 가장 작은 $n_0 \in \mathbb{N}$은 유일하게 존재하므로 $c_0 = b_{n_0}$으로 정의할때

모든 $n \in \mathbb{N}$에 대해 $c_0,c_1,\cdots, c_n \in \mathcal{C}^+\setminus \mathcal{C}$이 강귀납적으로 정의되면

$c_{n+1} \notin \{c_0,c_1,\cdots, c_n\}$이고 $\alpha_0,\alpha_1,\cdots, \alpha_{n}, \alpha_{n+1}\in A$에 포함되지 않는 상수를 $c_{n+1} \in \mathcal{C}^+ \setminus \mathcal{C}$로 정의한다.

모든 $n \in \mathbb{N}$에 대해 $\alpha_n\in A$에 포함되는 유일한 자유변수 $x_{i_n}$의 첨수를 $i_n \in \mathbb{N}$으로 표기할때

$\theta_n = (( \neg (\forall x_{i_n}) \alpha_n) \to (\neg $$\alpha_n[c_n / x_{i_n}]$$))$으로 정의하면 $\theta_n$은 문장이다.

 

$T\subseteq W\subseteq W^+$이고 모든 $n \in \mathbb{N}$에 대해 $\theta_n\in W^+$이므로 $T_n = T\cup \{ \theta_k : k< n \} \subseteq W^+$으로 정의할때

모든 $n \in \mathbb{N}$에 대해 $\mathcal{L}^+$-일차논리에서 $T_n$이 무모순임을 귀납법을 사용하여 증명한다.

$n = 0$일때

$\mathcal{L}$-일차논리에서 $T_0  = T$는 무모순이고 $T$의 모든 논리식은 $\mathcal{C}^+\setminus \mathcal{C}$의 상수들을 항으로 갖지 않으므로

$\mathcal{L}^+$-일차논리에서 $T$에 모순이 있으면 어떤 $\psi^+ \in W^+$에 대해 $\psi^+ , (\neg \psi^+)$가 $T$의 정리인데

$T$로부터 $\psi^+ , (\neg \psi^+)$의 증명에서 나온 $\mathcal{C}^+\setminus \mathcal{C}$의 상수들은 유한 개이고 변수집합은 무한이므로

증명에서 나오지 않는 변수들을 $\mathcal{C}^+\setminus \mathcal{C}$의 상수들에 대응시켜 치환하면

어떤 $\psi \in  W$에 대해 $\psi , (\neg \psi)$가 $T$의 정리이고 $\mathcal{L}$-일차논리에서 $T$가 무모순이라는 가정에 모순이므로 

$\mathcal{L}^+$-일차논리에서 $T_0 = T$는 무모순이다.

모든 $k \in \mathbb{N}$에 대해 $T_k = T\cup \{ \theta_0,\cdots ,\theta_{k-1}\}$가 무모순이라고 가정할때

$T_{k +1} = T \cup \{ \theta_0,\cdots ,\theta_{k-1},\theta_k\} = T_k \cup \{ \theta_k\}$에 모순있다고 가정하면

어떤 $\psi \in W^+$에 대해 $\psi , (\neg \psi)$가 $T_k \cup \{ \theta_k\}$의 정리이고 형식계 정리로 $T_k \cup \{ \theta_k\} \cup \{ (\neg (\neg \theta_k))\}$의 정리가 되어

$\theta_k$가 문장임에 따라 위 정리로 $(\neg \theta_k)$는 $T_k \cup \{ \theta_k\}$의 정리이고 $(\theta_k \to (\neg \theta_k))$는 $T_k$의 정리이다.

또 위 정리와 명제논리 정리로 $((\theta_k \to (\neg \theta_k)) \to (\neg \theta_k))$는 일차논리의 정리이므로 형식계 정리로 $T_k$의 정리가 되어

전건긍정으로 $(\neg \theta_k) = (\neg (( \neg (\forall x_{i_k}) \alpha_k) \to (\neg \alpha_k[c_k/x_{i_k}])) )$는 $T_k$의 정리이고

위 정리와 명제논리 정리로

$((\neg (( \neg (\forall x_{i_k}) \alpha_k) \to (\neg \alpha_k[c_k/x_{i_k}])) ) \to (\neg (\forall x_{i_k}) \alpha_k))$와 $((\neg (( \neg (\forall x_{i_k}) \alpha_k) \to (\neg \alpha_k[c_k/x_{i_k}])) ) \to \alpha_k[c_k/x_{i_k}])$가

일차논리의 정리이므로 형식계 정리와 전건긍정으로 $(\neg (\forall x_{i_k}) \alpha_k)$와 $\alpha_k[c_k/x_{i_k}]$는 $T_k$의 정리이다.

$c_k$의 정의로 $c_k \in \mathcal{C}^+ \setminus \mathcal{C}$는 $T_k = T \cup \{ \theta_0,\cdots, \theta_{k-1}\}$의 모든 논리식에 포함되지 않으므로

$T_k$로부터 $\alpha_k[c_k/x_{i_k}]$의 증명에서 나온 $c_k$를 포함하는 논리식은 $T_k$의 원소가 아니고 공리나 추론규칙으로 유도되어

$c_k$를 증명에 나오지 않은 변수기호 $y$로 치환가능하고 증명에 나온 모든 $c_k$를 $y$로 치환하면

$\alpha_k[y/x_{i_k}]$는 $T_k$의 정리이므로 일반화로 $(\forall y)\alpha_k[y/x_{i_k}]$는 $T_k$의 정리이고

위 정리와 형식계 정리로 $((\forall y)\alpha_k[y/x_{i_k}] \to (\forall x_{i_k}) \alpha_k)$가 $T_k$의 정리이므로

전건긍정으로 $(\forall x_{i_k}) \alpha_k$가 $T_k$의 정리이고 $T_k$에 모순 $(\forall x_{i_k}) \alpha_k,$ $(\neg (\forall x_{i_k}) \alpha_k)$가 있게 되어

귀납가정인 $T_{k}$가 무모순임에 모순이므로 $T_{k +1} = T\cup \{ \theta_0,\cdots,\theta_{k-1},\theta_k\} = T_k \cup \{ \theta_k\}$은 무모순이다.

따라서 모든 $n \in \mathbb{N}$에 대해 $T_n$은 무모순이고 $\displaystyle \bigcup_{n = 0}^\infty T_n$으로부터 논리식의 증명은 크기가 유한인 배열이므로

$\displaystyle \bigcup_{n = 0}^\infty T_n$도 무모순이 되어 위 정리로 $\displaystyle T\cup \{ \theta_n : n\in \mathbb{N}\}=\bigcup_{n = 0}^\infty T_n \subseteq T^+$이고

모든 문장 $\phi \in W^+$에 대해 $\phi \in T^+$ 또는 $(\neg \phi) \in T^+$중 하나만 성립하는 무모순인 집합 $T^+$가 존재한다.

 

$\mathcal{L}^+$-항집합이 $X$일때 $V \subseteq X$가 변수기호를 갖지 않는 모든 항들의 집합이면 $\{ b_0,b_1,\cdots \}\subseteq V$이므로 $V \ne \emptyset$이고

$t,u \in V$에 대해 $E(t,u)$이기 위한 필요충분조건이 $T^+ \vdash (t = u)$인 이항관계 $E$는 위 정리로 $V$의 동치관계이므로

$T^+$가 만족가능한 $\mathcal{L}^+$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$과 $\mathcal{M}$에 대한 항의 해석 $s : X \to M$를 다음과 같이 정의한다.

1. $\mathcal{M}$의 전체 $M$은 $E$에 대한 $V$의 몫집합 $M = V/E$로 정의한다.

2. 변수기호집합은 가부번이고 추가된 상수기호집합 $\{ b_0,b_1,\cdots\}$도 가부번이므로

항의 해석 $s$는 변수기호 $x_i$에 대해 $E$에 대한 상수 $b_i$의 동치류 $s(x_i) = [b_i]_E$로 할당된다.

3. 상수기호 $c \in \mathcal{L}^+$에 대응되는 $\mathcal{M}$의 상수 $c_\mathcal{M}\in M$은 $E$에 대한 $c$의 동치류 $c_\mathcal{M} = [c]_E$로 정의한다.

4. 함수기호 $f \in \mathcal{L}$에 대응되는 $\mathcal{M}$의 $n_f$항함수 $f_\mathcal{M}$은

임의의 $[t_1]_E,\cdots, [t_{n_f}]_E \in M$에 대해 $f_\mathcal{M}([t_1]_E,\cdots,[t_{n_f}]_E) = \displaystyle \bigcup_{u_1 \in [t_1]_E}\cdots \bigcup_{u_{n_f}\in [t_{n_f}]_E} [f(u_1,\cdots,u_{n_f})]_E$로 정의한다.

5. 관계기호 $R \in \mathcal{L}$에 대응되는 $\mathcal{M}$의 $n_R$항관계 $R_\mathcal{M}$은

임의의 $[t_1]_E,\cdots, [t_{n_R}]_E \in M$에 대해 $R_\mathcal{M}([t_1]_E,\cdots,[t_{n_R}]_E)$이기 위한 필요충분조건이

모든 $u_1 \in [t_1]_E ,\cdots, u_{n_R}\in [t_{n_R}]_E$에 대해 $T^+ \vdash R(u_1,\cdots,u_{n_R})$인 것이다.

 

위 정리의 집합열이 $X_0,X_1,\cdots \subseteq X$일때 모든 $n \in \mathbb{N}$에 대해

임의의 항 $t \in \displaystyle \bigcup_{i = 0}^nX_i$가 $t \in V$이면 $\mathcal{M}$에 대한 항의 해석 $s$에 대해 $s(t) = [t]_E$임을 귀납법으로 보인다.

$n=0$일때 $t \in X_0$가 $t \in V$이면 $t = c$인 상수기호이므로 

항의 해석 정의로 $c \in \mathcal{L}^+$에 대응되는 상수 $c_\mathcal{M} \in M$에 대해 $s(c) = c_\mathcal{M} = [c]_E $이다.

모든 $k \in \mathbb{N}$에 대해 $t \in \displaystyle \bigcup_{i = 0}^kX_i$가 $t \in V$이면 $s(t) = [t]_E$일때

 $t \in \displaystyle \bigcup_{i = 0}^{k+1}X_i$는 $t \in \displaystyle \bigcup_{i = 0}^{k}X_i$이거나 $t \in X_{k+1}$이므로 $t \in \displaystyle \bigcup_{i = 0}^{k}X_i$이면 귀납가정으로 $t \in V$일때 $s(t) = [t]_E$이고

$t \in X_{k+1}$가 $t \in V$이면 어떤 함수기호 $f \in \mathcal{L}$와 어떤 $t_1,\cdots,t_{n_f}\in \displaystyle \bigcup_{i = 0}^kX_i$에 대해

$t = f(t_1,\cdots,t_{n_f})$이고 $t$는 변수기호를 갖지 않으므로 $t_1,\cdots,t_{n_f}\in V$가 되어

$f $에 대응되는 $n_f$항함수 $f_\mathcal{M}$에 대해 위 정리로 $t_1 \in [t_1]_E ,\cdots, t_{n_f} \in [t_{n_f}]_E$이고

$s(\,f(t_1,\cdots,t_{n_f})\,)=f_\mathcal{M}([t_1]_E,\cdots,[t_{n_f}]_E) = \displaystyle \bigcup_{u_1 \in [t_1]_E}\cdots \bigcup_{u_{n_f}\in [t_{n_f}]_E} [f(u_1,\cdots,u_{n_f})]_E = [f(t_1,\cdots,t_{n_f})]_E$이다.

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고 $X = \displaystyle \bigcup_{i = 0}^\infty X_i$이므로 모든 $t \in X$에 대해 $t \in V$이면 $s(t) = [t]_E$이다.

 

위 정리의 집합열이 $W_0^+,W_1^+,\cdots \subseteq W^+$이고 $s$에 대한 값매김이 $v_s : W^+ \to \{\mathbf{F},\mathbf{T}\}$일때

모든 $n \in \mathbb{N}$에 대해 $\phi\in \displaystyle \bigcup_{i = 0}^nW^+_i$가 문장이면 $ T^+$ $\vdash$ $\phi$이기 위한 필요충분조건이 $v_s(\phi) = \mathbf{T}$임을 귀납법으로 보인다.

$n = 0$일때 $\phi \in W^+_0$는 원자논리식이므로 $\phi$가 문장이면 $\phi$에 포함되는 항들은 모두 $V$에 속하여

$\phi \in W^+_0$가 어떤 관계기호 $R \in \mathcal{L}$와 어떤 $t_1,\cdots,t_{n_R}\in V$에 대해 $\phi = R(t_1,\cdots,t_{n_R})$이면

$T^+ \vdash R(t_1,\cdots,t_{n_R})$일때 위 정리로 모든 $u_1 \in [t_1]_E ,\cdots, u_{n_R}\in [t_{n_R}]_E$에 대해 $T^+ \vdash R(u_1,\cdots,u_{n_R})$이므로

$R$에 대응되는 $n_R$항관계 $R_\mathcal{M}$에 대해 $R_\mathcal{M}([t_1]_E,\cdots,[t_{n_R}]_E)$이고

위에서 보인 것으로 $s(t_1) = [t_1]_E, \cdots, s(t_{n_R}) = [t_{n_R}]_E$이므로 $R_\mathcal{M}(s(t_1),\cdots,s(t_{n_R}))$이 되어

$v_s(\,R(t_1,\cdots,t_{n_R})\,) = \mathbf{T}$이다.

역으로 $v_s(\,R(t_1,\cdots,t_{n_R})\,) = \mathbf{T}$이면 모든 $u_1 \in [t_1]_E ,\cdots, u_{n_R}\in [t_{n_R}]_E$에 대해 $T^+ \vdash R(u_1,\cdots,u_{n_R})$이므로

위 정리로 $t_1 \in [t_1]_E ,\cdots, t_{n_R}\in [t_{n_R}]_E$임에 따라 $T^+ \vdash R(t_1,\cdots,t_{n_R})$이다.

$\phi \in W^+_0$가 어떤 $t_1,t_{2}\in V$에 대해 $\phi = (t_1 = t_2)$이면

$T^+ \vdash (t_1 = t_2)$일때 $E(t_1,t_2)$이므로 동치류 정리와 위에서 보인 것으로 $s(t_1) =[t_1]_E =[t_2]_E = s(t_2)$가 되어

$v_s(\,(t_1=t_{2})\,) = \mathbf{T}$이다.

역으로 $v_s(\,(t_1=t_{2})\,) = \mathbf{T}$이면 $[t_1]_E = s(t_1) = s(t_2) =[t_2]_E $이므로 동치류 정리로 $T^+ \vdash (t_1 = t_2)$이다.

모든 $k \in \mathbb{N}$에 대해 문장 $\phi\in \displaystyle \bigcup_{i = 0}^kW^+_i$가 $T^+ \vdash \phi$이기 위한 필요충분조건이 $v_s(\phi) = \mathbf{T}$일때

문장 $\phi\in \displaystyle \bigcup_{i = 0}^{k+1}W^+_i$가 $\phi\in \displaystyle \bigcup_{i = 0}^{k}W^+_i$이면 귀납가정으로 $T^+ \vdash \phi$와 $v_s(\phi) = \mathbf{T}$가 동치이다.

문장 $\phi\in \displaystyle \bigcup_{i = 0}^{k+1}W^+_i$가 $\phi \in W^+_{k+1}$이면

어떤 $\psi,\theta\in \displaystyle \bigcup_{i = 0}^{k}W^+_i$와 어떤 변수기호 $x$에 대해 $\phi = (\neg \psi)$ 또는 $\phi = (\psi \to \theta)$ 또는 $\phi = (\forall x)\psi$이므로

$\phi = (\neg \psi)$일때 

$T^+ \vdash (\neg \psi)$이면 $T^+$가 무모순임에 따라 $\psi$는 $T^+$의 정리가 아니므로

귀납가정으로 $v_s(\psi) = \mathbf{F}$가 되어 위 정리와 불 대수 정리로 $v_s(\,(\neg \psi)\,) = \neg v_s(\psi) = \neg \mathbf{F} = \mathbf{T}$이다.

역으로 $v_s(\,(\neg \psi)\,) = \mathbf{T}$이면

위 정리와 불 대수 정리로 $v_s(\psi) = \neg (\neg v_s(\psi)) = \neg v_s(\,(\neg \psi)\,) = \neg \mathbf{T} = \mathbf{F}$가 되어

귀납가정으로 $\psi$는 $T^+$의 정리가 아니고 $T^+$의 정의로 $\psi \in T^+$ 또는 $(\neg \psi) \in T^+$인데

$\psi \in T^+$이면 모순이므로 $(\neg \psi) \in T^+$가 되어 $T^+ \vdash (\neg \psi)$이다.

$\phi = (\psi \to \theta)$일때

$T^+ \vdash (\psi\to \theta)$이고 $v_s(\,(\psi \to \theta)\,) = \mathbf{F}$라고 가정하면

위 정리와 불 대수 정의로 $\mathbf{F}= v_s(\,(\psi \to \theta)\,)= v_s(\psi) \to v_s(\theta) = \neg v_s(\psi) \lor v_s(\theta)$가 되어

$v_s(\psi) = \mathbf{T}$이고 $v_s( \theta) = \mathbf{F}$이므로 귀납가정으로 $\psi$는 $T^+$의 정리이고 $\theta$는 $T^+$의 정리가 아니다.

$T^+$의 정의에 모순이 되지 않도록 $(\neg \theta )\in T^+$가 되어 $\psi,(\neg \theta)$는 $T^+$의 정리이고

위 정리와 명제논리 정리와 형식계 정리로 $(\psi \to ((\neg \theta) \to (\neg (\psi \to \theta))))$도 $T^+$의 정리이므로

전건긍정으로 $(\neg (\psi \to \theta))$는 $T^+$의 정리인데 $T^+ \vdash (\psi\to \theta)$를 가정하였으므로 $T^+$의 정의에 모순이 되어

$T^+ \vdash (\psi\to \theta)$이면 $v_s(\,(\psi \to \theta)\,) = \mathbf{T}$이다.

역으로 $v_s(\,(\psi \to \theta)\,) = \mathbf{T}$일때 $(\psi \to \theta)$가 $T^+$의 정리가 아니라고 가정하면

$T^+$의 정의에 모순이 되지 않도록 $(\neg (\psi \to \theta))\in T^+$가 되어 $(\neg (\psi \to \theta))$는 $T^+$의 정리이고

위 정리와 명제논리 정리와 형식계 정리로 $((\neg (\psi \to \theta))\to \psi)$와 $((\neg (\psi \to \theta))\to (\neg \theta))$가 $T^+$의 정리가 되어

전건긍정으로 $\psi,(\neg \theta)$가 $T^+$의 정리이므로 귀납가정으로 $v_s(\psi) = \mathbf{T}$이고 $v_s(\theta) = \mathbf{F}$인데

위 정리와 불 대수 정의와 불 대수 정리로 $\mathbf{T}=v_s(\,(\psi \to \theta)\,) = v_s(\psi) \to v_s(\theta) = \neg \mathbf{T} \lor \mathbf{F} = \mathbf{F}$인 모순이 되어

$v_s(\,(\psi \to \theta)\,) = \mathbf{T}$이면 $T^+ \vdash (\psi \to \theta)$이다.

$x$가 $\psi$의 자유변수가 아니고 $\phi = (\forall x)\psi$일때

$T^+ \vdash (\forall x) \psi$이면 공리4와 전건긍정으로 $T^+\vdash \psi$이고 $x$가 $\psi$의 자유변수가 아니므로 $\psi$는 문장이 되어

귀납가정과 위 정리로 모든 $r \in M$에 대해 $v_{s[r/x]}(\psi) =v_s(\psi) = \mathbf{T}$이고 $v_s(\,(\forall x) \psi\,) = \mathbf{T}$이다.

역으로 $v_s(\,(\forall x) \psi\,) = \mathbf{T}$이면

위 정리로 $v_s(\psi) = \mathbf{T}$이고 $\psi$는 문장이므로 귀납가정으로 $T^+\vdash \psi$가 되어 일반화로 $T^+ \vdash (\forall x) \psi$이다.

$x$가 $\psi$의 자유변수이고 $\phi = (\forall x)\psi$일때

$\psi$는 하나의 자유변수만 갖는 논리식이므로 $x = x_{i_m}$이고 $\psi = \alpha_m\in A$인 $m\in \mathbb{N}$이 존재하여

$v_s(\, (\forall x_{i_m})\alpha_m\,)  = v_s(\,(\forall x)\psi\,)= \mathbf{T}$이면 상수기호 $c_m \in \mathcal{C}^+\setminus \mathcal{C}$에 대해 공리5의 $((\forall x_{i_m}) \alpha_{m} \to \alpha_m[c_m/x_{i_m}])$는

위 정리로 일차논리의 논리적 귀결이므로 $v_s(\, ((\forall x_{i_m}) \alpha_{m} \to \alpha_m[c_m/x_{i_m}]) \,) = \mathbf{T}$가 되어

위 정리로 $v_s(\,(\forall x_{i_m})\alpha_m\,) \to v_s(\alpha_m[c_m/x_{i_m}]) = v_s(\, ((\forall x_{i_m}) \alpha_{m} \to \alpha_m[c_m/x_{i_m}]) \,) = \mathbf{T}$이므로

불 대수 정리로 $v_s(\alpha_m[c_m/x_{i_m}]) = \mathbf{T}$이고 $\alpha_m[c_m/x_{i_m}]$이 문장임에 따라 귀납가정으로 $T^+ \vdash \alpha_m[c_m/x_{i_m}]$이다.

문장 $(\forall x)\psi$가 $T^+$의 정리가 아니라고 가정하면 $ (\neg (\forall x)\psi)\in T^+$이므로 $T^+ \vdash (\neg (\forall x)\psi)$이고

위에서 보인 것으로 $\theta_m=((\neg (\forall x_{i_m})\alpha_m) \to (\neg \alpha_m[c_m/x_{i_m}]))$은

$ ((\neg (\forall x_{i_m})\alpha_m) \to (\neg \alpha_m[c_m/x_{i_m}]))  \in T^+$이므로 $T^+ \vdash ((\neg (\forall x_{i_m})\alpha_m) \to (\neg \alpha_m[c_m/x_{i_m}]))$가 되어

$(\neg(\forall x)\psi )=  (\neg (\forall x_{i_m}) \alpha_m)$로 $T^+ \vdash (\neg (\forall x_{i_m})\alpha_m)$에 대해 전건긍정으로 $T^+ \vdash (\neg \alpha_m[c_m/x_{i_m}])$인데

$\alpha_m[c_m/x_{i_m}], (\neg \alpha_m[c_m/x_{i_m}])$이 $T^+$의 정리이므로 $T^+$가 무모순임에 모순이 되어 $T^+ \vdash (\forall x)\psi$이다.

역으로 $T^+ \vdash (\forall x)\psi$일때 $v_s(\,(\forall x) \psi\,) = \mathbf{F}$라고 가정하면

$(\forall x)\psi = (\forall x_{i_m}) \alpha_m$로 $v_s(\, (\forall x_{i_m}) \alpha_m\,) = \mathbf{F}$이므로 위 정리로 $v_{s[r/x_{i_m}]}(\alpha_m) = \mathbf{F}$인 $r \in M = V/E$이 존재하고

$r$은 $E$에 대한 동치류이므로 $r = [t]_E$인 $t \in V$가 존재하여 위에서 보인 것처럼 $s(t) = [t]_E =r$이다.

$t\in V$는 변수기호를 갖지 않으므로 $\alpha_m$에서 $x_{i_m}$을 $t$로 치환가능하여 $\alpha_m[t/x_{i_m}]$은 문장이고

위 정리의 구성은 $\neg , \to ,\forall$에 따라 구성되어 $\alpha_m = \psi \in \displaystyle \bigcup_{i = 0}^{k}W^+_i$에 대해 $\alpha_m[t/x_{i_m}]\in \displaystyle \bigcup_{i = 0}^{k}W^+_i$이므로

위 정리로 $\mathbf{F} =v_{s[s(t)/x_{i_m}]}(\alpha_m) = v_s(\alpha_m[t/x_{i_m}])$에 대해

귀납가정으로 $\alpha_m[t/x_{i_m}]$은 $T^+$의 정리가 아니고 $(\neg \alpha_m[t/x_{i_m}]) \in T^+$이므로 $T^+ \vdash (\neg \alpha_m[t/x_{i_m}])$이다.

하지만 $T^+ \vdash (\forall x_{i_m}) \alpha_m$이고 공리5와 전건긍정으로 $T^+ \vdash \alpha_m[t/x_{i_m}]$이므로 $T^+$가 무모순임에 모순이 되어

$T^+ \vdash (\forall x)\psi$이면 $v_s(\,(\forall x) \psi\,) = \mathbf{T}$이다.

따라서 모든 $n \in \mathbb{N}$에 대해 가정이 성립하고 $W^+ = \displaystyle \bigcup_{i = 0}^\infty W^+_i$이므로

임의의 $\phi\in W^+$가 문장이면 $T^+$ $\vdash$ $\phi$이기 위한 필요충분조건은 $v_s(\phi) = \mathbf{T}$가 되어

$\mathcal{L} \subseteq \mathcal{L}^+$인 $\mathcal{L}^+$-구조 $\mathcal{M}$의 전체 $M$은 그대로 두고 상수기호에 대한 해석만 제한하여 $\mathcal{M}$을 $\mathcal{L}$-구조로 정의할때

$s$에 대한 값매김 $v_s$에 대해 모든 문장 $\phi \in T \subseteq T^+$는 $T^+ \vdash \phi$이므로 $v_s(\phi) = \mathbf{T}$가 되어

무모순인 $\mathcal{L}$-이론 $T$는 언어가 $\mathcal{L}$인 일차논리에서 만족가능하다.

 

 

 

정리13(가산 일차논리의 완전성[completeness])

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$와 임의의 $\mathcal{L}$-이론 $T\subseteq W$에 대해

임의의 문장 $\phi \in W$가 $T \models \phi$이면 $T \vdash \phi$이다.

증명

임의의 문장 $\phi \in W$에 대해 $T \models \phi$이면 형식계 정리로 $T \cup \{ (\neg \phi) \} \models \phi$이므로

모든 $\sigma \in T \cup \{ (\neg \phi) \}$에 대해 $v(\sigma) =\mathbf{T}$인 모든 값매김 $v$가 $v(\phi) = \mathbf{T}$인데

위 정리와 불 대수 정리로 $ \mathbf{T} = v(\,(\neg \phi)\,) = \neg v(\phi) = \neg \mathbf{T} = \mathbf{F}$가 되어

불 대수 정의에 모순이므로 $T \cup \{ (\neg \phi) \}$는 $\mathcal{L}$-일차논리에서 만족가능하지 않다.

따라서 위 정리의 대우로 $T \cup \{ (\neg \phi) \}$에는 모순이 있어

어떤 논리식 $\psi \in W$에 대해 $\psi ,(\neg \psi)$가 $T \cup \{ (\neg \phi) \}$의 정리이고 $\phi$가 문장이므로

위 정리로 $((\neg \phi) \to \psi), ((\neg \phi) \to (\neg \psi))$는 $T$의 정리이고

위 정리와 명제논리 정리와 형식계 정리로

$T\vdash (((\neg \phi) \to \psi) \to (((\neg \phi) \to (\neg \psi)) \to \phi))$가 되어 전건긍정으로 $T \vdash \phi$이다.

 

 

 

정리16

일차논리의 논리식집합이 $W$이고 임의의 부분집합이 $\Sigma \subseteq W$일때 다음이 성립한다.

1. 임의의 논리식 $\phi \in W$에 대해 $\phi,(\neg \phi)$는 $\{ (\neg (\phi\to \phi)) \}$의 정리이다.

2. $n \in \mathbb{Z}^+$개의 임의의 변수기호 $x_1,x_2,\cdots,x_n$과 임의의 논리식 $\phi \in W$에 대해

$\Sigma $ $\vdash $ $ (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$이기 위한 필요충분조건은 $\Sigma \vdash \phi$인 것이다.

증명

1.

위 정리와 명제논리 정리와 형식계 정리로

$((\neg (\phi \to \phi)) \to \phi)$와 $((\neg (\phi \to \phi)) \to (\neg \phi))$는 $\{ (\neg (\phi \to \phi))\}$의 정리이므로

전건긍정으로 $\phi,(\neg \phi)$는 $\{ (\neg (\phi \to \phi))\}$의 정리이다.

2.

$n\in \mathbb{Z}^+$에 대한 귀납법으로 증명한다.

$n = 1$일때 임의의 변수기호 $x_1$에 대해 $\Sigma \vdash \phi$이면 일반화로 $\Sigma \vdash (\forall x_1)\phi$이고

$\Sigma \vdash (\forall x_1)\phi$이면 공리4 또는 공리5로 $\Sigma \vdash ((\forall x_1)\phi \to \phi)$이므로 전건긍정으로 $\Sigma \vdash \phi$이다.

모든 $k \in \mathbb{Z}^+$에 대해 가정이 성립할때 $k+1$개의 변수기호 $x_1,x_2,\cdots,x_k,x_{k+1}$에 대해

$n =1$일때처럼 $\Sigma \vdash (\forall x_1)(\forall x_2)\cdots (\forall x_k)(\forall x_{k+1})\phi$와 $\Sigma \vdash (\forall x_2)\cdots (\forall x_k)(\forall x_{k+1})\phi$는 동치이고

귀납가정으로 $\Sigma \vdash (\forall x_2)\cdots (\forall x_k)(\forall x_{k+1})\phi$와 $\Sigma \vdash \phi$는 동치이므로

$\Sigma \vdash (\forall x_1)(\forall x_2)\cdots (\forall x_k)(\forall x_{k+1})\phi$이기 위한 필요충분조건은 $\Sigma \vdash \phi$인 것이다.

따라서 모든 $n \in \mathbb{Z}^+$에 대해 $\Sigma \vdash (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$이기 위한 필요충분조건은 $\Sigma \vdash \phi$인 것이다.

 

 

 

정리15

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합이 $W$일때

임의의 논리식 $\phi \in W$가 $\mathcal{L}$-일차논리의 논리적 귀결이기 위한 필요충분조건은 $\phi$가 $\mathcal{L}$-일차논리의 정리인 것이다.

증명

$\vdash \phi$일때 $\models \phi$임은 건전성으로 성립한다.

역으로 $\phi$가 $\models \phi$일때 $\phi$가 문장이면 완전성으로 $\vdash \phi$이다.

$\models \phi$인 $\phi$가 문장이 아닐때 자유변수 $x_1,x_2,\cdots,x_n$을 가지면 모든 $\mathcal{L}$-구조 $\mathcal{M}$에 대해 $\mathcal{M} \models \phi$이고

위 정리로 $\mathcal{M} \models (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$이므로 $\models (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$이다.

$\theta = (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$로 둘때 $\models \theta$이므로 형식계 정리로 $\{(\neg \theta)\}\models \theta$가 되어

$v(\, (\neg \theta)\,) =\mathbf{T}$인 모든 값매김 $v$가 $v(\theta) = \mathbf{T}$인데

위 정리와 불 대수 정리로 $ \mathbf{T} = v(\,(\neg \theta)\,) = \neg v(\theta) = \neg \mathbf{T} = \mathbf{F}$가 되어

불 대수 정의에 모순이므로 $ \{ (\neg \theta) \}$는 $\mathcal{L}$-일차논리에서 만족가능하지 않다.

따라서 위 정리의 대우로 $\{ (\neg \theta) \}$에는 모순이 있어

어떤 논리식 $\psi \in W$에 대해 $\psi ,(\neg \psi)$가 $ \{ (\neg \theta) \}$의 정리이고 $\theta$가 문장이므로

위 정리로 $((\neg \theta) \to \psi), ((\neg \theta) \to (\neg \psi))$는 $\mathcal{L}$-일차논리의 정리이고

위 정리와 명제논리 정리로 $\vdash (((\neg \theta) \to \psi) \to (((\neg \theta) \to (\neg \psi)) \to \theta))$가 되어

전건긍정으로 $ \vdash \theta$이므로 $\vdash (\forall x_1)(\forall x_2)\cdots (\forall x_n)\phi$이고 위 정리로 $\vdash \phi$이다.

 

 

 

정리17(가산 일차논리의 콤팩트성[compactness])

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$와 임의의 $\mathcal{L}$-이론 $T \subseteq W$에 대해 

$T$의 유한인 모든 부분집합이 $\mathcal{L}$-일차논리에서 만족가능하면 $T$도 $\mathcal{L}$-일차논리에서 만족가능하다.

증명

$T$의 유한인 모든 부분집합이 $\mathcal{L}$-일차논리에서 만족가능하면 위 정리로 $T$의 유한인 모든 부분집합은 무모순이다.

귀류법으로 $T$가 만족가능하지 않다고 가정하면

위 정리의 대우로 $T$에는 모순이 있어 어떤 $\psi \in W$에 대해 $\psi ,(\neg \psi)$가 $T$의 정리인데

$T$로부터 $\psi, (\neg \psi)$의 증명은 각각 크기가 유한인 배열이므로 증명에 사용된 $\psi,(\neg \psi)$의 가정도 유한 개가 되어

증명에 사용된 $\psi,(\neg \psi)$의 가정을 모두 포함하는 유한인 부분집합 $\Gamma \subseteq T$가 존재하므로

$\psi, (\neg \psi)$는 $\Gamma$의 정리가 되고 $\Gamma$가 무모순이라는 가정에 모순이므로 $T$는 무모순이다.

 

 

 

정리18(가산 뢰벤하임-스콜렘[Löwenheim-Skolem] 정리)

언어 $\mathcal{L}$이 가산인 일차논리의 논리식집합 $W$와 임의의 $\mathcal{L}$-이론 $T \subseteq W$에 대해 

$\mathcal{N} $ $\models$ $T$인 $\mathcal{L}$-구조 $\mathcal{N}$이 존재하면 $\mathcal{M} \models T$이고 전체 $M$이 가산인 $\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$이 존재한다.

증명

$\mathcal{N} \models T$이면 $\mathcal{N}$의 모든 값매김 $v_\mathcal{N}$에 대해 모든 $\phi \in T$가 $v_\mathcal{N}(\phi) = \mathbf{T}$이므로

$T$는 $\mathcal{L}$-일차논리에서 만족가능하여 위 정리로 $T$는 무모순이다.

위 정리에 나온 $\mathcal{L}$-구조 $\mathcal{M} = (M,f_\mathcal{M},R_\mathcal{M},c_\mathcal{M})$과 $\mathcal{M}$에 대한 항의 해석 $s$와 $s$에 대한 값매김 $v_s$에 대해

모든 $\phi \in T$가 $v_s(\phi) = \mathbf{T}$이고 $\phi$는 문장이므로

위 정리로 $\mathcal{M}$의 모든 값매김 $v_\mathcal{M}$에 대해 $v_\mathcal{M}(\phi) = v_s(\phi)= \mathbf{T}$가 되어 $\mathcal{M} \models T$이다.

따라서 위 정리로 확장된 언어에서 변수기호를 갖지 않는 항들의 집합은 가산이고

$\mathcal{M}$의 전체인 확장된 언어에서 변수기호를 갖지 않는 항집합의 몫집합도 몫집합 정리로 가산이므로 정리가 성립한다.

 

 

 

-------------------------------------------------------------------------------

정의의 링크 : 

https://openknowledgevl.tistory.com/62#def번호

번호는 해당 정의 옆에 붙어있는 작은 숫자입니다.

 

정리의 링크 : 

https://openknowledgevl.tistory.com/62#thm번호

번호는 해당 정리 옆에 붙어있는 작은 숫자입니다.

 

위 내용은 아래의 출처를 기반으로 정리한 내용입니다.

틀린 내용이 존재할 수 있습니다.

 

출처(저자 - 제목 - ISBN13)

Peter J. Cameron - Sets, Logics and Categories - 9791196120375

A. G. Hamilton - Logic for Mathematicians - 9780521368650

David Marker - Model Theory An Introduction - 9780387987606

Herbert B. Enderton - A Mathematical Introduction to Logic - 9780122384523