一阶逻辑

一阶逻辑是使用于数学、哲学、语言学及计算机科学中的一种形式系统。过去一百多年，一阶逻辑出现过许多种名称，包括：一阶断言演算、低端断言演算、量化理论或谓词逻辑。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑有使用量化变量。一个一阶逻辑，若具有由一系列量化变量、一个以上有意义的断言字母及包含了有意义的断言字母的纯公理所组成的特定论域，即是一个一阶理论。一阶逻辑和其他高端逻辑不同之处在于，高端逻辑的断言可以有断言或函数当做引数，且允许断言量词或函数量词的（同时或不同时）存在。在一阶逻辑中，断言通常和集合相关连。在有意义的高端逻辑中，断言则会被解释为集合的集合。存在许多对一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）的演绎系统。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。一阶逻辑是数学基础中很重要的一部分，因为它是公理系统的标准形式逻辑。许多常见的公理系统，如一阶皮亚诺公理和包含策梅洛-弗兰克尔集合论的公理化集合论等，都可以形式化成一阶理论。然而，一阶定理并没有能力去完整描述及范畴性地建构如自然数或实数之类无限的概念。这些结构的公理系统可以由如二阶逻辑之类更强的逻辑来获取。不像命题逻辑只处理简单的陈述命题，一阶逻辑还额外包含了断言和量化。断言像是一个会传回真或伪的函数。考虑下列句子：“苏格拉底是哲学家”、“柏拉图是哲学家”。在命题逻辑里，上述两句被视为两个不相关的命题，简单标记为p及q。然而，在一阶逻辑里，上述两句可以使用断言以更相似的方法来表示。其断言为Phil(a)，表示a是哲学家。因此，若a代表苏格拉底，则Phil(a)为第一个命题－p；若a代表柏拉图，则Phil(a)为第二个命题－q。一阶逻辑的一个关键要点在此可见：字符串“Phil”为一个语法实体，以当a为哲学家时陈述Phil(a)为真来赋与其语义。一个语义的赋与称为解释。一阶逻辑允许以使用变量的方法推论被许多组件共享的性质。例如，令Phil(a)表示a为哲学家，且令Schol(a)表示a为学者。则公式表示若a为哲学家，则a为学者。符号 → {displaystyle to } 被用来标记一个条件叙述。箭号的左边为假设，右边则为结论。此一公式的真值取决于标记成a的组件，及“Phil”和“Schol”的解释之上。“对于每个a，若a为哲学家，则a为学者”之类形式的断言，需要同时使用变量及量化。再次，令Phil(a)表示a为哲学家，且令Schol(a)表示a为一学者，则一阶叙述表示不论a代表什么，若a为哲学家，则a为学者。此处的 ∀ {displaystyle forall } （全称量化）代表宣称对“所有”a的选择，括弧内的叙述皆为真的想法。为了表明，声称“如果是一个哲学家然后是一个学者”是假的，一会显示有一些人是不是一个学者的哲学家。这与存在量词可以表示反诉 ： 若想证明“若a为哲学家，则a为学者”此一宣称是错的，有些人会证明存在有些不是学者的哲学家。此一反论可以用存在量化 ∃ {displaystyle exists } 来表示：其中，断言Phil(a)和Schol(a)都各只有一个参数。但一阶逻辑其实也可以表示具有一个以上参数的断言。例如，“存在一些人可以在任何时间被愚弄”可表示成这里，Person(x)解释为x是人，Time(y)为y是某段时间，且Canfool（x,y）则为（人）x可在（时）y被愚弄。清楚地说，上述叙述表示至少存在一个人可以在任何时间被愚弄，这比“在任何时间，至少存在一个人可以被愚弄”的叙述要强。后者并不意味着，被愚弄的人在任何时间时上总是要是同一位。量化的范围是由可以用来满足量化的对象所组成的集合（在本节中的一些非正式的例子里，量化的范围并没有被指定）。除了指定Person和Time等断言符号的意义，解释也必须指定一个非空集合，称为论域，做为量化的范围。因此， ∃ a Phil ( a ) {displaystyle exists a{text{Phil}}(a)} 之类形式的叙述在一特定解释下称之为真，若在可用来赋予断言中符号Phil意义的解释所指定的论域里存在着对象。一阶逻辑可分成两个主要的部分：语法决定哪些符号的组合是一阶逻辑内的合法表示式，而语义则决定这些表示式之前的意思。和英语之类的自然语言不同，一阶逻辑的语言是完全角式的，因为可以机械式地判断一个给定的表示式是否合法。存在两种合法的表示式：“项”（直观上代表对象）和“公式”（直观上代表可真或伪的断言）。一阶逻辑的项与公式是一串符号，这些符号一起形成了这个语言的词汇表。如同所有的形式语言一般，符号本身的性质不在形式逻辑讨论的范围之内；它们通常只被当成字母及标点符号。一般会将词汇表中的符号分成“逻辑符号”（总有相同的意思）及“非逻辑符号”（意思依解释不同而变动）。例如，逻辑符号 ∧ {displaystyle land } 总是解释成“且”，而绝不会解释成“或”。另一方面，一个非逻辑断言符号，如Phil(x），可以解释成“x是哲学家”、“x的个名为Philip　的人”或任何其他的1元断言，单看其解释为何。词汇表中存在若干个逻辑符号，虽然会因作者而异，但通常包括：需注意，并不是所有的符号都需要，只要有量化符号的其中一个、否定及且、变量、括号及等式就足够了。还存在许多定义了额外逻辑符号的变体：非逻辑符号用来表示论域上的断言（关系）、函数及常数。以前标准上会对所有不同的用途使用相同的无限集的非逻辑符号，而最近则会根据应用的不同而使用不同的非逻辑符号。因此变得需要枚举出使用于一特定应用中的所有非逻辑符号。其选择是经由标识来形成的。传统的做法是对所有的应用都只有单一个无限集的非逻辑符号。因此，根据传统的做法只会存在一种一阶逻辑的语言。这种做法现在依然很常见，尤其是在哲学方面的书籍。在当代的数理逻辑里，标识会因应用的不同而不同。数学里的典型标识，在群里为{1, ×}，或只为{×}；在有序域里为{0, 1, +, ×, <}。并没有限制非逻辑符号的数量，标识可以是空的、有限、无限，甚至是不可数的。例如，在勒文海姆–斯科伦定理的证明之中即会出现不可数的标识。根据最近的做法，每个非逻辑符号皆为下列两种类型的其中一种。如何分辨断言符号与函数符号？形成规则定义一阶逻辑的项及公式。因为项及公式被表示为一串符号，这些规则可被用来写成项及公式的形式文法。这些规则通常是上下文无关的（规则的每个结果在其左侧都会有单一个符号），除非允许有无限多符号，且有许多开始符号，如项中的变量。项可依如下规则递归地定义：只有可经由有限次地应用上述规则来得到的表示式才是项。举例来说，不存在包含断言符号的项。公式（或称合式公式）可依如下规则递归地定义：只有可经由有限次地应用上述规则来得到的表示式才是公式。由头两个规则得到的公式称为原子公式。举例来说，是公式，若f是1元函数符号，P是1元断言符号，且Q是3元断言符号。另一方面， ∀ x x → {displaystyle forall x,xrightarrow } 则不是公式，虽然这也是由词汇表中的符号组成的字符串。定义中的括号，其用途是为了确保任何公式都只能依递归定义以单一种方法得到（换句话说，每一个公式都只存在唯一的剖析树）。这个性质被称为公式的唯一可读性。对于括号要用在公式中的哪里存在有许多的惯例。例如，有些作者会使用冒号或句号来代替括号，或变更括号插入的地方。但每个作家个人的定义都必须证明会满足唯一可读性。定义公式的规则无法定义“若-则-否则”函数ite（c,a,b），其中的c是个以公式表示的条件，当c为真时传回a，为假时传回b。这是因为断言和函数都只能接受项当做其参数，但上述函数的第一个参数为公式。某些建构在一阶逻辑上的语言，如SMT-LIB 2.0，会增加此一定义。为了方便起见，会约定逻辑算符的优先性，来减少括号使用的情况。这些规则和算术中的运算顺序很像，一个常见的惯例为：此外，定义中不需要的额外标点符号也许会插入公式中，使公式更容易阅读。因此，公式可写成在某些领域里，常见使用中缀表示法来代表二元关系及函数，而非上面定义的前缀表示法。例如，在算术中，一般会写成“2+2=4”，而非“=(+(2,2),4)”。一般会将以中缀表示法表示的公式当做是以前缀表示法表示的对应公式的缩写。上面定义中的二元联结词，如 → {displaystyle to } ，是使用中缀表示法。一个较少见的惯例为波兰表示法，它将 → {displaystyle rightarrow } 、 ∧ {displaystyle wedge } 等放在参数的前面而非之间。这个表示法允许舍弃所有的标点符号。波兰表示法是简洁且优雅的，但因为对人类很难阅读，所以实务上不常使用。使用波兰表示法，公式会变成"∀x∀y→Pfx¬→ PxQfyxz"。在一个公式里，变量可能是自由的或约束的。直观上来看，一个变量在公式里若没有被量化则是自由的：在 ∀ y P ( x , y ) {displaystyle forall y,P(x,y)} 里，变量x是自由的，而y则是约束的。自由变量和约束变量可依如下规则递归地定义：举例来说，在 ∀ {displaystyle forall } x ∀ {displaystyle forall } y (P(x) → {displaystyle rightarrow } Q(x,f(x),z))里，x和y是约束变量，z是自由变量，而w则两者皆不是，因为它没有出现在公式之中。自由和约束也可以用来专指在公式里特定地方出现的变量。如在 P ( x ) → ∀ x Q ( x ) {displaystyle P(x)rightarrow forall x,Q(x)} 里，第一个x是自由的，而第二个则是约束的。换句话说，x在 P ( x ) {displaystyle P(x)} 里是自由的，而在 x {displaystyle x} 在 ∀ x Q ( x ) {displaystyle forall x,Q(x)} 里则是约束的。在一阶逻辑中，一个没有自由变量的公式称为一阶句子。此类公式在特定解释之下即会有良好定义的真值。例如，公式Phil(x)是否为真需看x代表什么，而句子 ∃ x Phil ( x ) {displaystyle exists x,{text{Phil}}(x)} 在一特定解释下则必为真或必为假。有序阿贝尔群的语言有一个常量0，一个一元函数−，一个二元函数 +，和一个二元关系≤。所以一阶语言的解释会对语言内的所有非逻辑常数赋予上意义，同时也决定能指明量化范围的论域。其结果为，每个项都会被赋予其代表的组件，每个句子也都会被赋予上一个真值。这样，解释即对语言内的项及公式提供了语义。研究形式语言的解释的学科称为形式语义学。论域D是由某种类型的“对象”所组成的非空集合。直观上来看，一阶公式是有关这些对象的叙述。例如， ∃ x P ( x ) {displaystyle exists xP(x)} 叙述存在一个对象x，能使得指涉此对象的断言P为真。论域即是此类考量的对象的集合，例如可取D为整数的集合。函数符号的解释是函数。举例来说，若论域由整数所组成，则一个2元的函数符号f能解释为给出其参数之和的函数。换句话说，符号f和在此解释下为加法的函数I(f)是相关连的。常数符号的解释是一个从单元素集合D0映射至D的函数，也可简单视为是D内的一个对象。例如，一个解释可将值 I ( c ) = 10 {displaystyle I(c)=10} 赋予常数符号 c {displaystyle c} 。n元断言符号的解释是由论域中的元素所组成的n对有序集。这意味着，给定一个解释、一个断言符号及论域中的n个元素，则可依给定的解释判断这些元素的断言是否为真。例如，一个2元断言符号P的解释I(P)可以是一对整数，能使得第一个整数小于第二个整数。依据这个解释，断言P在其第一个参数小于第二个参数时为真。指定一个解释的最常见方法是指定一个结构（或称做模型，见下文）。结构包括一个由论域及标识内的非逻辑项的解释I所组成的非空集合。这个解释自身是个函数：一个公式由给定的解释及将论域中的元素与每个变量相关连的变量赋值μ来决定为真或为假。需要变量赋值的原因是为了给予具自由变量的公式（如 y = x {displaystyle y=x} ）意义。上述公式的真值为何要看x和y是否标记着相同的个体。首先，变量赋值μ可以扩展到语言内的所有项，使每个项都能映射至论域中的单一元素。下列的规则被用来得到赋值：再来，每个公式皆可赋予一个真值。用来得到赋值的递归性定义称为T-模式。若一个公式不包含自由变量，即为一个句子，则一开始的变量赋值不会影响其真值。换句话说，一个句子根据M及 μ {displaystyle mu } 为真，当且仅当这个句子根据M及其他的变量赋值 μ ′ {displaystyle mu '} 为真。还有第二种常见的做法可以定义真值，而且不需要依靠变量赋值函数。给定一个解释M，首先将一组常数符号加至标识之中，每一个在M中的论域的元素对应一个常数符号：称对每个域论中的元素d，都会固定有一个常数符号cd。如此，解释就会被扩展至能使每一新的常数符号被赋予至其对应的论域元素上。现在可语法性地定义量化公式的真值如下：这个做法对所有的句子会给出和使用变量赋值的做法一样的真值。若句子φ在一给定解释M下为真，则称M 满足φ，标记为 M ⊨ ϕ {displaystyle MvDash phi } 。一个句子称为可满足的，若存在某个解释使其为真。具自由变量的公式的可满足性就较为复杂了，因为只用解释并无法决定此类公式的真值。一个常见的惯例是称一个具自由变量的公式在一个解释下为可满足的，若不论如何将论域中的个体赋予其自由变量，这个公式皆为真。这等价于称公式为可从足的，当且仅当其全称闭包为可满足的。一个公式是逻辑有效的（或简单称为有效的），若在每一个解释之下皆为真。此类的公式和命题逻辑中的重言式扮演着相似的角色。一个公式φ是公式ψ的逻辑结论，若每个使得ψ为真的解释皆会使得φ为真。在此一状况下，称φ被ψ逻辑蕴涵着。另一种赋予一阶逻辑语义的方法可经由抽象代数处理。这种方法是将命题逻辑的林登鲍姆-塔斯基代数扩展而成。有如下几种类型：这些代数都是纯粹扩展两元素布尔代数而成的格。塔斯基和葛范德于1987年证明，没有超过包在三个以上的量化内的原子句子的部分一阶逻辑，其表示力和关系代数相同。上述部分一阶逻辑令人十分地感到有兴趣，因为它已足够表示皮亚诺算术和公理化集合论，包括典型的ZFC。他们亦证明了，具有简单有序对的一阶逻辑和具有两个有序的投影函数的关系代数等价。一阶理论是由在一特定一阶标识内的一组公理所组成的。公理所组成的集合通常是有限的或递归可枚举的，此类的理论称为是有效的。有些作者要求理论也要包括所有由公理导出的逻辑结论。满足给定理论内的所有句子的一阶结构称为此理论的模型。基本类是由所有满足特定理论的结构所组成的集合。这些类是类型论里的研究主题。许多理论都有一个预期解释，即一个在研究理论时会在意的某种模型。例如，皮亚诺公理的预期解释是由一般的自然数和其一般的运算所组成的。不过，勒文海姆–斯科伦定理证明，大多数的一阶理论也都会有其他的非标准模型。一个理论是兼容的，若不可能由这个理论的公理中证明出矛盾来。一个理论是完备的，若对每个其标识内的公式，此公式或公式的否定会是个由理论公理导出的逻辑结论。哥德尔不完备定理证明，有效的一阶理论只要它强到足以蕴涵自然数的理论，即无法同时是兼容且完备的。上述定义需要任何一个解释的论域均为非空集合。但在如自由逻辑之中，设置空论域是被允许的。更甚之，若代数结构的类包含一个空结构（如空偏序集），当允许空论域时，这个类只能是一阶逻辑中的一个基本类，不然就要将空结构由类中移除。不过，空论域存在着一些难点：因此，若空论域是被允许的，通常也必须被视成特例。不过，大多数的作家会简单地将空论域由定义中排除。设 t是项。φ(x)是可能包含x作为自由变量的公式。φ(t)可定义为把自由变量x替代为t的结果，但前提是必须没有任何t在φ(x)中是约束的。若非如此，则x替代成t之前，必须先把φ中的约束变量，改为不同于t的符号。例如把公式φ(x)假定为∀y:y ≤ x（"x是极大的"）。若用t代换x，则φ(t)即∀y:y ≤ t就表示t是极大的。这里举个错误的例子，若在φ(x)中含有约束变量y的状况下，不去修改φ(x)中含有约束变量y，直接把x代换成y，代换结果如下∀y:y ≤ y如此一来即成为跟φ(x)意义完全不同的公式。正确的演算方法为先把φ(x)中的约束变量用到y的地方改成不同于y的符号，好比z即把∀y:y ≤ x改成∀z:z ≤ x，这两命题的意义一致。再把x代换成y，即为∀z:z ≤ y所以φ(y)表示∀z:z ≤ y，而不是∀y:y ≤ y忘记这个条件是声名狼籍的犯错误原因。肯定前件充当推理的唯一规则。叫做全称普遍化的推理规则是断言演算的特征。它可以陈述为这里的Z(x)假定表示断言演算的一个已证明的定理，而∀xZ(x)是它针对于变量x的闭包。断言字母Z可以被任何断言字母所替代。下面描述一阶逻辑的公理。如上所述，一个给定的一阶理论有进一步的非逻辑公理。下列逻辑公理刻画了本文的样例一阶逻辑的一种演算。对于任何理论，知道公理的集合是否可用算法生成，或是否存在算法确定合式公式为公理，是很有价值的。如果存在生成所有公理的算法，则公理的集合被称为递归可枚举的。如果存在算法在有限步骤后确定一个公式是否是公理，则公理的集合被称为递归的或“可判定的”。在这种情况下，你还可以构造一个算法来生成所有的公理：这个算法简单的（随着长度增长）一个接一个的生成所有可能的公式，而算法对每个公式确定它是否是个公理。一阶逻辑的公理总是可判定的。但是在一阶理论中非逻辑公式就不必需如此。下列四个公理是断言演算的特征：它们实际上是公理模式：表达式W表示对于其中任何wff，x不是自由的；而表达式Z(x)表示对于任何wff带有额外的约定，即Z(t)表示把Z(x)中的所有x替代为项t的结果。在一阶逻辑中对使用等式（或恒等式）有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果，区别主要在术语上。断言演算是命题演算的扩展，它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件来定义（可以有很多不同的方式），则断言演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说，断言演算采用的公理有：一个句子被定义为是在一阶逻辑中可证明的，如果可以通过从断言演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。如果我们有一个理论T（在某些语言中叫做公理的陈述的集合），则一个句子φ被定义为是在理论T中可证明的，如果在一阶逻辑中对于理论T的某个公理a, b,...的有限集合是可证明的。可证明性的一个明显问题是它好像非常特别：我们采用了显然随机的公理和推理规则的搜集，不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理确保这实际上不是问题：这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是，在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义（尽管在不同的可证明性的定义下证明的长度可能有巨大差别）。有很多不同（但等价）的方式来定义可证明性。前面的演算是"希尔伯特风格"演算的一个典型例子，它有许多不同的公理但只有非常少的推理规则。"根岑风格"断言演算有非常少的公理但有许多推理规则。文法上说断言演算在现存的命题演算上增加了“断言-主词结构”和量词。主词是给定的个体群组（集合）的一个成员的名字，而断言是在这个群组上的关系，一元断言在哲学中称为性质，在数学中称为指示函数，在数理逻辑中称为布尔值函数。下面列出了一些重要的元逻辑定理。用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中， p ∨ q {displaystyle plor q} 意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。带有等式的FOL不包含或允许定义if-then-else断言或函数if（c,a,b），这里的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，断言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。 断言if（c,a,b）如果重写为 ( c ∧ a ) ∨ ( ¬ c ∧ b ) {displaystyle (cwedge a)lor (neg cwedge b)} 就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况断言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这里的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。 其他人进一步扩展FOL使得函数和断言可以在任何位置接受项和公式二者。除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 ，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。单一参数断言可以用来在合适的地方实现类型的概念。例如：断言Man(x)可以被认为是一类“类型断言”（就是说，x必须是男人）。 断言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：容易写成 ∃ x M a n ( x ) → M o r t a l ( x ) {displaystyle exists xMan(x)rightarrow Mortal(x)} ，但这将等价与 ∃ x ¬ M a n ( x ) ∨ ∃ x M o r t a l ( x ) {displaystyle exists xneg Man(x)lor exists xMortal(x)} （“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。例如，在一阶逻辑中你不能断言实数的集合的上确界性质，它声称实数的所有有界的、非空集合都有上确界；这就需要二阶逻辑了。很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用断言逻辑完全表达。换句话说，没有断言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）断言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。&    ∨    ¬    ~    →    ⊃    ≡    |    ∀    ∃    ⊤    ⊥    ⊢    ⊨    ∴    ∵