论文标题
指数巨大的自然扣除证明是多余的：$ m_ \ supset $的初步结果
Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_\supset$
论文作者
论文摘要
我们通过比较（标记）节点的量与标签集的大小来估算标记树的大小。粗略地说，有指数式标记的树是任何标记的树，其大小，节点数量和标签集的大小之间具有指数差距。任何公式的子形式的数量在其大小上是线性的，因此，任何指数的大证明都具有$ a^n $的尺寸，其中$ a> 1 $和$ n $是其结论的大小。在本文中，我们表明，线性高度标记的树的大小具有指数差距，其标签集的大小至少可能发生了一个子树，它们在其中很多次呈指数次数。最小的含义逻辑（$ M_ \ supset $）中的自然扣除证明和推导本质上是标记的树。根据子形式的原则，从一组公式$γ= \ {γ_1，\ ldots，γ_n\} $中的公式$α$的任何正常衍生$α，γ_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.
