一阶逻辑

一阶逻辑(first order logic, FOL)也叫一阶谓词演算，允许量化陈述的公式，是使用于数学、哲学、语言学及计算机科学中的一种形式系统。一阶逻辑是区别于高阶逻辑的数理逻辑，它不允许量化性质。性质是一个物体的特性；所以一个红色物体被表述为有红色的特性。

逻辑程序的语言是一阶谓词演算的子集，因为它对许多任务有用。一阶谓词演算可以看作是一种对逻辑程序的语言，它可以增加disjunction析取和显式量化。一阶逻辑是一阶的，因为它允许对域内的个体进行量化。一阶逻辑既不允许谓词为变量，也不允许对谓词进行量化。

二阶逻辑允许对一阶关系和谓词进行量化，其参数是一阶关系。这些都是二阶关系。例如，二阶逻辑公式

它定义二阶关系对称，如果其参数为对称关系，则为真。一阶逻辑是递归可枚举的，这意味着会有一种完整的证明过程，在这个过程中，每一个真实的陈述都可以通过一个在图灵机上的证明程序来证明。二级逻辑不是递归的可枚举的，因此不存在可以在图灵机器上实现的完整的证明过程。

【来源ARTIFICIALINTELLIGENCE，URL：http://artint.info/html/ArtInt_288.html#id9】

举例：

不像命题逻辑只处理简单的陈述命题，一阶逻辑还额外包含了断言和量化。

断言像是一个会传回真或伪的函数。考虑下列句子：“苏格拉底是哲学家”、“柏拉图是哲学家”。在命题逻辑里，上述两句被视为两个不相关的命题，简单标记为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为学者。符号被用来标记一个条件叙述。箭号的左边为假设，右边则为结论。此一公式的真值取决于标记成a的元件，及“Phil”和“Schol”的解释之上。

对于每个a，若a为哲学家，则a为学者”之类形式的断言，需要同时使用变数及量化。再次，令Phil(a)表示a为哲学家，且令Schol(a)表示a为一学者，则一阶叙述

表示不论a代表什么，若a为哲学家，则a为学者。此处的（全称量化）代表宣称对“所有”a的选择，括弧内的叙述皆为真的想法。

为了表明，声称“如果是一个哲学家然后是一个学者”是假的，一会显示有一些人是不是一个学者的哲学家。这与存在量词可以表示反诉：若想证明“若a为哲学家，则a为学者”此一宣称是错的，有些人会证明存在有些不是学者的哲学家。此一反论可以用存在量化来表示：

其中，

• ┐是否定算符：为真当且仅当为假；换句话说，当且仅当a不是学者。
• ∧是合取算符：表示a是哲学家且不是学者。

断言Phil(a)和Schol(a)都各只有一个参数。但一阶逻辑其实也可以表示具有一个以上参数的断言。例如，“存在一些人可以在任何时间被愚弄”可表示成

这里，Person(x)解释为x是人，Time(y)为y是某段时间，且Canfool（x,y）则为（人）x可在（时）y被愚弄。清楚地说，上述叙述表示至少存在一个人可以在任何时间被愚弄，这比“在任何时间，至少存在一个人可以被愚弄”的叙述要强。后者并不意味着，被愚弄的人在任何时间时上总是要是同一位。

量化的范围是由可以用来满足量化的物件所组成的集合（在本节中的一些非正式的例子里，量化的范围并没有被指定）。除了指定Person和Time等断言符号的意义，解释也必须指定一个非空集合，称为论域，做为量化的范围。因此，之类形式的叙述在一特定解释下称之为真，若在可用来赋予断言中符号Phil意义的解释所指定的论域里存在着物件。

语法

一阶逻辑可分成两个主要的部分：语法决定哪些符号的组合是一阶逻辑内的合法表示式，而语义则决定这些表示式之前的意思。

词汇表

和英语之类的自然语言不同，一阶逻辑的语言是完全形式的，因为可以机械式地判断一个给定的表示式是否合法。存在两种合法的表示式：“项”（直观上代表物件）和“公式”（直观上代表可真或伪的断言）。一阶逻辑的项与公式是一串符号，这些符号一起形成了这个语言的词汇表。如同所有的形式语言一般，符号本身的性质不在形式逻辑讨论的范围之内；它们通常只被当成字母及标点符号。

