一阶谓词演算或一阶逻辑(fol)允许量化陈述的公式，比如"存在着x，..."(<math>\existsx</math>)或"对于任何x，..."(<math>\forallx</math>)，这里的x是论域(domainofdiscourse)的成员。一阶(递归)公理化理论是通过增加一阶句子/断定的递归可枚举集合作为公理，可以被公理化为一阶逻辑扩展的理论。这里的"..."叫做谓词并表达某种性质。谓词是适用于某些事物的表达。所以，表达"是黄色"或"喜欢椰菜"分别适用于是黄色或喜欢椰菜的那些事物。
一阶逻辑是区别于高阶逻辑的数理逻辑，它不允许量化性质。性质是一个物体的特性；所以一个红色物体被表述为有红色的特性。性质可以被当作物体只凭自身的一种构成(form)，它可以拥有其他性质。性质被认为有别于拥有它的物体。所以一阶逻辑不能表达下列陈述，"对于所有的性质p，..."或"存在着性质p，..."。
但是，一阶逻辑足够强大了，它可以形式化全部的集合论和几乎所有的数学。把量化限制于个体(individual)使它难于用于拓扑学目的，但它是在数学底层经典的逻辑理论。它是比句子逻辑强比二阶逻辑弱的理论。
一阶逻辑的定义
谓词演算构成如下
生成规则(就是形成合式公式的递归定义)。
变换规则(就是推导定理的推理规则)。
公理或公理模式的(可能的可数的无限)集合。
有两种类型的公理:逻辑公理，它是对于谓词演算有效的，和非逻辑公理，它是在特殊情况下为真的，就是说，在它所在的理论的标准解释中是真的。例如，非逻辑的皮亚诺公理在算术的符号主义标准解释下是真的，但是对于谓词演算它们不是有效的。
在公理的集合是无限的的时候，需要能判定给定的合式公式是否是一个公理的一个算法。进一步的，应当有可以判定一个推理规则的应用是否正确的算法。
[编辑]词汇表
"词汇表"构成如下
大写字母p,q,r,...是谓词变量。
小写字母a,b,c,...是(个别的)常量。
小写字母x,y,z,...是(个别的)变量。
小写字母f,g,h,...是函数变量。
表示逻辑算子的符号:¬(逻辑非)，<math>\wedge</math>(逻辑与)，<math>\vee</math>(逻辑或)，→(逻辑条件)和↔(逻辑双条件)。
表示量词的符号:<math>\forall</math>(全称量词)，<math>\exists</math>(存在量词)。
左右圆括号。
一些符号可以被简略为原语(primitive)并被采纳为简写；比如(p↔q)是(p→q)<math>\wedge</math>(q→p)的简写。算子和量词的最小数目是三个(如果我们定义了算子或非或者与非则是两个)；例如，¬，<math>\wedge</math>和<math>\forall</math>就足够了。项是一个常量、变量或n≥0个参数的函数符号。
[编辑]生成规则
合式公式(wff)的集合按如下规则递归的定义:
简单和复杂的谓词如果p是n元(n≥0)谓词，则<math>pa_1,...,a_n</math>是合式的。如果n≤1，则p是原子。
归纳条款i:如果φ是wff，则¬φ是wff。
归纳条款ii:如果φ和ψ是wff，则<math>(\phi\wedge\psi)</math>，<math>(\phi\vee\psi)</math>，(φ→ψ)和(φ↔ψ)是wff。
归纳条款iii:如果φ是包含变量x的一个自由实例的wff，则<math>\forallx\,\varphi</math>和<math>\existsx\,\varphi</math>是wff。(此后在<math>\forallx\,\varphi</math>和<math>\existsx\,\varphi</math>中x的任何实例都被称为约束的—而不是自由的。)
闭包条款:其他东西都不是wff。
[编辑]变换(推理)规则
肯定前件充当推理的唯一规则。如果没有公理模式，则还需要一个一致代换规则。
[编辑]演算
谓词演算是命题演算的扩展。如果命题演算被定义为十一个公理和一个推理规则(肯定前件)，不计算针对逻辑等价算子的额外定律在内，则谓词演算可以被定义为在其上添加四个补充的公理和一个补充的推理规则。
[编辑]公理扩展
下列四个公理是谓词演算的特征:
pred-1:<math>\forallxz(x)\rightarrowz(y)</math>
pred-2:<math>z(y)\rightarrow\existsxz(x)</math>
pred-3:<math>\forallx(w\rightarrowz(x))\rightarrow(w\rightarrow\forallxz(x))</math>
pred-4:<math>\forallx(z(x)\rightarroww)\rightarrow(\existsxz(x)\rightarroww)</math>
它们实际上是公理模式，因为其中的谓词字母w和z可以被任何谓词字母所替代，而不改变这些公式的有效性。
[编辑]推理规则
叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为
<math>\mathit\vdashz(x),\mathit\vdash\forallxz(x)</math>
这里的z(x)假定表示谓词演算的一个已证明的定理，而∀xz(x)是它针对于变量x的闭包。谓词字母z可以被任何谓词字母所替代。
注意：全称普遍化类似于模态逻辑的必然性规则，它是
<math>\mathit\vdashp,\mathit\vdash\boxp</math>
[编辑]一阶逻辑的元逻辑定理
在公告板中列出了一些重要的元逻辑定理。
不像命题演算，一阶逻辑是不可判定性的。对于任意的公式p，可以证实没有判定过程，判定p是否有效，(参见停机问题)。(结论独立的来自于邱奇和图灵。)
有效性的判定问题是半可判定的。按哥德尔不完备定理所展示的，对于任何有效的公式p,p是可证明的。
单体谓词逻辑(就是说，谓词只有一个参数的谓词逻辑)是可判定的。