Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK

Abstract

We give a self-contained development of the first-order block calculus in unsigned sequent-style notation: each node of the refutation tree carries a finite block $Π= Γ\cup \neg[Δ]$, negation is governed by explicit rules, and a branch closes on a complementary pair of literals. The calculus is Smullyan's, and so in substance are the theorems; what is offered here is a different arrangement of them. The structural properties are established in the order of dependence familiar from G3-style sequent calculi: closure on arbitrary formulae is admissible, weakening and the substitution of parameters are admissible with preservation of the height, every rule is height-preserving invertible, and cut is admissible, the last being derived from the first three rather than conversely. Soundness, completeness under a fair strategy, countable compactness and the countable model property follow, together with a syntactic criterion under which every fair construction terminates. The correspondence is then proved, in both directions and with cut included, with Gentzen's LK in its usual presentation with explicit weakening, which requires lemmas on parameters that set-based Gentzen systems do not need.