define a deduction from a set of wffs $\Sigma$ to be finite sequence $<a_0,a_1, \ldots, a_n>$ of wffs such satisfying either (i), (ii), (iii) for each $k \leq n$.

(i) $a_k$ is a tautology

(ii) $a_k \in \Sigma$

(iii) for some $i, j < k$, $a_i=a_j \rightarrow a_k$. this is the inference rule for PL, we'll use, named Modus Ponens.

 

if there exists a deduction ends with $\varphi$ from $\Sigma$, we'll symbolize this as $\Sigma \vdash \varphi$.

 

Soundness theorem : $\Sigma \vdash \tau \rightarrow \Sigma \models \tau$.

 

Proof : let $\Sigma \vdash \tau$. then there exists a deduction sequence from $\Sigma$ such that $<a_0,a_1, \ldots, a_n>$ which ends with $\tau$.

 

we'll use induction for all $k<i$. give inductive hypothesis that for all $i<k$,  $\Sigma \models a_k$. then by showing $\Sigma \models a_i$, our proof will be over.

 

since $a_k$ an element of deduction sequence, $a_k$ must satisfy one of (i), (ii), (iii). now check each case.

 

case 1 : $a_k$ is a tautology. then $\models a_k$. trivially $\Sigma \models a_k$ since tautology cannot be false in any case.

 

case 2 : $a_k \in \Sigma$. this case is also trivial. by definition, if $\Sigma$ is satisfied, clearly the member $a_k$ is true. thus $\Sigma \models a_k$.

 

case 3 : $a_k$ is obtained by some priorly made elements of deduction sequence $a_i$ and $a_j=(a_i \rightarrow a_k)$. and by inductive hypothesis, $\Sigma \models a_i$ and $\Sigma \models a_j$

 

consider any truth assignemnt for $\Sigma$ which is satisfied. then by hypothesis, we get $\bar{v}(a_i)=T$ and $\bar{v}(a_i \rightarrow a_k)=T$. let $\bar{v}(a_k)=F$. then since $\bar{v}(a_i)=T$ and $\bar{v}(a_k)=F$, we must get $\bar{v}(a_i \rightarrow a_K)=F$ which is contradicton. thus $\bar{v}(a_k)=T$. now $\Sigma \models a_k$.

 

all case is satisfied. now by strong mathematical induction, $\Sigma \models a_k$ for all $a_k$ of deduction sequence for $\tau$. hence, the last element $a_n=\tau$ is also satisfied. therefore, $\Sigma \models \tau$.

 

 

 

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

FOL(2) - semantics  (2) 2015.02.10
completeness theorem for PL  (2) 2015.02.07
First-Order Logic(1)  (3) 2015.02.01
induction for FOL  (0) 2015.01.30
compactness theorem for PL(3)  (0) 2015.01.23
Posted by 괴델
,