arXiv subjects

Simone Cuconato

Publications and source records attributed to Simone Cuconato.

3 recordsLinked to original sources

arXiv2026

Sequent-style tableaux for intuitionistic propositional logic

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.

math.LO↗

arXiv2026

Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization

Sequent-style tableaux are a one-sided refutation calculus for classical propositional logic, 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. Building on the correspondence between this block calculus and the cut-free sequent calculus, and following the programme of Kamide and Negri, we recast the calculus as a structural-rule-free G3-style sequent calculus $\mathbf{G}_t$ with shared contexts, and we introduce a G0-style sequent calculus $\mathbf{G}_0$ with independent contexts, explicit weakening and contraction, generalized initial sequents, and a primitive explosion rule. A theorem establishing the equivalence between $\mathbf{G}_0$ and $\mathbf{G}_t$ is proved, and the cut-elimination theorem for $\mathbf{G}_0$ is obtained as a consequence. We then introduce a natural deduction system $\mathbf{N}_g$ with general elimination rules matching the left rules of $\mathbf{G}_0$, and we prove a full normalization theorem for $\mathbf{N}_g$. The proof is achieved by means of bidirectional translations between $\mathbf{G}_0$ and $\mathbf{N}_g$: normal derivations correspond to cut-free derivations, and full normal form to the discipline in which every major premiss of an elimination rule is an assumption. We also determine the reach of the formula-succedent fragment, which is shown to have no theorems, so that the equivalence of the three systems is one of consequence and not of theoremhood, and we show that classical logic is recovered on the succedent side, and recovered exactly, by adjoining the rule of indirect proof.

math.LO↗

arXiv2026

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

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.

math.LO↗