Processing math: 100%


 

 

define a deduction from a set of wffs Σ to be finite sequence <a0,a1,,an> of wffs such satisfying either (i), (ii), (iii) for each kn.

(i) ak is a tautology

(ii) akΣ

(iii) for some i,j<k, ai=ajak. this is the inference rule for PL, we'll use, named Modus Ponens.

 

if there exists a deduction ends with φ from Σ, we'll symbolize this as Σφ.

 

Soundness theorem : ΣτΣτ.

 

Proof : let Στ. then there exists a deduction sequence from Σ such that <a0,a1,,an> which ends with τ.

 

we'll use induction for all k<i. give inductive hypothesis that for all i<kΣak. then by showing Σai, our proof will be over.

 

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

 

case 1 : ak is a tautology. then ak. trivially Σak since tautology cannot be false in any case.

 

case 2 : akΣ. this case is also trivial. by definition, if Σ is satisfied, clearly the member ak is true. thus Σak.

 

case 3 : ak is obtained by some priorly made elements of deduction sequence ai and aj=(aiak). and by inductive hypothesis, Σai and Σaj

 

consider any truth assignemnt for Σ which is satisfied. then by hypothesis, we get ˉv(ai)=T and ˉv(aiak)=T. let ˉv(ak)=F. then since ˉv(ai)=T and ˉv(ak)=F, we must get ˉv(aiaK)=F which is contradicton. thus ˉv(ak)=T. now Σak.

 

all case is satisfied. now by strong mathematical induction, Σak for all ak of deduction sequence for τ. hence, the last element an=τ is also satisfied. therefore, Στ.

 

 

 

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

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 괴델
,