复旦大学：《离散数学 Discrete Mathematics》英文讲稿_14 Soundness Completeness Compactness

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