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 k≤n.
(i) ak is a tautology
(ii) ak∈Σ
(iii) for some i,j<k, ai=aj→ak. 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=(ai→ak). 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(ai→ak)=T. let ˉv(ak)=F. then since ˉv(ai)=T and ˉv(ak)=F, we must get ˉv(ai→aK)=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 |