Soundness( Cont Theorem(Soundness) If a is tableau provable, then a is valid, i.e. Fa=FaSoundness(Cont.) . Theorem (Soundness) . . If α is tableau provable, then α is valid, i.e. ⊢ α ⇒⊨ α. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 10 / 17