younghwanjoo1608

ㅎㅇ

6 minute read


Completeness(완전성)와 compactness(콤팩트성)은 논리학이 갖거나 갖지 않는 성질. Propositional logic에 대한 이야기는 이 성질에 대한 것으로 끝!

논리학이란, 한 문장의 참으로부터 다른 문장들을 추론하는 규칙을 갖는 formal language. 만일 문장 $G$가 문장들의 set $\mathcal{F}$로부터 이러한 규칙들에 의해 추론된다면 $\mathcal{F} \vdash G$라고 쓴다. 반면 $\mathcal{F} \models G$는 $\mathcal{F}$의 각 문장들이 참일 때마다 $G$ 또한 참이 된다는 의미. $\mathcal{F} \vdash G$이면, $\mathcal{F} \models G$이다. 그러나 그 역은, 반드시 참일 필요가 없다.


달리 말하면,
$\mathcal{F} \models G$는 $\mathcal{F}$가 $G$를 함의한다는 뜻.
$\mathcal{F} \vdash G$는 우리가 $\mathcal{F}$가 $G$를 함의한다는 것을 논리 규칙을 통해 증명할 수 있다는 뜻.
그러나 무언가가 참이라는 것이 우리가 이를 증명할 수 있다는 이유가 되지는 않는다. 모든 걸 증명하기엔 논리 규칙이 너무 약할 수도 있다.


만일 참인 모든 것을 증명할 수 있다면($\mathcal{F} \models G \rightarrow \mathcal{F} \vdash G$라면), 우리는 그 논리가 complete하다고 말한다.

(Completeness) $\mathcal{F} \models G$ iff $\mathcal{F} \vdash G$


Sec. 1.4에서 우리는 notation $\mathcal{F} \vdash G$를 규칙들의 목록으로 이루어진 propositional logic을 통해 정의했다. 그러나 completeness는 이러한 특정 규칙에 대한 서술이 아닌 논리 그 자체에 대한 서술로써 받아들여야 한다.


Completeness는 임의의 formula들의 set으로부터 모든 consequence들을 추론해내는 규칙 목록이 존재한다고 주장한다. 그런 목록이 있다는 걸 보여주면 이를 증명할 수 있다. Sec. 1.4의 table들과 resolution만으로 propositional logic은 충분하다.

Propositional logic의 completeness를 증명하기 위해, formula들의 set을 infinite set으로 확장해야 한다. $\mathcal{F}$가 finite이면 Thm. 1.8.11만으로 충분. 이제 $\mathcal{F}$가 infinite이라고 하자. $\mathcal{F}$가 CNF formula들의 set이라면, $\mathcal{F}$를 clause들의 set으로 볼 수 있다.


Set $Res^{n}(\mathcal{F})$은 clause들의 finite set으로써 정의되었다. $Res^{\ast}(\mathcal{F})$를 모든 $Res^{n}(\mathcal{F})$들의 union으로 나타내자.(단, $n \in \mathbb{N}$) $Res^{\ast}(\mathcal{F})$는 $\mathcal{F}$로부터 resolution에 의해 도출되는 모든 clause들의 set이다.

만약 $\mathcal{F}$가 infinite이면, $Res^{\ast}(\mathcal{F})$도 infinite이고, formula의 형태로 볼 수 없게 된다.
[그러한 모든 clause들의 infinite set이 satisfiable] iff [Set의 각 clause들을 model하는 assignment가 존재]


따라서, 다음을 보이면 충분하다.


Proposition 1.9.1

$\mathcal{F}$가 CNF formula들의 set이라고 하자. 그러면,

\[ \varnothing \in Res^{\ast}(\mathcal{F}) \textrm{ iff } \mathcal{F} \textrm{ is unsatisfiable.} \]


Finite $\mathcal{F}$에 대해 이는 Prop. 1.8.7과 Prop. 1.8.9를 다시 쓴 것일 뿐. 이들의 증명을 다시 읽어보자.

Prop. 1.8.9에서 $F$가 unsatisfiable이라고 가정했고, 이때 $\varnothing \in Res^{\ast}(F)$임을 $F$에 등장하는 atomic formula의 수 $n$에 대한 induction으로 보였다. 그러나 mathematical induction은 오직 모든 finite $n$에 대해서 증명할 뿐. $\mathcal{F}$가 무한히 많은 atomic formula를 갖는다면, Prop. 1.8.9와 같은 방법은 쓸 수 없다!


반대 방향을 생각하자. $\varnothing \in Res^{\ast}(\mathcal{F})$이면, 어떤 $n$에 대해 $\varnothing \in Res^{n}(\mathcal{F})$이다. 즉 우리는 $\mathcal{F}$로부터 유한한 단계를 거쳐 $\varnothing$을 도출할 수 있다. 그러므로, $\mathcal{F}$의 어떤 finite subset $F$로부터 $\varnothing$가 도출된다. 이제 Prop. 1.8.7로부터 $F$는 unsatisfiable. $F$가 $\mathcal{F}$의 subset이므로, $\mathcal{F}$ 역시 unsatisfiable이어야 한다.

