否定完全交互式证明的逻辑

可在www.sciencedirect.com在线获取理论计算机科学电子笔记300（2014）47-70www.elsevier.com/locate/entcs否定完全交互式证明的逻辑（认知决定者的形式理论）西蒙·克雷默simon.kramer@a3.ep p.ch摘要我们从现有的非单调或即时交互式证明（LiiP）的逻辑对应物中产生了一个可判定的经典正规模态逻辑的内在否定完备，从而产生了判别LDiiP内化了以代理为中心的证明理论，这些理论是否定完备的（最大）和一致（因此严格弱于，例如，皮亚诺算术），并享受析取性质（类似直觉逻辑）。换句话说，内部化证明理论是超过滤器，所有内部化证明目标都是在可证明或可证伪的意义上定义的 通过反言内在化证明（也称为认知决定者）。 不过，LDiiP本身是类-sical（单调的，非构造性的），负不完全的，并且不具有析取性质。我们交互式证明的否定完备性的代价是它们的非单调性和非公共性（仅适用于单例代理社区）。作为一个正常的模态逻辑，LDiiP享有标准的Kripke语义，我们通过调用LiiP的选择公理来证明，然后根据 一个具体的预言机可计算函数。LDiiP关键词：代理作为证明检查器，建设性Kripke语义，析取明确doxastic和认知逻辑，认知决策者作为决定性证据，交互式和预言计算，多代理系统，否定失败，证据作为充分证据，证明条款作为真值。1引言本文的研究对象是经典的非单调交互式证明的正规模态逻辑，即，否定完全因而析取交互式证明（LDiiP）的新模态逻辑和非析取因而否定不完全交互式证明（LiiP）的现有模态逻辑（cf. [20]和[19]）。(We用小写字母替换与互动相关的形容词。）我们这里的目标是从LiiP中公理化和语义化地生成LDiiP。请注意，就像在[20，19，17]中一样，我们仍然将交互式证明理解为预期资源无限的证明检查代理（尽管他们是部分工作由卢森堡国家研究基金AFR 894328资助，该基金由欧盟委员会玛丽-居里行动（FP 7-COFUND）共同资助[18]。1571-0661 © 2013由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。http://dx.doi.org/10.1016/j.entcs.2013.12.01148S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47⊥无法猜测），并为未来的工作留下概率和多项式时间的资源界限。1.1动机我们对LDiiP的直接动机首先是理论概念， 我们的交互式证明的否定完全变体的实际应用[20，19，17]。LDiiP的首要动机是为交互式计算提供直观的基础。见[17]一个程序化的动机。1.1.1理论概念就像在一个单一的证明者-验证者代理的非交互式设置中一样，否定完全（最大）和一致的逻辑理论（或超过滤器[6]）及其外部和内部证明概念的动机是获得认知，建设性和计算内容。回想一下，一个逻辑理论T根据定义是否定完备的，<$φ∈T，且T是一致的：i <$φ/∈T（因此T/ =L），其中”（《论语·子贡》），“伪也”。请注意，每一个这样的逻辑理论（命题的过滤器1）都是根据一个特征属性来定义的，因此与它是如何产生的无关（例如，基于一些证明系统或饱和关系），并且不一致的理论是平凡的否定完备的以及经典的。非平凡的负完全（一阶）定理（有等式，但没有集合）的经典例子有：塔斯基给定T的递归公理化2和T的外部证明概念，否定完备性和一致性对应于元定理模式►Tφ或φT<$φ（NC）和/φT<$。也就是说，对于所有φ∈L，φ或<$φ是T的定理，或者，从模型理论上讲，有效性，即，一个普遍的真理。对于否定完全相容模态理论，这意味着没有局部真理不是全局真理，因此它们的模态点（这是非平凡局部真理，即，真理在一些，但不是所有的他们指出，（m odels）是无效的。（如果φTφ，则φ是一个单向的，而t是全局的真值;如果/φTφ，则φT<$φ是T的否定完备性，而t是一个单向的，因而是全局的真值，因此φ不可能是T的一致性的局部真值所以在某种意义上，负完备模态理论是平凡的，即使它们是相容的。幸运的是，我们的模态LDiiP是否定的-完全否定。只有LDiiP内在化的证明概念才是否定完备的。与LDiiP的内在化的以代理为中心的证明概念相比►LDiiP<$（MVa），其中M表示证明（消息），而A表示证明（消息）。[1]（逻辑）格中的子集是定义的过滤器，当且仅当它在交（合取）和格序（蕴涵）下是闭的[6，Lindenbaum-Tarski代数]。2即，T有一组算法上可判定的公理。这是任何实用逻辑理论的最低要求;它保证了其公理的可识别性S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4749拟校对代理人。注意元逻辑否定和析取如何内化为它们的对象逻辑对应物。此外，注意到我们的内在判断比它的外部对应物更具体，在这个意义上，第一个谈论的是一个具体的（内在的）证据（充足的证据）M，而后者只说出一个b 计算完整性意味着M表示足够的数据（例如，记录为日志文件的本地系统历史的完成）用于决定是否有某个语句（例如，关于全局历史给出的当前系统状态）是真还是假。 希尔伯特希望一个否定完全相容的理论为整个数学，因为，在他的话，没有否定完全相容的理论，在某种意义上，他们是认知理想：所有（内化）的证明目标是明确的[23]，在这里的意义上，他们的真理或虚假可以确定明确的（在这里甚至有效地由一个代理）通过（内化）的证明（因此也称为认识论的决定者）。此外，否定完备理论虽然必然是非直觉主义的（！），然而，我们仍然享受直觉逻辑（IL）的析取性质，3这是，如果<$ILφ<$φJ那么<$ILφ或<$ILφJ（DP）[30]。因此，它们有相当多的建设性内容，这甚至通过保存排中律的演绎方便 为了理解为什么负完全理论必然是经典的，假设存在一个非经典的负完全理论T（即，/<$Tφ<$φ，andd<$Tφor<$T<$φ），并通过考虑右和左引入定律（集合φJ：=<$φ），由此导出一个直接矛盾，即如果<$Tφ或<$TφJ，则<$T φ <$φJ（并且在IL中也是valid）。事实上，对于经典逻辑理论，否定完备性在经典上等价于析取性质。这是一个众所周知的结果，我们在这里回顾一下定理1.1对于经典逻辑理论（布尔代数或格中的过滤器），否定完备性（极大性或作为超过滤器）经典等价于析取性质（作为素过滤器的性质）。证据 见附录A.1。Q将否定完全证明理论内在化，LDiiP因此将其分解内在化 财产，作为的定理模式P2P（MVa（φ<$φJ））→（（MVaφ）<$（MVaφJ）），这就是为什么我们称我们的内在化证明也是析取的。然而，首先给出LDiiP的经典性（和正规性），其次给出适用于LDiiP内在化的理论的定理1.1，我们也可以将内在化的析取性质规定为公理模式，然后从中导出内在化的否定完备性作为定理模式。也就是说，在任意经典正规模态逻辑中，我们可以做出以下推论，其中第1行中φ和φJ上的泛元量化是左隐式的：(i) <$Q（φ<$φJ）→（Qφ<$QφJ）假设的内在析取性质(ii) <$Q（φ<$φ）→（Qφ<$Q<$φ）1，特殊化（集合φJ：=<$φ）(iii) 经典重言式[3]关于严格低于经典命题逻辑的其他所谓超直觉主义或中间逻辑的综述，参见[5 ]，这些逻辑也享有析取性质。50S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47(iv) φ）3，必然性（正规性）(v) 2，4，肯定前件。（内在否定完备性）为了也看到具有递归公理化的否定完备相容理论中的计算内容，如前所述，从经典递归理论中回忆一下，这样的理论实际上也是递归的（算法上可判定的），一个整体，即，不仅在它们的公理集合中：一个理论的公理的递归性意味着它的定理的递归可枚举性。因此，为了确定对于这样的理论T的语言L中的给定φ∈L，φ∈T是否成立，开始T. 根据T的否定完备性在这个过程中会出现φ或<$φ如果φ出现则停止，并得出φ∈T;如果<$φ出现则停止，并通过T的一致性得出φ/∈总之，认知，建设性的，和计算内容的复发-分别从最大相容性、析取性和算法可判定性三个方面对公理化的否定完全相容理论进行了研究。然而，他们的目标是远离一个希尔伯特的希望：哥德尔确定了否定的完整性，任何递归公理化的一致的4更糟糕的是，包含PA的相容理论在算法上也是不可判定的[22]。Noý standing，递归公理化的否定完全相容理论，因此严格弱于PA，对于实际应用至关重要。（最大相容集对于理论应用也是至关重要的，例如公理完备性证明的规范模型构造，参见。附录A.4.2.）1.1.2实际应用否定完全性的外在形式和内在形式都有重要的实际应用。否定完备性的外部形式“φ或<$φ“的重要实际应用在那里，外部形式如果φ的每一个可能的证明都失败了，那么就可以推出<$φ[4，27]。否定作为失败的模态逻辑变体“/Ka（φ）意味着Ka（φ）“的另一个重要的实际应用在那里，这种否定作为失败的认知变体产生了多代理分布式系统的知识的非单调逻辑。(This也是我们所知道的唯一相关工作。）我们的否定完备性的内部化形式<$LDiiP（MVaφ）<$MVa<$φ的一个重要实际应用是可靠的多代理分布式系统的责任（例如，电子投票系统[16]，更普遍的是整个互联网[21]）。一个多代理分布式系统S通过定义是可问责的，当且仅当S是无滥用和可审计的：对于S中的所有代理b，（无滥用），每当b行为正确（作为S中的代理），b可以向所有代理a证明（包括4虽然自然数形成实数的严格子集，但负不完全PA不能是前面提到的负完全初等实数算术（R）的子集;自然数在R语言中是不可定义的[11]。S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4751她自己）在S中这样做，并且，（可验证性），每当b行为不正确（因此是错误的）时，S中的每个或至少一个其他代理人c最终将能够向S中的所有代理人a（包括她自己和b）证明b是错误的，（参见[15]对于这种自然语言的公式化的正式转录）。在这样一个系统S中，每一个主体b（MVacorrect（b））MVa<$correct（b）换句话说，M必须构成决定性的证据，或者换句话说，在b的正确性（短暂的）问题上，M必须是a的认识决定者（B可以改变她的行为！）也就是说，LDiiP是认知决定者的形式理论。为了避免滥用（可验证性），证明者b（c）必须（最终）知道这样一个M，写作bkM（ckM）。我们将在第2节中给出正式的定义，并在未来的工作中提供一个完整的正式[15]初步的、非公理化的问责制案例研究。最后，请注意，引起法官a注意的用于正确（b）的决定性证据M可以被视为一种法医痕迹，因为M允许 A来决定B是否正确，从而决定B是否犯了错误。1.2贡献概念贡献我们在本文中的概念贡献如下。首先，我们产生了一个新的模态逻辑的否定完全，从而析取交互式证明（参见。定理2.17），它内化了以主体为中心的否定完全一致性证明理论（具有析取性质），具有重要的理论和实际应用。第二，我们观察到，否定的完整性和析取性的代价是由此产生的以代理人为中心的证明概念的非单调性和非公共性（参见第二章）。事实2.5和2.14，分别），这也是标准KD 45-信念的否定完全析取显式细化推论2.9）。第三，我们贡献了一个析取但否定的--对S4-可证明性的不完整的显式精化（参见推论2.10），由我们的证明概念构造而成。技术贡献我们的技术贡献如下。 首先，我们为LDiiP提供了一个标准的，但也是预言计算和集合理论构造的Kripke语义（参见。第2.2节）。像在[20，19]中一样，我们赋予证明模态一个标准的Kripke语义[1]，但其可达性关系MRa我们首先根据初等集合论构造来建设性地定义，即MRa，5在松散的类比与集理论的建设性，而不是纯粹的公理定义的数量[7]有序对（例如，Kuratowski的标准定义，以及其他众所周知的定义[23]）52S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47然后匹配到标准形式的抽象语义接口（抽象地规定了可访问性关系的特征属性[9]）。我们将说MRa是MRa的范例（或实现）。（模态可及性的集合论构造性但非直觉主义定义的一个简单例子是众所周知的认知可及性定义，即根据状态投影的相等性定义的状态不可及性[8]。LDiiP的Kripke语义是oracle计算的，在这个意义上（参见。定义2.11）个人证明知识（比如M）可以被认为是由一个虚构的计算预言机提供的，它因此充当了我们交互式证明的一个假设的提供者和虚构的认识源。其次，我们证明了定理2.8，它建立了证明项作为真值的观点以及单例主体论域的特殊情况的标准形式第三，我们证明了有限模型的性质（cf。定理2.18）和LDiiP的算法可判定性（cf.推论2.19）。（否定完备性意味着算法的可判定性，如1.1.1节所示，但与LDiiP测试相反。1.3路线图在下一节中，我们通过一个紧凑的闭包算子公理化地介绍了我们的析取即时交互证明逻辑（LDiiP），该闭包算子诱导了我们所寻求的希尔伯特式证明系统。然后，我们获得（句法）的洞察力，否定的完整性意味着非单调性（参见。事实2.5），并在所得到的系统中证明了上述定理2.8以及推论2.9和2.10接下来，我们介绍具体构造的语义以及LDiiP的标准抽象语义接口（参见第2.2节），并证明证明系统的公理充分性关于这个接口（参见。定理2.17）。我们通过援引LiiP的选择公理来证明LDiiP的构造性语义的存在（参见。表1），然后也构造它在一个具体的甲骨文可计算的功能，从中我们获得（语义）的洞察力，否定的完整性意味着非公共性（参见表1）。事实2.14）。最后但并非最不重要的是，我们证明了有限模型性质（参见。定理2.18），并由此，算法的可判定性（cf.推论2.19）的LDiiP。2LDiiP2.1语法上与即时交互式证明逻辑（LiiP）类似，选言即时交互式证明逻辑（LDiiP）提供了一种通用消息项语言之上的模态公式语言。LDiiP的公式语言表示命题构造器，一个关系符号akM），以及用于关于证明的命题的模态构造器MVaφ）。简而言之，LDiiP是经典命题逻辑的最小扩展，具有交互式广义附加运算符（证明模态）和证明项语言。注意，LDiiP的语言与S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4753（MVaφ）<$MVa<$φ（否定完备性）MVaφLiiP[20 ， 19] 中 的 一 个 实 现 了 Proof-modalityNotation ， 其 中 LiiP 中 的 Proof-modalityNotation是定义2.1[LDiiP的语言]设• A表示代理名称a、b、c等的非空有限集合• M表示消息术语M的语言，使得a∈M• P表示命题变量P的可数集，其约束使得对于所有a∈ A和M∈ M，（akM）∈P（对于一个原子命题（个人知识）(So，对于a∈ A，ak·是一元关系符号。）• L 3φ：：= P. -是的φφ。把我们的逻辑公式语言φ，其中MVaφ读作请注意以下宏定义：T：=aVaaka，φ：=<$T，φφJ：=<$（<$φ<$φJ），φ→φJ：=<$φ<$φJ，以及φParticipateφJ：=（φ→φJ）<$（φJ→φ）。然后，LDiiP具有以下公理和演绎规则模式，其中灰色阴影表示与LiiP的其余基本差异（参见[20]和[19]）。定义2.2[LDiiP的公理和演绎规则]设• Γ0表示经典命题逻辑·• r2：= r0< $r1 <${·MVaakM（自知）· （MVa（φ→φJ））→（（MVaφ）→MVaφJ）（克里普克· （MVaφ）→（akM→φ）（认识真性）· <$（MVa）（证明一致性）{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}指定LDiiP的公理模式。然后，Cl0（r）：=r2< $r：=n∈NCln（n），其中对于所有的Γ<$L：Cln+1（Γ）：= Cln（Γ）{φJ|{φ，φ→φJ}<$Cl n（Γ）}<$ （肯定前件，MP）{MVaφ|φ∈ Cl n（Γ）}<$（必然性，N）.我们称LDiiP为一个基理论，而Cl（Γ）则是对任意Γ∈ L的LDiiP-理论。LDiiP：=Cl（λ）Γ1表示kM54S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47注意LDiiP的逻辑顺序，它像LiiP一样从LiiP（cf. [20]和[19]），我们回顾Kripke定律（K），认识真实性定律和必然性定律（N）的讨论显然，对于这样的主体，如果M是φ→φJ和φ的充分证据，那么M对φJ也是充分证据。然后，认知真实性对交互性的重要性在于，在真正分布式的多代理系统中，并非所有代理都知道所有证明，即，代理对于消息不是无所不知的。否则，为什么要互相交流呢？所以有一个证明并不意味着知道这个证明。当一个代理人a不知道这个证明，并且代理人不能通过猜测自己凭空生成证明时，只有来自对等体的通信，对等体因此充当了一个预言者，可以使代理人a知道这个证明。其次，对N的证明是，在交互式设置中，有效性，因此更重要的是重言式（在命题片段的有效性的严格意义上），在某种意义上是琐碎的。要理解为什么，回想一下模态有效性在所有指向模型中都是真的（参见。定义A.1），因此不值得在给定模型中从一点传达到另一点，例如，通过特定的交互式证明。（没有什么比用重言式说话更令人尴尬的了。）因此，有效性值得武断的证明。值得交流的是比有效性弱的真理，即标准模型论意义上的局部真理（参见《自然》）。定义A.1），这可能并不普遍。否则为什么要互相交流呢？我们继续讨论剩余的新公理和规则。如上所述，LDiiP的消息语言M是通用的，因此kM将需要适合于所选M∈M的项结构的公理（例如LiiP [20，19]所需的公理）。自我知识公理模式的有效性是由预言计算证明的：从一个甲骨文，那么一个会知道M定义2.11）。(The自我认识定律在LiiP中也是有效的，在那里它对应于theo-rem[而不是xiom]schemaM：：aakM。）一致性和否定完备性的公理系统分别内在化了（外部理论）一致性和否定完备性（参见第1.1.1节）。注意，内在否定完备性的定义独立于证明项结构（M是抽象的），正如逻辑理论的（外部）否定完备性的定义独立于其可能的证明系统结构一样。然而，这个抽象的定义是一个间接的、结构性的约束：毕竟，不是任何证明系统结构都能产生否定完备理论。命题2.3（希尔伯特式证明系统）设• ΦLDiiPφ：i ifΦLDiiPthenφ∈ LDiiP• φE <$LDiiPφJ：i <${φ}<$LDiiPφJ和{φJ}<$LDiiPφ•LDiiP φ：i换句话说，在[ 28，定义3.7.4]的意义下，<$LDiiP<$2 L×L是一个闭包条件系统。举例来说S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4755(i) 对所有公理φ∈Γ2，(ii) 对于肯定前件，{φ，φ→φJ}<$LDiiPφJ(iii) 对于必然性，{φ}<$LDiiPM Vaφ。（在节省空间的水平希尔伯特记法“Φ LDiiP φ“中，Φ不是一组假设，而是一组前提，参见。肯定前件和必然性）。然后，可以将CLLDiiP视为由Cl诱导的希尔伯特式证明系统定义的。 事实上， Cl：2 L→ 2 L是一个标准的结果算子，即，一个替换不变的紧致闭包算子。证据如[17]。 众所周知，希尔伯特式证明系统可以被视为由紧凑闭包算子诱导的（例如，见[12]）; Cl确实是这样一个算子，可以通过检查Cl的归纳定义来验证;替换不变性来自我们对公理模式的定义使用。6Q推论2.4（正规性）LDiiP是正规模态逻辑。证据共同由克里普克提案2.3）。Q注意，在LDiiP中，原始LiiP规则的模拟{akMParticipakMJ}LiiP（MJ：：Caφ）ParticipM：：Caφ（参见[20，19]）将是无效的（因为与否定完整性不兼容），因此在LDiiP中不被更不用说，这是一个更强的原始LiP规则的模拟{akM→akMJ}<$LiP（MJ：Caφ）→M：Caφ（参见[20，17]）然而，当在成对数据MJ下可以推导出单调性LiP（M：Caφ）→（M，MJ）：Caφ的过程时因此，我们断言关于我们的否定完全证明的下列否定事实事实2.5否定完备性意味着非单调性。请注意，如果我们将证明项的配对构造器引入LDiiP的消息语言M（与LiiP一样，参见表1），事实2.5意味着/LDiiP（MVaφ）→（M，MJ）Vaφ 。事实2.6(i) {φ→φJ}<$LDiiP（MVaφ）→MVaφJ（正则性）(ii) <$LDiiP<$（MVa <$）Participate（（MVaφ）→<$（MVa<$φ））(iii) LDiiP（MVa<$φ）参与MVa（φ→φ）[6]作为公理模式的替代，我们可以使用公理和一个附加的替换规则集{σ[φ]|φ∈Cln（Γ）}在Cln+1（Γ）的定义下.56S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47证 据 1 和 2 是 众 所 周 知 的 必 然 模 态 任 意 正 规 模 态 逻 辑 。 对 于 3 ， 考 虑<$LDiiP<$φParticipate（φ→<$），因为<$φ Participate（φ→<$）是经典重言式，然后由1推导出结论。Q引理2.7(i) LDiiPMVa（（MVaφ）→φ）（真实性的自证明）(ii) LDiiP（MVa（MVaφ））→MVaφ（验证密度）证据 见附录A.2Q真实性和证明密度的自我证明定律也适用于LiiP [20，19]。我们继续介绍关于LDiiP的第一个重要结果定理2.8（证明项作为真值）(i)LDiiP（MVa<$φ）Participi<$（MVa <$φ）（最大一致性）(ii) <$LDiiP（MVa（φ<$φJ））Participate（（MVaφ）<$MVaφJ）（proofconjunctionsbis）(iii) <$LDiiP（MVa（φ<$φJ））Participate（（MVaφ）<$MVaφJ）（IDPbis）(iv) <$LDiiP（MVa（φ→φJ））参与（（MVaφ）→MVaφJ）（Kbis）(v)LDiiP（MVa（φParticipiφJ））Participi（（MVaφ）ParticipiMVaφJ）（Bi-K）(vi)LDiiP（MVa（MVaφ））参与MVaφ（模态幂等性）(vii) <$LDiiPbkM→（（MVb（MVaφ））ParticipateMVaφ）（模态幂等bis）证据 见附录A.3Q“IDP”表示“内部分离属性”。这些法律是按照尊重其各自的证据先决条件的（总）顺序列举的。注意定理2.8.2他们断言LDiiP的证明模态在（二元）布尔运算符上是完全分配的。虽然证明合取bis和模态幂等律在LiiP中也成立[20，19]，但只有IDPbis和Kbis的if方向在LiiP中成立。还请注意，模态幂等性结合了证明密度（cf.引理2.7.2）和证明传递性（cf.模态幂等性证明的第l行）。像LiiP和LiP一样，模态幂等性有效性的关键是每个主体（例如，a）可以自己作为证明检查员，更多细节见[17，第3.2.2节]。模态幂等二定律是模态幂等的推广。注意，当|一|= 1，定理2.8意味着在复合LDiiP公式中的证明模态的所有出现都可以被编译掉，在这个意义上，所有这些出现都可以被推到可能被否定的原子子公式之前（即，文字）的复合公式，与公理公式MVaakM作为基础情况。 因此，在这种情况下，我们可以按照构造性逻辑的一种可实现性解释的精神，将证明项理解为真值[29，7.8节]。 否则，即，当|一|> 1个（回想一下定义2.1，A是），可能不是所有的表面现象在化合物中，公式可以被编译掉（参见定理2.8.7）。下面的推论断言，我们的否定完备的，因而是判别式的证明模态也是标准（隐式）信念的一个明确的细化S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4757模态[24]。推论2.9（否定完全析取显式信念）“M V a · ” 是 显 式 主 体 信 念 的 一 个 负 完 全 析 取 K D 4 5 - m o d a l i t y ， 其 中M 表 示 能 够 证 明 主 体 a 信 念 的 显 式 证 据 项 .是的。 考虑到“M V a ·” 满足Kripk e的l a w（K，cf. 定义2.2），D-定律（在定义2.2中称为定理2.8.6的唯一如果部分），必要性（cf.定义2.2）和否定的完整性（cf.定义2.2），因此内在的分离属性（参见。定理2.8.3的if部分）。该(i) <$LDiiP<$（MVa <$φ）→（MVa<$φ）唯当-定理2.8.1(ii) 定理2.8.6[<$φ]的仅当部分(iii) <$LDiiP<$（MVa <$φ）→MVa（MVa<$φ）1，2，→(iv) 如果-定理2.8.1的一部分，则LDiiP（MVa<$φ）→<$（MVaφ）(v) <$LDiiP（MVa（MVa<$φ））→MVa<$（MVaφ）4，正则性(vi) <$LDiiP<$（M Vaφ）→ M Va<$（M Vaφ）3，5，→的传递性。Q由于认识论的真实性，akM是“M V a ·”不像标准的S5-知识模态那样表现的一个充分条件►LDiiPakM→（（MVaφ）→φ）。T-lawx在下面的推论中，我们也构造了一个反言但否定的--在（隐式）S4-可证明性的完全显式精化中推论2.10（析取e显式可证明性）'ak M M V a · '是显式主体可证明性的析取但否定不完全的S4-模态，其中 M代表明 确 的证据项，它确实证明了代理人a的 知 识 。证据 由推论2.9和真理律LDiiP（ak M M Vaφ）→ φ对于m o dali y'ak M M V a · '等于认识真理性的L a w的事实（参见 定义2.2）。注意，尽管"a k M“是明显的分离性的<$LDiiP （ak M <$M Va（ φ<$φJ） ） → （ （ak M <$M Vaφ ）<$ （ak M <$MVaφJ）），它是否定的-i n完全的，因为/<$LDiP（akM<$MVaφ）<$（akM<$MVa<$φj），因为/<$LDiPakM，又因为Γ 1的任意性（参见：定义2.2）。固定Γ1，使得无法猜测的资源无限代理a知道所有消息M只能对A={a}有意义。否则，即，当所有代理都知道所有消息时，为什么要相互交互？Q58S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）47一：：=0 succ（s）.M一初始状态为一一2.2语义上我们继续提出具体构造的语义以及标准的抽象语义接口LDiiP，并证明了公理充分性的证明系统相对于这个接口。我们通过调用LiiP的选择公理[20，19]来证明LDiiP的构造性语义的存在2.2.1具体表1显示了LiiP的具体语义的成分，我们将从中构建LDiiP的具体语义。由此，我们将只需要S和msgs a的具体实例以及cl s的抽象实例作为LDii P的成分。注意到LiiP的具体可及性MRCa是一个完全定义的真（非函数）关系。然而，我们确实需要一个具体的可达性关系的LDiiP是功能性的，因为LDiiP（LDiiP的证明一致性公理对应于这样一个关系的总体属性。幸运的是，LiiP的具体可达性MRCa是完全定义的，因此我们可以通过选择AC[MRCa]的公理来了解，我们可以将其应用于MRCa，MRCa可以被对于所有s∈S，s ∈S，则s∈sJ∈ S，使得sMRCasJ蕴涵MRCa不是一个严格定义的x存在f：S→S，使得对所有的s∈S，sMRcaf（s）. （AC[MRCa]）`MRCa可以是请注意，选择公理是非建设性的，因为它抽象地断言 某个f的条件存在，但实际上没有提供fsuc hanf的具体例子。我们现在的问题是为MRCa找到这样的一个f，这将允许我们为LDiiP构建一个功能性的具体可访问性在定义2.11中，我们在根据某些广义后继函数归纳构造的具体状态上构造这样的f作为预言计算函数σM定义2.11至表1中的基本区别用灰色阴影表示。定义2.11[语义成分]对于LDiiP的集合论构造性、模型论研究，• S3Ssenti，其中0可以被理解为零数据点（表示为示例），succM可以读作消息M（例如来自充当oracle的另一个代理S. Kramer/Electronic Notes in Theoretical Computer Science 300（2014）4759.cla：2M→ 2M表示紧闭包算子，并定义cla：2M使得cl（D）：= cl（msgs（s））≠D是一一一）：=n∈N cl（msgs（s）Dna一）σ：S → S，使得σ（s）：=MM一一.SsuccM（s）otherwise（oracleinput）如果M∈cl（n），且是一一msgs（succM（s））：=msgsa（s）{M}ifa=b，and让• S $指定状态空间-一组系统状态• msgsa：S→2M表示提取（不分析）（有限）集合的原始数据提取器生成a也就是说，消息a（s）是a来自系统状态s的消息，代理a∈A已经生成（假设只有a可以· CL：2→2指定数据挖掘操作员 成使得cl （D）：= cl (msgs（s）发展中国家S一MM是一a a）：=n∈Na aCL (msgs（s）D），其中对于所有D M：nCL（D）：={a}D0一cl（D）：= cl（D）n+1个na a{M，M|（M，M）∈ cl（D）}<$（非配对）{（M，M）|{M，M}{M，M}（D）}配对′′na′恩一{{[M] }| M ∈ cl (D)}∪(personal signature synthesis)n一一{（M，b）|{[M]} ∈cl（D）}（通用签名分析）nBa·

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