加名字核证逻辑的极小系统，本文主要内容关键词为：极小论文,逻辑论文,名字论文,系统论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
美国逻辑学家M.斐汀在2010年对核证逻辑与混合逻辑的组合进行了初步尝试，给出了第一个混合版本的核证逻辑系统JT及其完全性和显式性定理的证明。(cf.Fitting，2010)由于技术原因，这个逻辑在证明内在化定理时要用到对自返性典范的事实公理，所以它还不是这一族逻辑中最小的系统。本文旨在把斐汀建立的逻辑弱化到核证逻辑J的对应，给出该族逻辑的一个极小系统，进而简化系统JT的元定理证明，从而解决斐汀在其文章最后提出来的一个主要问题。 一、背景 混合逻辑(hybrid logics)“内在化”(internalize)了其自身的语义学：
它的意思是说，公式
是在系统内可证的，当且仅当公式X在模型中的可能世界i上为真。句法中添加的名字i指称唯一一个可能世界。名字的添加促进了模态逻辑完全性理论、内插定理以及其他基础理论的发展。最近出现的核证逻辑(justification logics)家族则核证了自身的证明结构：
这种“内在化”的核证是说，公式t：X在系统内是可证的，当且仅当t是公式X在系统内的证明的一个显式性抽象。这两种逻辑各自将自身系统的语义和句法成分内在化，如果能把这两个逻辑的性质结合到一起，得到的逻辑将更充分、直接地将逻辑的内部性质与所要表达的对象联系起来，拥有更强的表达力。2010年，斐汀建立了第一个组合混合逻辑与核证逻辑的混合核证逻辑系统JT。它带有事实公理“u：X→X”(对应于认知模态逻辑的真值公理，直观上是说“任何有证据的信念都是真的”)，所以对所有自返框架类具有强完全性，也就对应于普通模态逻辑中的逻辑T。 斐汀之所以要在该逻辑中加入事实公理，乃是因为核证逻辑通常需要具备一个重要的性质——内在化。一般来说，只有有了这个性质，在核证逻辑与模态逻辑之间起着对应关系的性质——显式性(realization)才会成立。为了证明这个逻辑的内在化定理，斐汀加入了事实公理，已顺利得出证明内在化定理的一个重要组成部分。当然，对于这个证明而言，加入事实公理有些牵强。斐汀自己也意识到了这一点，他认为至少需要下面两个公理模式才能证明出内在化定理：
。但实际上并非如此，我们现在就来做这样一个工作。 二、基本混合核证逻辑 基本混合核证逻辑是斐汀将混合逻辑的一部分与核证逻辑进行组合得到的产物。我们与斐汀的设置保持一致，依然不为这个逻辑预设带名字的世界。唯一不同之处是他认为由于技术原因而只能选择生成JT的混合版本，而我们将弱化到J的混合版本；这是本文的主要贡献。我们建立的弱化后的逻辑称作“基本混合核证逻辑J”(basic hybrid-J)。 1.语言与公理 混合核证逻辑的语言是将核证逻辑J的语言与混合逻辑H(＠)的部分语言结合在一起，再外加一些符号所得到的。我们今后用
来指称这种语言的一个极小版本。首先定义核证项：
核证项是核证逻辑独有的新元素，是有两个算子即应用“·”和加“+”的证明多项式，代表着公式的可证性抽象。核证项由核证常项和核证变项构成。核证常项通常用
等表示，指代系统不再继续分析下去的原子性核证，核证变项用
等表示，指代不明确的核证。对于应用算子，如果t是X→Y的核证并且u是X是的核证，那么t·u就是Y的核证；加算子组合核证，例如t+u就核证了所有t所核证的和u所核证的。一个核证项是封闭的是说它不包含核证变项。新添加的符号包括核证项和两个核证项算子，它们与名字有关：对于一个名字i，存在一个核证常项
和两个核证算子
，分别称作远程事实核查、远程核证正检查和远程核证负检查。关于它们的核证项构造规则是：如果t是一个核证项，那么
也是。我们的公式定义如下：
除常见的命题变元、永假式、否定式、析取式，公式还包括名字i，核证断言式t：X(简称“核证式”)和可满足式
；其他命题联结词定义如常。名字(nominal)来自混合逻辑的语言；为了区别于命题变元，名字用i、j、k指称。对于每一个名字i，存在着一个前置算子
称作可满足算子，意思是说，
在模型的任意点上为真当且仅当X在i所命名的点上是可满足的；i所命名的这个点在模型中是独一无二的，也就是说，每个名字只能命名一个可能世界。核证式来自核证逻辑，需要额外的构造规则，即如果t是一个核证项并且X是一个公式，那么t：X也是一个公式。这条规则的意思是说，t：X断定X是t作为其核证所确定的事件。记法方面，我们设定冒号有更强的结合力，因此尽可能略去括号，比如，t：X→X实际上表示的是(t：X)→X。 2.公理系统。基本混合核证逻辑J的公理(模式)包括：
前八条公理来自普通混合逻辑(它们的直观意义可参看：Areces et al，2007，Blackburn et al 2001的相关章节)，公理9-10来自核证逻辑，其直观意义与各自的算子意义相一致。后三条公理对应三个新添加的核证项。从技术角度来看，它们及其规则的设置是为了帮助证明内在化定理中混合核证逻辑的可满足式(形如
)部分；但斐汀认为它们在哲学上也是有根据的。他引用维特根斯坦的话说：“在逻辑空间中的诸事实就是世界。”(维特根斯坦，1.13)公理11就是要求基本事实属于某个世界的真实性必须得到核证。注意，它是我们唯一一个非公理模式的情况，其中p只代表命题字母而不能被任意公式所替换。如果公理11是公理模式，那样得到的逻辑会更强，证明内在化定理也会更加方便。而之所以没有这样做，一是为了尽可能地生成一个逻辑的极小版本，更重要的是对
的定位，它相当于是我们对世界i的认识。如果换作公理模式，那意味着我们对世界i是全知的，认知逻辑要尽量回避这个性质。如果断言说t在世界i上核证某个X，那么这个发生在某个带名字的世界上的核证的真实性，需要在整个模型的每一个可能世界得到检验，这就需要一个进一步的证据，公理12-13即来源于此，
相当于所有核证式是否存在在世界i上的证据。推理规则中，＠必然化是模态必然化规则的一个变体，叠置公理必然化规则体现了常项符号作为核证不再被进一步分析的性质，也就是说，公理和常项符号本身的用法是不再讨论的。假设X是一个公理，用上面的规则得到
的可证性。我们会把
看作X的一个核证，而
是对
核证了X这一事实的核证。因为一条公理无论在哪个世界上都仍然是公理，我们希望在带名字的世界上的这些公理可以有证据来予以确定，这就是叠置远程公理必然化规则设置的理由。利用这一规则可以不断增加这个公式的长度，并且利用下标将其有序排列，这样做在具体操作中会有帮助，为此，我们引入常项规范的概念。 定义1 对于一个逻辑L而言，一个常项规范CS是满足下面封闭性条件的一个形如
的公式的集合，其中每一个
是核证常项而A是逻辑L的公理。 封闭性：如果
。 简单来说，CS规定了哪些常项可以用在哪些公理上。通常根据集合的大小，常项规范根据大小可以分为很多种。我们这里要求常项规范是“公理适宜的”，这是说，如果X是一个公理模式的实例，那么对于任意自然数n存在着常项
。 3.内在化 斐汀在他的文章中给出了核证逻辑basic-hybrid JT的内在化证明，但他借助了事实公理，而且认为至少需要下面两个公理模式才能证明出内在化定理：
实际并非如此。我们现在来证明这个定理，我们的证明大部分内容是与斐汀原文一致的，只是在归纳证明的一个步骤上不使用事实公理而从其他现有公理中得出结论。
接下来的证明在内在化定理的证明中起着重要作用，证明方法是施归纳于公式的复杂度(这个归纳证明的归纳基始与斐汀的相同；参见Fitting，2010中的引理3.1)。归纳步骤共分六种情况，分别是蕴涵式、可满足式和形如w：Y的公式以及它们的否定情况。另外四种情况我们和斐汀原文的证法相同，不同之处在于可满足式及其否定，斐汀的证明借助事实公理而我们避开了事实公理。 命题3 对于每一个公式X，不仅仅是原子式，以及每一个名字i，存在封闭核证项t和u使得
在基本混合核证逻辑J中是可证的。 证明：施归纳与X的复杂度，包括联结词、＠符号和核证词在公式中出现的次数(归纳基始已由斐汀证明；参见Fitting，2010的引理4.1)。因为要证明两个公式的可证性，而公式的性质分为三种，我们的归纳步骤包括六种情况。X是Y→Z的正子情况和X是Y→Z的负子情况已经由斐汀给出证明(参看Fitting，2010)。我们接下来给出的证明不使用事实公理：
(3)X是w：Y的正子情况：远程核证正检查公理足以证明。 (4)X是w：Y的负子情况：远程核证负检查公理足以证明。证完。 内在化定理的证明细节已经由斐汀给出，这里仅为基本混合核证逻辑J重述类似的结果如下： 定理4(内在化定理)如果X是基本混合核证逻辑J的一个定理，那么存在一个封闭的核证项t使得t：X也是一个定理。 4.语义 一个基本混合核证逻辑的模型M是一个四元组〈G，R，ε，V〉，其中G和R分别是论域和可达关系，V是赋值，把每一个命题字母指派到论域的一个子集上，新的条目是ε，它被称为“可容许核证函数”或者“证据函数”，是把某些点的集合指派到每一个核证项t和每一个公式X上，如果一个核证项t在某些点上被认为是公式X的相关证据，ε(t，X)就指代论域中的这些点的集合。我们说ε(c，X)在某个点u上为真是说u∈ε(c，X)，说ε满足了常项规范CS是说，如果c：X∈CS，那么ε(c，X)=G。 因为新公理的加入，模型必须有一些条件上的限制。对于·运算和+运算，可容许核证函数ε必须满足这两个条件： 弱化：ε(s，X)Uε(t，X)
(s+t，X) 应用：ε(t，X→Y)∩ε(u，X)
ε(t·u，Y) 因为我们的模型是一个混合模型，所以我们必须保证V(i)的值是一个单元素集，这是符合混合逻辑模型的条件。而因为我们没有假设带名字的世界的存在性，所以我们不把名字满射映到论域上。最后，因为增加了三个核证项上的运算，可容许核证函数ε的定义必须扩大：
接下来我们定义可满足关系，其中出现的符号│├用法如常，根据核证逻辑的记法传统，这里用Г、Δ这类符号来指称G中的元素。 M，Г│├p当且仅当Г∈V(p)，其中p是一个命题字母 M，Г│
⊥ M，Г│├X→Y当且仅当M，Г｜
X或者M，Г│├Y M，Г│├t：X当且仅当M，Δ│├X，其中对于所有的Δ∈G都有ГRΔ并且Г∈ε(t，X)。 M，Г│├
当且仅当M，V(i)│├X。 前三个条款解释如常，最后一个条款来自混合逻辑，对应于可满足算子的性质。要注意的是第四个条款，它要求t：X在Г上为真当且仅当X在Г的所有可及世界Δ上为真和t在Г上核证X的证据这两个条件同时满足。第四个条款还有一个强化的版本，它使得模型满足“彻底解释性”，这个性质是说对于ГRΔ中的所有Δ∈G，如果M，Δ│├X，那么M，Г│├t：X。也就是说，万事皆有因。 5.完全性和显式性 在这一节中我们先定义几个概念：一个模型M=〈G，R，ε，V〉在Г∈G上满足常项规范CS是说对于所有CS中的公式t：X，Γ∈ε(t，X)。而模型M=〈G，R，ε，V〉满足CS是说在每一个ΓεG上满足CS。我们要证明的完全性定理表述如下： 定理5(完全性定理)确定一个公理适宜的常项规范CS，我们证明：一个公式X在带有CS的基本混合核证逻辑J中有一个证明，当且仅当，X在所有满足规范CS的基本混合核证逻辑J模型的所有点上都为真，当且仅当，X在彻底解释的并且满足规范CS的所有基本混合核证逻辑J模型的所有点上都为真。 证明：可靠性方向的证明比较普通，我们完全略去。对于完全性的方向，我们的证明和斐汀的原证明大致上相同，也是要分成三步：第一步先生成一个基础的模型，第二步再保证一个名字只被这个模型上的一个点所赋予，第三步验证生成的模型是否符合之前列出的语义条件。由于在这里可及性关系R不具有自返性，所以在构造模型上还是与斐汀的证明有所区别。我们大致概述一下证明方法。
第三步关于条件的验证在这里从略。而接下来只要证明真值引理，完全性结果现在可以用标准的方式得到了。证完。 证明了完全性定理，接下来的工作是证明这个逻辑的显式性定理。对此，斐汀已经给出了一个关于基本混合逻辑JT的语义版本的证明。因为在语言上没有任何不同，这个定理可以同样视作是基本混合逻辑J的定理，我们直接把它引用过来。 定理6(显式性定理)对任意基本混合逻辑的定理，存在某个对□和
的替换，对应生成带有某个公理适宜的CS的基本混合核证逻辑J的定理。 三、结语 我们在本文中完成了弱化的目标，在不带有事实公理的情况下，建立了第一个极小的混合核证逻辑系统——基本混合核证逻辑J，并证明了其完全性定理等元理论研究。 当然，还有很多问题值得进一步讨论。第一，斐汀建立了basic hybrid-JT，我们的工作把T去掉了，生成一个相对较小的逻辑，但这个逻辑是否正是极小的混合核证逻辑?在我们看来，公理12-13和叠置远程公理必然化规则的设置可能还有继续弱化的余地。这三条公理的设置是为内在化定理的证明而量身定制的，因此，可能存在弱于它们但依然足以证明内在化定理和完全性定理的公理，当然这仍将会是一个技术性难题。第二，混合版本的核证逻辑的显式性定理的构造性证明也相当困难，关键在于句法上对可满足算子的处理。最后，可以考虑把基本混合逻辑的模型强化到名字模型(named models)的情况。
标签：逻辑模型论文; 公理系统论文; 关系逻辑论文;
