On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing $M_{\imply}$ Super-Polynomial Proofs

TL;DR

This paper analyzes super-polynomial proofs in natural deduction for minimal implicational logic, revealing that such proofs contain super-polynomial redundancy, which has implications for proof compression and complexity class equivalences.

Contribution

It introduces a precise definition of huge proofs in natural deduction and demonstrates super-polynomial redundancy in these proofs, refining previous compression methods and offering an alternative proof that CoNP=NP.

Findings

Most large proofs contain highly repeated sub-proofs.

Super-polynomial redundancy is prevalent in almost all huge proofs.

The results suggest new directions for proof compression and complexity theory.

Abstract

This article precisely defines huge proofs within the system of Natural Deduction for the Minimal implicational propositional logic \mil. This is what we call an unlimited family of super-polynomial proofs. We consider huge families of expanded normal form mapped proofs, a device to explicitly help to count the E-parts of a normal proof in an adequate way. Thus, we show that for almost all members of a super-polynomial family there at least one sub-proof or derivation of each of them that is repeated super-polynomially many times. This last property we call super-polynomial redundancy. Almost all, precisely means that there is a size of the conclusion of proofs that every proof with conclusion bigger than this size and that is huge is highly redundant too. This result points out to a refinement of compression methods previously presented and an alternative and simpler proof that CoNP=NP.