一阶逻辑是指研究由个体、函数及关系构成的命题，由这些命题经使用量词和命题联结词构成的更复杂的命题以及各种命题之间的推理关系的逻辑。在一阶逻辑中，量词仅作用于个体变元。一阶逻辑是数理逻辑中发展得最为成熟的部分。在为数学的语言和推理建立形式系统的过程中，它处于核心地位，又称谓词逻辑。

一阶谓词演算或一阶逻辑（FOL）允许量化陈述的公式，比如"存在着 x，..." (x) 或 "对于任何 x，..." （砢），这里的 x 是论域(domain of discourse)的成员。一阶（递归）公理化理论是通过增加一阶句子/断定的递归可枚举集合作为公理，可以被公理化为一阶逻辑扩展的理论。这里的"..."叫做谓词并表达某种性质。谓词是适用于某些事物的表达。所以，表达"是黄色"或"喜欢椰菜"分别适用于是黄色或喜欢椰菜的那些事物。

一阶逻辑是区别于高阶逻辑的数理逻辑，它不允许量化性质。性质是一个物体的特性；所以一个红色物体被表述为有红色的特性。性质可以被当作物体只凭自身的一种构成（form），它可以拥有其他性质。性质被认为有别于拥有它的物体。所以一阶逻辑不能表达下列陈述，"对于所有的性质 P，..." 或"存在着性质 P，..."。

但是，一阶逻辑足够强大了，它可以形式化全部的集合论和几乎所有的数学。把量化限制于个体（individual）使它难于用于拓扑学目的，但它是在数学底层经典的逻辑理论。它是比句子逻辑强比二阶逻辑弱的理论。

一阶逻辑的定义

谓词演算构成如下

生成规则（就是形成合式公式的递归定义）。

变换规则（就是推导定理的推理规则）。

公理或公理模式的（可能的可数的无限）集合。

有两种类型的公理：逻辑公理，它是对于谓词演算有效的，和非逻辑公理，它是在特殊情况下为真的，就是说，在它所在的理论的标准解释中是真的。例如，非逻辑的皮亚诺公理在算术的符号主义标准解释下是真的，但是对于谓词演算它们不是有效的。

在公理的集合是无限的的时候，需要能判定给定的合式公式是否是一个公理的一个算法。进一步的，应当有可以判定一个推理规则的应用是否正确的算法。

"词汇表"构成如下

大写字母 P,Q,R,... 是谓词变量。

小写字母 a,b,c,... 是（个别的）常量。

小写字母 x,y,z,... 是（个别的）变量。

小写字母 f,g,h,... 是函数变量。

表示逻辑算子的符号： ┐ （逻辑非），∧ （逻辑与），∨（逻辑或），→ （逻辑条件）和（逻辑双条件）。

表示量词的符号：（全称量词），（存在量词）。

左右圆括号。

一些符号可以被简略为原语（primitive）并被采纳为简写；比如 是的简写。算子和量词的最小数目是三个（如果我们定义了算子或非或者与非则是两个）；例如，┐，∨ 和 ㄢ足够了。项是一个常量、变量或 个参数的函数符号。

合式公式（）的集合按如下规则递归的定义：

简单和复杂的谓词 如果 P 是 n 元（）谓词，则

是合式的。如果，则 P 是原子。

归纳条款 I: 如果 Φ 是 wff，则 ┐ Φ 是 wff。

归纳条款 Ⅱ：如果 Φ 和 ψ 是，则和是。

归纳条款 Ⅲ：如果 φ 是 包含变量 x 的一个自由实例的 wff，则 砢，φ和x，φ 是 。（此后在x，φ 和x，φ 中x 的任何实例都被称为约束的 — 而不是自由的。）

闭包条款：其他东西都不是。

肯定前件充当推理的唯一规则。如果没有公理模式，则还需要一个一致代换规则。

谓词演算是命题演算的扩展。如果命题演算被定义为十一个公理和一个推理规则（肯定前件），不计算针对逻辑等价算子的额外定律在内，则谓词演算可以被定义为在其上添加四个补充的公理和一个补充的推理规则。

下列四个公理是谓词演算的特征：

PRED-1:

PRED-2:

PRED-3:

