we proved compactness theorem. now introduce corollary to it.

 

theorem : If $\Sigma \models \tau$, then there is a finite $\Sigma_0 \subseteq \Sigma$ such that $\Sigma_0 \models \tau$.

 

use the fact(*) $\Sigma \models \tau$ iff $\Sigma;(\neg \tau)$ is unsatisfiable.

 

proof for (*).

 

$(\rightarrow)$. let $\Sigma \models\tau$ and $\Sigma; (\neg \tau)$ be satisfiable. by definition, every truth assignment must meet $\bar{v}(\Sigma)=\{T\} \rightarrow \bar{v}(\tau)=T$. but there exist truth assignment which meets $\bar{v}(\Sigma)={T} \wedge \bar{v}(\neg \tau)=T$ which is contraction. thus rightarrow conditional is proved.

 

$(\leftarrow)$. let $\Sigma;(\neg \tau)$ is unsatisfiable and $\Sigma \models\tau$. then truth assignment such that $\bar{v}(\Sigma)={T} \wedge \bar{v}(\neg \tau)=\{T\}$ cannot exist. but since $\Sigma \models\tau$, there exist some truth assignmnet $v$ such that $\bar{v}(\Sigma)=\{T\} \wedge \bar{v}(\tau)=F$ which is contradiction. thus leftarrow conditional is proved.

 

using (*), prove corollary. suppose corollary is false.

 

then $\Sigma_0 \models \tau$ for all finite $\Sigma_0 \subseteq \Sigma$.

$\Rightarrow$ $\Sigma_0;(\neg \tau)$ is satisfiable for all finite $\Sigma_0 \subseteq \Sigma$.

$\Rightarrow$ $\Sigma$ is finitely satisfiable(since $\Sigma_0 \subseteq \Sigma_0;(\neg \tau)$ is finite thus satisfiable).

 

now consider $\bar{\Sigma} \subseteq \Sigma;(\neg \tau)$ which is finite. if $(\neg \tau) \notin \bar{\Sigma}$, then $\bar{\Sigma}=\Sigma_i$ where $\Sigma_i \subseteq \Sigma$. since $\Sigma$ is finitely satisfiable, so is $\bar{\Sigma}$. if $(\neg \tau) \in \bar{\Sigma}$, $\bar{\Sigma}=\Sigma_j;\neg \tau$ where $\Sigma_j \subseteq \Sigma$. thus $\bar{\Sigma}$ is satisfiable.

 

$\Rightarrow$ $\Sigma;(\neg \tau)$ is finitely satisfiable.

$\Rightarrow$ $\Sigma;(\neg \tau)$ is satisfiable.

$\Rightarrow$ $\Sigma \models \tau$

 

this derives contraction.

 

thus corollary is proved.

 

 

 

 

'학문 > 수리논리학' 카테고리의 다른 글

induction for FOL  (0) 2015.01.30
compactness theorem for PL(3)  (0) 2015.01.23
compactness theorem for PL(1)  (0) 2015.01.23
recursion theorem  (1) 2015.01.21
Propositional Logic(2)  (0) 2015.01.18
Posted by 괴델
,