We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_\supset$

Abstract: We estimate the size of a labelled tree by comparing the amount of (labelled) nodes with the size of the set of labels. Roughly speaking, a exponentially big labelled tree, is any labelled tree that has an exponential gap between its size, number of nodes, and the size of its labelling set. The number of sub-formulas of any formula is linear on the size of it, and hence any exponentially big proof has a size $a^n$, where $a>1$ and $n$ is the size of its conclusion. In this article, we show that the linearly height labelled trees whose sizes have an exponential gap with the size of their labelling sets posses at least one sub-tree that occurs exponentially many times in them. Natural Deduction proofs and derivations in minimal implicational logic ($M_\supset$) are essentially labelled trees. By the sub-formula principle any normal derivation of a formula $\alpha$ from a set of formulas $\Gamma=\{\gamma_1,\ldots,\gamma_n\}$ in $M_\supset$, establishing $\Gamma\vdash_{M_\supset}\alpha$, has only sub-formulas of the formulas $\alpha,\gamma_1,\ldots,\gamma_n$ occurring in it. By this relationship between labelled trees and derivations in $M_\supset$, we show that any normal proof of a tautology in $M_\supset$ that is exponential on the size of its conclusion has a sub-proof that occurs exponentially many times in it. Thus, any normal and linearly height bounded proof in $M_\supset$ is inherently redundant. Finally, we briefly discuss how this redundancy provides us with a highly efficient compression method for propositional proofs. We also provide some examples that serve to convince us that exponentially big proofs are more frequent than one can imagine.
Comments: This version has a simpler proof of the main result than the previous. Moreover, we decided to focus only on the use of this result to compress Natural Deduction huge proofs. Any relationship with computational complexity is discussed in an article that will appear in a logic journal
Subjects: Logic in Computer Science (cs.LO)
ACM classes: F.4.1; F.3.1
Cite as: arXiv:2004.10659 [cs.LO]
  (or arXiv:2004.10659v2 [cs.LO] for this version)

Submission history

From: Edward Haeusler [view email]
[v1] Mon, 16 Mar 2020 05:26:52 GMT (25kb)
[v2] Sun, 7 Jun 2020 04:06:59 GMT (27kb)

Link back to: arXiv, form interface, contact.