따라서, Prop. 1.9.1의 한쪽 방향은 이전 Sec.의 결과. 유한한 case로부터 무한한 case를 추론해낼 수 있었다. 원래 방향도 유사한 idea가 필요. $\mathcal{F}$가 unsatisfiable이면, $\mathcal{F}$의 어떤 finite subset이 unsatisfiable이어야 한다. 이것이 바로 compactness!

(Compactness) $\mathcal{F}$ is unsatisfiable iff some finite subset of $\mathcal{F}$ is unsatisfiable.


달리 말하면, compactness는 [$\mathcal{F}$가 satisfiable] iff [$\mathcal{F}$의 모든 finite subset이 satisfiable]이라고 말한다. completeness에서처럼, compactness의 한쪽 방향은 언제나 성립. 만약 $\mathcal{F}$이 satisfiable이면, $\mathcal{F}$의 모든 finite subset 또한 satisfiable. 그러나 그 역이 항상 성립할 이유는 없다. 다음 문장을 생각해 보자.

$F_{0}=``\textrm{There are finitely many objects in the universe.}”$
$F_{1}=``\textrm{There is at least one object in the universe.}”$
$F_{2}=``\textrm{There are at least two objects in the universe.}”$
$F_{3}=``\textrm{There are at least three objects in the universe.}”$
$\cdots$
$F_{n}=``\textrm{There are at least n objects in the universe.}”$
$\cdots$


이들을 모두 취하게 되면 모순적인 문장이 만들어진다. 각 $n$에 대해 $n$보다 많은 수의 object들이 존재한다면, $F_{0}$가 말하는 것처럼 유한히 많은 object들이 존재할 수 없게 된다. 그러나 위 문장 중 유한한 갯수만큼을 취한다면 아무런 문제가 없다. 위 문장들의 임의의 finite subset은 satisfiable이나, 전체 collection은 그렇지 않다.

Propositional logic의 compactness를 보이기 위해, 먼저 lemma가 필요.


Lemma 1.9.2

$X$를 finite binary string들의 infinite set이라고 하자.
그러면 어떤 infinite binary string $\bar{w}$가 존재하여 $\bar{w}$의 임의의 prefix가 또한 $X$의 무한히 많은 $\bar{x}$들의 prefix가 된다.


Proof.


Binary string(이진 문자열)이란 $0$과 $1$로 이루어진 수열을 말한다. String $1$, $10$, $101$, $1011$은 $1011$의 prefix(전위)가 된다.

유한한 길이의 string들을 갖는 infinite set $X$가 존재한다. $0$과 $1$로 이루어진 infinite string $\bar{w}$를 구성하고자 한다. 이때 $\bar{w}$의 prefix는 $X$에 존재하는 무한히 많은 string들의 prefix이기도 해야 한다.


$\bar{w}$를 왼쪽부터 단계별로 구성한다. 각 단계마다 우리는 두 가지 할 일이 있다. $n$-번째 step에서, $\bar{w}$의 $n$-번째 자리가 무엇인지 결정하고 이와 다른 것을 $X$에서 지워나가야 한다.

$\bar{w}$의 첫 번째 자리를 결정하기 위해 $X$의 모든 string들의 첫 번째 자리들을 보자. 두 가지 가능성이 존재한다. $1$이 무한히 많이 존재하거나, 그렇지 않거나. 만약 $1$로 시작하는 $X$의 string들이 무한히 많다면, $\bar{w}$의 첫 자리를 $1$로 하고, $0$으로 시작하는 $X$의 string들은 전부 삭제한다. 만약 $1$로 시작하는 $X$의 string들이 무한히 많다면, 이들을 모두 지우고 $\bar{w}$의 첫 번째 자리를 $0$으로 결정.


이제 $\bar{w}$의 첫 $n$-개 자리가 결정되었다고 하자. 또한 $X$에서 $\bar{w}$와 같은 $n$-개 자리로 시작하지 않는 string들은 모두 삭제되고 infinite set $X’$가 남았다고 하자. $\bar{w}$의 ($n+1$)-번째 entry를 구하기 위해 $X’$의 ($n+1$)-번째 자리를 보자. 현재 $X’$에는 길이가 $n+1$보다 같거나 긴 string들이 무한히 많이 존재. 다시 두 가지 가능성이 존재. $1$로 시작하는 $X’$의 string들이 무한히 많다면 $\bar{w}$의 ($n+1)-번째 자리를 $1$로 결정하고….

이 과정을 계속하면 무한한 수열 $\bar{w}$와, $\bar{w}$와 처음 $n$-자리가 같은 $X$의 무한히 많은 수열들을 얻을 수 있다. $\bar{w}$를 현실적으로 구성할 수는 없으나, $\bar{w}$의 존재성은 보였다! $\square$


Theorem 1.9.3 [Compactness of Propositional Logic]

[Propositional logic의 sentece들의 set이 satisfiable] iff [모든 finite subset이 satisfiable]


Proof.


이전에 언급한 대로 $[\Leftarrow]$ 방향만 보이면 충분. $\mathcal{F}= \{F_{1}, F_{2}, \dots \}$를 formlua의 set이라 하고, $\mathcal{F}$의 모든 finite subset이 satisfiable이라고 하자.

