Proof Compression via Subatomic Logic and Guarded Substitutions
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.
Keywords
Cite
@article{arxiv.2505.20009,
title = {Proof Compression via Subatomic Logic and Guarded Substitutions},
author = {Victoria Barrett and Alessio Guglielmi and Benjamin Ralph and Lutz Straßburger},
journal= {arXiv preprint arXiv:2505.20009},
year = {2025}
}