  We prove the syntactic soundness of classical tableaux with free variables
and on-the-fly Skolemization. Soundness proofs are usually built from semantic
arguments, and this is to our knowledge, the first proof that appeals to
syntactic means. We actually prove the soundness property with respect to
cut-free sequent calculus. This requires great care because of the additional
liberty in freshness checking allowed by the use of Skolem terms. In contrast
to semantic soundness, we gain the possibility to state a cut elimination
theorem for sequent calculus, under the proviso that completeness of the method
holds. We believe that such techniques can be applied to tableaux in other
logics as well.
