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 SaSoundness . 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