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
Completeness 「The eorem Suppose P is a noncontradictory path through a complete systematic tableau T from S with root Fa There is then a structure A in which a is false and every sentence in s is true
Completeness Theorem Suppose P is a noncontradictory path through a complete systematic tableau τ from S with root Fα. There is then a structure A in which α is false and every sentence in S is true. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 6 / 1
Completeness( Cont emma Let the notation be as above o If FB occurs on P, then B is false in A o If TB occurs on P, then B is true in A
Completeness(Cont.) Lemma Let the notation be as above 1 If Fβ occurs on P, then β is false in A. 2 If Tβ occurs on P, then β is true in A. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 7 / 1
Property of CST Proposition If every path of a complete systematic tableau is contradictory, then it is a finite tableau
Property of CST Proposition If every path of a complete systematic tableau is contradictory, then it is a finite tableau. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 8 / 1
Property of CST orollar or every sentence a and set of sentences S of L, either o the CsT from s with root Fa is a tableau proof of a from o there is a noncontradictory branch through the complete systematic tableau that yields a structure in that a is false and every element of s is true
Property of CST Corollary For every sentence α and set of sentences S of L, either 1 the CST from S with root Fα is a tableau proof of α from S. or 2 there is a noncontradictory branch through the complete systematic tableau that yields a structure in that α is false and every element of S is true. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 9 / 1
Completeness and Soundness Theorem(Completeness and Soundness) o a is a tableau provable from S+ a is a logical consequence of s o If we take a to be any contradiction such as B AnB in 1, we see that s is inconsistent if and only if s is unsatisfiable
Completeness and Soundness Theorem (Completeness and Soundness) 1 α is a tableau provable from S ⇔ α is a logical consequence of S. 2 If we take α to be any contradiction such as β ∧ ¬β in 1, we see that S is inconsistent if and only if S is unsatisfiable. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 10 / 1
