一阶逻辑(
FOL)是数学家、哲学家、语言学家使用一种形式演绎系统。它有很多名字包括:
一阶谓词演算(
FOPC)、
低等谓词演算、
一阶逻辑的语言或
谓词逻辑。不像自然语言如英语，FOL 使用由数学结构来解释的完全无歧义的
形式语言。FOL 是通过允许在给定
论域的个体上的量化而扩展
命题逻辑的
演绎系统。例如，在 FOL 中可陈述“所有个体都有性质 P”。
命题逻辑处理简单的声明性命题，一阶逻辑补充覆盖了
谓词和量化。例如下列句子:“苏格拉底是男人”，“柏拉图是男人”。在
命题逻辑中，它们是两个无关的命题，比如指示为
p 和
q。但是在一阶逻辑中，这两个句子将由同一个性质联系起来: Man(x)，这里的 Man(x) 意味着 x 个男人。在 x=“苏格拉底”的时候我们得到了第一个命题
p，而在 x=“柏拉图”的时候我们得到了第二个命题
q。这种构造在介入了量词的时候允许更加强力的逻辑，比如“对于所有 x...”。例如，“对于所有 x，如果 Man(x) 则...”。没有量词的话，所有在 FOL 中的有效论证在命题逻辑中也有效的，反之亦然。
一阶理论构成自
公理的集合(通常有限的或
递归可枚举的)和给定底层可演绎性关系从它们可演绎出的那些陈述。“一阶理论”通常意味着某个公理集合和“与之在一起的完备(和可靠)的一阶逻辑公理化”，它闭合在 FOL 的规则之下。(对任何这种系统 FOL 将引出同样的抽象可演绎性关系，所以我们在头脑中不需要有固定的公理化系统。) 一阶语言有足够的表达能力来形式化两个重要的数学理论:
ZFC 集合论和
皮亚诺算术。但是一阶语言不能无条件的表达
可数性的概念，即使它在一阶理论 ZFC 中在 ZFC 符号论的
预期释义下是可表达的。这种想法可以用二阶逻辑无条件的表达。
