一阶逻辑
一阶逻辑，是使用于数学、哲学、语言学及电脑科学中的一种形式系统，也可以称为：一阶断言演算、低阶断言演算、量化理论或谓词逻辑。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑包含量词。
高阶逻辑和一阶逻辑不同之处在于，高阶逻辑的断言符号可以有断言符号或函数符号当做引数，且容许断言量词或函数量词。在一阶逻辑的语义中，断言被解释为关系。而高阶逻辑的语义里，断言则会被解释为集合的集合。
在通常的语义下，一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。
一阶逻辑是数学基础中很重要的一部份。许多常见的公理系统，如一阶皮亚诺公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗兰克尔集合论都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数大小，因根据勒文海姆–斯科伦定理和康托尔定理，可以构造出一种＂病态＂集合论模型，使整个模型可数，但模型内却会觉得自己有“不可数集”。类似地，可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为斯科伦悖论。但一阶的直觉主义逻辑里，勒文海姆–斯科伦定理不可证明，故不会有以上之现象。
简介
在命题逻辑里，“苏格拉底是哲学家”、“柏拉图是哲学家”只能简单标记为 p 及 q 。
而一阶逻辑先将符号 Phil(x) 解释为 “ x 是哲学家”，然后以 s 代表苏格拉底；b 代表柏拉图，则 Phil(s) 对应到 p ； Phil(b) 对应到 q 。也就是赋予断言符号“Phil(x) ”语意的解释，而这个解释预设一个“所有人类的群体”（也就是语义解释的论域），将变数 x 解释为自群体取出来的某人。
其实断言符号可以包含一个以上的变数，像是把 Cp(x,y) 解释为“x与y是夫妻”，这样
- Cp(s,y)
就解释成“苏格拉底和y是夫妻”。
一阶逻辑和命题逻辑相同，断言符号和变数还能与逻辑符号组成更复杂的叙述：如将断言符号 Schol(x) 解释为 x 为学者。则“若x为哲学家，则x为学者”可表示为
- Phil ( x ) ⇒ Schol ( x )
而“对所有x，若x为哲学家，则x为学者”则记为
- ∀ x ( Phil ( x ) ⇒ Schol ( x ) )
也就是自左方开始阅读，以 ∀ x 代表“对所有x”；将之理解为“对所有的x， ∀ x 右方的叙述为真。”而 ∀ x 这个符号称为 x 的全称量词。
直观上还会有“若所有x是哲学家，那x的长子也会是哲学家”这样＂合理＂的叙述，为此将 Son(x) 解释为 “x的长子”，那这段＂合理＂叙述可记为
- ∀ x Phil ( x ) ⇒ Phil [ Son ( x ) ]
这种解释为成与 x 有唯一对应的那个对象的符号，称为函数符号。而事实上这段直观为真的叙述，经过适当的扩展以后就是一阶逻辑其中的一条公理。
而对于“有x是哲学家”，则引入另一种量词表记为：
- ∃ x ( Phil ( x ) )
自左方开始阅读，以 ∃ x 代表“存在x”；也就是解释为“有x使 ∃ x 右方的叙述为真”。而 ∃ x 被称为 x 的存在量词。全称量词和存在量词一起被简称为量词。
而直观上，“并非所有x不是哲学家”，和“有x是哲学家”是等价的；且“不存在x不是学者”也跟“所有的x是学者”在直观上也是等价的。所以只要有“否定”这个逻辑概念，那一阶逻辑就能以全称量词为基础，作以下的符号定义（ ¬ 解释为 “否定”， 而 A 代表一段＂叙述＂）：
- ∃ x A := ¬ [ ∀ x ( ¬ A ) ]
而将存在量词定义为全称量词的衍伸。
形式理论
一阶逻辑的形式理论可分成几个部份：
- 语法：决定哪些符号组合是合式公式。（直观上的＂语法无误的叙述＂）
- 推理规则：由合式公式符号组合出新合式公式的规则（直观上的＂推理＂）
- 公理：一套合式公式（直观上的基本假设）
标准语义
一阶逻辑的标准语义源于波兰逻辑学家Alfred Tarski所著《On the Concept of Truth in Formal Languages》。根据上面语法一节，公式是由原子公式递回地添加逻辑连结词而来的，而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确，就要规定项的取值，然后检验这样的取值会不会落在断言符号所对应的关系里。由此延伸出所有公式的＂真假值＂。
也就是一套一阶逻辑的语义解释，要包含
- 变数取值的论域
- 如何解释函数符号（为论域中的某个函数）与常数符号（为论域中的某特定元素），以便从特定的变数取值得出项的取值。
- 如何将断言符号与论域里的某关系做对应。
通常一套解释方法（简称为解释）会以代号 M 表示。
一阶逻辑的元定理
下面列出了一些重要的元逻辑定理。
- 不像命题演算，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程，判定P是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）
- 有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式P, P是可证明的。
- 一元断言逻辑（就是说，断言只有一个参数的断言逻辑）是可判定的。
转换自然语言到一阶逻辑
用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，<math>p \lor q</math>意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。
参见
→ 学科目录： 哲学（目录）
