A Subatomic Proof System for Decision Trees

TL;DR

This paper introduces a novel proof system for propositional logic that combines Boolean functions and decision trees, resulting in more regular and efficient proofs, especially for certain tautologies that are hard in traditional systems.

Contribution

The paper presents a new proof system integrating Boolean functions and decision trees, achieving polynomial proofs for tautologies that are exponential in sequent calculus, and introduces a regular, cut-free proof construction.

Findings

The system generates polynomial cut-free proofs for Statman tautologies.

Proofs are more regular and efficient due to the integration of decision trees.

Atoms as superpositions enable natural proof projections without cuts.

Abstract

We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: the system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic. Thanks to this regularity, cuts are eliminated via a natural construction. The second reason is that the system generates efficient proofs. Indeed, we show that a certain class of tautologies due to Statman, which cannot have better than exponential cut-free proofs in the sequent calculus, have polynomial cut-free proofs in our system. We achieve this by using the same construction that we use for cut elimination. In summary, by expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient. That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each atom into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of the constructions in this paper. To accommodate self-dual non-commutativity, we compose proofs in deep inference.