PRED-4:

它们实际上是公理模式，因为其中的谓词字母 W 和 Z 可以被任何谓词字母所替代，而不改变这些公式的有效性。

叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为

这里的 假定表示谓词演算的一个已证明的定理，而 是它针对于变量 x 的闭包。谓词字母 Z 可以被任何谓词字母所替代。

注意：全称普遍化类似于模态逻辑的必然性规则，它是

在公告板中列出了一些重要的元逻辑定理。

不像命题演算，一阶逻辑是不可判定性的。对于任意的公式 P，可以证实没有判定过程，判定 P 是否有效，（参见停机问题）。（结论独立的来自于阿隆佐·邱奇和艾伦·麦席森·图灵。）

有效性的判定问题是半可判定的。按哥德尔不完备定理所展示的，对于任何有效的公式 P,P 是可证明的。

单体谓词逻辑（就是说，谓词只有一个参数的谓词逻辑）是可判定的。

在一阶逻辑中描述一个数学理论，首先会涉及这个理论所讨论的对象、定义在这些对象上的函数、

以及这些对象之间的关系或性质。数学理论所讨论的对象称为个体，由个体组成的非空集合称为论域或个体域。按通常数学中的定义，一个n元函数就是从论域A的个体的所有n元组的集合至A中的一个映射。A中个体的n元组（）经映射F对应到A中的个体表示为。函数增加了个体的表达形式。人们也考虑论域A中哪些n元组满足关系R，即A中哪些n元组（）使得为真。此时的就是一个命题。

在各种关系中，相等关系是经常要用的。因为常常需要知道不同个体的表达式是否指称同一个对象。例如与是否表示同一个数。

可以将关系或命题用命题连接词来构成更复杂的关系或命题。当描述一些个数为无穷的对象的性质时，就需要引进量词。例如说“对任何一个自然数，都有一个比它大的素数”时，就引进了量词“所有个体”及“存在个体”，并且将关系或命题经量词构成了更复杂的关系或命题。“论域中的所有个体

”称为全称量词，由它所构成的命题“论域中所有的个体有某性质”，当论域中所有个体都有此性质时，此命题是真的，否则为假。“论域中存在个体”称为存在量词，由它所构成的命题“论域中存在个体有某性质”，当论域中某些个体有此性质时为真，否则为假。

“所有个体”、“存在个体”中，量词加在论域的个体上，称为一阶量词。在一阶逻辑中使用的量词仅限于一阶量词。“所有函数”、“存在函数”、“所有关系”和“存在关系”是二阶量词。此外还有更高阶的量词。相应地也有二阶逻辑、高阶逻辑等。

按照建立形式系统的一般原则（见逻辑演算），一阶逻辑的形式系统应包括它的语言，即一阶语言，以及逻辑公理和推理规则。

一阶语言的符号包括以下几类。

① 个体变元

② 函数符号（表示函数），g，h，…；个体符号（表示论域中的个体） α，b，с，…；及谓词（表示关系）p,Q，R，…。其中有一个二元谓词=，称为等词（表示恒同关系）。

③ 命题联结词┐，∧，∨，→，以及量词（存在量词），（全称量词）。

①，③及等词称为逻辑符号，其他符号，即等词外的②称为非逻辑符号。

归纳地定义一阶语言的项和公式，也称之为形成规则。项的定义：

① 变元和个体符号是项。

② 若是项，是一个n元函数符号，则（）是项。

公式可定义为：

① 若是项，p是n元谓词符号，则是公式，也称为原子公式。

② 若A是公式，则是公式；若A，B是公式，则是公式。

③ 若A是公式，则，是公式。

如果变元x出现在公式 A中形如或的部分，称这个出现为x在A中的约束出现；否则，称为x在A中的自由出现。例如在公式中，第一个x是自由出现，第二、三个x是约束出现。没有变元自由出现的公式称为闭公式。

