Rule-Elimination Theorems

TL;DR

This paper offers a new, non-algorithmic proof of the cut-elimination theorem for propositional logic, introduces the concept of normal sequent structures, and generalizes rule-elimination theorems within an abstract framework to clarify their fundamental nature.

Contribution

It provides an abstract, non-algorithmic approach to rule-elimination theorems, extending the understanding of cut-elimination beyond specific proof algorithms.

Findings

Non-algorithmic proof of cut-elimination for propositional logic

Introduction of normal sequent structures and abstract sequent structures

Establishment of rule-elimination theorems with converses in an abstract setting

Abstract

Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen's proof of the cut-elimination theorem for the system $\mathbf{LK}$, several other proofs have been proposed. Even though the techniques of these proofs can be modified to sequent systems other than $\mathbf{LK}$, they are essentially of a very particular nature; each of them describes an algorithm to transform a given proof to a cut-free proof. However, due to its reliance on heavy syntactic arguments and case distinctions, such an algorithm makes the fundamental structure of the argument rather opaque. We, therefore, consider rules abstractly, within the framework of logical structures familiar from universal logic \`a la Jean-Yves B\'eziau, and aim to clarify the essence of the so-called ``elimination theorems''. To do this, we first give a non-algorithmic proof of the cut-elimination theorem for the propositional fragment of $\mathbf{LK}$. From this proof, we abstract the essential features of the argument and define something called ``normal sequent structures'' relative to a particular rule. We then prove two rule-elimination theorems for these and show that one of these has a converse. Abstracting even more, we define ``abstract sequent structures'' and show that for these structures, the corresponding version of the ``rule''-elimination theorem has a converse as well.