Proof Compression via Subatomic Logic and Guarded Substitutions
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915305618407424 |
|---|---|
| author | Barrett, Victoria Guglielmi, Alessio Ralph, Benjamin Straßburger, Lutz |
| author_facet | Barrett, Victoria Guglielmi, Alessio Ralph, Benjamin Straßburger, Lutz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_20009 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Proof Compression via Subatomic Logic and Guarded Substitutions Barrett, Victoria Guglielmi, Alessio Ralph, Benjamin Straßburger, Lutz Logic in Computer Science 03F03 F.4.1 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. |
| title | Proof Compression via Subatomic Logic and Guarded Substitutions |
| topic | Logic in Computer Science 03F03 F.4.1 |
| url | https://arxiv.org/abs/2505.20009 |