Sequent-style tableaux for intuitionistic propositional logic

Abstract

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.