Discrete mathematics Yi Li Software school Fudan universit June12,2012
Discrete Mathematics Yi Li Software School Fudan University June 12, 2012 Yi Li (Fudan University) Discrete Mathematics June 12, 2012 1 / 1
Review Tableau proof o Complete systematic tableaux
Review Tableau Proof Complete Systematic Tableaux Yi Li (Fudan University) Discrete Mathematics June 12, 2012 2 / 1
utline Soundness o Completeness o Compactness
Outline Soundness Completeness Compactness Yi Li (Fudan University) Discrete Mathematics June 12, 2012 3 / 1
Tableau proof amp dle Consider a sentence GyR(, y)v P(, y))V(VXR(x,x). There is a model A
Tableau Proof Example Consider a sentence (∃y)(¬R(y, y) ∨ P(y, y)) ∨ (∀x)R(x, x). There is a model A. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 4 / 1
Soundness emma If T= UTn is a tableau from a set of sentences s with root Fa, then any L-structure a that is a model of SUt-naf can be extended to one agreeing with every entry on some path P through T. Recall that A agrees with Ta(Fa) if a is true (false) in A) Theorem(Soundness) If there is a tableau proof r of a from S, then Sha
Soundness Lemma If τ = ∪τn is a tableau from a set of sentences S with root Fα, then any L-structure A that is a model of S ∪ {¬α} can be extended to one agreeing with every entry on some path P through τ .( Recall that A agrees with Tα(Fα) if α is true(false) in A.) Theorem (Soundness) If there is a tableau proof τ of α from S, then S |= α. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 5 / 1