一阶逻辑是逻辑学中的一种形式系统，用于表达关于对象及其性质和关系的陈述。它通过引入变量、谓词和量词，扩展了命题逻辑。“一阶”意味着，量化变量的取值范围是论域中的个体对象，而不是直接以性质或关系为取值。它的形式语言、解释和推理规则，为分析演绎推理提供了框架。除非另有说明，这一术语通常指经典一阶逻辑，且一般包含等号。(builds.openlogicproject.org)
语言与句法
一阶语言区分逻辑符号和选定的非逻辑词汇，后者通常称为该语言的符号表。逻辑符号包括变量、否定和合取等联结词，以及量词 ∀（“对所有”）和 ∃（“存在”）。非逻辑符号包括常量符号、函数符号和谓词符号，其中每个函数符号或谓词符号都有规定的参数个数。(people.math.wisc.edu)
句法以递归方式定义表达式。项指称对象：变量或常量符号都是项，将函数符号应用于适当的项，也会得到一个项。原子公式由谓词应用于项而成，或表示两个项相等。复合公式则使用联结词和量词构造。二元谓词可以表达二元关系，例如“小于”。变量的某次出现若受量词约束，就是约束出现；否则就是自由出现。没有自由变量的公式称为语句。(people.math.wisc.edu)
例如，
[ \forall x\bigl(H(x)\rightarrow M(x)\bigr) ]
可以表达“所有人都会死”。它对论域中的每个对象陈述了一项条件性质，但本身并未断言人存在。要表达存在性，还需补充诸如 (\exists x,H(x)) 这样的陈述。(cs.cmu.edu)
解释与真值
语义学通过结构赋予表达式意义。在标准表述中，结构包含一个非空论域，以及对每个非逻辑符号的解释。常量符号指称论域中的元素，函数符号指称论域上处处有定义的函数，谓词则指称具有相应元数的关系。等号若被列为逻辑符号，就表示同一关系。变量赋值为自由变量提供取值。(cs.cmu.edu)
真值以递归方式定义。全称量化公式成立，当且仅当其中的公式对被量化变量的每个可能取值都为真。存在量化公式成立，当且仅当至少有一个取值使其中的公式为真。因此，量词的顺序十分重要：
[ \forall x\exists y,R(x,y) \qquad\text{与}\qquad \exists y\forall x,R(x,y). ]
第一个公式允许每个 (x) 对应不同的 (y)；第二个公式则要求存在同一个 (y)，对所有 (x) 都满足条件。(cs.cmu.edu)
满足某理论中每个语句的结构，称为该理论的模型。一个语句若在其语言的每个结构中都为真，就具有逻辑有效性。语义后承记为 (\Gamma\models\varphi)，表示前提集 (\Gamma) 的每个模型都满足 (\varphi)。这些区分是模型论的基础。(cs.cornell.edu)
演绎与完备性
演绎演算规定如何根据前提和逻辑规则构造形式证明。常见的形式包括自然演绎、公理式演算和相继式演算。量词规则包括全称实例化：从 (\forall x,P(x)) 可以推出 (P(t))，但代入必须避免意外的变量约束。证明论研究这类演算及其中的推导。(builds.openlogicproject.org)
可靠性意味着可推导性蕴含语义后承。对于适当的经典一阶演算，哥德尔完备性定理确立了反方向也成立：
[ \Gamma\vdash\varphi \quad\Longleftrightarrow\quad \Gamma\models\varphi. ]
因此，即使前提集是无限的，每个语义后承也都有有限的形式推导。(builds.openlogicproject.org)
这必须与哥德尔不完备定理区分开来。逻辑的完备性涉及在所有模型中成立的后承关系。不完备性则涉及一致、可有效公理化且足以表达算术的理论所受到的限制：这样的理论未必能判定其语言中的每个语句。某个语句在理论中既不能被证明，也不能被否证，并不因此意味着其基础逻辑缺乏完备性。(builds.openlogicproject.org)
紧致性与表达能力的限制
紧致性定理指出，如果一个一阶语句集的每个有限子集都有模型，那么整个语句集也有模型。等价地说，如果一组前提不一致，那么其中有限个前提就已足以体现这种不一致。(cs.cornell.edu)
勒文海姆–斯科伦定理施加了进一步的限制。对于可数语言，任何具有无限模型的理论，都有一个可数无限模型，并且对每个无限基数，都有一个具有该基数的模型。因此，一阶公理无法在所有结构中唯一刻画一个无限结构，即使只要求在同构意义下唯一也不行。(cs.cornell.edu)
紧致性也使得一阶理论不可能恰好以所有有限结构为模型。对每个正整数 (n)，加入要求至少存在 (n) 个不同对象的语句后，每个有限子集仍然可满足，因而整个理论必然有一个无限模型。不过，利用等号仍然可以表达特定的有限大小。(builds.openlogicproject.org)
在二阶逻辑中，变量的取值范围可以是性质或关系。不过，当集合本身就是论域中的对象时，一阶逻辑也能讨论集合，集合论就是如此；两者的区别在于如何解释量化，而不在于是否提及集合。(builds.openlogicproject.org)
可计算性
不受限制的一阶逻辑有效性是不可判定的：不存在一种算法，能对每个输入语句都在有限时间内终止并给出正确答案。不过，对于以有效方式给出的语言，有效性是半可判定的。系统地枚举证明，最终会找到任何有效语句的证明，但对于无效语句，这一过程可能永远持续下去。完备性与可判定性之间的这种差别，确立了机械化证明搜索的一项根本限制。(builds.openlogicproject.org)