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 $\Pi = \Gamma \cup \neg[\Delta]$, 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.
Sequent-style tableaux are a refutation calculus in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. In their original, classical form they rest on an involutive De Morgan negation and on closure upon a complementary pair. We show that both may be dispensed with. Replacing unsigned formulae by signed ones, we obtain a block calculus $\mathbf{B}_{ti}$ for intuitionistic propositional logic in which the whole of intuitionism is carried by one rule, the rule decomposing $\mathsf{F}(A \to B)$, which deletes the $\mathsf{F}$-part of the context on passing to the child block. The rules so obtained are, up to the presentation, those of Fitting's signed tableaux; what is new is the block format, in which the structural rules are absorbed rather than admissible, and what follows from it. We identify the semantic reason for this rule and for the one other anomalous one: of the signed compounds of the language, exactly those governed by the implication fail to be locally decomposable, and the two failures are repaired, respectively, by retaining the principal formula and by purging the context. We prove that $\mathbf{B}_{ti}$ is the multiple-succedent sequent calculus $\mathbf{G}_{ti}$ read upside down, that $\mathbf{G}_{ti}$ admits the structural rules, and that $\mathbf{B}_{ti}$ is sound and complete for Kripke semantics, with the finite model property and a block-theoretic proof of the disjunction property.
