指数巨大自然演绎证明是冗余的：关于$M_\supset$的初步结果
Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_\supset$
摘要：
我们通过比较（标记的）节点的数量与标签集的大小来估计标记树的大小。粗略地说，一个指数级大的标记树是任何标记树，它的大小，节点数和它的标记集的大小之间有指数级的差距。任何公式的子公式的数量与其大小成线性关系，因此任何指数级大的证明都有一个大小$a^n$，其中$a>1$和$n$是其结论的大小。在这篇文章中，我们表明，线性高度标记的树的大小有一个指数的差距，其标签集的大小，至少有一个子树，在他们的指数出现多次。最小蕴涵逻辑（$M_\supset$）中的自然演绎证明和推导本质上是标号树。通过子公式原理，从$M_\supset$中的公式集合$Γ=\{γ_1,\ldots,γ_n\}$中的公式$α$的任何正常推导，建立$Γ\vdash_{M_\supset}α$，只有公式$α,γ_1,\ldots,γ_n$的子公式出现在其中。通过标记树和$M_\supset$中的推导之间的这种关系，我们证明了在$M_\supset$中的重言式的任何正常证明都具有一个子-因此，在$M_\supset$中的任何正常的和线性的高度有界证明本质上是冗余的。最后，我们简要地讨论了这种冗余如何为我们提供一个高效的压缩方法的命题证明。我们还提供了一些例子来说服我们，指数大的证明比人们想象的更频繁。
英文摘要：
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 $α$ from a set of formulas $Γ=\{γ_1,\ldots,γ_n\}$ in $M_\supset$, establishing $Γ\vdash_{M_\supset}α$, has only sub-formulas of the formulas $α,γ_1,\ldots,γ_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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
