A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization

TL;DR

This paper provides the first syntactic proof of soundness for classical tableaux with free variables and on-the-fly Skolemization, connecting tableau methods to sequent calculus and enabling cut elimination results.

Contribution

It introduces a novel syntactic soundness proof for tableaux with Skolemization, bridging semantic and syntactic approaches and facilitating cut elimination theorems.

Findings

Proves syntactic soundness of tableaux with free variables and Skolemization

Establishes a connection to cut-free sequent calculus

Enables potential application to other logics' tableaux

Abstract

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.