Completeness( Cont. Theorem(Completeness If a is valid, then a is tableau provable, i.e. Fa=ha In fact, any finished tableau with root entry Fa is a proof of a and so, in particular, the complete systematic tableaux with root Fa is such a proof.Completeness(Cont.) . Theorem (Completeness) . . If α is valid, then α is tableau provable, i.e. ⊨ α ⇒⊢ α. In fact, any finished tableau with root entry Fα is a proof of α and so, in particular, the complete systematic tableaux with root Fα is such a proof. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 13 / 17