指数级庞大的自然演绎证明是冗余的：关于 $M_\supset$ 的初步结果

我们通过比较（带标签的）节点数量与标签集合的大小来估计带标签树的规模。粗略地说，指数级庞大的带标签树是指其规模（节点数）与其标签集合的大小之间存在指数级差距的任意带标签树。任意公式的子公式数量关于其大小是线性的，因此任意指数级庞大的证明具有规模 $a^n$，其中 $a>1$ 且 $n$ 为其结论的大小。在本文中，我们证明了那些规模与其标签集合大小存在指数级差距的线性高度带标签树，至少含有一个在其中出现指数多次的子树。自然演绎证明与极小蕴涵逻辑（$M_\supset$）中的推导本质上即是带标签树。由子公式原理，在 $M_\supset$ 中从公式集 $\Gamma=\{\gamma_1,\ldots,\gamma_n\}$ 对公式 $\alpha$ 的任意正规推导（确立 $\Gamma\vdash_{M_\supset}\alpha$）中，仅出现公式 $\alpha,\gamma_1,\ldots,\gamma_n$ 的子公式。借助带标签树与 $M_\supset$ 中推导之间的这一关系，我们证明了 $M_\supset$ 中任一关于其结论大小呈指数级的重言式正规证明，含有一个在其中出现指数多次的子证明。因此，$M_\supset$ 中任意正规且高度线性有界的证明本质上是冗余的。最后，我们简要讨论了该冗余性如何为我们提供一种针对命题证明的高效压缩方法。我们还给出了一些例子，足以使我们相信指数级庞大的证明比人们所能想象的更为常见。