soundness theorem(a) : $\Gamma \vdash \varphi \rightarrow \Gamma \models \varphi$.

 

soundness theorem(b) : if $\Gamma$ is satisfiable, then $\Gamma$ is consistent.

 

(a) and (b) are equivalent. we'll prove this.

 

first, give definition.

 

Define $\Gamma$ to be satisfiable iff there is some $\mathfrak{A}$ and $s$ such that $\mathfrak{A}$ satisfies every member of $\Gamma$ with $s$.

 

 

proof

 

$((a) \rightarrow (b))$. suppose (a) holds and (b) does not. then we get $\Gamma$ is satisfiable, but $\Gamma$ is inconsistent. then by definition of inconsistent, we get $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$. then by (a), we get $\Gamma \models \varphi$ and $\Gamma \models \neg\varphi$. so we get both $\Gamma \models \varphi$ and $\Gamma \models \varphi$ which is contradiction. thus $(a) \rightarrow (b)$ holds.

 

$((b) \rightarrow (a))$. suppose (b) holds and (a) does not. then $\Gamma \vdash \varphi$ and $\Gamma \not\models \varphi$. since $\Gamma \vdash \varphi$, we get $\Gamma;\neg\varphi$ is inconsistent(see reductio ad absurdum in syntax(2)). then $\Gamma;\neg\varphi$ is unsatisfiable(contraposition of (a)). that is, there does not exist $s$ and $\mathfrak{A}$ such that $\mathfrak{A}$ satisfies every member of $\Gamma;\neg\varphi$ with $s$. so, for all $s$ and $\mathfrak{A}$, $\Gamma$ with $s$ is unsatisfiable or $\not\models_{\mathfrak{A}} \neg\varphi[s]$.

 

now consider $\Gamma \not\models\varphi$. this means, there exist some $\mathfrak{A}$ and $s$ such that $\Gamma$ with $s$ is satisfiable but $\not\models_{\mathfrak{A}} \varphi[s]$. then we get $\models_{\mathfrak{A}} \neg\varphi[s]$. by above fact, we must get $\Gamma$ with $s$ is unsatisfiable which is contradiction.

 

this proves (a) and (b) are equivalent. 

 

 

P.S. 다음 글에서는 completeness theorem을 증명할 생각입니다. completeness and its equivalent theorem~compactness theorem and its equivalence의 증명이 앞으로 고비일 듯 합니다. 그 이후에는 불완전성 정리에 대한 개념 도입 전까지는 증명이 심하게 길지는 않을 듯 싶습니다.

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

FOL(9) - compactness theorem and its equivalnce  (2) 2015.02.13
FOL(7) - completeness and its equivalence  (0) 2015.02.13
FOL(5) - soundness theorem  (1) 2015.02.12
FOL(4) - syntax(2)  (2) 2015.02.12
FOL(3) - syntax(1)  (2) 2015.02.11
Posted by 괴델
,