Formal logic uses proof systems to verify whether arguments are valid. Different proof systems can represent the same logical truths but organize the reasoning differently, making some tasks easier than others. This paper focuses on classical propositional logic, the basic logical system dealing with statements connected by "and," "or," "not," and similar connectives. The starting point is a style of proof called sequent-style tableaux, which works by trying to find a contradiction in a set of assumptions, thereby refuting their joint consistency. The authors connect this approach to a more standard family of proof systems called sequent calculi, which come in different flavors depending on how they handle bookkeeping rules like weakening (adding irrelevant assumptions) and contraction (merging duplicate assumptions).
The main technical contribution is building two sequent calculi, called G0T and G3T, that correspond to the tableau system but present the reasoning in different ways. G3T absorbs all the bookkeeping into the structure of the rules themselves, while G0T makes those bookkeeping steps explicit as separate rules. The authors prove these two systems are equivalent and use that equivalence to establish cut-elimination for G0T. Cut-elimination is a foundational result showing that any proof can be reorganized so it never uses a "shortcut" that introduces a formula not present in the final conclusion, which is important for the proof system's reliability and for analyzing its properties.
The paper then introduces a natural deduction system called NgT, which presents proofs in a style closer to how mathematicians actually reason, using assumptions and steps of introduction and elimination for each connective. A normalization theorem is proved for NgT, meaning any proof can be simplified into a clean, non-redundant form. The key insight connecting everything is a pair of translations between G0T and NgT: cut-free proofs in the sequent calculus correspond precisely to normal proofs in natural deduction, and a stricter notion of full normal form corresponds to a disciplined pattern of reasoning where elimination rules are only ever applied directly to basic assumptions.