一般会将词汇表中的符号分成“逻辑符号”（总有相同的意思）及“非逻辑符号”（意思依解释不同而变动）。例如，逻辑符号总是解释成“且”，而绝不会解释成“或”。另一方面，一个非逻辑断言符号，如Phil(x)，可以解释成“x是哲学家”、“x的个名为Phil的人”或任何其他的1元断言，单看其解释为何。

1.逻辑符号

词汇表中存在若干个逻辑符号，虽然会因作者而异，但通常包括：

1. 量化符号及。
2. 逻辑联结词：且、或、条件、双条件及否定。偶尔还会包括一些其他的逻辑联结词。
3. 括号、方括号及其他标点符号。此类符号的选择依文章不同而有所不同。
4. 无限集的变数，通常标记为英文字母末端的小写字母，也常会使用下标来区别不同的变数。
5. 一个等式符号=。详见下面的“等式”一节。需注意，并不是所有的符号都需要，只要有量化符号的其中一个、否定及且、变数、括号及等式就足够了。还存在许多定义了额外逻辑符号的变体：
6. 有时也会包括真值常数，用T、Vpq或来表示“真”，并用F、Opq或来表示“假”。若没有此类零参数的逻辑算符，这两个常数就只能用量化来表示。
7. 有时也会包括额外的逻辑联结词，如谢费尔竖线、NAND及异或。

2.非逻辑符号

非逻辑符号用来表示论域上的断言（关系）、函数及常数。以前标准上会对所有不同的用途使用相同的无限集的非逻辑符号，而最近则会根据应用的不同而使用不同的非逻辑符号。因此变得需要列举出使用于一特定应用中的所有非逻辑符号。其选择是经由标识来形成的。

传统的做法是对所有的应用都只有单一个无限集的非逻辑符号。因此，根据传统的做法只会存在一种一阶逻辑的语言。这种做法现在依然很常见，尤其是在哲学方面的书籍。

1)对每个整数，皆存在一组元断言符号。因为这些断言符号表示个元素间的关系，因此也称为关系符号。对每个参数量，皆能有无限多个断言符号：

2)对每个整数，皆存在无限多个元函数符号：在当代的数理逻辑里，标识会因应用的不同而不同。数学里的典型标识，在群里为或只为；在序体里为。并没有限制非逻辑符号的数量，标识可以是空的、有限、无限，甚至是不可数的。例如，在勒文海姆–斯科伦定理的证明之中即会出现不可数的标识。

语法

一阶逻辑可分成两个主要的部分：语法决定哪些符号的组合是一阶逻辑内的合法表示式，而语义则决定这些表示式之前的意思。

• 词汇表

和英语之类的自然语言不同，一阶逻辑的语言是完全形式的，因为可以机械式地判断一个给定的表示式是否合法。存在两种合法的表示式：“项”（直观上代表物件）和“公式”（直观上代表可真或伪的断言）。一阶逻辑的项与公式是一串符号，这些符号一起形成了这个语言的词汇表。如同所有的形式语言一般，符号本身的性质不在形式逻辑讨论的范围之内；它们通常只被当成字母及标点符号。

