Proof Compression via Subatomic Logic and Guarded Substitutions

TL;DR

The paper develops TBLS, a strictly linear subatomic proof system equipped with explicit and guarded substitutions to compress proofs. It shows that guarded substitutions support powerful superpositions, enabling polynomial-time p-simulations of Frege systems with substitution, even in the cut-free fragment, by mapping subatomic proofs to standard SKS derivations and composing three phases (superposition, eversion, guarded substitutions). The approach unifies cut and substitution-based compression under a single, linear framework and provides a robust interpretation mechanism to transfer completeness from SKS to TBLS. The work also outlines potential extensions of guarded substitutions to broader proof systems, highlighting practical implications for proof complexity and formal verification. Overall, guarded substitutions deliver a new, efficient avenue for proof compression within a subatomic, deep-inference setting.

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.

Figures (11)

• Figure 1: Evolution of $\cut$ from the sequent calculus via deep inference to subatomic proof theory
• Figure 2: The interpretation map $\intof{\,\cdot\,}\colon \SADerv \to \StDerv$
• Figure 3: The derivation $\derb$ in Phase I of the p-simulation construction
• Figure 4: A $\TBLScf$ proof which p-simulates the $\sFzo$ proof $\dera$. Here $\vec{\nu}$, $\vec{\sigma}$, and $\vec{\tau}$ abbreviate $\nu_n\dots\nu_1$, $\sigma_h\dots\sigma_1$, and $\tau_1\dots\tau_h$ respectively.
• Figure 5: Explicit substitution case for the proof of Lemma \ref{['lemma:mergemedial']}

Theorems & Definitions (87)

• Definition 1
• Definition 4
• Remark 5
• Definition 6
• Definition 8
• Example 9
• Definition 10
• Example 11
• Definition 12
• Definition 13