谓词演算作为一个形式系统，可以规定它的解释。给定一个论域，对于谓词演算中出现的个体符号、函数符号及谓词依次解释为论域中的个体及定义在此论域上的函数及关系。此论域及其对于谓词演算中形式符号的解释称为该演算的一个结构或模型。由对于个体符号和函数符号的解释可知，项可解释为复合函数，它指称个体。原子公式解释为所指称的个体满足n元关系p。若公式A(x）表示关系，则解释为论域中所有个体满足关系A，解释为论域中存在某个体满足关系A。

谓词演算的推理规则可规定如下：

谓词演算的逻辑公理陈述逻辑符号的性质，分为三类：

① 命题公理 将重言式（见命题逻辑）中出现的命题变元代之以谓词演算中的任意公式后得

到的公式；

② 恒同公理及相等性公理

③ 替换公理 及，其中表示将公式A中所有x的自由出现代之以项α。

谓词演算的公理，即逻辑公理并不界定具体的函数或关系，而仅仅处理逻辑词项的一般性质。换言之，对它的个体符号、函数符号、及谓词的解释可以是任意论域中的任意个体、函数及关系。谓词演算的这个抽象性质对于近年来模型论的发展是本质的。

在谓词演算的框架中，用形式语言表述数学的公理（并不一定能完全表述），就得到不同数学理论的形式系统。这类形式公理刻画了某些具体的非逻辑符号的性质，称为非逻辑公理。例如：

全序理论的形式系统中仅有一个非逻辑符号二元谓词≤。除逻辑公理外，它还有非逻辑公理：①②；③；④。自然数集合及其上的顺序关系就是全序理论的一个模型。

群论的形式系统中只有两个非逻辑符号：个体符号1及二元函数符号·。它的非逻辑公理为：① ②；③任何一个群都是它的模型。

数论的形式系统中的非逻辑符号有：个体符号0，一元函数符号s及两个二元函数符号+及·。数论（或皮亚诺算术）的公理为：①，②③④ ，⑤⑥⑦若A为系统内的公式，x0在A中自由出现，则对每个这样的公式A，有公理自然数的算术

就是它的一个模型。

陈述在一阶语言中，由逻辑公理、非逻辑公理及推理规则推出的全部形式定理（见逻辑演算）称为一阶理论，记为T。为区别不同的一阶理论T，只要指出T的语言中的非逻辑符号及非逻辑公理就够了。任何一阶理论都包含了谓词演算作为它的子系统。

在谓词演算的任意模型中均为真的公式称为永真的或有效的公式。例如，公式就是有效的公式，而就不是有效的。因为在全序结构中，对x，y在个体域中的任意取值，该公式的解释均为真。而在半序结构中，例如该结构的论域为一个集合的全体子集的集合，≤解释为集合的包含关系，那么上式的解释当x，y取任意的两个子集时就不都是真的了。

直观上看，逻辑的定理应当是在一切可能的世界中均为真的定理。在一定意义下，谓词演算满足这个性质。可以验证，谓词演算的公理均为有效的，它的推理规则的假设有效则结论也必有效。因此，谓词演算的所有定理都是有效的。这个性质称为谓词演算的有效性或可靠性。反之，任意有效的公式必为谓词演算的定理。这就是著名的哥德尔完备性定理。由库尔特·卡塞雷斯于1930年证明。

用├A表示A是谓词演算的形式定理，即A 是系统内的定理。而可靠性与完备性刻画了整个形式系统的性质，是关于系统的定理，也称为元定理。形式系统的性质是数理逻辑主要的研究对象之一。

由谓词演算的有效性及完备性容易推知一阶理论的可靠性与完备性。使一阶理论 T的所有公理为真的结构称为T 的一个模型。若T的一个公式A在T 的任意模型中均有效，称A在T中有效，记为。A是T的定理记为。那么T的可靠性与完备性就可以陈述为的充分必要条件为。

若不存在A使得，则称T是协调的。

若T 是协调的，则T 必有模型（广义完备性定理）。

形如 的公式称为前束型公式，其中表示或，B 是一个不含量词的公式。任何一个一阶理论T（当T 的非逻辑公理集为空集时就是一个谓词演算）的公式A，都有一个公式A′，使得，其中A┡为前束型公式，且B中的非逻辑符号均在A中出现。A′也称为A的前束范式。此性质可用于对谓词演算或一阶理论的公式进行分类上。此时只需考虑前束范式中的量词，将它作为公式复杂性的一种测度。