이제 의미론과 비교할 일계논리의 형식추론계를 정한다. 이 장에서는 가정으로 사용하는 논리식들을 문장으로 제한한다. 따라서 전칭 일반화 규칙을 사용할 때 자유변수를 가진 가정 때문에 생기는 부가조건을 따로 적을 필요가 없다. 자유변수를 가진 가정까지 허용하려면 일반화되는 변수가 모든 미해제 가정에서 자유롭게 나타나지 않는다는 표준적인 제한이 필요하다.
명제논리와 마찬가지로 다음 세 공리틀을 사용한다.
- (A1) \(\phi\to(\psi\to\phi)\)
- (A2) \((\phi\to(\psi\to\theta))\to((\phi\to\psi)\to(\phi\to\theta))\)
- (A3) \((\neg\phi\to\neg\psi)\to(\psi\to\phi)\)
한정기호를 위한 공리틀은 다음과 같다.
- (A4) \((\forall x)\phi\to\phi[t/x]\), 단 \(t\)는 \(\phi\)에서 \(x\)에 대해 자유롭게 대입 가능하다.
- (A5) \((\forall x)(\phi\to\psi)\to(\phi\to(\forall x)\psi)\), 단 \(x\)는 \(\phi\)에서 자유롭게 나타나지 않는다.
등호를 위한 공리틀은 다음과 같다.
- (E1) \(t=t\)
- (E2) \((t=u)\to(u=t)\)
- (E3) \((t=u)\to((u=v)\to(t=v))\)
- (E4) \((t=u)\to(\phi[t/x]\to\phi[u/x])\), 단 \(t,u\)는 모두 \(\phi\)에서 \(x\)에 대해 자유롭게 대입 가능하다.
(E4)는 같은 대상을 논리식 안에서 서로 바꾸어도 진릿값이 변하지 않는다는 등호의 치환 원리를 나타낸다.
추론규칙은 다음 두 가지이다.
- (R1) MP: \(\phi\)와 \(\phi\to\psi\)로부터 \(\psi\)를 추론한다.
- (R2) 전칭 일반화: \(\phi\)로부터 \((\forall x)\phi\)를 추론한다.
문장들의 집합 \(\varSigma\)에서 출발하여 위 공리틀과 추론규칙을 사용하여 논리식 \(\phi\)를 증명할 수 있으면 \[ \varSigma\vdash\phi \] 라고 쓴다.
문제 16.1. 상수기호 \(c\), 1항 관계기호 \(P\), \(Q\), 2항 관계기호 \(R\)이 있다고 하자. 다음 논리식이 (A4) 또는 (A5)로부터 곧바로 얻을 수 있는 식인지 판정하시오. 올바르지 않으면 어느 부가조건이 실패하는지 설명하시오.
- \((\forall x)P(x)\to P(c)\).
- \((\forall x)(\exists y)R(x,y)\to(\exists y)R(y,y)\).
- \((\forall x)(P(y)\to Q(x))\to(P(y)\to(\forall x)Q(x))\).
- \((\forall x)(P(x)\to Q(x))\to(P(x)\to(\forall x)Q(x))\).
(2)에서 단순한 기호 치환이 변수 포획을 일으키는 과정을 구체적으로 설명하시오.
정의 16.1. (일계논리의 무모순성)
문장들의 집합 \(\varSigma\)에 대해 어떤 문장 \(\phi\)도 \[ \varSigma\vdash\phi \quad\text{와}\quad \varSigma\vdash\neg\phi \] 를 동시에 만족시키지 않으면 \(\varSigma\)가 무모순(consistent)이라고 한다.
문제 16.2. \[ \varSigma=\{(\forall x)(P(x)\to Q(x)),\;(\forall x)P(x)\} \] 라고 하자. (A4), MP, 전칭 일반화만을 사용하여 \[ \varSigma\vdash(\forall x)Q(x) \] 임을 보이시오. 증명의 각 줄에서 어떤 공리틀 또는 추론규칙을 사용했는지 표시하시오.
문제 16.3. \(a,b,c\)가 상수기호이고 \(R\)이 2항 관계기호라고 하자. 등호 공리틀을 사용하여 다음을 형식적으로 유도하시오.
- \(a=b\vdash b=a\).
- \(a=b,\;b=c\vdash a=c\).
- \(a=b,\;R(a,c)\vdash R(b,c)\).
(3)에서는 (E4)에 사용할 논리식 \(\phi(x)\)를 명시하시오.
다음 추론 정리는 명제논리의 추론 정리와 같은 역할을 한다.
정리 16.2. (일계논리의 추론 정리)
\(\varSigma\)가 문장들의 집합이고 \(\sigma\)가 문장이면 \[ \varSigma\cup\{\sigma\}\vdash\phi \quad\Longrightarrow\quad \varSigma\vdash\sigma\to\phi. \]
증명 증명 길이에 대한 수학적 귀납법을 사용한다. 공리, \(\varSigma\)의 원소, 가정 \(\sigma\), MP 단계는 명제논리의 추론 정리와 같다. 남은 것은 전칭 일반화 단계이다. \(\phi=(\forall x)\psi\)가 \(\psi\)에서 일반화되어 얻어졌다고 하자. 귀납가정에 의하여 \[ \varSigma\vdash\sigma\to\psi. \] 전칭 일반화를 적용하면 \[ \varSigma\vdash(\forall x)(\sigma\to\psi). \] \(\sigma\)는 문장이므로 \(x\)가 \(\sigma\)에서 자유롭게 나타나지 않는다. 따라서 (A5)와 MP를 적용하여 \[ \varSigma\vdash\sigma\to(\forall x)\psi \] 를 얻는다.
정리 16.3. (건전성 정리)
\(\varSigma\)가 문장들의 집합이고 \(\phi\)가 문장일 때 \[ \varSigma\vdash\phi \quad\Longrightarrow\quad \varSigma\models\phi. \] 특히 \(\vdash\phi\)이면 \(\models\phi\)이다.
증명 \(\mathcal M\models\varSigma\)라고 하고, 증명 길이에 대한 수학적 귀납법을 사용하여 증명의 각 논리식이 \(\mathcal M\)에서 임의의 변수 값매김 아래 참임을 증명한다. (A1)–(A3)은 명제논리의 항진식이다. (A4)는 치환의 의미와 “자유롭게 대입 가능” 조건으로부터 참이고, (A5)는 \(x\)가 \(\phi\)에서 자유롭지 않다는 조건 때문에 참이다. (E1)–(E4)는 실제 동일성의 성질과 보조정리 15.4의 치환 보조정리에 의하여 유도된다. \(\varSigma\)의 원소는 문장이므로 \(\mathcal M\models\varSigma\)에 의해 모든 값매김에서 참이다.
MP가 참을 보존하는 것은 함의의 의미에서 바로 유도된다. 전칭 일반화의 경우 귀납가정은 \(\phi\)가 \(\mathcal M\)에서 모든 값매김 아래 참이라는 뜻이다. 따라서 임의의 값매김 \(s\)와 임의의 \(a\in M\)에 대해 \[ \mathcal M,s[x\mapsto a]\models\phi \] 이고, 곧 \[ \mathcal M,s\models(\forall x)\phi \] 이다. 마지막 논리식 \(\phi\)가 문장이므로 \(\mathcal M\models\phi\)를 얻는다.
문제 16.4. 건전성 정리를 사용하여 다음을 보이시오.
- \(\nvdash(\exists x)P(x)\to(\forall x)P(x)\).
- \(\{(\forall x)P(x)\}\nvdash(\exists x)\neg P(x)\).
각 경우에 두 원소 이하의 영역을 갖는 반례 구조를 직접 제시하시오.
다음으로 일계논리의 완전성을 살펴보자. 완전성의 핵심은 반대 방향, 즉 무모순인 문장 집합에서 실제 모형을 만드는 일이다. 먼저 새 상수를 도입하는 단계가 무모순성을 보존함을 확인한다.
보조정리 16.4. (새 상수 보조정리)
\(\varSigma\)가 무모순인 문장 집합이고 \((\exists x)\phi(x)\)가 문장이며 \(c\)가 \(\varSigma\)와 \((\exists x)\phi(x)\)에 나타나지 않는 새 상수기호라고 하자. 그러면 \[ \varSigma\cup\{(\exists x)\phi(x)\to\phi(c)\} \] 도 무모순이다.
증명 \(H=(\exists x)\phi(x)\to\phi(c)\)라고 하자. \(\varSigma\cup\{H\}\)가 모순적이라고 가정하면 추론 정리와 명제논리의 법칙을 사용하여 \[ \varSigma\vdash\neg H \] 를 얻는다. 따라서 \[ \varSigma\vdash(\exists x)\phi(x), \qquad \varSigma\vdash\neg\phi(c) \] 가 모두 성립한다. 두 번째 증명에서 새 상수 \(c\)를 그 증명에 쓰이지 않은 변수 \(y\)로 일률적으로 바꾸면, \(c\)가 \(\varSigma\)에 나타나지 않으므로 \[ \varSigma\vdash\neg\phi(y) \] 인 증명을 얻는다. 전칭 일반화를 적용하면 \[ \varSigma\vdash(\forall y)\neg\phi(y), \] 즉 변수 이름을 바꾸어 \[ \varSigma\vdash\neg(\exists x)\phi(x) \] 를 얻는다. 이는 \(\varSigma\)의 무모순성에 모순이다.
보조정리 16.5. (헨킨 확장)
\(\mathcal L\)이 가산 언어이고 \(\varSigma\)가 무모순인 \(\mathcal L\)-문장 집합이면, 새로운 상수기호들을 가산 개 추가한 언어 \(\mathcal L^*\)와 다음 성질을 갖는 완전한 무모순 이론 \(T^*\supseteq\varSigma\)가 존재한다.
- 모든 \(\mathcal L^*\)-문장 \(\phi\)에 대해 정확히 하나의 \(\phi,\neg\phi\)가 \(T^*\)에 속한다.
- \((\exists x)\phi(x)\in T^*\)이면 어떤 상수기호 \(c\)가 존재하여 \(\phi(c)\in T^*\)이다.
- \(T^*\)는 연역적으로 닫혀 있다. 즉 \(T^*\vdash\phi\)이면 \(\phi\in T^*\)이다.
증명 개요 먼저 서로 다른 새 상수기호들의 가산 집합 \[ C=\{c_0,c_1,\ldots\} \] 을 준비하고 \(\mathcal L^*=\mathcal L\cup C\)로 둔다. \(\mathcal L^*\)도 가산이므로 그 문장들과 존재문장들을 차례로 나열할 수 있다. 존재문장 \((\exists x)\phi(x)\)를 만날 때마다 그 문장과 현재까지의 구성에 나타나지 않은 상수 \(c\in C\)를 하나 골라 \[ (\exists x)\phi(x)\to\phi(c) \] 를 추가한다. 보조정리 16.4에 의해 이러한 헨킨 문장을 추가해도 무모순성이 보존된다. 그 뒤 각 문장 \(\theta\)에 대해 \(\theta\) 또는 \(\neg\theta\) 가운데 무모순성을 보존하는 하나를 차례로 추가한다. 유한한 증명은 어떤 유한 단계에 이미 포함되므로 전체 합집합도 무모순이다. 마지막으로 그 연역적 폐포를 취하면 원하는 \(T^*\)를 얻는다.
보조정리 16.6. (항 모형)
보조정리 16.5의 \(T^*\)는 모형을 가진다.
증명 닫힌항들의 집합에서 \[ t\sim u \quad\Longleftrightarrow\quad T^*\vdash t=u \] 로 정의한다. 필요하면 새 상수 하나를 더하여 닫힌항(closed term)이 적어도 하나 존재하게 한다. (E1)–(E3)에 의해 위 관계는 동치관계이다. \([t]\)를 \(t\)의 동치류라고 하고, 이 동치류들의 집합을 영역으로 삼는다.
함수기호와 관계기호를 \[ \begin{gathered} f^{\mathcal M}([t_1],\ldots,[t_n]) =[f(t_1,\ldots,t_n)],\\[3pt] ([t_1],\ldots,[t_n])\in R^{\mathcal M} \quad\Longleftrightarrow\quad R(t_1,\ldots,t_n)\in T^* \end{gathered} \] 로 해석하고 \(c^{\mathcal M}=\)로 둔다. (E4)에 의해 대표원을 바꾸어도 결과가 변하지 않으므로 이 정의들은 잘 정의되어 있다.
논리식의 구조에 대한 귀납법을 사용하여 다음 진리 보조정리를 얻는다. \(\phi\)의 자유변수가 \(x_1,\ldots,x_n\) 가운데에 있고 \(t_1,\ldots,t_n\)이 닫힌항이라고 하자. \(s(x_i)=[t_i]\)가 되도록 값매김 \(s\)를 잡으면 \[ \mathcal M,s\models\phi \quad\Longleftrightarrow\quad \phi[t_1/x_1,\ldots,t_n/x_n]\in T^*. \] 아톰논리식과 결합자 단계는 정의와 \(T^*\)의 완전성에서 따른다.
전칭 한정기호 단계에서 \((\forall x)\psi\in T^*\)이면 (A4)에 의해 모든 닫힌항 \(t\)에 대해 \(\psi[t/x]\in T^*\)이다. 반대로 \((\forall x)\psi\notin T^*\)이면 \(T^*\)의 완전성에 의하여 \[ \neg(\forall x)\psi\in T^* \] 이다. 고전 명제논리의 이중부정 법칙과 한정기호 규칙에 의하여 \[ \neg(\forall x)\psi\leftrightarrow(\exists x)\neg\psi \] 가 증명 가능하므로 \[ (\exists x)\neg\psi\in T^* \] 이다. 이제 헨킨 성질에 의하여 적당한 상수 \(c\)에 대하여 \[ \neg\psi\in T^* \] 이다. 따라서 전칭문장은 모형에서도 거짓이다.
특히 모든 \(\sigma\in T^*\)에 대해 \(\mathcal M\models\sigma\)이다. 따라서 \(\mathcal M\models T^*\), 나아가 \(\mathcal M\models\varSigma\)이다.
문제 16.5. 언어 \(\mathcal L^*\)에 상수기호 \(c,d\), 1항 함수기호 \(f\), 1항 관계기호 \(P\)가 있다고 하자. 완전한 헨킨 이론 \(T^*\)가 \[ T^*\vdash c=d, \qquad T^*\vdash f(c)=d, \qquad P(c)\in T^* \] 를 만족시킨다고 하자. 보조정리 16.6의 항 모형 \(\mathcal M\)에서 다음을 보이시오.
- \( [ c ] = [ d ] \).
- \(f^{\mathcal M}( [ c ] ) = [ c ]\).
- \( [ c ] \in P^{\mathcal M}\).
- 일반적으로 \( [ t ] = [ u ] \)이면 \[ P(t)\in T^* \quad\Longleftrightarrow\quad P(u)\in T^* \] 임을 (E2), (E4), \(T^*\)의 연역적 닫힘을 사용하여 설명하시오. 이것이 관계기호의 해석이 대표원의 선택과 무관함을 어떻게 보장하는지도 설명하시오.
정리 16.7. (완전성 정리)
\(\mathcal L\)이 가산 일계논리언어이고 \(\varSigma\)가 \(\mathcal L\)-문장들의 집합, \(\phi\)가 \(\mathcal L\)-문장이면 \[ \varSigma\models\phi \quad\Longrightarrow\quad \varSigma\vdash\phi. \] 따라서 \[ \varSigma\models\phi \quad\Longleftrightarrow\quad \varSigma\vdash\phi. \]
증명 대우를 보인다. \(\varSigma\nvdash\phi\)라고 하자. 만약 \[ \varSigma\cup\{\neg\phi\} \] 가 모순적이면 추론 정리와 고전 명제논리의 법칙을 이용하여 \(\varSigma\vdash\phi\)를 얻으므로 모순이다. 따라서 \(\varSigma\cup\{\neg\phi\}\)는 무모순이다. 보조정리 16.5와 16.6에 의해 이를 만족시키는 구조 \(\mathcal M\)이 존재한다. 그러면 \[ \mathcal M\models\varSigma, \qquad \mathcal M\not\models\phi, \] 이므로 \(\varSigma\not\models\phi\)이다.
건전성과 완전성을 합치면 일계논리에서 의미론적 귀결과 형식적 증명 가능성이 정확히 일치한다. 특히 문장 집합은 만족 가능할 필요충분조건에 의하여 무모순이다.