Proof Compression via Subatomic Logic and Guarded Substitutions

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. This work was supported by the Inria Exploratory Action IMPROOF and PHC Sophie Germain "Formal Verification for Large Language Models"

• In the next section we present our system KSubG. We introduce the principles of subatomic proof theory, as presented in [2], [4], together with the explicit substitutions of [6], and our guarded substitutions.

• Then, in Section III, we show how subatomic proof theory is related to standard proof theory.

• In Section IV, we discuss the cut and cut elimination in subatomic systems, and we formalize the notion of superposition.

• In Section V, we formally introduce Frege systems with substitution.

• And finally, in Section VI, we prove our main result, showing that the cut-free fragment of our system KSubG polynomially simulates Frege systems with substitution.