$F_{1}$에 등장하는 atomic formula 중에서, $F_{2}$에 등장하는(그러나 $F_{1}$에는 등장하지 않는) atomic formula들 뒤에 등장하는 것들의 set을 $A_{1}$이라고 하자. 마찬가지로 $F_{2}$에 등장하는 atomic formula 중에서, $F_{3}$에 뒤따라 등장하는 것들의 set을 $A_{2}$라고 하고…. 이렇게 반복 없이 list $A_{1}, A_{2}, \dots$가 있다고 하자.

$\mathcal{F}$의 모든 finite subset들이 satisfiable이므로, 각 $n$에 대해 어떤 assignment $\mathcal{A}_{n}$이 존재해서 $\mathcal{A}_{n} \models \bigwedge_{i=1}^{n} F_{i}$이다. 따라서 $\mathcal{F}$의 각 $F_{i}$는 이러한 모든 유한한 수의 assignment들에서 성립한다(즉, $F_{m}$은 $\mathcal{A}_{1}, \dots , \mathcal{A}_{m}$에서 성립). 우리는 $\mathcal{A}_{n}$을 오직 $\{F_{1}, \dots, F_{n} \}$에서 나타나는 atomic formula들에 대해서만 정의된다고 가정할 수 있다. 각 $n$에 대해, $A_{1}, A_{2}, \dots$에 할당되는 $\mathcal{A}_{n}$의 진릿값은 $0$과 $1$로 이루어진 finite sequence라고 할 수 있다. 따라서 $X=\{ \mathcal{A}_{n} | n=1,2,\dots \}$는 finite binary sequence들의 infinite set이 된다. Lm.1.9.2에 의해, infinite binary sequence $\bar{w}$가 존재해, $\bar{w}$의 모든 prefix들이 $X$에 존재하는 무한히 많은 sequence들의 prefix가 된다.


모든 $A_{n}$에 대해 assignment $\mathcal{A}$를 다음과 같이 정의: $\mathcal{A}(A_{n})$은 $\bar{w}$의 $n$-번째 자릿수.
$\mathcal{F}$의 모든 formula $F$가 $\mathcal{A}$ 아래에서 성립함을 보여야 한다. $F$가 $X$에 존재하는 모든 유한한 숫자의 assignment 아래에서 성립하므로 이는 당연.

자연수 $m$이 존재해서, 우리 list에서 $A_{m}$을 지나면 $F$가 더 이상 atomic formula를 포함하지 않게 된다. 그러면 $\mathcal{A}_{n} \models F$를 만족하는 $\mathcal{A}_{n} \in X$가 존재하고, $\mathcal{A}_{n}$의 첫 $m$개 entry들은 $\mathcal{A}$와 같게 된다. 이로써 $\mathcal{A} \models F$. $\square$


Compactness로부터 Prop. 1.9.1이 나온다. 이제 propositional logic의 completeness를 증명할 수 있다. Thm. 1.8.11의 증명에서 Prop. 1.8.7과 Prop. 1.8.9를 Prop. 1.9.1로 대체하면 그만.

그러나, 여기 더 직접적인 증명이 있다.


Theorem 1.9.4 [Completeness of Propositional Logic]

임의의 sentence $G$와 sentence들의 set $\mathcal{F}$에 대해, $\mathcal{F} \models G \textrm{ iff } \mathcal{F} \vdash G$


Proof.


$[\Leftarrow]$ Thm. 1.4.9.

$[\Rightarrow]$ $\mathcal{F} \models G$를 가정. 그러면 $\mathcal{F} \cup \{ \neg G\}$는 unsatisfiable이다. compactness에 의해, $\mathcal{F} \cup \{ \neg G\}$의 어떤 finite subset 역시 unsatisfiable. 따라서 어떤 finite $\mathcal{F}_{0} \subset \mathcal{F}$가 존재해, $\mathcal{F}_{0} \cup \{ \neg G\}$가 unsatisfiable이고, $\mathcal{F}_{0} \models G$를 얻는다. $\mathcal{F}_{0}$가 finite이므로, Thm. 1.8.11을 적용해 $\mathcal{F}_{0} \vdash G$를 얻는다. 끝으로 monotonicity에 의해 $\mathcal{F} \vdash G$. $\square$


  1. [Thm. 1.4.9](http://younghwanjoo1608.github.io/logics/prl1.4/#theorem-149) 참조. ↩

  2. Second-order logic에서는 completeness가 성립하지 않음을 Ch. 9에서 확인할 수 있다. 이차 논리 문장들의 set으로부터 나오는 모든 consequence들을 추론해내는 멋진 규칙 list를 우리는 제시할 수 없다! ↩

  3. 그래도 여전히 $X$에는 무한히 많은 string들이 존재. ↩

  4. 물론 무한히 많은 string들이 있기에 모든 자리들을 한 번에 볼 수는 없지만, 전지적 시점으로 볼 수 있다고 하자. ↩

  5. 즉, 우리는 disjoint한 atomic formula들의 set을 만들고자 한다. ↩

You may also enjoy