{"id":"arxiv/2607.28555","url":"https://arxiv.org/abs/2607.28555","tags":["math.LO"],"score":0,"title":"Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK","domain":"math.LO","source":"arxiv","authors":["Simone Cuconato"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-30","reactions":{}}