构造性S4的对偶和公理系统的正式验证及其等同性证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记348（2020）61-83www.elsevier.com/locate/entcs构造性S4的对偶和公理系统，正式验证的等同性Lourdes del Carmen González Huesca1，2，3法维奥·EMiranda-Perea2，4 P.Selene Linares-Arévalo SeleneLinares-Arévalo2，5Departamento de Matemáticas，Facultad deCiencias UNAM，Circuito Exterior S/N，CD. Universitaria 04510，CdMx，墨西哥摘要本文给出了构造模态逻辑S4的两个演绎系统等价性的一个证明。 一方面，受Hakli和Negri从模态逻辑K的假设导出的希尔伯特式系统的启发，给出了一个公理化的特征 另一方面，Pfenning的判断重建和戴维斯通过所谓的双重自然演绎方法，区分有效，真实和可能的公式。这两个系统及其等价性的证明都使用CO q证明助手进行了正式验证。关键词：模态逻辑S4，构造性逻辑，自然演绎，对偶演算，形式验证，Coq1介绍模态逻辑在哲学和数学中的相关性已经很好地建立起来。此外，它在计算机科学中的重要性已经成熟（参见[14]从计算机科学的角度简要介绍模态逻辑）。例如，模态逻辑[6，4]对各种类型理论的一元和计算解释与并发和分布式计算[21，32]密切相关。这些应用需要一个验证过程，现在没有证明助理的帮助是无法想象的1 由DGAPA-墨西哥国立自治大学博士后研究金支助。2由PAPIME UNAM PE 102117提供部分支助。3 电子邮件地址：luglzhuesca@ciencias.unam.mx4 电子邮件地址：favio@ciencias.unam.mx5电子邮件地址：selene_linares@ciencias.unam.mxhttps://doi.org/10.1016/j.entcs.2020.02.0051571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。62L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61为了能够在这些软件程序的帮助下执行严肃的验证任务，我们需要为它们提供类似于人类（数学）思维的演绎方法的实现。这在模态推理的情况下提出了一个问题，其中文献中的典型演绎系统是公理化的或精心设计的演算（例如参见[26]）。此外，模态逻辑的一些已知的自然演绎表示是复杂的形式主义，它们要么涉及语义学，如标记演绎系统（[31]，另见[15]模态自然演绎系统的全面概述）;要么需要一些笨拙的约定，使它们难以在证明中实现，例如，在Fitch风格系统中使用特殊的子证明（框）和约定（[5]，[9]，[10，第1.6节]，[19，第34页]）或详细的情况，如[3]，用于构造性必要性的特定情况。在构造模态逻辑S4的情况下（见[29，1.5节]对构造模态逻辑的简要介绍），这些问题通过考虑Pfenning和Davies [24]提出的这种逻辑的判断重建而得到缓解。他们使用的方法遵循马丁-勒夫[22]的建设性哲学，通过假设和绝对判断。我们在这里的具体目标是证明这个系统（由Kavvos [17]称为对偶自然演绎）与Hakli和Negri[13]风格的公理系统之间的等价性。 这确保了对偶系统精确地对应于模态逻辑的更常见的公理形式。据我们所知，文献缺乏这样的证明（虽然，对于建设性的必要性的情况下，这已经解决了卡夫沃斯[17]和我们以前的工作[12]）。这种等价性产生了两个演绎形式主义的必要性，一个提供了一个友好的系统来执行实际的模态证明的建设性的必要性。如前所述，这与计算机科学应用有关，但也与围绕必然性的数学或哲学讨论有关，这些讨论需要开发实际的推导，而在公理系统中获得这些推导可能非常曲折。这里给出的结果扩展了我们以前关于构造必要性的工作[12]，增加了Q可能性算子作为原语，从而给出的模态是QA和QA，它们的通常含义分别是：“A是必要的”和“ 在建设性的背景下，没有双重的。 Q和Q模态算子之间的关系。公理系统的扩展是直接的，因为我们只需要添加与Q相关的公理。然而，在自然演绎的情况下，系统不仅需要处理公式，还需要处理模态判断（Atrue，A poss），说明公式可以是真的或可能的。 值得注意的是，这些限定词，以及有效性， 是根据Kripke的可能世界的语义直觉定义的这个特性允许我们在句法上描述模态知识，同时仍然对我们的机械化提出了一些挑战。这里采用的证明方法是从纯数学纸笔推理和机械化证明尝试之间的充分协同作用中获得的（参见定理3.1的证明以获得实际示例）。这条路让我们找到了一些新的证据L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6163N►⊥¬ ⊥↔ ¬ ¬技术.例如，本文提出的几个推理规则的可容许性不能用6个导子（的高度或长度）的结构归纳法来证明。相反，一个更简单的结构归纳法在已证明的序列的上下文上（例如见定理3.3和引理4.11的证明）。这是因为上下文被实现为归纳列表数据结构，而不是集合或多集合。此外，这里提出的大多数证明都大量使用了结构规则，这些规则的特定形状是从交互式验证过程中获得的。这是一个重要的区别，相对于其他演绎系统的治疗，结构规则是不存在的，或其使用是隐含的，一个功能，不能转换到CO q形式的发展。我们的论述开始于模态逻辑S4的公式和上下文的语法。公理系统在第三节中作了简要的讨论。自然演绎系统S4在第4节中得到了发展，关于它的替换性质的讨论出现在第5节中。这些系统的等价性在第6节中得到证明。最后，我们在第7节中给出一些最后的评论。完整的CO q开发可在https://bitbucket.org/luglzhuesca/mlogic-formalverif/src/master/S42公式和上下文我们在这部著作中采用了通过假设判断（序列）ΓA对模态可导性概念的表征，其中Γ是一个有限的假设集合，称为上下文，A是一个公式。这样的一个假设可以读作在这个简短的部分中，我们回顾了公式和上下文的定义。模态公式由以下语法生成A，B：：= p n|A→B|QA|QA其中pn表示从命题变量的无限供应中获取的元素注意到蕴涵是唯一的命题连接词，特别是我们既不考虑否定也不考虑常量。因此，我们将处理用必然性和可能性的模态算子扩展的最小逻辑[28]的蕴涵片段。这里考虑的逻辑被称为构造性的，因为它的特定Kripke语义在这里没有讨论（见[1]）。构造模态逻辑在几个方面不同于经典和直觉主义版本（见[16，27，29]）。例如，在经典逻辑中，对偶公理QAQA成立，但在直觉主义系统中不成立，其中包括公式Q作为公理，在构造模态逻辑中被拒绝的相同公式。上下文被实现为从空列表构建的公式的有限列表，在这里由y·表示，以及从givenonebyy生成新列表的构造器。6.如果导子被认为是树，则在高度上，如果它们是类似于本作品中的序列，则在长度上64L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61ZH在其右端添加一个新元素。它们的正式定义如下：r：：=·|Γ，A值得注意的是，在上下文中的公式A不一定是新公式。此外，两个上下文Γ和ΓJ的附加操作用Γ; ΓJ上的一个符号表示。这个操作是以明显的方式递归定义的。我们对上下文的实现选择，即上述语法的归纳定义，是由引言中提到的证明方法指导的。证明助手需要几个所谓的关于上下文的低级属性完成正式的核查程序。这样的性质，像列表的附加是结合的事实，对应于纸笔证明中使用的背景结果的类型，而无需进一步通知。它们的特殊形式被设计成能够以最佳方式自动化它们。然而，由于篇幅所限，在我们的论述中没有提到它们，但请参阅定理3.1证明后的注释，以获得一个实际的重要例子。3S4公理系统与通常的公理化演绎系统相反，这里提出的系统，最初由Hakli和Negri在[13]中为经典模态逻辑K给出，是专门设计来从假设而不仅仅是从公理或先前的定理导出结果的正如Hakli和Negri深入讨论的那样，这是能够验证演绎定理的关键，这有时被认为是模态逻辑无效的，因为在缺乏对使用假设的证明的精确定义的情况下，这些假设被认为是额外的临时公理，这是演绎定理无效的根源定义模态逻辑S4的公理集A是A1A→（B → A）A3. A→（B → C）→. B→（A→C）A2. A→（A → B）A →（A → B）A4（B → C）→. （A→B）→（A→C）KQ（A→B）→（QA→QB）QKQ（A→B）→（QA→QB）TQA→AQ TA→QA4 QA → QQAQ4 QQA → QA从这些公理中，我们通过下面的归纳定义生成一个模态可导性关系ΓS4A，其中，如前所述，L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6165H►→H►→H►→→H►→→H公司简介·H→→H∈H∈H→H∈ZH►→HHZH·H→→H→·是有限的公式列表。A∈Γ（HYP）Γ-4AA∈ A（AX）Γ-4AI^HS4AI^HS4A→B（MP）·I ^HS4A（NE c）I;让我们观察到，必要性规则允许我们仅当要装箱的公式是定理时才引入Q算子。这个限制解决了围绕演绎定理有效性的争论。此外，（MP）规则（MP）以乘法（独立上下文）风格陈述。原因是，这是建立S4与通常的公理系统（即那些不处理假设的公理系统）的对应的自然方式。这一选择与Kavvos [17]的处理不同，也对形式验证提出了一些挑战，正如我们以前的工作[12]所讨论的那样。让我们也注意到，因为公理Q-T存在，所以不需要涉及Q算子的推理规则（尽管参见下面的引理3.6）。下面讨论演绎定理和其他可接受的规则定理3.1（推论）F或任意上下文Γ与A，B的位置，若Γ， A∈HS ~ 4B，则ΓHS4A→B。证明 结构归纳7 关于Γ，AS4湾（HYP）的情形接着是对假设BΓ，A的分析。出现两种情况：B是A或BI. 在第一种情况下，S4 BB直接来自公理A1和A2。对于第二种情况，BΓ意味着ΓS4B.从这片土地上S4 B（A）B），这是公理A1的一个实例，我们得到期望的ΓS4A B乘以（MP）。对于公理规则（AX）的情况，证明成功了（MP）和一个充分的公理A1的例子。对于（NE c）规则，目标是证明ΓS4 一QC，假设S4 C.这是由公理A1的（MP）实现的，形式为：S4 QC（A）QC），以及由（NE c）假设得出的ΓS 4QC最后，对于规则（MP）的情况，我们有Γ 1S4 C（1）和Γ2S4 CB（2），其中Γ 2; Γ 1= Γ，A.从这个方程中产生了两种情况：要么Γ1为空，或者它的最后一个元素是A(i) 如果Γ 1=，则Γ，A= Γ 2，假设（1）变为S4C。根据（2），归纳假设得到ΓS4一（C）B）。 这个公理与公理A3的一个实例一起，通过（MP）产生了公理S4C（AB）。最后，S4 一B是通过将（MP）再次应用于最后一个矩阵而获得的。 假设（1）。[7]这是CO q机械化的实际的本土归纳原则。这个证明也可以看作是对推导长度的归纳66L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61.·H2O →1 2 HS4ZH∈∈·公司简介(ii) 如果A是Γ 1的最后一个元素，则存在另一个上下文ΓJ，使得Γ =ΓJ，A. 这意味着r=r; rJ。 由（CB）（AC）→（A→B）（公理A4）和假设（2）得到了Γ 2<$S4（A→ C）→（A→B）. 最后，由y，y（MP）（来自应用于（1）的归纳法）得出：Γ2;ΓJ<$HS4A→B，其中h与Γ<$HS4A→B相同.Q值得注意的是，演绎定理在没有进一步约束的情况下也是有效的，这是由于必然性规则的具体定义已经强制了上述证明提供了一个从人机交互中获得的替代演示的例子。一个源于[13]中给出的一个已经很好建立的证明的机械化尝试。在上述证明中出现的两个案例分析实例在CO q中借助于两个先前形式化的低级结果被机械化，即，如果BΓ，A，则BΓ或B恰好是A的事实;以及关于上下文分解的引理， 如果r2; r1= r，A，则r1为空且r2= r，A，或者存在上下文rJ使得r1= rJ，A且r2; rJ= r。演绎定理的逆蕴涵，也被称为分离原理，也很容易实现。定理3.2（分离原理）对任意上下文Γ和A，B命题，若Γ<$HS4A→B，则Γ，A<$HS4B.通过对该论文中的By（MP）和A.Q从严格的角度来看，在本节中的序列A→S4A是不正确的（A不是一个文本）。而我们应该使用·， AHS4A。在我们中间，产生了Σ i，AS4B，并且在上下文中使用了Γ i，A= Γ，A这一事实的简单等式推理产生了期望的Σ i。 这又是一个低层次的正义化过程所需要的CO q。由于上下文是列表，演绎定理允许我们在上下文中只解除最后一个假设。为了能够解除任何假设，我们必须要么隐含地使用结构规则，要么证明一个概括。我们选择第二种选择，并详细说明证明，虽然很简单，但据我们所知，证明推理规则的可接受性的新方法是当然，这里的新之处在于使用列表（上下文）上的一个简单归纳来证明规则的可接受性定理3.3（广义演绎定理）设Γ， ΓJ 成为背景，A、B是命题。规则是可以接受的I，A;IJ，H，S4BI;I; I^HS4A→B（GDT）L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6167HZH证明 关于ΓJ的基本情况ΓJ=·正是演绎定理3.1。对于归纳步骤，假设Γ，A;ΓJ， C<$HS4B，其中根据定理3.1，h暗示Γ，A;ΓJ<$HS4C →B。的I.H.得到n owr;rJHS4A→C →B。由此通过（MP）得到公理A3的一个充分的例子，我们得到Γ;Γj∈HS4 C →A→B。最后，由定理3.2得出结论：Γ;ΓJ， C∈HS4A→B.Q由于推导定理及其逆定理的可用性，得到了系统S4我们提出了其中的下两个，关于上下文置换和收缩，这将需要稍后来显示公理和自然演绎方法之间的等价性S4。引理3.4（结构规则）对于任何上下文Γ， ΓJ和公式A，规则I; I;I;I;IΓJ; ΓHS4A是可以接受的Γ; Γ βHS4A（CTX-cONT）Γ-4A在每种情况下证明关于Γ的归纳法。定理3.3和分离原理将是非常有用的。Q重要的是要注意，上述规则保证了在两个上下文的置换下并通过收缩重复的上下文来保持推导过程。另一方面，追加操作;既不是可交换的，也不是幂等的。接下来，我们证明了两个规则，允许导出模态公式，即钻石引进规则和neccesitation规则的推广时，上下文是非空的，但只包括盒装公式的容许性。定义3.5给定上下文Γ =[A0，.，A n]，我们将盒装上下文Γ Q定义为ΓQ=[QA0，.，QA n]。引理3.6（模态引入规则）对于任何上下文Γ， ΓJ和公式A，规则ΓQHS4AΓHS4A是可以接受的rQ; rjHS4（GEN NEc）QA伊尔-4（DIA）QA证明对于第一个规则，通过（CTX-P）规则，它表面上表明，ΓJ; ΓQS4QA，这是通过对Γ的归纳法来验证的。第二个规则可以直接从公理QT和（MP）导出。Q这就完成了我们对S4公理系统的介绍。接下来我们讨论自然演绎形式主义。68L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61N| 中国4中四自然扣减这里讨论的S4的形式主义，记为S4，是一个自然演绎系统 在文献[15]中，我们称之为S系统，在这里命题是被判断性地分析的。它对应于Pfenning和Davies在[24，第5节]中提出的关于必然性和可能性的形式系统，这是一部基于马丁-洛夫类型理论[23]的哲学发展的著作。这种形式系统利用直观的语义概念隐含在一个本质区别的三个基本判断，其目的是描述模态知识没有明确使用的世界。 的 一个真正的判断是指如何在假设的判断下，即在现实的给定世界中验证A。一个有效的代表，通过直言判断，一个命题，其真理不依赖于真正的假设，也就是说，一个命题，在任何给定的世界。最后，Aposs代表一个可能的真理，这意味着A必须是假言判断中唯一可用的真假设，从而代表一个特定的世界，在这个世界中，我们除了A的真理之外什么都不知道。重要的是要注意到，这些判断的定义仅仅是直观的，因为下面没有涉及形式语义学。相反，我们可以使用全局、局部和唯一等标签。有效假设和真实假设之间的区别与拟合的局部和全局假设的概念有关[8，p.177]。但我们更愿意保留[24]的术语。我们的自然演绎方法处理形式为Δ ΓS4J的序列，其中前因Δ和Γ分别是有效和真实假设的上下文，而后继J是结论判断，这是对真理或可能性的判断，正式定义为：J：：= A true|一种可能让我们观察到，语境包含公式，而不是像原始表述中那样包含判断，在原始表述中，从严格的观点来看，只有一个语境被分成两部分，这在CO q中是一个操作起来相当复杂的选项。相反，我们的选择简化了上下文和序列的表示和实现。例如，不需要显式判断有效性（A valid），因为上下文是作为两个不相交的列表实现的，使得真和有效标签的使用变得多余。也就是说，元变量Δ和Γ都表示由第2节中的语法生成的列表。这特别意味着Δ可以作为正确的语境出现在一个动词的先行词中（见命题5.4和5.5），并且对Δ或Γ的成分没有句法限制。例如，一个盒装公式QA可以在Δ和Γ中出现（但请参见第4.2节，了解在上下文中移动公式Kavvos在[17]中将这种分离的语境此外，既不需要明确考虑可能性假设，因为它们是由唯一的真假设建模的，也不需要明确考虑作为结论的有效性判断，因为它们由判断QA真表示。与原始提法的另一个区别在于，L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6169NS4NS4Δ ΓB真作者提到，他们的系统有一个显式的命题推理，只有一个隐式的判断推理，说可导性关系受制于Aposs中包含Atrue。实现此功能的更方便的方法是通过一个显式规则（TP），它将True判断转换为Possibility判断。在这里，可导性关系通过下面的推理规则给出的归纳定义来机械化，这对应于可导性的浅嵌入。因此，规则（TP）的显式声明和使用是强制性的。 这条规则，可以被认为是一个介绍，在[24]中作为一种替代表述被提到，它不如当前系统有效，只包括模态算子的定义和规则（TP）作为Aposs判断的引入。系统NS4由以下推理规则定义：Δ |Γ，A; Γ J<$ A true（T HYP）Δ，A; Δ J|ΓAtrue（V HYP）Δ |Γ，ANS4 BtrueΔ |ΓNS4 A → B true（→ I）Δ |ΓNS4A→ B trueΔ|铁卫S4 Atrue（→E）| ►NS4Δ|·S4AtrueΔ |ΓNS4QA true（Q I）Δ |ΓNS4 QA trueΔ，A|铁卫S4 Ctrue（QE）Δ|铁卫S4 CtrueΔ |ΓNS4 QA trueΔ，A|铁卫S4 Cposs（QE-POSS）Δ|铁卫S4 C阳性Δ|铁卫S4 A真实（TP）Δ |ΓNS4A poss（QI）Δ |ΓNS4 A possΔ |ΓNS4QA trueΔ |ΓNS4 QA trueΔ |AZNS4 阳性（Q和E）Δ|铁卫S4 C阳性我们有两个起始规则对应于这两种类型的假设，它们以最一般的方式陈述，允许我们推断属于上下文的任何公式，而不仅仅是第一个或最后一个。引入必要性规则（QI）通过一个范畴判断准确地捕捉了有效性的定义，而必要性排除规则（QE）则表现为一个替换或切割规则，其中公式QA被用作有效假设中的引理A，以证明关于C的结论判断。判断Aposs由规则（QE-POSS）、（TP）、（QI）和（QE）用有效判断和真实判断的组合来解释。给出了Q算子的第二个消除规则，以得出局部真值为：70L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61NCposs，这个规则利用了形式为QAtrue的引理。Q算子的引入和消去规则实际上是[24]中给出的可能性的定义下面让我们展示S4中对应于S4的模态方案公理的推导。实施例4.1 [方案T]|公司简介 QA→Atrue在NS4中是可导出的。1.·|QAWINS4 QAtrue（THYP）2.一|QANS4 A true（V HYP）3.·|QANS4A true（Q E） 1，24.·|公司简介 QA→Atrue（→I）3实施例4.2 [方案4]|·QNS4QA → QQA真可在N S4。1.一|·INNS4A true（V HYP）2.一|·CSNS4QA true（Q I）13.一|QANS4QQA true（Q I）24.·|QANS4QA true（T HYP）5.·|QANS4QQA true（Q E）4，36.·|公司简介 QA→QQAtrue（→I）5实施例4.3 [方案K]|·NS4Q（A→B）→（QA→QB）真可在N S4中导出。1.A，A→B|·INNS4A true（V HYP）2.A，A → B |A → B true（V HYP）3 .第三章。A，A→B|·NS4B true（→ E） 二，一4.A，A → B |Q（A → B），QA NS4 QB true（Q I）35.一|Q（A → B），QA <$NS4 Q（A → B）true（T HYPER）6.一|Q（A → B），QA NS4 QB true（Q E）5，47.·|Q（A → B），QA NS4 QA true（T HYP）8.·|Q（A→B），QANS4QB true（Q E）7，69.·|Q（A→B）NS4QA→ QB true（→ I）810.·|公司简介 Q（A→B）→（QA→QB）真（→I）9L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6171实施例4.4 [方案Q]|公司简介 A→QAtrue在NS41. ·|ANS4 A true（T HYP）2. ·|APOSS（TP） 13. ·|ANS4QA true（Q I）24.·|公司简介 A→QAtrue（→I）3实施例4.5 [方案Q4]|公司简介 QQA→QAtrue可在N S4。1.·|ANS4 A true（T HYP）2.·|APOSS（TP）13.·|QANS4 QA true（T HYP）4.·|QAPURSNS4 A poss（Q E）3，25. ·|QQANS4 QQA true（T HYP）6. ·|QQANS4 A poss（Q E）5，47. ·|QQANS4 QA true（Q I）78.·|公司简介 QQA→QAtrue（→I）8实施例4.6 [方案QK]|公司简介 Q（A→B）→（QA→QB）真可以在NS4中导出。1.A→B|ANS4A→ B true（V HYP）2.A→B|ANS4 A true（T HYP）3.A→B|ANS4 B true（→ E）1，24.A→ B |A/CNS4 B poss（TP）35.A→B|Q（A→B），QANS4 QA true（T HYP）6.A→B|Q（A→B），QA NS4B poss（Q E）4，57.A→B|Q（A→B），QANS4 QB true（Q I）68.·|Q（A→B），QA→NS4 Q（A→B）true（THYPP）9.·|Q（A→B），QANS4 QB true（Q E）7，810.·|Q（A→B）NS4 QA→QBtrue（→I）9十一岁·|公司简介 Q（A→B）→（QA→QB）true（→I）10最后一个更详细的例子涉及使用这两个规则的Q消除。72L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61示例4.7：|公司简介 Q（A→B）→Q（QA→QB）真可导L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6173在NS4中。1.A→B|Q（A→B），QA，ANS4A→ B true（V HYP）2.A→B|Q（A→B），QA，ANS4A true（T HYP）3.A→B|Q（A→B），QA，ANS4B true（→ E） 一、二4.A→B|Q（A→B），QANS4QA true（T HYP）5.A→B|Q（A→B），QANS4B true（Q E）4，36.A→B|Q（A→B），QANS4B poss（TP）57.A→B|Q（A→B），QANS4QB true（Q I）68.A→B|Q（A→B）NS4QA→ QB true（→I） 79.A→B|Q（A→B）NS4QA→ QB poss（TP）810.· |Q（A→B）NS4Q（A→ B）true（T HYP）11.· |Q（A→B）→NS4QA→ QB poss（Q E-POSS）10，912.· |Q（A→B）NS4Q（QA→ QB）true（Q I）1113岁· |·NS4Q（A→B）→Q（QA→QB）真（→ I）124.1容许规则在这一节中，我们提出了一些有用的可接受规则，这些规则虽然很自然，但据我们所知，除了引理4.10之外，它们是从与CO q证明助手的充分相互作用中再次获得的原始贡献。下面的语句是我们的形式化中所包含的语句的一个简略表示在那里，不同的规则是类似的陈述，分别为有效和真实的上下文制定，并结合真实和可能的结论。引理4.8（弱化）设Δ，Γ，Γ J是上下文，A，B是公式，J是结论判断. 规则Δ |Γ; Γ jNS4JΔ |Γ，B; ΓjNS4J是可以接受的（WEAK-THYPS）Δ; ΔJ|ΓNS4 JΔ，B; ΔJ|ΓNS4J（WEAK-VHYPS）证明每个规则都证明了结构归纳对给定的推导。Q接下来我们证明规则（→I）和（QI）是可逆的。引理4.9（→和Q的反演）设Δ，Γ是上下文和A，B公式。74L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61规则Δ|铁卫S4 A→Btrue（DET）Δ |Γ，ANS4 BtrueΔ |ΓNS4QAtrue（Q I-I N v）Δ |ΓNS4A poss是可以接受的分离规则（DET）是弱化和（→E）的直接结果。利用规则（TP）和（QE）证明了Q-引进的逆.Q引理4.10（交换）设Δ，Γ，Γ J是上下文，A，B是公式，J是结论判断。规则Δ |Γ，A，BNS4 JΔ |Γ，B，ANS4J是可以接受的（EX cH-THYPS）Δ，A，B|ΓNS4JΔ、B、A|ΓNS4J（EX cH-VHYPS）证明J是C真的情况下，直接证明与削弱的帮助下，而那些Cposs证明通过归纳对给定的推导。Q下一个引理给出了引理4.8和4.10的弱化和交换规则的一些推广。引理4.11（结构上下文规则）设Δ，Δ J，Γ，Γ J是上下文，A是公式，J是真的或可能的判断。规则• 上下文弱化：Δ |ΓNS4JΔ |Γ; ΓjNS4JΔ |ΓNS4J(TCTX-WEAKR）(VCTX-WEAKR）Δ |ΓNS4JΔ |ΓJ;ΓNS4JΔ |ΓNS4J(TCTX-WEAKL）(VCTX-WEAKL）Δ; ΔJ|ΓNS4 J• 上下文交换：Δ |Γ，A; Γ J<$NS4JΔ|（r; rJ），ANS4J是可以接受的（cTX-EXcH-cONc）ΔJ; Δ |ΓNS4JΔ|（r; r J），ANS4JΔ |Γ，A; ΓJ<$NS4J（cTX-EXcH-SNOc）证明每个弱化规则都是通过对上下文Γ J和Δ J的归纳来证明的。交换规则的证明，当J是Cposs时，通过在前提上的结构归纳进行，否则通过在上下文ΓJ上的归纳进行。接下来我们展示（ctx-excH-CON c）的情形.基本情况是直接的，对于Γ，A;·=（Γ;·）， A，因此b个序列，前提和结论是相同的.对于归纳步骤，我们假设Δ|（Γ，A）;（Γ J，B）NS4C为真，需要证明Δ|（r; r J，B），A ∈NS4 C true. 从我们得到的假设来看L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6175|中国→|N→N|►→NN1998年，张晓刚（E）。IH现在产生Δ（Γ; ΓJ），AS4 BCtrue根据规则（D ET）（引理4.9），我们得到Δ（Γ; ΓJ），A，BS4 C正确。 菲-最后通过交换（引理4.10）和一些低级的等式推理，我们得到Δ|（r; rJ，B），A∈NS4C true.Q类似于上述规则，对于有效假设的上下文的情况，可以用类似的方式证明现在我们可以证明蕴涵引入规则的一个推广，它允许我们排除任何真实的假设。引理4.12（广义蕴涵引论）设Δ，Γ，Γ J为上下文，A，B公式. 规则是可以接受的Δ |Γ，A; ΓJ<$NS4BtrueΔ |Γ; Γ J<$NS4 A → Btrue（GEN→ I）充分利用交换规则，证明了关于ΓJ的归纳法Q4.2上下文之间的公式转换我们接下来讨论一个在[24]中没有的结果，即上下文中的转移过程。这是一个推理原则，它捕捉了有效公式是必然真理的事实，这意味着属于有效上下文的公式A可以被认为是必然真理。这是通过从有效假设的上下文中删除A，同时将QA添加到真假设的上下文中来在另一个方向上，我们可以通过将不带框的公式移动到有效假设的上下文中来摆脱真实假设上下文中的框式从而将一个封闭的假设转化为一个纯粹的命题假设。命题4.13（有效公式是必然真理）设Δ，Δ J，Γ是上下文，A是命题，J是结论判断。规则是可以接受的证明 关于ΔJ的归纳。Δ，A; ΔJ|ΓNS4JΔ; ΔJ|Γ，QANS4J（VAL TO TRUE）如果J是C真，那么基本情况是（QE）消除规则的结果，适当地使用弱化。否则，基例通过前提上的归纳来解决。Q我们可以将上述性质的应用以这样一种方式进行验证，即有效公式的上下文变为空，这种选择对于S4中的实际证明构造是不够的，但是在我们的演绎系统76L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61→推论4.14设Δ，Γ是上下文，J是结论判断. 如果Δ |ΓNS4 J然后，|J.作为另一个推论，我们得到一个规则，允许有效假设的放电。推论4.15（有效性的蕴涵引入）设Δ，Γ是语境，A，B是命题。规则是可以接受的Δ，A; ΔJ|ΓNS4 B trueΔ，Δ J|ΓNS4 QA → B true（→I VAL）证明 关于ΔJ的归纳。Q上述规则对于条件的某些特殊解释似乎很重要，例如在宽松逻辑的情况下，宽松蕴涵可以定义为QA B（见[24，第7节]）。此外，根据以下命题，该规则是可逆的。命题4.16（对盒装公式的分离）设Δ，Γ，Γ J为上下文，A，B为公式。规则Δ;ΔJ|ΓNS4QA → B true（Q D ET）Δ，A; Δ J|ΓNS4 B true是可以接受的证明使用（→E），（QI）和弱化。Q这个命题允许我们证明命题4.13的逆规则的以下版本。命题4.17（必要真理是有效的）设Δ，Γ，Γ J是语境，A是命题，J是判断。规则是可以接受的证明 关于ΓJ的Δ |Γ，QA，ΓjNS4JΔ，A| Γ，Γ jNS4J（TRUE TO VAL）当J是C真的情况下，直接证明，而Cposs的情况下，证明了通过归纳对给定的推导。Q命题4.13和4.17一起提供了上下文之间的公式转移原理。这是一个重要的工具，为实际发展的推导，一个让我们能够操纵模态公式的上下文中考虑他们L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）6177有能力。N作为纯命题（非模态命题），反之亦然。这个特性大大简化了证明的实际构造，有时还允许我们用一个更简单的命题推理来代替模态推理。就像下面的例子一样，这里不需要使用规则（QE）提供的模态推理例4.18.|公司简介 Q（A→B）→Q（QA→QB）真的是推导出来的。1.A→B，A|A→ B true（V HYP）2.A→B，A|·INNS4A true（V HYP）3 .第三章。A→B，A|·NS4B true（→ E）1，24.A→B，A|公司简介 QB true（Q I）35.A→B|·QSNS4QA→ QB true（→ I V AL）46.A→B|公司简介 Q（QA→QB）true（QI）57.·|公司简介 Q（A→B）→Q（QA→QB）真（→I VAL）6接下来，我们讨论另一个强大的工具，实际推导，即替换或削减规则。5NS4中的替换属性在本节中，我们证明S4具有替换或复合性质（类似于微积分中的切割规则），这确保了推导在复合下是封闭的，或者从更实际的角度来看，保证了借助于辅助引理组织的证明的正确性（假设被切割或替换，有利于实际证明）。由于系统区分了两种假设或结论，因此通过遵循特定假设（有效或真实）和特定结论判断（真实或可能）的组合，可以获得多个替代属性。组合的总数是八个，但只有五个是适当的，并且已经由Pfenning和Davies [24，5.1节]给出，其中的证明虽然没有出现，但提到是通过前提上的结构归纳法。然而，在我们的开发中，五个证明中只有两个遵循这种方法，而其他的则直接从原始和结构规则中获得。规则的枚举是在[24，定理2]中给出的前两个原则涉及一个辅助引理A，它被证明为真（意味着判断A为真），并被用作真或有效的假设，以得出判断C为真的结论。引理5.1（真结论的替换）设Δ， ΔJ， Γ， ΓJ是上下文78L.C. González Huesca et al. /Electronic Notes in Theoretical Computer Science 348（2020）61→并且A、C是公式。 规则Δ |ΓNS4 A trueΔ |Γ，A; ΓJ<$NS4C真（SUBST-1）Δ |Γ; Γ jNS4 CtrueΔ|·NS4AtrueΔ，A;ΔJ|ΓNS4C真（SUBST-3）Δ; Δ J|ΓNS4C true是可以接受的证明规则（SUBST-1）是直接从（→E）使用上下文弱-ening（TCTX-WEAKR）和（GEN →I）。 规则（SUBST