Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic

TL;DR

This paper introduces a method to compress large proofs in minimal implicational logic into polynomial-sized certificates using DAG structures, enabling efficient verification and contributing to the NP vs CoNP debate.

Contribution

It presents a novel approach to collapsing redundant proof structures into succinct certificates, improving proof verification efficiency in minimal implicational logic.

Findings

Proofs can be compressed into polynomial-sized DAG certificates.

Verification of proof validity can be performed in polynomial time.

The approach relates to the NP=CoNP conjecture.

Abstract

A previous article shows that any linear height bounded normal proof of a tautology in the Natural Deduction for Minimal implicational logic $M_{\supset}$ is as huge as it is redundant. More precisely, any proof in a family of super-polynomially sized and linearly height bounded proofs have a sub-derivation that occurs super-polynomially many times in it. In this article, we show that by collapsing all the repeated sub-derivations we obtain a smaller structure, a rooted Directed Acyclic Graph (r-DAG), that is polynomially upper-bounded on the size of $\alpha$ and it is a certificate that $\alpha$ is a tautology that can be verified in polynomial time. In other words, for every huge proof of a tautology in $M_{\supset}$, we obtain a succinct certificate for its validity. Moreover, we show an algorithm able to check this validity in polynomial time on the certificate's size. Comments on how the results in this article are related to a proof of the conjecture $NP=CoNP$ appears in conclusion.