一般会将词汇表中的符号分成“逻辑符号”（总有相同的意思）及“非逻辑符号”（意思依解释不同而变动）。例如，逻辑符号总是解释成“且”，而绝不会解释成“或”。另一方面，一个非逻辑断言符号，如Phil(x），可以解释成“x是哲学家”、“x的个名为Philip的人”或任何其他的1元断言，单看其解释为何。

• 逻辑符号

词汇表中存在若干个逻辑符号，虽然会因作者而异，但通常包括：

• 量化符号∀及∃
• 逻辑联结词：且∧、或∨、条件→、双条件↔及否定¬。
• 括号、方括号及其他标点符号。此类符号的选择依文章不同而有所不同。
• 无限集的变数，通常标记为英文字母末端的小写字母x、y、z、…，也常会使用下标来区别不同的变数：x0、x1、x2、…。
• 一个等式符号=。详见下面的“等式”一节。

需注意，并不是所有的符号都需要，只要有量化符号的其中一个、否定及且、变数、括号及等式就足够了。还存在许多定义了额外逻辑符号的变体：

• 有时也会包括真值常数，用T、Vpq或来表示“真”，并用F、Opq或来表示“假”。若没有此类零参数的逻辑算符，这两个常数就只能用量化来表示。
• 有时也会包括额外的逻辑联结词，如谢费尔竖线、NAND及异或。

• 非逻辑符号

非逻辑符号用来表示论域上的断言（关系）、函数及常数。以前标准上会对所有不同的用途使用相同的无限集的非逻辑符号，而最近则会根据应用的不同而使用不同的非逻辑符号。因此变得需要列举出使用于一特定应用中的所有非逻辑符号。其选择是经由标识来形成的。

传统的做法是对所有的应用都只有单一个无限集的非逻辑符号。因此，根据传统的做法只会存在一种一阶逻辑的语言。这种做法现在依然很常见，尤其是在哲学方面的书籍。

1. 对每个整数n ≥ 0，皆存在一组n元断言符号。因为这些断言符号表示n个元素间的关系，因此也称为关系符号。对每个参数量n，皆能有无限多个断言符号：#:Pn0, Pn1, Pn2, Pn3,…
2. 对每个整数n ≥ 0，皆存在无限多个n元函数符号：f n0, f n1, f n2, f n3,…

在当代的数理逻辑里，标识会因应用的不同而不同。数学里的典型标识，在群里为{1, ×}，或只为{×}；在有序体里为{0, 1, +, ×, <}。并没有限制非逻辑符号的数量，标识可以是空的、有限、无限，甚至是不可数的。例如，在勒文海姆–斯科伦定理的证明之中即会出现不可数的标识。

根据最近的做法，每个非逻辑符号皆为下列两种类型的其中一种。

1. 具有0个或0个以上参数的断言符号（或关系符号）。通常标记为大写字母P、Q、R、…。
   • 0参数的关系可以视同为命题变数。例如可以代表任何叙述的P。
   • 令P(x)为具有1个参数的断言变数，其中一个可能的解释为“x是个人”。
   • 令Q(x,y)为具有2个参数的由词变数，其中一些可能的解释有“x大于y”或“x是y的父亲”。
2. 具有0个或0个以上参数的函数符号。标常标记为小写字母f、g、h、…。
   • 举例来说，f(x)可以解释成“x的父亲”；在算术里，可代表“-x”；在集合论里，可代表“x的幂集”。g（x,y）在算术里可代表“x+y”；在集合论里，可代表“x和y的联集”。
   • 0参数的函数符号也称为常数符号，常标记成英文字母前端的字母a、b、c、…。a可代表“苏格拉底”；在算术里，可代表0；在集合论里，可代表空集。

形成规则

形成规则定义一阶逻辑的项及公式。因为项及公式被表示为一串符号，这些规则可被用来写成项及公式的形式文法。这些规则通常是上下文无关的（规则的每个结果在其左侧都会有单一个符号），除非允许有无限多符号，且有许多开始符号，如项中的变数。

• 项

项可依如下规则递归地定义：

1. 变数。每个变数皆是项。
2. 函数。每个具有n个参数的表示式f（t1,...,tn，其中每个参数ti是项，且f是具有n个参数的函数符号）是项。另外，常数符号是0参数的函数符号，因此也是项。

只有可经由有限次地应用上述规则来得到的表示式才是项。举例来说，不存在包含断言符号的项。

• 公式

公式（或称合式公式）可依如下规则递归地定义：

1. 断言符号。若P是一个n元断言符号，且t1, ..., tn是项，则P(t1,...,tn)是公式。
2. 等式。若等式符号算是逻辑的一部分，且t1及t2是项，则t1 = t2是公式。
3. 否定。若φ是公式，则φ是公式。
4. 二元联结词。若φ及ψ是公式，则（φ ψ）是公式。其他的二元逻辑联结词也可相似的规则。
5. 量化。若φ是公式，且x是变数，则及都是公式。

只有可经由有限次地应用上述规则来得到的表示式才是公式。由头两个规则得到的公式称为原子公式。

举例来说，

是公式，若f是1元函数符号，P是1元断言符号，且Q是3元断言符号。另一方面，则不是公式，虽然这也是由词汇表中的符号组成的字串。

定义中的括号，其用途是为了确保任何公式都只能依递归定义以单一种方法得到（换句话说，每一个公式都只存在唯一的剖析树）。这个性质被称为公式的唯一可读性。对于括号要用在公式中的哪里存在有许多的惯例。例如，有些作者会使用冒号或句号来代替括号，或变更括号插入的地方。但每个作家个人的定义都必须证明会满足唯一可读性。

定义公式的规则无法定义“若-则-否则”函数ite（c,a,b），其中的c是个以公式表示的条件，当c为真时传回a，为假时传回b。这是因为断言和函数都只能接受项当做其参数，但上述函数的第一个参数为公式。某些建构在一阶逻辑上的语言，如SMT-LIB 2.0，会增加此一定义。

• 自由变数和约束变数

在一个公式里，变数可能是自由的或约束的。直观上来看，一个变数在公式里若没有被量化则是自由的：在里，变数x是自由的，而y则是约束的。自由变数和约束变数可依如下规则递归地定义：

1. 原子公式。若φ是原子公式，则x在φ里是自由的，当且仅当x出现在φ里。更甚之，在原子公式中不存在约束变数。
2. 否定。x在φ里是自由的，当且仅当x在φ里是自由的。x在φ里是约束的，当且仅当x在φ里是约束的。
3. 二元联结词。x在（φ ψ）里是自由的，当且仅当x在φ或ψ里是自由的。x在（φ ψ）里是约束的，当且仅当x在φ或ψ里是约束的。相同的规则也适用于其他的二元联结词之上。
4. 量化。x在y φ里是自由的，当且仅当x在φ里是自由的，且x是个和y相异的符号。而且，x在y φ里是约束的，当且仅当x是y或x在φ里是约束的。相同的规则也适用于之上。

在一阶逻辑中，一个没有自由变数的公式称为一阶句子。此类公式在特定解释之下即会有良好定义的真值。例如，公式Phil(x)是否为真需看x代表什么，而句子在一特定解释下则必为真或必为假。

可证明的恒等式

可能增加的推理规则

【描述来源：wiki, URL：https://zh.wikipedia.org/wiki/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91】

发展历史

描述

过去一百多年，一阶逻辑出现过许多种名称，包括：一阶断言演算、低阶断言演算、量化理论或断言逻辑（一个较不精确的用词）。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑有使用量化变数。一个一阶逻辑，若具有由一系列量化变数、一个以上有意义的断言字母及包含了有意义的断言字母的纯公理所组成的特定论域，即是一个一阶理论。

一阶逻辑和其他高阶逻辑不同之处在于，高阶逻辑的断言可以有断言或函数当做引数，且允许断言量词或函数量词的（同时或不同时）存在。在一阶逻辑中，断言通常和集合相关连。在有意义的高阶逻辑中，断言则会被解释为集合的集合。

存在许多对一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）的演绎系统。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。

一阶逻辑是数学基础中很重要的一部分，因为它是公理系统的标准形式逻辑。许多常见的公理系统，如一阶皮亚诺公理和包含策梅洛-弗兰克尔集合论的公理化集合论等，都可以形式化成一阶理论。然而，一阶定理并没有能力去完整描述及范畴性地建构如自然数或实数之类无限的概念。这些结构的公理系统可以由如二阶逻辑之类更强的逻辑来取得。

在计算机领域中，一阶逻辑应用于很多系统中，如专家系统expert systems,、定量推理quantitative reasoning,和混合数据库and hybrid databas。

1990年，Halpern, J. Y.提出了两种解决一阶逻辑概率的方法。1998年，Chiara Ghidini也在提出了Distributed First Order Logic应用于也是应用于distributed knowledge representation and reasoning systems (DKRS)系统中。2002年，Anand Ranganathan Æ Roy H. Campbell基于一阶逻辑的背景感知系统，将不能量化的信息用一阶逻辑进行表示。2012年，Fitting, M.将一阶逻辑应用于自动定理的证明

主要事件

发展分析

瓶颈

一阶逻辑既不允许谓词为变量，也不允许对谓词进行量化，它是需要其他的逻辑语言来一起支持证明或推理的。于此同时，即使一阶逻辑广泛运用于专家系统，定量推理等等系统中，它的入门需要一定的数学基础，所以对于开发者的本身的自身知识要求较高。

未来发展方向

将自然语言的逻辑化是必经之路，这是让无法量化或无法建模的东西进入到可计算世界的一种途径。除此之外，它可以对需要严谨的系统提供的证明的依据，使得一个系统被证明它是没有错误的，形式化语言也是正在逐渐兴起中，这种语言可以通过证明让一些军用系统或者医疗系统等需要高严谨的系统无BUG。

Contributor: Ruiying Cai