2020/03/16 by Edward Hermann Haeusler, Edward Hermann Hæusler, Haeusler, Edward Hermann · 1 citation
Computer Science · #Advanced Algebra and Logic #F.3.1 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.2004.10659
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
openalex publication_date 2020/03/16 · arxiv created 2020/06/07 · arxiv updated 2020/06/09 · openalex created_date 2024/04/10 · openalex updated_date 2026/07/28
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 an, 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_⊃) are essentially labelled trees. By the sub-formula principle any normal derivation of a formula α from a set of formulas Γ=\γ1,…,γn\ in M_⊃, establishing Γ\vdashM_⊃α, has only sub-formulas of the formulas α,γ1,…,γn occurring in it. By this relationship between labelled trees and derivations in M_⊃, we show that any normal proof of a tautology in M_⊃ 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_⊃ 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.