Discrete mathematics Yi Li Software school Fudan universit June4,2013
. . Discrete Mathematics Yi Li Software School Fudan University June 4, 2013 Yi Li (Fudan University) Discrete Mathematics June 4, 2013 1 / 17
Review o Tableau proof o Complete systematic tableaux
Review Tableau Proof Complete Systematic Tableaux Yi Li (Fudan University) Discrete Mathematics June 4, 2013 2 / 17
utline o Soundness Completeness o Compactness
Outline Soundness Completeness Compactness Yi Li (Fudan University) Discrete Mathematics June 4, 2013 3 / 17
Tableau proof amp dle Consider a sentence GyR(, y)v P(, y))A(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 4, 2013 4 / 17
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 SUnna 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 Sa
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 4, 2013 5 / 17
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 4, 2013 6 / 17
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 4, 2013 7 / 17
Property of CST oposItion 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 4, 2013 8 / 17
Property of CST orollar For 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 4, 2013 9 / 17
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 4, 2013 10 / 17