English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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 biglabelled tree, is any labelled tree that has an exponential gap between itssize, number of nodes, and the size of its labelling set. The number ofsub-formulas of any formula is linear on the size of it, and hence anyexponentially big proof has a size $a^n$, where $a>1$ and $n$ is the size ofits conclusion. In this article, we show that the linearly height labelledtrees whose sizes have an exponential gap with the size of their labelling setsposses 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 anynormal 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 betweenlabelled trees and derivations in $M_\supset$, we show that any normal proof ofa tautology in $M_\supset$ that is exponential on the size of its conclusionhas a sub-proof that occurs exponentially many times in it. Thus, any normaland linearly height bounded proof in $M_\supset$ is inherently redundant.Finally, we briefly discuss how this redundancy provides us with a highlyefficient compression method for propositional proofs. We also provide someexamples that serve to convince us that exponentially big proofs are morefrequent than one can imagine.

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