IL 0的PSPACE困难性与封闭的片段转化为IL 0

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）47-54www.elsevier.com/locate/entcsIL的闭片段是PSPACE困难的F'soubou1，2巴塞罗那大学概率、逻辑与统计系西班牙巴塞罗那Joost J. Joosten Joosten1，3巴塞罗那大学逻辑、历史和科学哲学系西班牙巴塞罗那摘要在本文中，我们考虑IL0，封闭的片段的基本可解释性逻辑IL。我们证明了我们可以将Göodel-Löob的伪逻辑GL的一个可变片段GL 1转化为IL 0.通过对GL 1的PSPACE完全性的一个证明，我们得到了IL 0的PSPACE困难性.关键词：可解释性逻辑，计算复杂性，闭片段，PSPACE，范式。1引言对于命题逻辑L，该逻辑的闭片段-我们记为L0-由L的那些根本不包含任何命题变量的对于各种逻辑，已知闭合片段比完整逻辑本身容易得多。封闭片段的简单性可以通过定理的决策过程的复杂性类来捕获。此外，在所有的情况下，在这个意义上，L0是已知的比L简单，我们有一组标准形式的L0和一个标准形式定理，每个封闭的公式可以写在一个独特的方式作为一个特殊的组合标准形式的公式。也许这种现象最典型的例子是经典命题逻辑。经典命题逻辑中的定理是共NP的1作者感谢西班牙教育和科学部（项目TASSAT TIN 2010 -20967-C 04 -01和RYC-2008-02649）和加泰罗尼亚政府（项目2009 SGR-1433/34）。2电子邮件：bou@ub.edu3电子邮件：jjoosten@ub.edu1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.00548F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）47完整的，而封闭的片段在LOG时间是可判定的。在这种情况下，根据定义，仅有的两个正规形式的公式是T和T。对于各种模态逻辑，情况是相似的，但略有不同。对于可证明性逻辑GL，定理是已知的PSPACE完全问题（见[2，定理18.29]），而闭片段中公式的可证明性是已知的PTIME可判定的（见[3，定理9]）。此外，范式定理（[1，第7章]）指出，闭片段中的每个公式都可证明等价于形式为Qn<$其中n∈ω的公式的布尔组合。可解释性逻辑是GL的自然扩展。逻辑GL只有一个模态算子QA来捕捉可解释性逻辑有一个额外的二元模态ADB来捕捉这些可解释性逻辑总是被定义为一些核心部分IL，如下所述，以及一些额外的原则。然而，一旦附加原理证明了某个相当弱的原理F，其技术细节目前无关紧要，则封闭的可解释性公式可以在没有模态D的情况下表示，并且标准形式与GL的标准形式相同：形式为Qn∈ω的公式的布尔组合（参见[5]）。在这里强调一下，所有具有有趣的元数学内容的可解释性逻辑都包含原则F。对于低于ILF的逻辑，特别是IL本身，不知道是否存在一组自然的范式。并不是所有模态逻辑都有L0比L简单的情况.特别地，已知最小模态逻辑K及其闭片段K0都是PSPACE完备的（见[3，推论4]）。传递框架的模态逻辑K4也是如此（参见[3]）。我们将在本文中看到，逻辑IL与逻辑K和K4相似，因为IL的闭片段也是PSPACE难的，从而解决了一个开放问题，[8]关于封闭片段是否允许一个很好的表征，这是否定的2可解释性逻辑可解释性逻辑主要用于在形式化的设置中研究二元模态算子所捕获的相对化可解释性的概念D. 短语pDq应理解为（T连同q的翻译）不同的理论T证明不同的模态原理是成立的。然而，所有允许语法编码并因此形式化可解释性概念的理论都验证了一些称为IL的核心逻辑。2.1逻辑IL我们记得GL是具有一个模态Q的正常模态逻辑，其非逻辑公理是以下公理方案的实例化(i) Q（A→B）→（QA→QB）F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）4749(ii) Q（QA→A）→QA众所周知，GL证明了传递性公理，即，QA → QQA。逻辑IL在具有两个模态Q和Q的命题模态逻辑中被公式化。D. 我们将使用以下阅读惯例。最强的结合算子是<$和Q，其次是<$N和<$N，它们的结合力又比D强。最弱的约束连接词是蕴涵参与→。我们将写Q作为<$Q<$的简写。定义2.1逻辑IL是一个包含GL的正规模态逻辑，其规则是肯定前件和必然性，其公理而不是所有命题重言式是下列公理方案的实例J1Q（A→B）→ADBJ2（ADB）→ADCJ3（ADC）→ABDC J4ADB→（QA→QB）J5QADA从J1和J 4可以得出，Q可以用IL中的D表示：IL<$QAParticipate <$AD<$。逻辑ILF是通过将公理F加到IL上而得到的。F：=QA→ <$（AD QA）这个原理可以看作是哥德尔第二不完全性定理的自然推广.哥德尔第二不完备性定理指出，一个任意递归理论，只要是相容的，就不能证明它自己的原则F指出，任何递归理论，只要是一致的，甚至不解释它自己的一致性。2.2IL的语义逻辑IL允许自然Kripke语义，其中二元模态D由三元关系建模。我们倾向于将D的语义视为二元关系的集合定义2.2IL模型，也称为Veltman模型， 四重<$W，R，{Sx：x∈W}，D<$其中W是一个非空的世界集，R是W上的一个二元关系，它是传递的，反之是良基的。对于每个x∈W，二元关系Sx是传递的和自反的，使得而且(i) ySxz→xRy <$xRz;(ii) xRyRz → ySxz。关系D是一个通常的强制关系，可以被看作是一个映射，它为每个命题变量p分配一个p成立的世界W的子集v（p）。我们50F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）47写xDp表示x∈v（p）。关系D被扩展到所有公式的集合，规定：(i) xD QA优惠xRy（xRy→y D A）;(ii) x D A D B 优惠 （xRy→dz（ySxzdz））。众所周知，IL对于所有Veltman模型的类来说是合理和完备的（见[4]）。2.3片段我们用IL0表示IL的片段，它由可在IL中证明的不含命题变量的模态公式组成。同样地，我们用GL1来表示那些用GL语言表示的公式，这些公式只包含一个变量，并且是GL的定理。3将GL1转换为IL0设p为GL1的变量。我们将把这个变量转换成IL的封闭片段中的某个公式，它基本上使用D模态。很容易看出存在这样的公式在[8]（第5.4节）和[7]中给出了示例我们在这里使用的公式与[7]中公开的公式相同3.1我们翻译在本节中，我们将暴露一个翻译，减少定理GL1IL0，从而建立PSPACE硬度后者。这种翻译的动机主要是语义上的。我们将通过使公式TD QT在x处为真当且仅当xDp来编码关于p在世界x中是否成立的信息。在这种程度上，我们可以将两个新世界 x1和 x2与xRx1Rx2和4x2Sxx1惠xDp粘合在一起。因此，IL中的所有Sx关系都是充分独立的。这个想法应该激发我们为什么把p翻译成QQT→ TD QT。此外，通过这种方法，我们感兴趣的点，即原始点，变得很容易由公式QQT定义。因此，当量化我们感兴趣的点时，我们应该相对于我们的旧域。这就解释了为什么我们要把QA翻译成Q（QQT →A<$），其中A<$是A的翻译。我们将在3.3小节中看到，我们实际上并不需要粘合这么多不同的新世界来为模型中所有x的所有行为编写x的代码通过传递性，它只在模型的顶部添加一些世界4我们应该在模型的已有部分上添加更多的S x关系。对于这里的动机部分，我们只关注新添加的世界x1和x2。F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）47513.2翻译我们考虑GL1的公式到IL0的公式的以下翻译：（i）=(ii) pt=QQT →（TD QT）(iii) （A→B）<$=A<$→B<$(iv) （QA）<$=Q（QQT →A<$）引理3.1设A是 GL的一个公式，它只包含命题变量p.如果GL =A，则IL = A。证据 因此，假设IL/λA。 然后，存在IL模型M=<$W，R，{Sx：x∈W}，Dj，以及一个世界w∈W，使得M，wD/N=<$WJ，RJ，DJ定义为：(i) WJ：={w}<${x∈W：M，xDQQT}，(ii) RJ：=R（WJ×WJ），(iii) x D Jpi <$M，x D p<$（对于每个x∈WJ）。A[2]。 接下来，我们考虑GL模型我们指出定义WJ的并集可以是不相交的并集。使用N的定义，可以直接证明（通过公式长度的归纳），对于每个只包含命题变量p的公式B，N，xDJBi <$M，xDB<$（对于每个x∈WJ）。特别地，我们得到N，w/DJA。 因此，GL/CVA。Q引理3.1是我们将看到的等价的更容易的方向。特别是，引理允许一个简单的证明理论证明。证据所以，假设GL是A。我们知道GL有一个无割证明π（参见[6]中的系统G1），从而满足子公式性质。因此，π中的每个π至多包含变量p。这是一个简单的检查，证明只包含p保存在†。Q3.3模型构建在本小节中，我们将证明引理3.1的逆命题。引理3.2设A是 GL的一个公式，它只包含命题变量p.如果IL =A，则GL = A。证据通过IL和GL的完备性证明，我们知道，MONITOR[MONITOR]-型号MM |= A<$= AGL-型号N N| = A]，或等效地n∈N N，nDA=[1].M∈M M，mD A<$].52F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）47ee我我Q1我L1L在这种程度上，我们将展示GL模型的转换，产生所需的IL模型。设N：= N，W，R，D，N是GL-模型，A是GL-公式最多包含变量p。由于GL对于有限树型模型是完备的，我们确实可以假设Nhas是这样一个有限树型模型。通过E={e1，...，el}我们表示N中的端点集合，它当然是有限的。我们考虑E的两个不相交副本（也与W不相交），即Eb={eb，.， eb}和Eq={eq，...， eq}。 我们的想法是点eb和eq作为一个长度为2的小R链，端点ei大于5，我我模型中的每个旧点将满足QQT。当R是一致成立的时，则eachx∈M是R=-below一些ei（这里x R=y是“x R y <$x = y“的简写）。现在，我们考虑IL模型M=ΣW J，RJ，{SxJ：x∈W J}满足：(i) WJ：=WEbEq，(ii) RJ是R<${（e，eb）：e∈E}<${（eb，eq）：e∈E}的传递闭包，(iii) SJb={（eq，eq）}（对每个eb∈ Eb）.(iv) S·J·Q =（对于每个eq∈ Eq）。(v) 对于每一个x∈W，Sxj是n { y}上的最小传递和恢复关系|x RJy}，其中包含Sx和RJ都 限制于{y |xRJy}使得对于每个e ∈ E，（eq，eb）∈SxJ i <$ N， xDp且x R=e.很容易检查是否存在满足这些条件的唯一IL模型。我们注意到，在定义WJ时，我们使用了符号来强调这些并确实是不相交的，并且我们没有在M中引入赋值DJ，因为我们的目的仅仅是对封闭公式（如A†）求值。首先，我们注意到，在M中，我们可以模态地定义N中的旧点，因为{x∈WJ：M，xDQQT}=W.下一步是证明对于每个公式B它只包含命题变量p，N，xDJBi <$M，xDB<$（对于每个x∈W）。这个主张的证明是通过对B的长度的归纳来进行的。• 对T或T来说，这种说法是空洞的。• 如果B=p，我们有p<$=QQT → TD QT。通过构造，M，xDQQT。通过构造，在x的任何R-后继者中，可以通过Sx转移到某个eb，其中QT成立。因此，实际上，M，xDTD QT。• 另一方面，如果N，x D <$p，那么M，x D QQT。 但在这种情况下，我们可以通过R-跃迁到某个e。 通过构造，没有从eq到QT成立的任何点的Sx-转移，由此M，x/DTDQT。• 对于布尔连接词和模态算子Q来说，这个命题的证明都是平凡的。5W.r.t. 当然是R关系。F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）4753既然这个主张成立了，引理就紧随其后。Q4IL0的计算复杂度首先，我们得到IL的PSPACE硬度。4.1PSPACE硬度如果我们将引理3.1和引理3.2结合起来，我们可以看到GL1的约简我是0。也就是说，对于任何至多有一个变量p的公式A，我们有GL-100A⇔IL A.A.†.由于GL1是PSPACE完备的（见[3，定理7]和[9]），我们得到了本文的主要结果。定理4.1 IL 0的计算复杂性是PSPACE困难的。如果除此之外，我们还知道IL在PSPACE中，我们将获得PSPACE完全性。人们普遍认为，完全IL的复杂性确实是PSPACE完全的，但到目前为止还没有人证明这一点。 这是一个有点 作者惊讶地发现，在可解释性逻辑领域实际上没有复杂性结果。因此，这个简短的说明很可能是在各种可解释性逻辑中进一步研究在可解释性逻辑的其他成熟领域中非常自然的复杂性问题4.2关于IL0的一个范式定理IL0的PSPACE完备性并不先验地排除IL的范式定理的可能性。甚至可以想象，存在IL0的一些容易识别的范式类，使得IL0语言中的每个公式都等价于这些范式的小型布尔组合。在这种情况下，范式本身可能是容易的，甚至是容易比较的，但是对于一个任意公式，仍然很难（PSPACE）看到它实际上是什么范式的组合，它是可证明等价的。这些观察结果使得IL0引用[1] G. 布洛斯证明的逻辑。剑桥大学出版社，1993年。[2] A. Chagrov和M.扎哈里亚舍夫模态逻辑，牛津逻辑指南第35卷。牛津大学出版社，1997年。[3] A. V.Chagrov和M. N.里巴科夫需要多少变量来证明模态逻辑的PSPACE-硬度？《模态逻辑进展》第4卷，第71-82页。2003年。[4] D. de Jongh和G.贾帕里泽证明的逻辑。在S.R.巴斯，编辑，证明理论手册，逻辑和数学基础研究，第475爱思唯尔，阿姆斯特丹，1998年。54F. Bou，J.J.Joosten/Electronic Notes in Theoretical Computer Science 278（2011）47[5] P. 哈杰克和V。 Szavejdar。 关于可解逻辑闭模的正规形的注记。 StudiaLogica，50（1）：25 -28，1991.[6] D. 雷万特算术可证性的模态逻辑证明理论Journal of Symbolic Logic，46（3）：531[7] V. Cac ic和M. Vukov ic. 关于系统il闭片断正规形的一个注记。 数学通信，出现。[8] A.维瑟可解释性逻辑概述。模态逻辑进展，第307-359页。CSLI Publications，Stanford，CA，1997.[9] V. Szavejdar。单原子概率逻辑的判定问题。数学课上的一个小插曲。 Logic，42（8）：763 -768，2003.