131网址：http://www.elsevier.nl/locate/entcs/volume67.html17页研究蕴涵直觉逻辑的可证明性：公式树方法Sabine Broda Lu s Damasfsbb，luisncc.up.ptDCC-FC LIACC波尔图大学葡萄牙波尔图摘要我们使用另一种图形表示的公式在蕴涵直觉逻辑，以获得和证明有关的可证明性的结果。我们证明了该方法在这方面的适当性，表明人们可以很容易地识别和证明新的结果，并简化别人的证明。因此，我们推广了一类已知的公式，- 正常的证明是真的，并定义一个新的一个是正规证明的唯一性。 我们还给出了一个精确的表征，一组可证明的单原子公式，并获得作为推论的一个必要条件，直觉定理一般。关键词：蕴涵逻辑，可证明性，证明的唯一性，公式树方法1介绍多年来，人们对直觉主义逻辑蕴涵片断（子系统）的可证明性做了大量的研究这些研究导致了几个主题的结果，包括[8]中的证明生成算法，[15]和[11]中的复杂性结果，[4]，[5]和[7]中小森在[13]中提出了在蕴涵直觉主义逻辑和BCK-逻辑的自然演绎系统中极小公式的正规证明是否唯一的问题，得到了正规证明唯一性的一些充分必要后者被证明是真实的减少，因此，2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。132为减少，由Hirokawa在[10]。另一方面，Mints在[14]中独立地证明了具有多个-正规证明的最小蕴涵直觉定理，另一方面证明了平衡公式的-正规的唯一性，Tatsuta在[16]中独立地证明了最小蕴涵直觉定理。在最后一篇论文中，龙田还展示了深度为2的极小公式的正规证明这些结果在某种程度上被Aoto和Ono统一了，他们表现出了独特性的- [1]中负非重复公式的正规证明。 唯一性Aoto在文献[2]中给出了极小公式无非素压缩可证的-正规证明在本文中，我们继续这条研究路线。本文证明，利用一种公式的图形表示，即[6]中首次引入的公式树表示，可以很容易地得到和证明这方面的新结果，而简化了其他结果的证明注意，通过Curry-Howard同构，cf.[12]中，每一个蕴涵公式都可以看作是单类型系统TA中a项的一个类型-calculus和任何这样的-术语可以被视为公式的证明。在本文中，我们使用-项作为证明的表示在第2节中，我们回顾了有关公式树表示的基本概念在第三节中，我们证明了利用公式树表示公式，- 正常的证明变得直接，事实上可以扩展，并有简单，几乎直接的证明。此外，我们证明了另一大类公式的正规证明的唯一性。在第四节中，我们得到了可证单原子公式集的一个简单的句法特征，并作为推论得到了一般直觉主义定理的一个必要条件。2背景我们假设熟悉微积分中的基本概念，并使用[3]和[9]中的标准符号。我们的符号与[3]中的符号不同，因为我们用\A，B，C，：“表示类型变量（原子），用小写希腊字母表示任意类型。对于类型赋值，我们考虑简单类型演算系统TA[9]或[3]。一 - 术语（正常形式），类型/公式可以被分配的被称为（正常）居民 .2.1公式树和证明树在下文中，我们回顾了公式/类型的替代树形表示的定义，称为公式树，在[6]中引入，它给了我们一个精确的133K、、K在公式/类型的正常证明/居民的构建过程中的不同阶段的想法。事实上，公式的公式树在其原始部分上定义了某种层次结构，可以用来构造由证明树表示的证明。定义2.1公式树是其节点由具有以下形式（P1）、（P2）或（P3）之一的原始部分组成的树：J(P1)：(P2)：一cc，，一（n个1）（P3）：A A1： ： ：ANJ以基元部分为节点的树是公式树，树的根是形式（P1）;树的每个内部节点具有形式（P2）;树的每一个叶子都是形式（P2）或（P3）。下面的算法计算一个模板的模板树tre（“）。我们使用虚线表示公式树的边，以便将它们与树的基本部分（节点）中的边区分开来。 注意，每个公式'可以唯一地写成'=1！“……”你好！其中A是原子，n为0。算法如下所示。J如果n =0，即 'A，thentre e（'）=.一如果n 1，则tre（'）=JcA、c、c、一其中t（A）=J对于k1t（1）：t（n）m1; ： ：;mk 0wede net（（11 ！ “ ……”1m1 ！ A1）！“ ……”（k1 ！“……”公里！ A k）！ A）=，A，，，，，，，，A1，、、、、、、*Ak、、、（11）： ：t（1m1）：t（k1） ：t（km ）的方式134注意，可以容易地定义逆算法，该逆算法在给定公式树FT的情况下计算mula'的唯一性，使得t re（'）=FT。例2.2公式（A！B）！ A！B）！（A！B）！ A！ B具有以下公式树Jc B，c.、C.、C.、、、均p0. 、.、、、.、B B= n jB A A...一J一即Jp4p1p2p3有原始部件的Jp0=BBp1==nBABp2=jA一p3=J一p4=：J定义2.3由一棵二叉树tre（'）构造的一棵树的前序是通过连接tre（'）的本原部分来得到的，该本原部分标识出相同类型变量的重叠（不重叠）发生。我们称之为有效证明树，如果证明树中的所有叶子都具有形式（P3）;每当原始部分Pi出现在形式树Tree（“）中的某个原始部分Pj之下时，则Pj在形式树Tree（”）中的每次出现都至少出现一次。C135请注意，'的公式树在其原始部分上定义了某种层次结构，这必须由从tre（'）构建的树的每个有效程序来表示。特别地，这意味着从tre（'）构建的每个有效的树的根是tre（'）的根。例2.4例2.2中公式的有效证明树是Jp0Bp2看起来像jp3aJ另一方面，在一项研究中，p0p2p4不是有效的证明树（尽管它具有相同的外观），因为它不遵守公式树给出的层次结构均p0C.. 、、、p1cCp4cp2p3（A！ B）！ A！ B）！ （A！ B）！ A！ B，它要求p4只能在botp0和p1同时出现时使用。其他树木的价值是136均p0p1p2p3p4和p0p1p2p3p3两人的外表JB= nB A：J J一J2.2证明树和（长）正规居民一个类型的-正规居民M称为i的长正规居民，M中的每个变量出现z后面都跟着最长的参数序列，所有参数都被它的ty p e所包围，即。例如，一个具有形式（zP1： Pn），（n0），不处于功能位置的元素具有原子类型。通过对一个项M进行-约化而得到的所有项的（nite）集合称为M的-族，记为fMg.它被证明（cf。[4]，[9]）的长正规居民的-族将的正规居民的集合划分为互不重叠的nite子集，每个-族只包含一个长成员。此外，Ben-Yelles（cf.[4]，[9]）证明了一个类型的每个正常居民“可以扩展为一个唯一的（最多为-版本）长正常居民”。在[9]中可以找到一个简单的扩展因此，当寻找一个类型的正常居民时，计算它的长正常居民的集合是足够的，所有正常居民都可以通过约简得到。在[6]中定义了一个算法，它给出了一个公式'的长居民M，计算树PT（M）的一个有效概率。 文[6]给出了求一个mula't= tre（'）的mula树和由它构造的一个有效证明树的 逆 算 法 ，计算了mula't = tre（'）的长闭正规居民的集合Terms（'）。命题2.5（在[6]中）(i) 若M是一个类型p '的长正规居民，则PT（M ）是一个由p'构造的有效pre。(ii) 这是从某种类型的公式中建立的一个有效的公式。 那么Term s（）的每一个numberer都是'的一个numbered longnormal居民。137此外，这两个算法是互补的，在这个意义上，对于每一个封闭的长正常居民M的'有M2项（PT（M））。继续，类型“的每个正常居民对应于从tre（”）建立的一个有效证明树，从tre（“）建立的每个有效树的前序对应于”的正常居民的集合，并且不同的有效树的前序对应于不同的且不相交的正常居民的集合。3蕴涵直觉逻辑中正规证明的统一性1986年，Komori在文[13]中提出了在蕴涵直觉主义逻辑和BCK-逻辑的自然演绎系统中，极小公式的正规证明Hirokawa在[10]中证明了后者对于-约化是正确的，因此1对于-约化是正确的。 另一方面，Mints在[14]中独立地证明了具有多个正规证明的最小蕴涵直觉定理，而Tatsuta在[16]中证明了平衡公式的正规证明的唯一性。在这最后一份文件龙田还显示了独特的-正常的证明最小公式的深度2。Aoto和Ono在文[1]中给出了负非重复公式的-正规证明的唯一性，在某种程度上统一了这些结果。Aoto在[2]中给出了无非素压缩可证极小公式的正规唯一性证明在这一节中，我们表明，使用公式树的公式表示，结果有关正常的证明变得简单，实际上可以扩展，并有简单，几乎直接的证明。此外，我们证明了另一大类公式的正规证明的唯一性。我们首先回忆一下文献[6]中关于算法Terms的定义，它给出了a的m ula'的mula树t，即 t=tre（'），以及由其构建的树的一个有效的程序，计算'的长闭正常居民的集合Term s（）=Term s（t;0;）。 在下面的翼让L表示一个集指定变量名称的原始部分t。然后，项s（t;k;;L）由以下定义。J让一是...的根源并考虑A在t中的对应出现，1 注意，非正规证明的唯一性意味着非正规证明的唯一性。这是因为每个-正规形式都是一个特殊的-正规形式.1380在n0。现在，让L0 =L[f（p;xk）]ing.0、项s（t;k;;L）=fxk： xk：xj（p;x）2L0g：ppn形式JA，你好，1：我我J一如果的形式让A，则取相应的原始部分p=JJ和否则，的形式1NJccA，cc，1：M其中m为1，且对于i= 1;：;m，i的根为Bi。考虑对应的原始部分p一cc，令s（t;k;;L）=B1：BMfxk：xk：xM： Mj（p;x）2L; M2Terms（t; k+1;;L）;1jmg：1n1m j j引理3.1Let'e是一个公式和一个由mt=tre（'）建立的tre的有效命题。然后，只有当至少一个原始部分在证明树的分支中被使用了不止一次时， jTerms（）j > 1。证据通过对的深度的归纳，很容易表明，如果在的任何分支中没有本原部分被使用超过一次，则在计算项s（）期间，在ny步中，集合L0对于任何本原部分p，至多包含一对形式（p;x）。结果是直接的。2139定义3.2公式中出现的子公式定义为正或负，如下所示。积极地发生在;如果子公式的出现在中为正（负），则它为负（分别为 positi ve）in！“的;如果子格式发生是positivein，则它是positivein。你要进去！“的。一个公式如果每个原子最多有一个负的出现，则称为负非复制。注意，负非重复公式类适当地包含了本节开头提到的所有其他类，即平衡公式类、无需非素压缩即可证明的极小公式类等。因此，[1]中的以下结果包含了关于-正规证明唯一性的所有其他结果。我们现在表明，当使用公式树时，它变得几乎简单，并给出了一个相当简单的证明。定理3.3每一个可证的负非重复公式恰好有一个-正常的证明。证据考虑一个具有公式树tre（）的可证负非重复公式。请注意，底部的每个原子（分别为 在tre（）中的一个基本部分的顶部（top）对应于一个位置（resp. 原子的存在。因为是负非复制的，这意味着对于每个原子A，在tre（）中最多有一个在其顶部有A的本原部分。 在构造证明树的过程中，没有选择，这仅仅是证明树唯一性的存在。另一方面，它也表明，在任何分支中，都不可能使用一个原始部分超过一次，因为这将导致不间断重复。最后，我们从引理3.1得出结论，尽管每个证明树一般对应于一个nite数n， 1的- 正规形式，只有当至少一个原始部分在证明树的分支中被使用了不止一次时，才有n>12前面的结果的证明使我们能够确定一个更大的一类公式的唯一性减少是真的。140C定义3.4一个公式被称为确定的i在构造有效证明树的每一步都没有替代选择。例3.5例2.2中的公式不是确定性的，因为在第一步骤中，有两种可能的选择。事实上，我们可以在原始部分p1或p2之间进行选择，以追求有效证明树的构造推论3.6每个确定性公式都有一个- 正常的证明。请注意，确定性公式的类正确地包括负非重复公式的类。此外，确定性公式非常容易识别2。例3.7考虑下面的公式[2]。该公式不是负非重复的，因此不属于已证明的-约化唯一性的公式类。=（（S！ P）！ S！ Q）！ （P！ Q）！R）！ （P！ Q）！ R它的mulatreetre（）是R，cc，RQcc，，CP S PS2 给定一个公式对于n个原子的出现，最多需要n个步骤来决定是否是决定性的。Q.Q.P141nn我阿i并且在构造的唯一有效证明树期间没有选择。Rcc，，Q QPPJSJ我们的结论是恰好具有一个- 正常的证明。在本节的其余部分，我们提出了一类新的公式，我们证明了唯一性的正规形式。定义3.8一个公式被称为-free，如果没有形式为1的子公式的正出现！“……”你好！A！其中A和B是原子。免费的名称是公正的以下。定理3.9-自由型的所有-族都是单例族.证据通过检查算法术语，很容易验证，为了构造一个类型的长居民M，一个不正常的形式，必须构造M的某个（子）项，其形式为 xk： xk：xM* Mx k.1N1m1n在这里，xk是原子类型的，从M是长居住者得出。因此，PnB（对应于xk的部分）必须具有以下形式：J对于一些原子B，因此，存在一些子公式的正发生，形式1 ！“……”n1 ！B！B！其中A和B是原子。 最后的结论从树的定义（）得出。事实上，无论何时，t（i1）： t（im）142occursintre（），则i1 ！ “ ……”Imi ！一个很好的机会。若是i=B，则不 - 免费的2推论3.10每一个可证的负非重复和-自由公式在NJ中都有唯一的-正规证明。推论3.11每一个可证明的决定论和 - 免费配方具有独特的-在新泽西州的正常证明。例3.12例3.7中的公式不属于此类，因为它有（S！ P）！ S！Q也是P！ Q. 事实上，有两个正常的证明。4蕴涵直觉逻辑定义4.1只有一个类型变量出现的类型称为单原子类型.以下关于单原子公式的正规证明集的基数的结果最初是针对类型给出的，并且对于-和正规都是正确的。forms.定理4.2（Ben-Yelles，1979）设是以下形式的单原子分子式=1！“……”m！一M............. 0。然后，(i) 如果至少一个i是复合的，即非原子的，则没有或只有有限数量的正规证明;(ii) 如果1=：=m= A，则有m个正规证明。143、csscss例4.3考虑公式=（（A！ A）！ A！ A）！（（A！ A）！（A！ A）！ A）！ （A！（A！ A）！ A）！ A）！ A）！ （A！A）！ A！ 一关于Formula Tree一ss。. 、、、S一ssscSc一AA..AAassscScA A. 、、AAAA、AA a....A A从Ben-Yelles的结果中我们得出结论， 正常的证明。但事实上，它有任何？下面我们给出可证单原子公式集的一个简单的句法刻画。定义4.4一个公式树被称为完全的，如果所有的叶子都是（P3）的形式，参见。定义2.1.修剪公式树意味着删除虚线边缘处的分支（以及以这些边缘为根的子树）。定理4.5一个单原子公式在至少一个完全子树上 是 可 证 的 ， 通过修剪tre（）可以得到。证据如果的部分很容易。为了构造一个有效的证明树，使得通过修剪tre（）可以得到一个完整的子树，只需在这个完整的子树中遍历虚线相对两侧的变量的并发。F或唯一的如果部分让e是一个从tre（）构建的树的有效程序=JcA，.c、c、t（1）：t（k）、144、、ı，A，、我们在深度n上用归纳法证明了这个结果。对于深度n= 1，我们有J一=A;thust（j）=JJ;对于某个j2f1; ：;kg，结果为真。F或n>1考虑j2f1; ：;kgsuch，t（j）=，，，，，，，A1，、、、、、、*Ap、、、（11）： ：t（1m1）：t（p1）： ：t（pmp）对应于用于=JA，，：因此，每个i，1你好，ı我p的深度为 n，可以由1：p. .. .J.A，，，，：、、、.t（1）：t（k）t（i1）： t（imi）J我们从归纳假设中得出结论，A，2..ft（1）; ：;t（k）;t（i1）; ：;t（imi）g是完备的。结果如下所示，事实上，这对所有的i2f1; ：;pg都是真的。2例4.6下面是通过例4.3中的tre（）得到 的一个完全子树。145CsA..一ssscsscA.A...另一个是一、、、AA a一..一因此，委员会认为， 是可证明的，并且有无穷多的正规证明。请注意，从任何可能非单原子的可证明公式中，通过实例化可以获得可证明的单原子公式因此，我们从定理4.5得到了一般公式可证的必要条件推论4.7对于每个可证公式，通过修剪tre（）至少可以得到一个完全子树。25结论本文用公式树表示公式，以获得和证明蕴涵直觉逻辑中有关可证性的结果。公式的这种表示的一个主要优点是，它使它们的许多性质变得明显，并且证明它们非常直观和容易。事实上，公式的公式树为我们提供了公式的基本部分的层次结构。这些原始部分可以组合起来，以构建有效的证明树（构建工作类似于多米诺骨牌游戏，其中必须连接同一个原子的不同出现，同时尊重公式树给出的层次结构）。每个证明树对应于公式的一个正规证明集，并且每个正规证明仅由一个有效证明树表示。请注意，有效的证明树使用所有原始部分至少（分别）。精确地或至多）一旦基本上对应于相关公式的证明（分别地，BCI-或BCK-）逻辑。这使得这种表示也足以研究这些子系统中的属性。146本文说明了这种表示的充分性，证明了正规证明的唯一性和单原子公式的可证性。但是还有很多其他的应用。例如，为了证明[4]中给出的（长）正态居民计数算法的极限的存在性和正确性，它有一个非常长和复杂的证明（见[9]），注意以下内容几乎是足够的：1. 长正规居民的深度等于其对应的有效证明树的深度;2. 如果有效证明树中的任何分支在类型中具有深度数量的不同原子，则至少有一个原子在该分支中出现两次，并且可以重复这两次出现之间的部分（如您所希望的那样频繁），从而增加深度并获得新的证明树或等效的正常居民;3. 一个类型最多具有j个原始部分，其中j j是原子在中出现的次数;因此，分支中可用原始部分的不同集合的数量（由于公式树给出的原始部分上的层次结构）是j;因此，在深度>j的每个分支中，至少有一个原子在可用原始部分的相同集合中出现两次;因此，这两次出现之间的部分可以被切掉，导致更短的证明树。致谢本文中介绍的工作得到了LIACC的部分资金支持，这些资金是通过Plancima de Financiamento Pluri-anual、Fundac~aopa raaC i^eTecnol ogia和Prog ramaPOSI提供的。引用[1] T. Aoto和H. 小野 f中正规正态性的唯一性^g-NJ的片段。研究报告IS-RR-94-0024 F，信息科学学院，JAIST。[2] T. Aoto，Uniformity of Normal Proofs in Implicational Intuitionistic Logic. Journalof Logic，Language Information，8（2）：217{247，1999.[3] H.巴伦德雷Lambda结石的类型。在Abramsky，Gabbay和Maibaum编辑的背景：计算结构，计算机科学逻辑手册第2卷，第117页。牛津科学出版社，1992年。[4] C.- B.本·耶尔斯演算中的类型赋值;语法和语义。 数学系博士论文威尔士斯旺西大学，英国，1979年。[5] S. Broda和L.达马斯主栖的计算一个类型的主要居民的第四届类型化λ演算及其应用国际会议论文集，TLCA'99，计算机科学讲义1581，页ag。69-82，Springer Verlag，1999。147[6] S. Broda和L.达马斯关于一类正规项的结构。2000年第七届WoLLIC会议论文集，pp。33{43，2000.[7] S. Broda和L.达马斯计算一个类型的（主要）居民。Fundamenta Informaticae，45：33{51，2001.[8] M.W.邦德蕴涵逻辑的证明算法。理论计算机科学，232：165{186，2000。[9] J. R.辛德雷简单类型理论剑桥理论计算机科学。剑桥大学出版社，1997年。[10] S.广川BCK-lambda-terms的主要类型。 理论计算机科学， 107：253{276，1993。[11] S.广川注意：在证明的初始性中（）是多项式空间完备的。理论计算机科学，206：331{339，1998.[12] W. A.霍华德 公式作为类型的构造概念。 在J.P.Seldin和J.R.作者声明：To H.B. Curry ： Essays on Combinatory Logic ， Lambda Calculus and Formalism ， pp.479{490. 中国科学院出版社，1980年.[13] Y.小森BCK代数和lambda演算。第10届半群对称会议论文集，pp。5{11，1986.[14] G. E. 薄荷糖Carnival闭范畴凝聚定理的一个简单证明In G. E.薄荷教育，在证明理论中的论文集，pp。213{220. 1992年，《图书馆》。[15] R.斯塔曼直觉命题逻辑是多项式空间完备的。理论计算机科学，9：67{72，1979。[16] M.辰太极小公式正规证明的唯一性。 Journal of Symbolic Logic ，58（3）：789{799，1993.
我的内容管理
展开
