≤→→可在www.sciencedirect.com在线获取理论计算机科学电子笔记315（2015）31-46www.elsevier.com/locate/entcs在最小逻辑中证明一个重言式需要多少次假设关于经典推理的压缩能力的示例*Edward HermannHaeuslerDepartamentodeInform'aticaPUC-Rio巴西里约热内卢摘要本文给出了一个新的公式，n，需要至少2n次假设发生纯蕴涵最小命题逻辑（M）的自然演绎法中任何正规证明中的另一个公式β n。在经典的蕴涵逻辑中，每一个逻辑都有最多使用一个假设发生的正规证明。因此，在M中，正规证明是指数下界的，而在其经典版本中是线性下界的。事实上，2n也是无割序贯证明的下限。这类公式的存在性对设计基于这类系统的自动证明过程有很强的指导意义。讨论了纯蕴涵经典逻辑中的重言式在其最小对应项为指数大小时如何由多项式大小的导子关键词：命题逻辑复杂性，自然演绎，最小命题逻辑，证明理论1引言为命题重言式提供证明似乎是一项艰巨的任务。巨大的证明是这样的，它们的大小是关于它们的结论的大小的超多项式。知道有一个经典的命题逻辑重言式只有巨大的证明关系到知道NP是否=CoNP[2]。 直觉主义逻辑是PSPACE完备的[11]，Richard Statman [17]证明了纯蕴涵最小逻辑（M→）也是PSPACE完备的。我们在[8]中证明，如果一个命题逻辑有一个具有子公式性质的自然演绎（ND），那么它是在PSPACE中。这是因为M→多项式编码 任何具有这种ND系统的命题逻辑因此，大量证据的存在作者感谢CAPES和CNPq项目PIER的财政支持。电子邮件地址：hermann@inf.puc-rio.brhttp://dx.doi.org/10.1016/j.entcs.2015.06.0041571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。32E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31对于一个更一般的命题逻辑类，它与M→中存在大量的证明有关，这些证明相当于知道PSPACE是否=NP 这些计算复杂性类与大型证明的存在之间的关系实际上涉及任意的证明系统。例如，NP=PSP ACE是这种情况，当且仅当，对于任何M→重言式，存在一个证明系统，该证明系统产生该重言式的多项式大小的证明任意证明系统的理论研究不在本文的范围之内。然而，研究关键逻辑的特定证明系统，如M→或经典逻辑，可以从存储的效率和经济性的角度出发，对实现命题定理证明器的实际方面有所启发。M→携带了几乎所有的证明理论和逻辑信息，以在良2命题逻辑中产生多项式有界证明。对M→的集中考察值得注意。M→有许多证明系统。最著名的是结构/分析证明系统。众所周知的系统是基于序列微积分[4]，自然演绎[4，14]和表格[1，16]的。这些系统，主要是第一和第三类，在提供自动生成证明的手段方面相当不错。反向链接过程，例如，如果应用于基于顺序演算的证明系统，提供了一种自动生成证明的方法。这些证明程序的问题是，何时必须决定应用哪一条规则，以及在这种情况下如何处理不可证明的公式关于处 理无效公 式的这 一特征 ，关于序 列演算 和表格 这两个系 统的文 献由于CoPSPACE=PSPACE，在M→中提供一个反模型是如此困难，以至于无法提供一个证明。 反模型的大小可以是关于公式的超多项式。有趣的是，研究这与M→中的证明的大小如何相关，或者至少有一个具体的证据，证明巨大的证据可能是这样的。大多数著名的大型证明在文献中被认为是在经典逻辑中。在古典逻辑中如此，在最小逻辑中也是如此。我们的意图不仅仅是在M→中展示巨大的证明。我们可以使用文献[17]或[8]中报道的多项式平移，从完全最小逻辑到M→生成鸽子洞原理的公式。从[9]中我们知道，这个公式在归结中只有超多项式大小的证明，因此在无割序贯微积分和正常的自然演绎中也是如此。很难从这些翻译中发现为什么它们在M→中是巨大的，因为没有什么是M→特有的。关注M→是有希望的，因为M→具有更少的组合选择，更少的逻辑常数，更少的替代演绎系统。M→中的大型证明的起源可能会为命题逻辑的复杂性提供一些新的线索。这是强调的事实，这里显示的公式没有大量的证明时，考虑到经典推理。这篇文章的目的是展示如何使用经典逻辑可以提高规模的证明所获得的自动证明过程的那种，是能够产生正常的和切自由推导。定理证明器的开发人员必须了解2具有子公式属性E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3133设计一个高效的系统。任何可以指导设计师的信息都是有帮助的。证明中公式的副本数量可能是高效实现的“瓶颈”。为了节省内存，一个明显的解决方案是在表示证明时使用引用而不是副本。引用的数量是指数级的，但在大多数情况下，对公式的引用少于公式。 这种方法指出了使用图（有向图， 事实），以证明。在文献中报道了在这个方向上所做的许多发展它们中的大多数都是语义驱动而不是实现驱动。Proof-nets [5]代表了一种方法，它捍卫了使用图作为证明的最适当表示。我们同意这一点，并且我们认为这是采用有向图而不是树来表示证明的实际动机[15]。值得一提的是，希尔伯特系统中的证明的大小与自然演绎证明中的证明的大小之间存在着一个重要的关系。希尔伯特系统由一组公理模式和一组推理规则构成。当我们有多个前提的推理规则时，证明可以表示为序列或树。基本上，当处理树时，如果一个公式在证明中被使用了不止一次，那么它可以在证明中出现不止一次。 在处理序列时，公式被引用而不是被复制。推理规则是通过引用证明中已经假设的公式来应用的序列到树的朴素映射可能会使我们看到证明中的大小（ 公式出现的次数）明显增加然 而 ，通过一个非常巧妙的机制，Krajicek[10]证明了，对于α的每个证明，在经典逻辑的希尔伯特系统中：size（size tree）≤ poly（size（size seq）），其中poly是一个变量的多项式。 由于自然演绎可以看作是一个希尔伯特系统，证明被表示为树，Krajicek多项式模拟证明树的证明序列适用于自然演绎。最后要注意的是，→-引入规则不过是希尔伯特系统中的演绎定理。同样，演绎定理可以用结论的证明不大于前提的证明的方式来证明。因此，我们可以将我们的讨论建立在自然演绎中的树上，并将其带到任何希尔伯特系统中，保持模多项式模拟的结论。在第四节中，我们引入了公式n，0≤n。 在第5节中，我们证明了它们在M→的通常自然演绎中具有指数大小的正规证明。在同一节中，我们证明这是M→中的下界。在经典命题逻辑中，这些公式有线性大小的证明，如第4节所示。第2节和第3节分别提醒我们纯蕴涵最小逻辑和经典逻辑的基础知识本文中的所有形式命题证明/推导都是在Prawitz风格的自然演绎（ND）中呈现的。这些正常的证明/推导的大小是多项式模拟的无切序贯演算（SC）和/或表。因此，这里所示的下限也适用于它们。34E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31→2纯蕴涵最小逻辑（纯）蕴涵最小逻辑M→是只包含逻辑常数→的最小逻辑片段。它的语义是仅限于→的直觉Kripke语义。给定一个命题语言L，M→模型是一个结构<$U，≤，V<$，其中U是非空集（世界），≤是U上的偏序关系，V是从U到L的幂集的函数，使得如果i，j∈U且i≤j则V（i）<$V（j）。给定一个模型，满意度关系|=世界之间，在模型中，公式定义为：• U，≤，V| = ip，p∈ L，i ∈ V（i）• U，≤，V |= iα1→ α2，i <$，对任意j ∈ U，使得i ≤ j，如果<$U，≤，V <$|= jα1然后，U，≤，V，|= jα2。Obs：在（完全）最小逻辑中，没有特殊意义，因此没有项目声明U，≤，V|= i.我们提醒M→在它的语言中没有通常，公式α在模型M中有效，即M| = α，当且仅当，它在模型的每个世界i中都是满意的，即i∈UM| = iα。一个公式是M→重言式，当且仅当它在每个模型中都有效。一个公式在M→中是可满足的，如果它在M→的模型M中是有效的。知道一个公式是否满足的问题在M→中是微不足道的。每个公式在模型<${*}，≤，V <$中都是可满足的，其中*是唯一的世界，p∈ V（*），对每个p。因此，SAT不是M→中的有趣问题。同样的事情不能告诉我们一个公式是否是M→重言式。我们知道，对于M→Kripke语义，只有→-规则（下面是→-Elim和→-Intro）的最小逻辑的Prawitz自然演绎系统是可靠的和完备的。因此，根岑的LJ系统[18]只包含右和左→规则也是健全和完整的。众所周知，这些规则之一是不可逆的3。基于M→的反向链接的朴素证明过程，仅仅基于这种通常的根岑微积分是不可能的。在下一节中，我们提出并讨论了纯蕴涵经典逻辑的自然演绎系统的一个主要方面。[α]|βα→β→-Introα α→β -Elimβ3泛蕴涵经典逻辑如果我们只考虑逻辑常数→，我们就可以将最小可证明性与它的经典对应部分区分开来。 例如，皮尔士在3规则是可逆的，也就是说，只要前提有效，结论就有效，只要任何前提无效，结论也无效。E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3135（（A→B）→A）→Ac−α[A]a（（A→B）→A）→A→-I[(((A→B）→A）→A）→B]cBa→-I→-EBA→B[（（A→B）→A）]Ab→−IP规则（（A→B）→A）→A图1. 用K中的P -规则证明Peirce→-E[12]中，基于Glyvenko类定理，讨论了一个具有正规化过程和多项式平移到M→的P-M蕴涵经典逻辑（K→在本节中，我们总结了[12]中与本文讨论的例子有关的主要在[12]中提出的系统是基于皮尔士规则的。事实上，为了证明皮尔士[α→β]|αP规则利用这个规则，很容易推导出皮尔士由于P规则既不是引入规则，也不是消除规则，这是特别考虑的。置换约化，如Seldin自然演绎中的经典规则，被认为是从任何导数获得正规导数的主要归约步骤，如[12]所述。 这里给出了一个正规形式的定义，称为P-正规形式。这个定义，如下所示，在推导中使用了分支的概念。在推导中的分支是序列δ0，.，公式出现次数的δ k，使得δ0是一个假设， 或不. δk是一个→-E规则的一个小前提，或者是一个结论，每个i = 0，...，k− 1，δi是一个→-E的大前提或一个→-引入以δi+1为结论的规则定义3.1K→中的一个导子是P-正规型的，即，对于K →中的每一个分支，没有公式出现是一个消去规则和一个引入规则的结论的前提，除此之外，K →中的P-规则结论也不是该分支中一个→-E或一个→-I应用规则的前提例如上面的（（A→B）→A）→A的导数是P-正规导数。导子的归约，这里称为置换，如图2所示，确保了在K→中从Γ导出α的任何导子都可以变换为从Γ导出α的导子，在K→中每次应用P-规则都导出形式为β→A的公式，其中A是原子。通过迭代应用图2中的归约，我们得到原子公式作为任何P-规则应用所释放的蕴涵的右手边一个P-正规推导/证明，其中P-规则的每次应用都释放形式为α→A的公式，其中A是原子的，被称为原子扩展的36E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31[β1→（β2→β3）]aΠβ1αβ1转化为[β1]b[β1→β3]aβ3β2→β3bβ1→（β2→β3）Πβ1αβ1图2.在P-规则应用程序中减少排出公式右侧的次数P-正规推导/证明，也称为AEP-正规推导/证明。在[12]中，证明了以下定理：定理3.2 α从Γ ={γ1，…，K→中的γk}可以转化为α从K →中的Γ的AEP正规导子。从AEP-正规推导中的分支的形式得出以下陈述，该陈述也被称为Glyvenko定理，因为它与经典逻辑和直觉主义逻辑中的可证明性之间的原始Glyvenko对应相似。见[6]，[13]，见[14]，见[15]，见[16]，见[17]，见[18]，见[19]，定理3.3设α是一个纯蕴涵公式，{p1，…，pk}出现在α中的命题变量的集合。因此，<$K→α，当且仅当<$M→（α→p1）→（（α→p2）. （（α→pn）→α）.. . ）的。从上述定理的证明，在[12]中，我们可以得出结论：引理3.4设λ是α在K →中的AEP-正规证明，使得λ的大小（公式出现的次数）为s，则（α→p1）→（（α→p2）. （（α→pn）→α）.. . ）在M→中有界于s2上面的引理说K→中的正规证明是多项式模拟的，M→.虽然K→证明了Peirce定律，但它不是一个完整的经典系统。它所缺乏的是直觉主义的否定。为了有一个完整的系统，我们必须加上直觉荒谬规则4。这个系统我们称之为KI→。 在这个系统中，我们可以把否定<$α定义为α → α。⊥β当我们考虑β原子时，上面的规则有一个限制形式，即从β原子推断B。这一限制不是必要的。重复使用下面的变换，我们可以将KI中α的任何证明→转化为KI中α的证明→使用原子形式的ex-falso-sequitur-quolibet，而不是它的一般形式。这种对原子应用的简化是由于Prawitz（见[14]）。4也被称为前法-推论-Quodlibet原理E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3137βΠ⊥β1→β2转化为Π⊥2β1→β 2→-I包含直觉荒谬规则的系统，而不是一般的系统，对于纯蕴涵经典逻辑来说也是完整和合理的。原子直觉荒谬规则系统有助于理解如何在K→中多项式模拟KI→。下面的命题是这个多项式模拟的基础，因为它涉及公式的多项式有界平移这个命题是Ingebrigt Johansson定义的从直觉主义逻辑到最小逻辑的转换的一个变体。命题3.5设α是语言{→，}中的公式，使得{p1，.， pk}是出现在α中的命题变量的集合。如果rp i，对于每个i，和α是公式（r→p1）→（（r→p2）. （（r→pn）→α）.. . ），则<$KI→α，当且仅当<$K→α<$。上述结果意味着经典逻辑中的大型证明的存在性蕴含着M→中的大型证明的存在性。这篇文章，通过在接下来的部分中暴露的材料，研究一些这些巨大的，可以说是超多项式有界的证明是如何的，以及如何使用经典推理在某些情况下可以切割这个超多项式下界。4需要大量的假设在[3]中，我们可以找到一个讨论的事实，即当证明定理的逻辑弱于经典逻辑，需要使用一个假设一次以上，一个强大的解释是多么复杂的证明程序，因此，决策程序的这种逻辑。在这里，我们可以找到公式（A→B）→A）→A）→B）→B.考虑到前面提到的ND和CS的证明系统，这个公式需要使用假设（（A→B）→A）→A）→B至少两次，以便在M→中证明。 受此启发，我们可以定义一类公式，在使用假设时没有限制这表明，在M→的自动证明过程中限制假设的使用并不是确保完备性的替代方案。在续集中，我们定义了公式类。下面是（A→B）→A）→A）→B）→B的一般证明。 注意，它不能用少于2个假设来证明（A→B）→A）→A）→B.下面的公式结合了上面提到的公式的两个实例，以便有一个需要4倍假设的公式((((A→B）→A）→A）→B）→C（1）其中，n=（（（D→C）→D）→D）→C。[5]当然，没有皮尔士规则的这个系统38E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）311在图4中，我们展示了上述公式1的正常推导。我们可以看到它有4个假设（（A→A）→A）→A）→A）。它们来自图3所示的推导中的两个假设发生，在图4的证明中使用了两次[A]1（（A→）→A）→A（（A→）→A）→A →A[（A→B）→A]2一个2（（A→B）→A）→A（（A→B）→A）→Bξ图3.图4中使用的推导公式我们可以看到如何使用这种模式，如果它重复n次，我们定义一个公式n，这样，任何正常的证明n必须使用一个假设至少2n次，见第5节。在我们继续讨论命题的定义之前，我们必须证明，对于经典命题逻辑来说，重复假设的需要并不是这样现在考虑这个逻辑是纯蕴涵经典逻辑，K→，而不是纯粹的隐含最小逻辑。考虑到K，我们仅使用一个假设来证明公式1，如图5所示。 这是因为（D→C）→D）→D）是皮尔士规则的蕴涵形式的一个实例， 所以它是可证明的。从这个证明和 n=（D→C）→D）→C，我们证明了C。通过证明皮尔士A）→排出证明所需公式的样本。纯蕴涵经典逻辑也可以在[7]中看到，在那里我们可以找到纯蕴涵经典逻辑的详细介绍，其中有一些证明理论的结果，而不是像[12]中那样的自然演绎。在某些情况下，例如这种情况下，使用经典逻辑可以将证明变小。[(((A→B）→A）→A）→B]5[D]3个月（D→C）→D）→D）C3D→C[（D→C）→D]4D4[(((A→B）→A）→A）→B]5Σ（（D→C）→D）→DC5（A→B）→A）→A）→B）→C图4. 纯蕴涵最小逻辑中公式R_25在M中没有发生假设的界限→在本节中，我们证明对于每个n，都有一个公式nn，使得nn的任何正常证明至少有2n个相同公式的出现假设，即E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3139电子邮件2（（D→C）→D）→D电子邮件1（（A→）→A）→A[（（（A→）→A）→]1C1（A→B）→A）→A）→B）→C图5.纯蕴涵经典逻辑中公式E_2的证明所有人都在一个介绍规则中被解雇下面的命题5.4通过展示使用2n个证明n的证明的正规证明来展示2n是一个上界。定理5.5表明，在M→中，在少于2n个假设的情况下，没有任何一个n的正规证明。我们在《易经》中，正如在第4节中已经说过的那样，RNN是从前面的例子中推导出的迭代过程中产生的定义5.1设χ[X，Y] =（（（X→Y）→X）→X）→Y。 使用χ[X，Y]，我们递归地定义了一个公式族。考虑命题字母C和Di，i>0。设i=0，i >0，为公式：1=χ[D1，C]（2）i+1=χ[Di+1，使用这个公式族，我们定义公式n，n>0，使得对于任何i≥0：i+1=我们可以观察到，可以通过使用证明（如图3所示），用C代替，用D1代替A，并应用→-引理作为最后一条规则来证明1=1→C所得到的证明有2个公式的出现假设。图4中的证明是对图2的证明，用图1代替图1，用图2代替A，用图1代替D，结果是下面的证明。[D1]3[（D2→D1）→D2）→D2）→D1]5Σ（D1→C）→D1）→D1）1C[（D2→D1）→D2）3D1→C[（D1→C）→D1]4→D）→D]52 1D14（（D1→C）→D1）→D11C5（D2→D1）→D2）→D2）→D1）→C下面的引理将用于命题5.4的证明。引理5.2在公式i，i> 0中，如果我们同时用1替换C，并且对于每个k > 0，用Dk+1替换Dk，则所得公式为χ[Di+1，i]。证明这个引理是由归纳证明的i。 我们观察到，对于R1，替换C40E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31我由1和D1由D2在1，得到的公式是χ[D2，1]。 假设对于i> 0，用k 1代替C，并且对于每个k = 1，.，i，同时用Di+1替换Di，得到χ [Di+1，Xi]。观察到i+1=χ[Di+1，i]，并且通过归纳假设，在i，k= 1，i中同时用1替换C和用Dk+1替换Dk，得到i+1。由于Di+1不出现在i中，最终在i+1=χ[Di+1，i+1]中用Di+2替换Di+1得到χ[Di+2，i这证明了归纳步骤。QQ另一个观察是，如上所示的引理中的替换，如果应用于M→中的派生树，则意味着结果树也是有效的派生。这一事实是通过观察替换总是在原子公式上，并且M→的规则没有由于这些替换而不满足的附带条件来证明的。因此，我们有以下事实。事实5.3如果α是γ1的导数，...，γ1和一个代换S（在原子式上）应用于α，则S（α）是S（γ 1）的一个导子，.，S（γl）。除此之外，如果n是正常的，那么S（n）也是正常的。命题5.4对于任何n > 0，有一个正规的证明，其中有2 n个相同假设的发生，这些假设被证明的最后一个规则所排除。证明通过归纳法进行。基n= 1是图3所示的证明。这个证明也是在图6中的证明之内，作为一个子推导出现。假设i，i >0有一个正规证明i，它有2 i次i出现，由它的最后一个推理规则排出。因此，我们有一个C的正规导子<$i，来自于<$i的2 i次出现，记住<$i=<$i→C。我们认为，如果我们同时将C替换为k1，并且对于每个k = 1，...，i，用Dk+1代替Dk，则根据引理5.2和事实5.3，我们将得到从χ[Di+1，i]的2i次出现的1的正规导子。让我们把这种推导称为“非线性”。下面的推导（见图6）是C从（Di+1→Di）→Di+1）→ D i +1）→Di）→C的推导，即， 是C从i+1导出，因此，通过→-引入应用，我们有i +1的正常导出，排除公式i+1的2 i+2 i= 2 i+1假设。QQ[D1]3[（Di+1→Di）→Di+1）→Di+1）→Di]5伊什（D1→C）→D1）→D1）C[（Di+1→Di）→Di+1）3D1→C[（D1→C）→D1]4D14→Di+1）→Di]5伊什（（D1→C）→D1）→D1iC5（（（（Di+1→Di）→Di+1）→Di+1）→Di）→C图6. 在M→中的Proofφi+1，其中2i+1是φi+1的充要假设定理5.5表明，2i是假设发生次数的下界。E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3141在M→中的任何正规证明中唯一公式的唯一性。定理5.5在M →中的任何正规证明都至少有2个i假设出现-i。证明我们证明了，对于任何i，有没有正常的证明，有小于2i的假设发生的i。 我们首先观察到，((((D1→C）→D1）→D1）→C）→C不能仅用一次出现的1=（D1→C）→D1）→D1）→C）来证明。 如果是这样的话，我们会从分析的形式，C的一个正规证明，（（D1→C）→D1）→D1是可证的在M→中，这是不可能的，因为这个公式只在经典上有效。一个有两个世界的克里普克模型，在第一个世界中C和D1都不成立，在第二个世界中D1成立但C不成立（D1→C）→D1）→D1）。 即随着M={*1，*2}，{*1≤*1，*1≤*2，*2≤*2}，{V（*1）=，V（*2）={D1}}则M| = α<$i（D1→C），i = 1，2，so，M| = αi（D1→C）→D1，i = 1，2.因此，我们有M| = α1（（D1→C）→D1）→D1.考虑到有正常的证明，小于2i的假设发生-i。所以有最小的k（k>0），使得，有一个正常的证明，有少于2k个的假设出现。让 阿 斯克成为这样的证明。由于k=k→C，这个证明如下。我们记得，每个开放的假设都有一个形式，[k]lkClk→C由于k=χ[Dk，k−1] =（Dk→k−1）→Dk）→k−1，它必须是→-elim规则的大前提如果不是这种情况，那么k将是具有k→β形式的大前提的→-elim规则的小前提。这个公式又必然是这个分支的开假设的子公式，因为推导是正规的，而αk→β只能是一个应用的结论。→-elim规则。因为在Bokk中唯一的开放假设是Bokk本身，所以Bokk作为小前提的情况是不可能的。因此，由于“k”是一个大前提，“k”具有以下形式，记住“k”是如何的，在本段的第一行中显示42E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31s（n）拉吉（Dk→k−1）→Dk）→Dk）[（（Dk→k−1）→Dk）→k−1]lk−1克Clk→C请注意，J是k的子导子，它也必须将k作为开放假设。它必须有一个开放的假设，因为（Dk→Dk−1）→Dk）→Dk）在M→中不可证明。由于Rankk是Rankk中唯一可能的开放公式，则Rankj至少有一次Rankk在其中开放非常重要的是要注意到，每个出现在k中的k都有一个形式为J的伴随导子，其中k是开的。因此，如果我们从k中删除每个J，我们最终得到以下证明：[k−1]lk−1Cl→C上面的证明是在最后一条规则排除了小于2k−1次假设出现的情况下证明了k−1这是因为我们在移除J时至少移除了一个关于k的假设。 也就是说，我们至少将假设出现的次数除以2。因此，得到的修剪导子与k是保持此性质的最小数的事实相矛盾，因为它是小于2k− 1的k−1→ C的导子。 QQ我们证明了，任何正规证明都至少有2n个假设出现. n（s（无论n的大小是多少，它的任何正常证明都至少有2 n次出现大小为s（n）−2的公式，因为s（n）+ 2 = s（n）。因此，我们可以得出结论，任何正规证明的最小尺寸是超多项式有界的，当与尺寸相比，它本身。设n是n的任何正规证明，则比率s（n）为：s（n）>s（n）s（n）×2n（s（n）+2）现在让我们考虑这个事实，根据n的大小来估计n的正规证明的大小。为了简化计算，我们认为公式的长度是其中出现的命题字母的数量，其实际大小与我们在这里称之为长度的东西成线性比例，因为对于每个命题字母，最多有一个→符号。在此评估中将忽略括号。通过后面的讨论，我们可以看到2×len（n）≥s（n）。分析将使用length（len）来测量字符串的大小E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3143ns（m）.n的形式是 n是以循环的方式定义的χ[Di，ni−1]，其中n i1=（（D1→C）→D1）→D1。由于len（1）= 5且len（i+1）= 2×len（i）+3，我们可以推出6，len（n）= 2n−1×（5 + 3）−3，因此len（n）= 2n−1×（5 + 3）− 2。从前面的讨论中，我们发现公式n是n上的超多项式.实际上，表示它们的字符串在n上是巨大的。然而，在任何正规的证明中，最小的出现次数不少于2n，所以我们有：（2n）×（2n−1×（5 + 3）−2） 1，使得s（n）= κs（n）。n6论经典逻辑本文讨论了在K→和KI→中的正则证明。我们证明了在KI→或K→中的任何正规证明都不是超多项式有界的。其主要原因是χ[Dk，k−1] =（Dk→k−1）→Dk）→k−1有一个大小为k×η×s（k）的正规证明，其中η是一个常数。作为一个清晰的展示，我们在图7中展示了图5中的证明，它适应并迭代了我们目前的 讨论。克-1（（Dk−1→k−2）→Dk−1）→Dk−1克-2.克（（Dk→k−1）→Dk）→Dk克-1[（Dk→k−1）→Dk）→Dk）→k−1]12001年。（（D1→C）→D1）→D11C1（Dk→k−1）→Dk）→Dk）→k−1）→C记住并且图7. 在纯KI中证明了1=（D1→C）→D1）→D1）→Ck−1=（Dk−1→6使用你最喜欢的方法解递归方程44E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31→►→►→►→联系我们[答]B →A（B→A）<$（A→B）[（（B→A）<$（A→B））→B]BA →B（B→A）<$（A→B）[（（B→A）<$（A→B））→B]B(((B→A）→B）→B）→B图8.达米特公式的证明[答]AA[（AA）→]⊥欧阿AA[（AA）→]⊥（（A<$A）→）→图9.三次非数据公式的证明至少需要两个重复假设所有的证明都有9×（s（i））+3）。这可以通过图1中的证明中的检查来检查，使A=Di和B=Dii。我们可以注意到s（i）≤s（k），i= 1，k，因此整个证明的大小上界为k×9×（s（k））+3）。在这种特殊情况下，K→比M→节省更多的空间。我们可以认为这是一个非常特殊的情况。事实并非如此。图9和图8是经典重言式的证明的例子，这些重言式可以用来获得类似的公式类，而在正规证明中需要指数级的假设。这一次，我们必须使用完全命题最小逻辑，也就是说，具有其他逻辑常数{，，<$，<$}的最小逻辑，关于它的经典对应物也是一样。因此，在这些图中证明的公式可以用来提供通过使用经典推理获得的压缩功率的其他例子。我们将在下一篇文章中解决这个猜想我们可以概括这里讨论的情况设α使得Mα，有β和γ，使得αMβ和γ，β Mα。我们可以得出结论，KIα，如下文右推导所示除此之外，在左导子具有αβ的指数多个假设 的情况下，我们猜想，通过应用于公式类的情况的类似推理，我们可以使用K1→ K2 → K3 →K4 →K5→ KE.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）3145[γ]|[γ][γ]|α¬α⊥γα [α→β]β|β′γ→β′|α [α→β]β（（α→β）→β¬⊥β|β′γ→β′|α¬α⊥α7结论考虑到M→是定义有效证明过程的最困难和最具代表性的命题逻辑，我们展示了一个例子，提醒人们允许无限使用假设对于任何完整的证明过程都是值得的。这个例子在M→中运行。我们不知道一个类似的运行在经典逻辑。经典命题逻辑比M→更有效，如果这样的例子不存在。命题逻辑的复杂性有很多结构，从主要复杂性类之间的关系开始。本文的唯一目的是提供一个例子，证明的指数增长与析取和组合原则（如鸽子洞7）无关。从经典重言式中以类似的方式得到的公式类就是这样的例子。8致谢作者要感谢教授。感谢Gilles Dowek听到和阅读了这里提出的我们感谢杰·埃尔森·多斯桑托斯就改进案文提出的建议引用[1] E.W. 贝 丝 语 义 蕴 涵 与 形 式 可 导 性 。 Mededelingen der Koninklijke Nederlandse Akademie vanWetenschappen：Afd.莱特昆德北荷兰Uitgevers Maatschappij，1961年。[2] Stephen A.厨师. 定理证明过程的复杂性 在Proceedings of the Third AnnualACM Symposium onTheory of Computing ， STOC '71 ， pages 151-158 ， New York ， NY ， USA ， 1971 。 ACM 。http://doi.acm.org/10.1145/800157.805047网站。[3] Gilles Dowek和Ying Jiang 特征变量、括号与正极小的可判定性谓词逻辑Theoretical Computer Science，360（13）：193- 208，2006. http://www.sciencedirect的网站。com/science/article/pii/S030439750600257X.7鸽子洞原理被用来为Robinson的（提议的）分辨率提供一个超多项式下界。46E.H. Haeusler/Electronic Notes in Theoretical Computer Science 315（2015）31[4] G.根森我们的后勤工作很顺利。Mathematische Zeitschrift，39：176-210，1935. 英文版本见[？]，原始版本在线http://eudml.org/doc/168546。[5] 让-伊夫·吉拉德Proof-nets：证明理论的并行语法在p.Agliano和A.Ursini，编辑，逻辑与代数马塞尔·德克尔，纽约，1996年。[6] V. I.格利文科在我的逻辑中有几个要点。布劳威尔。布尔数学会，15：183-185，1929.[7] L.戈尔杰耶夫存在peirce规则时的割消元。Archiv fr mathematische Logik und Grundlagenforschung，26：147-164，1987.[8] 爱德华·赫尔曼·豪斯勒。命题逻辑的复杂性与子公式性质。CoRR，cs/1401.8209v1，2014年。也是DCM2014 研 讨 会 的 会 议 记 录 ， 2014 年 维 也 纳 逻 辑 夏 季 ， 维 也 纳 ， 2014 年 7 月 ， 和http://arxiv.org/cs/1401.8209v1。[9] A.哈肯 难以解决的问题。 Theoretical Computer Science，39（2[10] 扬·克拉是个好孩子。 下限为恒深比例尺的大小。 JournalofSym bolicLogic，59（1）：73 -86，1994.[11] Richard E.拉德纳模态命题逻辑系统中可证明性的计算复杂性。SIAM Journal on Computing，6（3）：467[12] 放大图片作者：Luiz Carlos Pereira，Edward Hermann Haeusler，Vaston G. Costa和Wagner Sanz。经典命题逻辑蕴涵片段的一种新的规范化策略。Studia Logica，96（1）：95[13] Luiz Carlos Pereira，Edward Hermann Haeusler，and Maria da Paz N.德梅代罗斯。具有经典否定 的 命 题 逻 辑 片 断 的 一 些 结 果 。 OQueNosFazPensar ， 23 ： 105http://www.oquenosfazpensar.com/adm/uploads/artigo/alguns_resultados_sobre_fragmentos_com_fragmentao_da_logica_classica/23_Alguns_resultados_sobre_fragmentos.pdf。[14] D. 普拉维茨自然演绎：一个证明理论研究。Almqvist Wiksell博士论文，1965年。[15] Marcela Quispe-Cruz ， Edward Hermann Haeusler ， and Lew Gordeev. 最 小 蕴 涵 逻 辑 的 证 明 图 。 在Proceedings 2013 International Workshop onDevelopments in Computational Models，EPTCS第144卷，第16-29页，2014年[16] R. M. Smullyan。 Springer-Verlag，New York，1968.[17] 理查德·斯塔曼直觉命题逻辑是多项式空间完备的。Theoretical Computer Science，9（1）：67[18] G. 武由提证明理论。研究逻辑和数学基础1987年北荷兰
