Absorbing the Structural Rules in the Sequent Calculus with Additional Atomic Rules

TL;DR

This paper demonstrates that structural rules are admissible in sequent calculus systems extended with certain atomic rules, with applications to pure logic and equality.

Contribution

It shows that structural rules can be absorbed into atomic rule extensions of the sequent calculus, simplifying proof systems.

Findings

Structural rules are admissible over atomic rule sets.

Admissibility extends to sequent calculus with added atomic rules.

Applications include pure logic and equality calculus.

Abstract

We show that if the structural rules are admissible over a set R of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in R to G3[mic]. Two applications to pure logic and to the sequent calculus with equality are presented.