（逻辑学专业论文）一个限制量化的高阶逻辑——和它在语言推理上的应用.pdf

论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作 所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集 体已经发表或撰写过的作品成果。对本文的研究作出重要贡献的个人和集体，均 已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名： 当圃衾 吼叩月 日 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即：学校有权保留学位 论文并向国家主管部门或其指定机构送交论文的电子版和纸质版，有权将学位论 文用于非赢利目的的少量复制并允许论文进入学校图书馆、院系资料室被查阅， 有权将学位论文的内容编入有关数据库进行检索，可以采用复印、缩印或其他方 法保存学位论文。 学位论文作者签名： 苏闯导师签名：幽 日期妒7 年月乡日 日期矽7 年6 月日 谨以此文怀念 一个伟大的现代逻辑学灵魂 l e o nh e n k i n ( 1 9 2 1 2 0 0 6 ) 摘要 本文的主题是一个限制量化的高阶逻辑，记为丁，主要内容是形式化丁和研 究它的模型论性质另外本文还分析丁在自然语言推理上的应用 二阶逻辑的不完全性是哥德尔不完全性定理的一个直接推论在二阶逻辑的 标准语义中，谓词变元的取值范围是个体论域的幂集但是l h e n k i n 2 1 1 发展了 所谓的一般语义，其中谓词变元的取值范围的定义放宽为“个体论域的幂集的任 意子集”二阶逻辑在一般语义中是完全的，而且类似的结果可以推广到高阶逻 辑与这种“放宽模型”的策略相对，本文构造丁所采用的是“限制句法 的策略， 即通过限制量化公式的形式使约束变元的取值范围限制在某类表达式的解释中 换而言之，这种策略通过限制句法来实现约束变元的取值范围从整个论域到它 的某个子集的相对化本文第一部分证明丁相对于标准语义的完全性定理、分 析“限制句法 与一般模型的关系和h e n k i n 构造法在丁上的进一步应用和局限 性 另一方面，继蒙太古 2 6 】 2 7 】 2 8 】以来，语言逻辑学家开始广泛地运用类型论 和模型论语义中的技术分析语言本文第二部分关注丁在“罗素式”非直谓句的 推理中的应用这部分的内容包括分析罗素式非直谓句与限制量化的关系，并且 分析如何借鉴 2 8 】发展一个辅助机制，以增强丁作为在自然语言推理上的应用 这个机制包含一个句法理论和一系列对应规则，自然语言和逻辑表达式能够通过 它统一地相互翻译我们只在一个局部范围实现该机制，并以例子来说明如何利 用丁和该机制证明一个具体的自然语言推理 本文的研究属于形式逻辑和语言逻辑范畴 关键词高阶逻辑限制量化自然语言的推理 l l a b s tr a c t w ep r e s e n tah i g h e r - o r d e rl o g i co fr e s t r i c t e dq u a n t i f i c a t i o n ，d e n o t e db yt t h ec o n t e n to ft h i st h e s i sc a nb ed i v i d e di n t ot w op a r t s ：t of o r m u l a t eta n d i n v e s t i g a t es o m eo fi t sm o d e l - t h e o r e t i cp r o p e r t i e s ，a n dt oa n a l y z ei t sa p p l i c a b i l i t y a sa r e a s o n i n gm o d e lo fn a t u r a ll a n g u a g e t h ei n c o m p l e t e n e s so fs e c o n d - o r d e rl o g i c ( s o l ) i sa ni m m e d i a t ec o r o l l a r y o fg 6 d e l si n c o m p l e t e n e s st h e o r e m i ns o l ss t a n d a r ds e m a n t i c s ，t h ed o m a i nf o r p r e d i c a t e - v a r i a b l e si st h ep o w e rs e to fd o m a i no fi n d i v i d u a l s h o w e v e r ，l h e n k i n 【2 1 】d e v e l o p e dt h es o - c a l l e dg e n e r a ls e m a n t i c s ，i nw h i c ht h er a n g eo fp r e d i c a t e - v a r i a b l e si sr e l a x e dt ob ea l la r b i t r a r ys u b s e to ft h ep o w e rs e to fi n d i v i d u a ld o m a i n s o li sc o m p l e t ew i t hr e s p e c tt ot h eg e n e r a ls e m a n t i c s a n dt h es a m er e s u l th o l d s i nh i g h e r - o r d e rl o g i c s c o n t r a r yt ot h ep r e c e d i n gm o d e l - s t r a t e g y , w ea d o p ta s y n t a x - s t r a t e g yi nf o r m u l a t i n gt ，i nw h i c h ，b ys e t t i n gq u a n t i f i e df o r m u l a st ob e as p e c i a lf o r mw h i l ed e f i n i n gt h es y n t a xo f 丁t h ev a l u e so fh i g h - o r d e rb o u n d e d v a r i a b l e sa x ec o n f i n e di nt h ei n t e r p r e t a t i o no fc e r t a i ne x p r e s s i o n s i no t h e rw o r d s ， w er e a l i z ei nt h el e v e lo fs y n t a xt h er e l a t i v i z a t i o no ft h er a n g e so fh i g h e r - o r d e r b o u n d e dv a r i a b l e si n t os m a l l e rs e t s b ys o - d o i n go u rm a i na c h i e v e m e n ti st h e c o m p l e t e n e s so ftw i t hr e s p e c tt os t a n d a r ds e m a n t i c s t h el i n kb e t w e e no u r s y n t a x - s t r a t e g ya n dt h eg e n e r a ls e m a n t i c sa n dt h ef u r t h e ra p p l i c a t i o no fm e t h o d o fh e n k i n sc o n s t r u c t i o na r ea l s oe x p l o r e d o nt h eo t h e rh a n d ，a f t e rm o n t a g u e 2 6 】 2 7 2 8 】t h e r ea p p e a r sl i t e r a t u r e i n v e s t i g a t i n gt h ep r o p e r t i e so fo r d i n a r yl a n g u a g ev i at e c h n i q u e sd e v e l o p e di nf o r - m a ll o g i c s w - h a tw ec o n c e r ni st h er e a s o n i n gp r o b l e mo fap a r t i c u l a rk i n do f i m p r e d i c a t i v es e n t e n c e s i n s p i r e db y 【2 8 】a n df o rt h ep u r p o s eo fe n h a n c i n gt h e a p p l i c a b i l i t yo ft ，w ed e v e l o pa na c c e s s o r i a lm e c h a n i s m ，i nw h i c he x p r e s s i o n si n as m a l lf r a g m e n to fe n g l i s ha n di ntc a nb et r a n s l a t e di n t oe a c ho t h e re f f e c t i v e l y a tt h ee n dw eg i v ea ne x a m p l et oi l l u s t r a t eh o wta n dt h i sm e c h a n i s mw o r k t o g e t h e r k e yw o r d sh i g h e r o r d e rl o g i c ，r e s t r i c t e dq u a n t i f i c a t i o n ，n a t u r a ll a n - g u a g er e a s o n i n g i n 1 v 中文摘要 英文摘要 目录 第一章导论 1 1 逻辑、语义和完全性。 1 2 逻辑和语言 第二章限制量化的高阶逻辑丁 2 1 丁的句法和标准语义 2 2 从广义量词角度看限制量化 2 3 丁的证明论 2 4 丁的完全性一h e n k i n 构造法 2 5 限制量化和一般模型 2 6 丁的内插定理 第三章关于r i s 的推理2 3 3 1r i s 与限制量化2 3 3 2 丁的辅助机制2 4 3 3 证明一个r i s 推理2 8 第四章总结 参考文献 3 1 3 3 i 一 1 1 4 7 7 9 o 1 6 8，l_l，上 导论 本文的主题是一个限制量化的高阶逻辑我们从它的模型论性质和在语言分 析中的应用这两个方面来研究该逻辑其中第一个方面为本文的重点，而第二个 方面具体为该逻辑在非直谓语句的推理中的应用在这一章里，我们对应这两个 方面介绍相关的预备知识和研究背景 1 1 逻辑、语义和完全性 “逻辑”这个词对不同的人意味着不同的东西说起“逻辑”，有的人指三段 论和韦恩图，有的人指一个数学的分支，有的人指人类的思维或说理方式讨 论“逻辑”的定义或者本质不属于本文的研究范围但是本文的主题可以用“构 造一个逻辑”来描述一逻辑在此是一个被研究的对象，因此有必要简短地谈谈 本文所考虑的逻辑大概是什么在前面一句话中，一个“逻辑”指的是一个逻辑 系统直观上讲，一个逻辑系统是一个数学游戏，游戏的内容是从已有的符号推 导出新的符号以下我们给出关于逻辑的一个数学描述令s 为一个非空集合， 而p ( s ) 是s 的幂集则s 上的一个闭包运算是一个映射c ：p ( s ) 一p ( s ) 使 得对任意x ，y p ( s ) ，( 1 ) 若x y 则c ( x ) c ( y ) ，( 2 ) x c ( x ) ，和( 3 ) c ( c ( x ) ) = c ( x ) 那么，二元组( p ( s ) ，c ) 则可以看作一个( 单调) 逻辑，s 是该 逻辑的语言集 为了更好地说明逻辑的结构，下面我们引用k a y e 2 3 】的一个简单而有启发 性的逻辑系统，将其记为l 三的语言集既为所有由0 或1 组成的有穷符号串的 集合定义优( 既) 为满足以下条件的最小集合：对任意x 既 ( 1 ) x c l ( x ) ； ( 2 ) 若s x ，贝0s o ，s l c l ( x ) ； ( 3 ) 若s o ，s l x ，贝0s c 2 ( x ) 容易验证既为一个闭包运算若s 既( x ) ，又记为x 卜工s 在某些文献中 称卜l 为l 的证明系统，因为xf - l8 的意思是“若以x 中的符号串为前提，符号 串s 能被证明”我们称这样证明为形式证明比起其它数学证明，在l 中做形式 这样抽象地定义的逻辑称为泛逻辑 1 第一章导论 2 证明的优点是显然的：要做的仅仅是严格而机械地根据规则操作符号串但同时 这也是它的缺点：纯粹对符号的操作是无意思的我们需要知道x 卜ls 的数学 意义，正如我们知道“4 1 + 5 7 = 9 8 ”这个等式的数学意义一样换而言之，我们需 要给x 卜l8 一个数学解释我们理解前面的等式，是因为我们知道“4 1 、“5 7 和“9 8 代表的是某些数因此要理解x 卜l8 的意义，首先寻问由0 和1 组成的 符号串代表了什么学过高等数学的人容易想到，它们能代表一个二元树中的点， 其中s 0 和s 1 代表8 的两个后继进一步( 需要一些创造性) 他们会发现x 卜ls 的意思与下面这个数学命题相符： 存在s 7 x 使得，对每一条路径p ，若p 通过s 则它通过s 用x l8 表示上面那个命题，则x l8 可以看作x 卜l8 的数学解释这个 对l 中的语言一即由0 和1 组成的有穷符号串8 一和对x 卜ls 的解释机制称 为l 的语义在数论中，我们对具体的算术运算不感兴趣，而对关于自然数的性 质感兴趣同样地，在逻辑中，我们也不对关于符号的形式证明感兴趣，而对关于 这个逻辑的性质感兴趣显然，一个逻辑一例如l 一的最重要性质便是x 卜ls 与x l8 的关系 命题x 卜l8 当且仅当x l 8 具体的证明过程请见f 2 3 1 中的3 1 从左到右的方向称为可靠性定理，可靠性 定理的直观意思是“能证明的都是正确的”( 这里的“正确”相对于它们的数学解 释而言) ，另一个方向称为完全性定理，完全性定理的直观意思是“不能证明的都 不是正确的”通常一个逻辑的可靠性能够被直接证明，相对而言它的完全性的 证明则复杂得多证明一个逻辑( 相对于某种语义) 的完全性的一个通常方法是 利用逻辑的语言构造一个特殊的数学结构本文的主要工作之一便是证明一个逻 辑的完全性 对于一个逻辑系统，我们可以从两个出发点来考察：一是从证明系统出发， 二是从语义出发在上面对l 的介绍中，我们采用了第一个出发点，即先给出它 的证明系统，再为它寻找合适的语义这一出发点突出下面这点：一个逻辑的完 全性是相对于某种语义而言的但是在数学研究中往往存在这样的情况，某个逻 辑( 或者它的证明系统) 是被用来研究特定的某类( 个) 抽象结构的( 而这类( 个) 抽 象结构称为该逻辑的模型) 在这种情况下，这个逻辑的语义是固定的，而谈论 它的完全性便是谈论它相对于固定的语义的完全性例如，一阶逻辑用于研究 一般的代数结构，而一阶算术用于研究自然数模型下面我们逐一谈谈关于这 两个逻辑的完全性的内容值得一提是，要谈的这两个方面都与二十世纪两位 第一章导论 3 重要的逻辑学家有关第一位理所当然是k 哥德尔( 1 9 0 6 - 1 9 7 8 ) ，而第二位是l h e n k i n ( 1 9 2 1 2 0 0 6 ) 哥德尔为逻辑学做的第一项贡献是一阶逻辑的完全性定理 ( 1 9 2 9 年) ，但他的原创证明比较艰涩，后来h e n k i n ( 1 9 4 9 年) 改进了这一定理的证 明方法，即上面提到的利用逻辑的语言构造一个特殊的数学结构的方法h e n k i n 的方法一本文称之为h e n k i n 构造法一不仅由于其清晰易懂而成为现在的逻辑 教科书中的通用方法，而且成为独立于完全性定理证明的利用语言构造模型的一 般方法哥德尔的另一项更重要的贡献是著名的哥德尔不完全性定理( 1 9 3 1 年) ， 结合本文的上下文，这条定理可以粗略概括为：不存在一个一阶算术的证明系统， 使得所有且仅仅所有在自然数模型上为真的公式都能在其中被证明9 哥德尔不 完全性定理在逻辑学上甚至哲学上具有重要意义f 2 0 1 二阶逻辑是一阶逻辑的拓展，它的语言除了包含个体变元，还包含谓词变元 这使得二阶逻辑具有比一阶逻辑更强大的表达力一阶逻辑的紧致性定理是它的 完全性定理的一个简单推论，由一阶逻辑的紧致性定理可以得到许多数学上重要 的概念一例如有限性、可数性、最小闭包和良序性一都无法在一阶语言中刻画， 而这些概念都能在二阶语言中刻画出来在语义方面，在一阶逻辑语义的基础上， 令( 受约束的) 谓词变元的取值范围为个体论域的幂集这是二阶逻辑的标准的语 义，简称标准语义，所定义的结构称为二阶逻辑的标准模型二阶逻辑的不完全 性是哥德尔不完全性定理的一个直接推论，以下粗略地解释如何由哥德尔的不完 全性定理得到二阶逻辑的不完全性对于任意一个一阶算术公式妒，存在一个二 阶公式，使得在所有标准模型中为真( 有效) 当且仅当妒在自然数模型中为 真，所以如果存在一个二阶逻辑的证明系统，使得所有且仅仅所有有效公式能够 在其中被证明，那么就存在一个一阶算术的证明系统，使得所有且仅仅所有在自 然数模型中为真的一阶算术公式能够在其中被证明，而这与哥德尔不完全性定理 矛盾，因此二阶逻辑是不完全的 然而，可能存在一至少在理论上一另一种具有数学意义的二阶逻辑的语义， 使得二阶逻辑相对于这种非标准的新语义是完全的这一想法由h e n k i nf 2 1 1 首 先实现，他指出： “在这种 标准语义的】定义下，我们只能从哥德尔的证明结果得出该 【二阶】演算是不完全的这个推论但是存在这样一个的更大的模型集： 当中的模型为一个与通常的公理和推理规则相一致的演算的符号系 统提供一个解释如果我们重新定义有效公式，使得它们指称那些 在所有这些模型中为真的命题，那么我们能够证明二阶逻辑的通常的 关于哥德尔不完全性定理证明的一个简单介绍，见【1 9 】，第6 章 第一章导论 4 公理系统是完全的，即，一个公式是有效的当且仅当它是一个形式定 理 h e n k i n 所发展的语义在文献中被称为一般语义或h e n k i n 语义粗略地讲，在这 种语义中，约束的个体变元的取值范围还是个体论域，但谓词变元的取值范围 是个体论域的幂集的任意非空子集显然一般语义中的模型( 简称一般模型或 h e n k i n 模型) 比标准模型的范围更广，但标准模型比一般模型更简单，因为后者 只需规定个体论域，而前者除了需要规定个体论域之外，还需要规定谓词变元的 取值范围在f 2 1 1 中，h e n k i n 证明了上述引文所声称的结果，即二阶逻辑相对于 一般语义的完全性定理，而且类似的证明可以推广到高阶逻辑但是一般语义 中的二阶逻辑( 包括高阶逻辑) 其实是一种多型的一阶逻辑一一阶逻辑的一个有 用但无本质区别的变异在一般模型中，由于谓词变元的取值范围不依赖于个体 论域，因此性质和关系都可以从根本上被看成抽象的“个体”，这样便得到了不同 类型的“个体 在技术上讲，对任意一个二阶公式妒，存在一个多型的一阶公式 矽，使得矽在所有一般模型为真，当且仅当妒7 在一阶逻辑的多型语义中是特定公 式集的语义后承5 1 尽管如此，一般模型已被广泛接受和研究，这一方面是由于 无穷集的幂集运算受到“直谓主义”数学家甚至经典数学家的质疑( 而连续统假设 的独立性则加重了质疑的程度) 1 3 】，另一方面是由于一般模型本身也包含了丰富 的数学内涵，如m a n z a n of 2 4 1 ( 1 7 2 页) 从代数角度给出一般模型的定义另外 5 】 还提到，v a nb e n t h e mf 4 1 为一般语义提供了一个辩护，认为一般语义采用了把性 质和关系换成对象的“几何”策略 1 2 逻辑和语言 逻辑与语言的联系可以追溯到逻辑学的鼻祖亚里士多德，要了解亚里士多德 对逻辑的看法一尽管“逻辑”一词没有出现在他的著作中，我们要先了解他对学 科或知识的著名的三区分亚里士多德把学科或知识分成三种：以真理为目的的 理论之学( 物理学、数学和神学) 、以行动为目的的实践之学( 政治和伦理等) 和以 制作为目的的技艺之学( 如造船之技) 根据亚里士多德，理论之学与后二者的区 别在于它是以自身为目的的知识他认为，实践之学和技艺都为人的目的所引导， 行动和制作需要不同的“理性状态的能力 ，但它们都不能形成稳定的知识而只能 形成意见“工具”一词就似乎就表明了亚里士多德给逻辑的定位：逻辑是一门技 事实上，【2 1 】证明了表达力更强的c h u r c h 的a 演算在一般语义中的完全性一个对h e n k i n 的证明的整理在【2 】的第五章 导论5 论研究的是关于词项和命题的推理，它给出了一系列有效的推理范式在亚里士 多德看来，对有效的推理方法的掌握是进行具体研究的预备他对逻辑的定位决 定了三段论只关注词项和命题本身，而不关注它们在外部世界中的所指，换而言 之，三段论的内容是关于语言形式的有效推理，而且关于这些推理范式的知识是 确定地为真的 学界普遍认为现代逻辑学诞生于德国伟大的哲学家和逻辑学家弗雷格弗雷 格的其中一个伟大洞见在于，他发现了一个无论多么复杂的语言表达式都是由简 单表达式系统地和一步一步地组合而成，而且这个过程的每一步都运用了一条在 语义上有意义的句法规则这就是所谓的意义的组合性原则沿着这一想法，弗 雷格发展了第一个现代逻辑系统b e g r i f f s s c h r i f t 这个逻辑系统具有比三段论强 大得多的刻画能力，例如它能够满意地解释在三段论中无法解释的多重量词的问 题弗雷格构造b e g r i f f s s c h r i f t 的首要目的是描述数学中的形式语言的使用规则， 但他的文章( 如 1 5 】， 1 6 ， 17 】) 也反应出他关注自然语言与逻辑的关系弗雷格的 意义的组合型原则容易让人想到语句的逻辑形式和它的语法形式之间存在着张 力，而这一点由罗素在他著名的论文“o nd e n o t i n g 中严正地指出罗素论证，语 句的语法形式是令人误解的，而语句的逻辑形式需要分析才得以显示弗雷格和 罗素等人的工作极大地影响了后来的逻辑实证主义，而后者对形而上学的攻击就 利用了语言的逻辑分析这一武器例如卡尔纳普指出许多形而上学命题都犯了语 法的错误 现代逻辑技术在语法分析上的直接应用是范畴语法的出现首先形式化范 畴语法的是波兰逻辑学家l e s n i e w s k i ，他在1 9 2 9 年发表了他称之为“s e m a n t i c c a t e g o r i e s ”的理论；后来另一位波兰逻辑学家i j d u c i e w i c z 在1 9 3 5 年的发展了 l e s n i e w s k i 的系统，而h j d u c i e w i c z 的系统又被b a r - h i l l e l 进一步发展 1 8 1 ( 9 2 页) 在此基础上，1 9 5 8 年l a m b e k 发展了l a m b e k 演算在l a m b e k 演算中，除了组合 规则，还有结合规则、函数符合规则、范畴提升和除法规则【1 4 1 但是逻辑学技术 真正广泛地应用于语言分析是在蒙太古语法诞生以后蒙太古语法是一个语义 理论，目标是为自然语言的语义提供一个符合直观但“数学上精确”的模型论解释 第一章导论 6 2 7 】蒙太古的想法激发了大批后续文献例如，c o o p e r 1 0 】从蒙 语的分析出发，给出一种处理量词辖域模糊性的方法v i l l a d s e n 在理论的解释范围上与蒙太古语法的“语言系统”，并给出它的证 逻辑丁 本章的安排如下：第一节给出丁的句法和标准语义在第二节我们从广义逻 辑的角度给出限制量化中的量词的解释第三节给出丁的证明系统第四节用 h e n k i n 构造法证明丁相对于标准语义的完全性，这节是本章的重点在第五节 我们从技术角度讨论限制量化和一般语义的关系，给出两个性质的证明第六节 再利用h e n k i n 构造法证明模型论上一个较重要的定理一c r a i g 插值定理，并分 析该方法应用在丁上的局限性 2 1 丁的句法和标准语义 类型集，记为t ，是一个满足以下条件的最小集合：i ，o t ；若口，p t ，则 q p t 其中i 是个体的类型，0 是两个真值的类型丁的词汇表一用a p 表示 一由以下给出： ( 1 ) 逻辑常项： ，一，v ，三 是 第二章限制量化的高阶逻辑t 8 丁- 表达式，因为x p 出现在口( o p ) 卢z p 中在本章第4 节我们会分析这一句法上的限 制带来的语义效应 用w e q 表示类型为o t 的丁- 表达式集，称w e o 中的成员为l 公式对于一 个合法的表达式，给定它最里面的符号的类型下标后，其它符号的类型下标皆 可计算出，因此我们可以省略它们同时我们也省略表达式最外面的括号例如， ( a 触b q ) p 可记为a 触b q 进一步，我们用没有类型下标的小写希腊字母妒，矽，7 表示i 公式例如，1 妒，矽一，y ，v z q ( a d q z a _ 妒) 都是丁- 公式再进一步，简写 比q ( a o a z a 一妒) 为v z 口a d a ( 妒) 我们定义以下符号 ( 1 ) 妒v 妒= 够1 妒_ 矽 ( 2 ) 妒a 矽= d ，( 妒_ 1 妒) ( 3 ) 妒h 砂- - - - a ( 妒_ 矽) a ( 矽_ 妒) ( 4 ) 3 x a a ( 妒) - - - - d 3 x q ( a z na 妒) = d ，1 v z n _ 1 ( a z q 妒) ( 5 ) a q 鼠= 彤- - , ( a n 三b q ) 以下是丁的标准语义给定一个非空集合d ，对每个类型口，论域集d a 由以 下定义： ( 1 ) d i = d ( 2 ) d 。= o ，1 ) ( 3 ) d a 口= d 2 卢 其中d l 称为个体论域丁的标准模型是多元组 m = ( d 。：o t t ) ，) ， 其中j 是解释函数，即 用o m 表示基于m 的指派，即， i ：a ahd n d a o m ：z qhd q d a 当m 在上下文中清楚时，我们只写盯 以下是丁的语义规则 ( 1 ) ( z a ) 盯= 盯( z a ) ，( n a ) 口= l ( o 口) ( 2 ) ( a q p 昂) 盯= ( a a 卢) 口( ( 邬) 仃) 制量化的高阶逻辑t9 ，若( a 阳) 盯( d ) = 1 ， 贝q ( 妒) 口f 。a d 。】= 1 其中盯 z 口d q 】( d a d a ) 表示这样的指派：它对除z n 之外的( 包括类型不是 q 的) 所有变元的指派相同，而州z 口d 口】( z 口) = 叱 若( 妒) 矿= 1 ，也记为盯 妒若对每个矽都有矿 妒，则记为盯# ：若 盯 蕴含仃 妒，则记为 妒若对任意指派一( 因此也对任意模型) ，都有 o r 7 妒，则记为 妒，此时称妒是丁中的有效式对于，若存在盯使得o r ，则 称是可满足的 2 2 从广义量词角度看限制量化 这一节中，我们把丁中的量词看成广义量词，给出它们的单独范畴解释分 别用( v k a 。) 盯和( 孔a a 。a ) 口表示两个相对化量词的解释令 ( v a d q ) 矿= x d q ：( a 0 口) 盯( d ) 1 ，对每个d d 。 ， ( | z n a ) 盯= x d q ：存在d x 使得( 月。) 盯( d ) 1 ) 再令 ( a ) 一矿= _ 【d d q ：( a 。q ) 盯( d ) = 1 ) 于是得到以下更直观但等价的解释 ( v x 口a ) 口= x d 口：( a ) 一盯x ) ， ( j z n a 。口) 盯= x d q ：( a o a ) 一口nx 仍) 可见， 厂：( a ) 盯h ( 比d 4 。q ) 口 9 ：( a ) 盯卜，( | z 口a 0 a ) 盯 分别为地a 和| z n 的解释容易验证，若令 ( 妒( 霉a ) 口= d a d 口：盯 妒盯 z q d 口】) ， 第二章限制量化的高阶逻辑丁 1 0 则有 即 o r v x a a 。a ( 妒) 当且仅当( 妒 a ) 仃( 比a a 。a ) 口， o r j z a a 。a ( 妒) 当且仅当( 妒( z a ) 盯( j z a a 。a ) 口 仃 v x a a 。q ( 妒) 当且仅当( t o ( z a ) 盯( a 。a ) 口， 口 3 x n a 。a ( 妒) 当且仅当( 妒 。) 盯n ( a d a ) 口0 2 3 丁的证明论 在本节和下一节中，如不特别指出，表达式或公式都指的是i 表达式或公 式量词的辖域和变元的自由出现的定义如同它们在一阶逻辑中的定义用 a p p q 既】表示用既替换a a 中所有自由出现的x n ( 若需要对山进行易字) 所 得到的表达式( 严格定义可参见一例如一 6 】第二章的定义2 2 、3 1 、3 3 和 3 9 ) 丁的公理是所有以下形式的公式 ( 1 ) t 中的所有命题重言式 ( 2 ) v z 口a ( 妒，妒) ，( b 乞q a 。q ( 妒) ，v z q a d q ( 矽) ) ( 3 ) ( a 。q x a _ 妒) _ v x n a o a ( c p ) ，其中z 口不在妒中自由出现 ( 4 ) v x 口a ( 妒) ( a b q _ 妒k a b 口】) ( 5 ) a n 三a n ，( a q 三风) _ ( 风三a n ) ， ( a a 三风) _ ( ( 玩三倪) _ ( a q 三q ) ) ( 6 ) ( 以口三a q 卢) _ ( ( 昂兰邬) _ ( 以p 兰a q p 昂) ) ( 7 ) ( 妒三妒) h ( 妒h 妒) 丁的推理规则包含以下几条： ( 1 ) 分离规则m p ( 2 ) r g e ( a z a 一妒) 号v x 口a ( 妒) ( 3 ) s u b 垆= 争妒陋a a q ，妒= 争妒 n 口a 口】 ( 4 ) f u n ( a 。o x o 三b q 卢z 口) = ( a n p 兰b 。p ) 一个k ( 1 k 通过m p 由前面 任何被假设的公 由忱通过r g e 得到( 5 ) 妒是妒k a a q 】或妒k a a l 这样形式的公式，其中z q 不在之前任何被 假设的公式中自由出现，或a a 不在它们任一个中出现，并且存在慨= 妒，其中 i k ，此时由慨通过s u b 得到( 6 ) 是a a b 兰鼠p 这样形式的公式，存在 忱= 4 。卢即兰鼠卢即，其中i k 并且即不在a 口p 、风p 和慨之前任何被假设的 公式中自由出现，此时讯由慨通过f u n 得到 用卜妒表示存在一个丁中的形式证明f p ，使得所有妒是f p 的最后一个 公式，并且f p 中被假设的公式都在中若对于任何妒w e 都有卜妒，我们 称是丁- 不一致的，反之则是i 一致的如不特别作说明，说一个i 公式集是 一致的，都指它是l 一致我们用卜妒作为0 卜妒的缩写，此时称妒是丁的定理 我们先给出几个引理，但省略它们的证明这几个引理在下文的证明中会利 用到 引理1 假设卜a q n q ，其中a n 不出现在a a 口和中的每个公式中，则是 不一致的 引理2 假设卜妒【z q a 。】，其中a q 不出现在妒和中的每个公式中，则 卜v x 口a ( 妒) 引理3 假设卜a q p 即三b q p 口卢，其中口卢不出现在a q p ，b q p 和中的每个公 式中，则卜a q p 三玩p 2 4 丁的完全性一h e n k i n 构造法 丁的可靠性可以被直接证明 定理4 f ，可靠性定理夕丁是可靠的，即，若卜妒，则 垆 证明容易验证：若妒是丁的公理，则妒是丁的有效式；若妒是有效式，而妒7 是 妒通过m p ，g r e ，s u b 或f u n 得到的，那么妒7 也是有效式具体证明过程从 略口 第二章限制量化的高阶逻辑丁 1 2 为了证明完全性，即上述定理中的另一个方向，我们要做一系列预备工作我 们证明完全性的在文献中被称为h e n k i n 构造法( 如见m a r k e r 2 5 ，第3 5 页) 先 考虑以下引理 引理5 ( a “z a b q 】) 盯= ( a 卢) 州z a d o l ，特豌抛，盯 妒 z a b q ，当且仅当，盯k q d q 】 妒，其中d a = ( 鼠) 口 证明按照表达式的复杂度施归纳于a 口，具体证明从略 口 对丁的词汇表按照以下方式进行扩充：对每个类型o l ，加入一个可数无穷的 新常元集c q ，则新词汇表a p 7 = a puu q tc q 将由此得到的新表达式集记为 w e ，如同前文，w 磁表示w e ，中类型为a 的表达式在一个词汇表中，说丁的 一个公式集是极大一致的，指它是一致的并且它不是任何一致公式集的真子集 引理6 若w e 。是极大致的，则它具有以下性质? ( 1 ) 咿和1 9 的其中一个属于 例妒- 妒当且仅当妒隹或者砂 俐若比a a 。o ( 妒) ，贝埘每个既，a 。n 既_ 纠z n 鼠】 陴) a q 三a q j 若a q 三b o ，则b n 三a q i 若a a 兰b a 且b a 三瓯，则a a 三g 俐若a 如三a a 卢且昂三邬h ，则a 如昂兰a 口p 邬 俐妒三矽当且仅当妒h 妒 证明从略 一个丁的h e n k i n 集日是一个极大一致集，而且它具有以下性质： ( 1 ) 若，比q a o q ( 妒) h ，则存在o a 使得a 鲫o a ，妒k a q 】h ( 2 ) 若a a 卢鼠卢h ，则存在叩使得a 口p o 卢鼠卢q p h ( 3 ) 对每一个a a ，存在a 。使得a q 三a q h 需要注意，极大一致集和h e n k i n 集都依赖于丁的词汇表 引理7 若w e 0 是致的，则存在h e n k i n 集日w e 使得h 证明列举w e 的成员： 妒1 ，妒t ， 口 第二章限制量化的高阶逻辑丁 1 3 然后按照以下方法构造一个公式集系列 o 1 2 使得它们满足以下条件： ( 1 ) 令e o = ( 2 ) 若mu 妒仇卜一致，则令e m + 1 = m ( 3 ) 若mu 【妒m ) 一致，且妒m = a a 兰a a ，则令m + 1 = e mu0 阳) u a q 兰 a a ) ，其中a a 是一个新常元，并且它不出现在m 和中易见m 和妒m 中 只包含有穷多个新常元，故这样的a a 一定存在，在下面的证明中也是如此现 在证明e m + 1 是一致的假设它不一致，则mu 妒仇) 卜a a a 口根据引理1 ， mu 妒m ) 不一致，矛盾 ( 4 ) 若mu _ 妒m ) 一致，且妒m = _ 1 v z 。a 。n ( 妒) ，则令e m + 1 = mu 妒m ) u a o a a q ) o 、妒k q a q 】) ，其中a n 是一个不出现在妒m 和m 中任一公式中的新 常元假设e m + 1 不一致，则mu 妒m ) 卜妒【z q a q 】根据引理2 ，mu 妒m ) 卜 比q 4 ( 妒) ，因此mu 妒m ) 不一致，矛盾 ( 5 ) 若mu 妒m ) 一致，且妒m = a a 卢b c , z ，则令e m + 1 = e 仇u 妒m ) u a a p a 口b q 芦n 卢) ，其中a q 是一个不出现在妒m 和m 中任一公式中的新常元 假设m + l 不一致，则mu 妒m ) 卜- a 。p 即三b a z a p 根据引理3 ，mu 妒m ) 卜 a n 口三b o p 因此mu 妒m ) 不一致，矛盾 ( 6 ) 若mu _ ( 妒m ) 一致，且不属于上述任一种情况，则令m + 1 = e mu 妒m ) 最后，令u m u e m = h 可以验证h 是极大一致的，而且它是h e n k i n 集，即 它具有h e n k i n 集的三个性质 口 下面我们利用h e n k i n 集日来构造一个丁的模型对每一个表达式 a q w e 7 ，令 i a 口i = 鼠：鼠三a a 日) 根据引理6 ，易证i a q i 是一个表达式的等价类用i w e l 表示所有类型为o 的表 达式的等价类的集合令个体论域为l w e , i ，以下我们根据类型的复杂度分情况 定义一个从i w e l 到d q 的单射圣 ( 1 ) 令圣( 1 a 1 ) = l a i ( 2 ) 令圣( 1 妒1 ) = 1 当且仅当妒h ( 3 ) 假设圣在l w e i ( 口o ) 和1 w e 名i 上已被定义，圣在1 w e o i 上的定义如 第二章限制量化的高阶逻辑丁 1 4 下：x , l 于每个如d 卢， 到知叭粕拶筹邬懈卢仁1 ， 其中z 2 疗是一个任意指定的变元我们需要证明圣是合法的单射根据引 理7 ，若i a ：口i = i a a p i ，且i 睇i = l 昂i ，则1 4 如昂l = i a a a b a i 所以上述定 义是合法的要证圣是单射，假设i a 品i i a 口p i ，即，a 如a q p h 所 以存在q 卢使得以口。卢a a p n 卢h ，即，i a 乙o p i i a 。p n 芦i 根据归纳假设， 圣( i a ：口。卢1 ) 中( i a q 芦a p i ) 所以西( 1 a ：口i ) 西( i a a 卢i ) ( 4 ) 假设垂已在1 w 砀l 上被定义，垂在i w e o p i 上的定义如下：对于每个 d 口d 口， 圣( i a 卵i ) ( 如) = 。垂( i a o a b a l ) 薯磊亨昂使得i 邬i = 如 ( 2 2 ) 类似情况( 3 ) ，也能证明圣是合法的单射进一步，根据h e n k i n 集的最后一个性 质，等式( 2 2 ) 与下述等式等价 西( i a 。卢1 ) ( d 卢) = 。西( i a o ；3 a a l ) 薯磊亨n 卢使得i n 卢i = d 卢 ( 2 3 ) 这就完成对西的定义 从现在开始，我们把垂( i a 口i ) 和l a q i 等同起来，圣( 川) 和m 等同起来接下 来我们要根据由来定义一个丁的模型和指派定义m h = ( d q ：o t t ) ：，) 使 得其中的d i = 1 w e ，i ( 因此 d a ：q t ) 已确定) ，j ：a q 卜i o q i 定义一个基于 m 日的指派：盯：x nhk i 定理8 在上述定义的模型和指派下，对于每个a a w e 7 ，有 ( 九) 盯= i a n | 特别地对于每个咿h 有 仃# ：妒 证明易见第二个分旬是第一个分旬的特殊情况，因此只考虑第一个分句的证明 对应表达式的5 条句法规则分情况进行归纳证明根据引理6 ，容易验证在前4 种情况中上述等式成立，故这里只证明它在量化的情况也成立 第二章限制量化的高阶逻辑丁 1 5 假设i 比n ( 妒) i = 0 根据h e n k i n 集的性质，存在a a 使得i n a i = 1 且 i 妒 z na 口】i = 0 根据定义和归纳假设，i o a l =