经典数理逻辑与强关联性逻辑定理的定量分析：自动向前演绎的逻辑基础

理论计算机科学电子笔记169（2007）87-97www.elsevier.com/locate/entcs经典数理逻辑后藤雄一琦玉大学邮编：338-8570景德城2琦玉大学邮编：338-8570摘要CLAS I A SICLL G ICINC L L G IC I N C LL 本文以强关联性作为判别经典数理逻辑中逻辑定理蕴涵悖论的标准，列举了经典数理逻辑中不满足强关联性的逻辑定理图式。这种定量分析表明，经典数理逻辑是远远不是一个合适的逻辑基础，自动向前演绎。关键词：知识表示和推理，自动正向推理，相关逻辑，强相关性1引言正向推理引擎是任何基于知识的系统发现新知识或预测未来事件的不可或缺的组件由于任何用于发现或预测的自动向前推导都没有明确指定的命题或定理作为目标，本质上，将所有推理规则应用于所有给定的前提和先前推导的结论是推导新知识或预测的唯一方法。这自然要求前向演绎引擎只推导出与给定前提肯定相关的结论1电子邮件地址：gotoh@aise.ics.saitama-u.ac.jp2电子邮件地址：cheng@aise.ics.saitama-u.ac.jp1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.03188Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）87在经典数理逻辑（CML）的框架内，一个有效演绎的结论并不一定与其前提有关，因为CML是建立在经典的有效性解释之上的众所周知，CML的逻辑定理中含有大量的另一方面，相关逻辑和强相关逻辑拒绝了这些蕴涵悖论作为它们的逻辑定理，并被采用作为自动向前演绎的逻辑基础[1，2，3，4，5]。然而，到目前为止，还没有人定量研究本文介绍了我们对CML中隐含悖论的定量分析结果，并解释了其含义。 我们以强关联性作为判别CML逻辑定理中蕴涵悖论的标准，并列举出不满足强关联性的CML逻辑定理图式。这种定量分析表明，CML是远远不是一个合适的逻辑基础，自动向前演绎。第二部分简单介绍了CML中的蕴涵悖论，并提到了强关联性。第三节给出了如何分析和分析。第4节给出了一些结论性意见。2隐含悖论2.1经典数理逻辑在逻辑学中，一个句子的形式是“如果... 那么... . 通常被称为条件命题或简单的条件命题。一个条件句必须涉及两个由连接词“如果......”连接的部分。那么... . “并把它的前件和后件称为条件句。一个条件句的真值不仅取决于它的前件和后件的真值，而且更重要的是取决于它的前件和后件之间的一种必要的相关和/或条件关系。在CML中，条件的概念本质上是内涵的，但不是真值泛函的，它由物质蕴涵的真值泛函扩展概念（本文用→表示）表示，定义为A→B=df<$（A<$$>B）或A→B=df<$A<$B，其中<$、<$和<$表示连接词，分别是连接、分离和否定然而，实质蕴涵在意义（语义学）上与条件概念有着本质的区别。它只不过是它的前件和后件的一个延伸的真值函数，但并不要求在前件和后件之间存在必然的相关和条件关系。其前因和后因，即公式A→B的真值取决于只有在A和B的真值上，虽然A和B之间不可能存在必然的相关和条件关系。正是这种实质蕴涵概念和条件蕴涵概念在意义上的内在差异导致了CML中著名的“蕴涵悖论问题”。问题在于，如果把实质蕴涵看作条件概念，把CML的每一个逻辑定理看作蕴涵或有效推理形式，那么，CML的许多逻辑公理和逻辑定理，如A→（B→B），Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）8789B→（<$A<$A）等等，呈现出一些悖论性质，因此它们在文献中被称为注意，CML的任何经典的保守扩展或非经典的替代，其中经典的有效性解释被采用作为逻辑有效性判据，条件的概念直接或间接地由实质蕴涵表示，都具有与CML [3]中的上述问题类似的问题。在CML及其各种保守扩展的框架中，即使一个演绎在CML意义上是有效的，也不一定能保证其前提与结论之间的必然相关性，也不一定能保证其结论在条件意义上是真的因此，任何向前演绎引擎都不能基于CML或其各种保守扩展仅演绎出与给定前提肯定相关的结论。2.2关联性强相关逻辑（Relevant logics，简称RL）的建立是为了获得一个摆脱蕴涵悖论的蕴涵概念[1，2]。然而，尽管强化学习已经摒弃了这些蕴涵悖论，但在强化学习的逻辑理论中仍然存在着一些Cheng提出了一些强相关逻辑，简称SRL，它们不包括悖论[4，5]。在SRL框架下，如果一个推理在SRL意义上是有效的，那么它的前提与结论之间的关联性以及它的结论在条件意义上的有效性都可以在一定的强关联意义上得到保证。强相关性是RL和SRL的一个性质：公式（或公式模式）中的每个命题变量（或模式变量）至少出现一次作为先行部分，至少出现一次作为结果部分[1]。前件部分和后件部分的定义如下，设A、B和C是合式公式或它们的图式，(i) A是A的后件，(ii) 如果B是A的后件（前件），则B是A的前件（后件），(iii) 如果B→C是A的后件（前件），则B是A的前件（后件），C是A的后件（前件），(iv) 如果BC或BC是A的后件（前件），则BC是A的后件（前件）。强相关性是一种性质，它形式上保证了前件和后件之间的关系，使得SRL的任何定理都满足强相关性[4，5]，RL的蕴涵否定片段中的任何定理也满足它[1]。另一方面，CML逻辑定理中的蕴涵悖论和RL逻辑定理中的合取-蕴涵悖论和析取-蕴涵悖论不满足强关联性。因此，我们可以通过检验来90Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）87公式（模式）是否满足强相关性。3定量分析3.1制备本文主要讨论命题演算中的CML的公理系统，因为CML的所有逻辑定理都可以用蕴涵和否定的联结词来表示我们定义我们在本文中研究的良构公式如下。定义3.1（i）命题变量p是一个合式公式，简称w，(ii) 如果A是一个w，那么A是一个w，(iii) A→B是一个w，如果A和B都是w，(iv) 只有i=iii是w。定义3.2子w是w的一部分，本身也是w。 每一个w都被看作是它自己的一个子w。请注意，我们并不关心包含双重否定的w，例如A是w的<$（<$A），作为我们分析中的子w另一方面，命题变量的数量是无限的，因此CML的逻辑定理集因此，我们处理的一套模式的逻辑定理。定义3.3一个w的模式是一个公式，它用模式变量替换了w中模式变量是它可以替代某些命题变量的变量。它们是具有顺序关系的符号，不包括在CML的词汇表定义3.4CML的逻辑定理模式是CML的逻辑定理的模式。定义3.5设deg→（A）=k表示k是A的蕴涵（→）的连接嵌套的次数。deg→（A）=k的定义如下。(i) 如果A中没有→，则deg→（A）= 0，(ii) deg→（<$A）=deg→（A），(iii) deg→（A→B）= 1+max（deg→（A），deg→（B））。定义3.6A是CML的一个k次逻辑定理模式，其中A是CML的一个逻辑定理模式，且deg→（A）=k。定义3.7k次模式片段是所有j次模式（1≤j≤k）的集合，记为Fk。Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）8791））以有根树为代表：蕴涵：否定连接模式变量：模式变量定义3.8CML的k次片段是CML（1≤j≤k）的所有j次逻辑定理模式的集合，记为Thk。T hk可以分为两个集合：T hk中所有蕴涵悖论的集合，记为IPk，以及所有无悖论定理的集合，记为T h Sk。关系量T hk、IPk和T hSk如下：(1)T hk= IPk<$T hSk。我们通过检查逻辑定理模式是否满足强相关性来区分蕴涵悖论和其他悖论。因此，我们可以通过三个步骤来列举悖论(i) 得到Fk中的所有模式，(ii) 将Fk分为两个集合：T hk和其他，通过检查每个模式是否Fk是不是逻辑定理。(iii) 以强相关性为标准，将Thk分为ThSk和IPk3.2分析首先，我们在F3中生成所有的模式。任何模式都可以用有根树结构表示;蕴涵的连接词是一个内部节点，它可以有一个父节点，但必须有两个子节点;否定的连接词是另一个内部节点，它可以有一个父节点，但必须有一个子节点;模式变量是一个标签，在树叶上。例如（<$（α→β）→γ）is可以用一个像图1这样的有根树来表示，它的→和<$分别是蕴涵和否定的连接词，α，β，γ是模式变量。 所有模式都可以按根树我们定义树干是树的一部分，它只由内部节点组成，没有叶子，例如，在图2中。我们可以从F（k）中出现的各种主干和长度为1 ~ 2k的模式变量的各种排列中产生Fk中的所有模式。一（（ Fig. 1. 一棵有根树的例子算法1产生F（k）中出现的所有类型的干线。(i) τ0=df{(ii) i←1(iii) 从IV循环到XVIII，92Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）87一后备箱叶先行子树图二. 有根树(iv)τi←φ，(v)从VI循环到XVII，(vi)从τi−1中选取一个树干(vii)从VIII循环到Xi，(viii)从τj（0≤j≤i−2）中提取主干η(ix)创建四个新的干线：（n→n），（n→n），<$（n→n），<$（n→n），(x)将这些主干添加到τi中，(xi)从viii开始重复直到将τj的所有元素取为η，(xii)从xiii循环到xvi，(xiii)从τi−1中选取主干θ，(xiv)创建两个新的主干：（θ→θ），<$（θ→θ），(xv)把这些主干加到τk中，(xvi)从xiii开始重复，直到将τi−1的所有元素取为θ，(xvii)从vi开始重复，直到将τi−1的所有元素取为π，(xviii)i← i +1，然后从iv开始重复，直到k = i。算法2创建长度为1到k的模式变量的各种排列。(i) ρ1=df{(ii) i←2(iii) 从IV循环到XIII，(iv)ρi←φ，(v)从vi循环到xii，(vi)从ρi−1中选取一个置换λ，(vii)从VIII循环到Xi，(viii)j←1(ix)通过将λ与j连接来创建新的置换，例如Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）8793KK(x)将置换加到ρi中，(xi)j←j+1然后从viii重复直到j=m，其中m是出现在λ中的模式变量的下标的最大数目(xii)从vi开始重复，直到将ρi−1的所有元素取为λ，(xiii)i← i +1，然后从iv开始重复，直到k = i。然后，我们通过检验一个图式是否普遍为真来区分逻辑定理图式和产生的图式集合中的其他图式。然后，我们判断这些逻辑定理图式是否满足强相关性。表1给出了Fk、IPk和ThSk（1≤k≤ 3）的元素个数。表1Fk、IPk和T hSk的元素个数KFkIPkT hSkIPk/T hSk11 .一、60× 1010的情况。00×100二、00×1000.002二、26×103二、16×1029 .第九条。80×1012.2031 .一、67× 1083 .第三章。94×107二、44×10616.13表2Fk的元素个数次数Fk42. 92×101951. 63 ×1045六四29× 1010371. 02×10235八点八。15 ×10527在我们的枚举方法中，当i大于3时，不能处理Fi，因为F4的量太大了。表2给出了F k的元素个数（4 ≤k≤ 8）。相对于k线性变大，Fk呈指数变大. 注意，可以计算Fk的元素数，但很难得到所有集合的元素。Fk的元素数可以计算如下。 Ti表示Fk中有根树的树干的种类，所有树的叶子数为i，嵌套蕴涵度为k。设Pi是某棵有根树的叶子上的模式变量的排列类型，当叶子的个数为i时，将其作为标签。 则F kis的元素数可由Ti计算和Pi。94Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）87K0其中，Ti的定义如下：T1= 2，Y. Goto，J.Cheng/Electronic Notes in Theoretical Computer Science 169（2007）8795D1KK不ek−1i−1MJT2=8，Ti= 0，（0≤k，i k + 1， 2k

下载后可阅读完整内容，剩余1页未读，立即下载