Proof Compression via Subatomic Logic and Guarded Substitutions

TL;DR

This paper introduces a novel proof compression method using guarded substitutions within a subatomic logic framework, enabling more efficient derivations that can simulate traditional systems without the cut rule.

Contribution

It presents a new proof compression technique called guarded substitutions in subatomic logic, allowing for linear derivations and simulation of Frege systems without cut.

Findings

Guarded substitutions enable superpositions of derivations.

Subatomic proof systems with guarded substitutions can simulate Frege systems.

The approach achieves proof compression without using the cut rule.

Abstract

Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units. In this paper, we introduce a powerful new proof compression mechanism that we call guarded substitutions, a variant of explicit substitutions, which substitute only guarded occurrences of a free variable, instead of all free occurrences. This allows us to construct ''superpositions'' of derivations, which simultaneously represent multiple subderivations. We show that a subatomic proof system with guarded substitution can p-simulate a Frege system with substitution, and moreover, the cut-rule is not required to do so.