Keywords
Beth tableaux
semantic tableaux
proof theory
subformula property
How to Cite
Abstract
This paper provides an expository comparison of two foundational proof systems in classical propositional logic: Gentzen's sequent calculus and Beth's semantic tableaux. Gentzen's sequent calculus is presented as a rule-based system built upon the single axiom $\alpha \Rightarrow \alpha$, whose key feature — the subformula property — guarantees that every provable formula admits a proof constructed entirely from its subformulas. Beth tableaux are introduced as a complementary, refutation-based method that establishes validity by decomposing a formula from its main connective into subformulas and deriving contradictions across all branches of a truth-value analysis. The correspondence between the two systems is demonstrated through parallel proofs of classical tautologies.
References
1. M. Borisavljevi´c, textit{Two measures for proving Gentzen’s Hauptsatz without mix}, Archive for Mathematical Logic, Springer-Verlag 2002, nr 42, p. 371–387.
2. J.Y. Girard, textit{Linear Logic: It’s syntax and semantics}, Advances in Linear Logic, Girard, Lafont, Regnier, London Mathematical Society Lecture Notes Series 222, Cambridge University Press 1995, p. 1-15.
3. von Plato, textit{A proof of Gentzen’s Hauptsatz without multicut}, Archive for Mathematical Logic, Springer-Verlag 2001, nr 40, p.9-18.
4. G. Restall, textit{An Introduction to Substructural Logics}, Routledge, New York 2000, p. 1-126.
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
Copyright (c) 2026 Zuzanna Rygiewicz Rygiewicz