一阶逻辑
一阶逻辑是使用于数学、哲学、语言学及计算机科学中的一种形式系统。
过去一百多年，一阶逻辑出现过许多种名称，包括：一阶谓词演算、低阶谓词演算、量化理论或谓词逻辑（一个较不精确的用词）。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑有使用量化变量。一个一阶逻辑，若具有由一系列量化变量、一个以上有意义的谓词字母及包含了有意义的谓词字母的纯公理所组成的特定论域，即是一个一阶理论。
一阶逻辑和其他高阶逻辑不同之处在于，高阶逻辑的谓词可以有谓词或函数当做引数，且允许谓词量词或函数量词的（同时或不同时）存在[1]。在一阶逻辑中，谓词通常和集合相关连。在有意义的高阶逻辑中，谓词则会被解释为集合的集合。
存在许多对一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）的演绎系统。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。
一阶逻辑是数学基础中很重要的一部份，因为它是公理系统的标准形式逻辑。许多常见的公理系统，如一阶皮亚诺公理和包含策梅洛-弗兰克尔集合论的公理化集合论等，都可以形式化成一阶理论。然而，一阶定理并没有能力去完整描述及范畴性地建构如自然数或实数之类无限的概念。这些结构的公理系统可以由如二阶逻辑之类更强的逻辑来取得。
简介
不像命题逻辑只处理简单的陈述命题，一阶逻辑还额外包含了谓词和量化。
谓词像是一个会传回真或伪的函数。考虑下列句子：“苏格拉底是哲学家”、“拍拉图是哲学家”。在命题逻辑里，上述两句被视为两个不相关的命题，简单标记为p 及q。然而，在一阶逻辑里，上述两句可以使用谓词以更相似的方法来表示。其谓词为Phil(a)，表示a 是哲学家。因此，若a 代表苏格拉底，则Phil(a)为第一个命题－p；若a 代表柏拉图，则Phil(a)为第二个命题－q。一阶逻辑的一个关键要点在此可见：字串“Phil”为一个语法实体，以当a 为哲学家时陈述Phil(a) 为真来赋与其语义。一个语义的赋与称为解释。
一阶逻辑允许以使用变量的方法推论被许多元件共享的性质。例如，令Phil(a)表示a 为哲学家，且令Schol(a)表示a 为学者。则公式
表示若a 为哲学家，则a 为学者。符号被用来标记一个条件叙述。箭号的左边为假设，右边则为结论。此一公式的真值取决于标记成a 的元件，及“Phil”和“Schol”的解释之上。
“对于每个a，若a 为哲学家，则a 为学者”之类形式的断言，需要同时使用变量及量化。再次，令Phil(a)表示a 为哲学家，且令Schol(a)表示a 为一学者，则一阶叙述
表示不论a 代表什么，若a 为哲学家，则a 为学者。此处的（全称量化）代表宣称对“所有”a的选择，括号内的叙述皆为真的想法。
为了表明，声称“ 如果是一个哲学家然后是一个学者”是假的，一会显示有一些人是不是一个学者的哲学家。 这与存在量词可以表示反诉 ： 若想证明“若a 为哲学家，则a 为学者”此一宣称是错的，有些人会证明存在有些不是学者的哲学家。此一反论可以用存在量化来表示：
其中，
是否定算符： 为真当且仅当 为假；换句话说，当且仅当a 不是学者。
是合取算符： 表示a 是哲学家且不是学者。
谓词Phil(a) 和Schol(a) 都各只有一个参数。但一阶逻辑其实也可以表示具有一个以上参数的谓词。例如，“存在一些人可以在任何时间被愚弄”可表示成
这里，Person(x)解释为x 是人，Time(y)为y 是某段时间，且Canfool(x,y)则为（人）x可在（时）y被愚弄。清楚地说，上述叙述表示至少存在一个人可以在任何时间被愚弄，这比“在任何时间，至少存在一个人可以被愚弄”的叙述要强。后者并不意味着，被愚弄的人在任何时间时上总是要是同一位。
量化的范围是由可以用来满足量化的物件所组成的集合（在本节中的一些非正式的例子里，量化的范围并没有被指定）。除了指定Person和Time等谓词符号的意义，解释也必须指定一个非空集合，称为论域，做为量化的范围。因此，之类形式的叙述在一特定解释下称之为真，若在可用来赋予谓词中符号Phil意义的解释所指定的论域里存在着物件。
语法
一阶逻辑可分成两个主要的部份：语法决定哪些符号的组合是一阶逻辑内的合法表示式，而语义则决定这些表示式之前的意思。
词汇表
和英语之类的自然语言不同，一阶逻辑的语言是完全角式的，因为可以机械式地判断一个给定的表示式是否合法。存在两种合法的表示式：“项”（直观上代表物件）和“公式”（直观上代表可真或伪的谓词）。一阶逻辑的项与公式是一串符号，这些符号一起形成了这个语言的词汇表。如同所有的形式语言一般，符号本身的性质不在形式逻辑讨论的范围之内；它们通常只被当成字母及标点符号。
一般会将词汇表中的符号分成“逻辑符号”（总有相同的意思）及“非逻辑符号”（意思依解释不同而变动）。例如，逻辑符号 总是解释成“且”，而绝不会解释成“或”。另一方面，一个非逻辑谓词符号，如Phil(x)，可以解释成“x 是哲学家”、“x 的个名为Philip 的人”或任何其他的1元谓词，单看其解释为何。
逻辑符号
词汇表中存在若干个逻辑符号，虽然会因作者而异，但通常包括：
量化符号 及
逻辑联结词：且、或、条件、双条件 及否定。偶尔还会包括一些其他的逻辑联结词。某些作家会使用 或Cpq 来表示，用 或Epq 来表示，特别是文中 被拿去做其他用途之时。更多地，也有用 来表示，用 来表示，用(~)、Np或Fpq 来表示，用||或Apq 来表示，以及用& 或Kpq 来表示，尤其是这些符号因技术上的原因无法输入时。
括号、方括号及其他标点符号。此类符号的选择依文章不同而有所不同。
无限集的变量，通常标记为英文字母末端的小写字母x、y、z、…，也常会使用下标来区别不同的变量：x0、x1、x2、…。
一个等式符号= 。详见下面的“等式”一节。
需注意，并不是所有的符号都需要，只要有量化符号的其中一个、否定及且、变量、括号及等式就足够了。还存在许多定义了额外逻辑符号的变体：
有时也会包括真值常数，用T、Vpq 或 来表示“真”，并用F、Opq 或 来表示“假”。若没有此类零参数的逻辑算符，这两个常数就只能用量化来表示。
有时也会包括额外的逻辑联结词，如谢费尔竖线、NAND 及异或。
非逻辑符号
非逻辑符号用来表示论域上的谓词（关系）、函数及常数。以前标准上会对所有不同的用途使用相同的无限集的非逻辑符号，而最近则会根据应用的不同而使用不同的非逻辑符号。因此变得需要列举出使用于一特定应用中的所有非逻辑符号。其选择是经由标识来形成的。
传统的做法是对所有的应用都只有单一个无限集的非逻辑符号。因此，根据传统的做法只会存在一种一阶逻辑的语言。这种做法现在依然很常见，尤其是在哲学方面的书籍。
对每个整数n ≥ 0，皆存在一组n 元谓词符号。因为这些谓词符号表示n 个元素间的关系，因此也称为关系符号。对每个参数量n，皆能有无限多个谓词符号：#:Pn0, Pn1, Pn2, Pn3, …
对每个整数n ≥ 0，皆存在无限多个n 元函数符号：
f n0, f n1, f n2, f n3, …
在当代的数理逻辑里，标识会因应用的不同而不同。数学里的典型标识，在群里为{1, ×}，或只为{×}；在有序体里为{0, 1, +, ×, <}。并没有限制非逻辑符号的数量，标识可以是空的、有限、无限，甚至是不可数的。例如，在勒文海姆–斯科伦定理的证明之中即会出现不可数的标识。
根据最近的做法，每个非逻辑符号皆为下列两种类型的其中一种。
具有0个或0个以上参数的谓词符号（或关系符号）。通常标记为大写字母P、Q、R、…。
0参数的关系可以视同为命题变量。例如可以代表任何叙述的P。
令P(x) 为具有1个参数的谓词变量，其中一个可能的解释为“x 是个人”。
令Q(x,y) 为具有2个参数的由词变量，其中一些可能的解释有“x 大于y”或“x 是y 的父亲”。
具有0个或0个以上参数的函数符号。标常标记为小写字母f、g、h、…。
举例来说，f(x) 可以解释成“x 的父亲”；在算术里，可代表“-x”；在集合论里，可代表“x的幂集”。g(x,y)在算术里可代表“x+y”；在集合论里，可代表“x和y的联集”。
0参数的函数符号也称为常数符号，常标记成英文字母前端的字母a、b、c、…。a 可代表“苏格拉底”；在算术里，可代表0；在集合论里，可代表空集。
形成规则
形成则定义一阶逻辑的项及公式。因为项及公式被表示为一串符号，这些规则可被用来写成项及公式的形式文法。这些规则通常是上下文无关的（规则的每个结果在其左侧都会有单一个符号），除非允许有无限多符号，且有许多开始符号，如项中的变量。
项
项可依如下规则递归地定义：
变量。每个变量皆是项。
函数。每个具有n 个参数的表示式f(t1,...,tn)（其中每个参数ti是项，且f 是具有n 个参数的函数符号）是项。另外，标记不同常数的符号是个0参数的函数符号，因此也是项。
只有可经由有限次地应用上述规则来得到的表示式才是项。举例来说，不存在一个同时是项且包含谓词符号的表示式。
公式
公式 (或称合式公式）可依如下规则递归地定义：
谓词符号。若P 是一个n 元谓词符号，且t1, ..., tn 是项，则P(t1,...,tn) 是公式。
等式。若等式符号算是逻辑的一部份，且t1 及t2 是项，则t1 = t2 是公式。
否定。若φ 是公式，则φ 是公式。
二元联结词。若φ 及ψ 是公式，则(φ ψ) 是公式。其他的二元逻辑联结词也可相似的规则。
量化。若φ 是公式，且x 是变量，则 及 都是公式。
只有可经由有限次地应用上述规则来得到的表示式才是公式。由头两个规则得到的公式称为原子公式。
举例来说，
是公式，若f 是1元函数符号，P 是1元谓词符号，且Q 是3元谓词符号。另一方面， 则不是公式，虽然这也是由词汇表中的符号组成的字串。
定义中的括号，其用途是为了确保任何公式都只能依递归定义以单一种方法得到（换句话说，每一个公式都只存在唯一的剖析树）。这个性质被称为公式的唯一可读性。对于括号要用在公式中的哪里存在有许多的惯例。例如，有些作者会使用冒号或句号来代替括号，或变更括号插入的地方。但每个作家个人的定义都必须证明会满足唯一可读性。
定义公式的规则无法定义“若-则-否则”函数ite(c,a,b)，其中的c是个以公式表示的条件，当c 为真时传回a，为假时传回b。这是因为谓词和函数都只能接受项当做其参数，但上述函数的第一个参数为公式。某些建构在一阶逻辑上的语言，如SMT-LIB 2.0，会增加此一定义。[2]
标示惯例
为了方便起见，会约定逻辑算符的优先性，来减少括号使用的情况。这些规则和算术中的运算顺序很像，一个常见的惯例为：
最先赋值；
下一个为 及 先赋值；
再下一个为量化先赋值；
则最后赋值。
此外，定义中不需要的额外标点符号也许会插入公式中，使公式更容易阅读。因此，公式
可写成
在某些领域里，常见使用中缀表示法来代表二元关系及函数，而非上面定义的前缀表示法。例如，在算术中，一般会写成“2+2=4”，而非“=(+(2,2),4)”。一般会将以中缀表示法表示的公式当做是以前缀表示法表示的对应公式的缩写。
上面定义中的二元联结词，如，是使用中缀表示法。一个较少见的惯例为波兰表示法，它将、等放在参数的前面而非之间。这个表示法允许舍弃所有的标点符号。波兰表示法是简洁且优雅的，但因为对人类很难阅读，所以实务上不常使用。使用波兰表示法，公式
会变成"∀x∀y→Pfx¬→ PxQfyxz"。
自由变量和约束变量
主条目：自由变量和约束变量
在一个公式里，变量可能是自由的或约束的。直观上来看，一个变量在公式里是自由的，若其没化量化：在 里，变量x 是自由的，而y 则是约束的。自由变量和约束变量可依如下规则递归地定义：
原子公式。若φ 是原子公式，则x 在φ 里是自由的，当且仅当x 出现在φ 里。更甚之，在原子公式中不存在约束变量。
否定。。x在φ 里是自由的，当且仅当x 在φ 里是自由的。x 在φ 里是约束的，当且仅当x 在φ 里是约束的。
二元联结词。x 在(φ ψ) 里是自由的，当且仅当x 在φ 或ψ 里是自由的。x 在(φ ψ) 里是约束的，当且仅当x 在φ 或ψ 里是约束的。相同的规则也适用于其他的二元联结词之上。
量化。x 在y φ 里是自由的，当且仅当x 在φ 里是自由的，且x 是个和y 相异的符号。而且，x 在y φ 里是约束的，当且仅当x 是y 或x 在φ 里是约束的。相同的规则也适用于之上。
举例来说，在x y (P(x) Q(x,f(x),z)) 里，x 和y 是约束变量，z 是自由变量，而w 则两者皆不是，因为它没有出现在公式之中。
自由和约束也可以用来专指在公式里特定地方出现的变量。如在 里，第一个x 是自由的，而第二个则是约束的。换句话说，x 在 里是自由的，而在 in 里则是约束的。
在一阶逻辑中，一个没有自由变量的公式称为一阶句子。此类公式在特定解释之下即会有良好定义的真值。例如，公式Phil(x) 是否为真需看x 代表什么，而句子 在一特定解释下则必为真或必为假。
例子
有序阿贝尔群的语言有一个常量0，一个一元函数−，一个二元函数 +，和一个二元关系≤。所以
0, x, y是原子项
+(x, y), +(x, +(y, −(z))）是项，通常写为x + y, x + y − z
=(+(x, y), 0)，≤（+(x, +(y, −(z))), +(x, y)）是原子公式，通常写为x + y = 0, x + y - z ≤ x + y
(∀x ∃y ≤（ +(x, y), z））∧（∃x =(+(x, y), 0)）是公式，通常写为 (∀x ∃y x + y ≤ z) ∧ (∃x x + y = 0)
语义
一阶语言的解释会对语言内的所有非逻辑常数赋予上意义，同时也决定能指明量化范围的论域。其结果为，每个项都会被赋予其代表的元件，每个句子也都会被赋予上一个真值。这样，解释即对语言内的项及公式提供了语义。研究形式语言的解释的学科称为形式语义学。
论域D 是由某种类型的“物件”所组成的非空集合。直观上来看，一阶公式是有关这些物件的叙述。例如， 叙述存在一个物件x，能使得指涉此物件的谓词P 为真。论域即是此类考量的物件的集合，例如可取D 为整数的集合。
函数符号的解释是函数。举例来说，若论域由整数所组成，则一个2元的函数符号f 能解释为给出其参数之和的函数。换句话说，符号f 和在此解释下为加法的函数I(f) 是相关连的。
常数符号的解释是一个从单元素集合D0 映射至D 的函数，也可简单视为是D 内的一个物件。例如，一个解释可将值 赋予常数符号。
n 元谓词符号的解释是由论域中的元素所组成的n 对有序集。这意味着，给定一个解释、一个谓词符号及论域中的n 个元素，则可依给定的解释判断这些元素的谓词是否为真。例如，一个2元谓词符号P 的解释I(P) 可以是一对整数，能使得第一个整数小于第二个整数。依据这个解释，谓词P 在其第一个参数小于第二个参数时为真。
一阶结构
主条目：结构 (数理逻辑)
指定一个解释的最常见方法是指定一个结构（或称做模型，见下文）。结构包括一个由论域及标识内的非逻辑项的解释I所组成的非空集合。这个解释自身是个函数：
每个n 元函数符号f 都会赋予一个从映射至的函数I(f)。特别地是，每个标识内的常数符号都会被赋予论域中的一个个体。
每个n 元谓词符号P 都会赋予一个在上的关系I(P)（或等价地说，一个从映射至的函数）。因此，每个谓词符号都被D 上的布林值函数所解释。
真值的赋值
一个公式由给定的解释及将论域中的元素与每个变量相关连的变量赋值μ 来决定为真或为假。需要变量赋值的原因是为了给予具自由变量的公式（如）意义。上述公式的真值为何要看x 和y 是否标记着相同的个体。
首先，变量赋值μ 可以扩展到语言内的所有项，使每个项都能映射至论域中的单一元素。下列的规则被用来得到赋值：
变量。每个变量x 皆可得到μ(x)。
函数。给定一组项（这些项皆已得到论域中的元素）及一个n 元函数符号f，则项 可得到。
再来，每个公式皆可赋予一个真值。用来得到赋值的递归性定义称为T-模式。
原子公式(1)。公式是依靠（其中 为项 的赋值，且 为 的解释）来决定其值是真是假。
原子公式(2)。公式 为真，若 及 得到论域中的相同物件（见下面等式一节）。
逻辑联结词。 及 等形式的公式是依据联结词的真值表（如命题逻辑一般）来赋值的。
存在量化。公式 根据解释M 和变量赋值μ 为真，若存在一个只和μ 在对x 的赋值上有所不同的变量赋值μ'，能使得φ 根据解释M 和变量赋值μ' 为真。此一形式定义是由“ 为真，当且仅当存在一种选择x 的方法，使得φ(x) 为真”的这个概念来的。
全称量化。公式 根据解释M 和变量赋值μ 为真，若φ(x)根据每个只和μ 在对x 的赋值上有所不同的变量赋值μ' 及解释M 为真。此一形式定义是由“ 为真，当且仅当每一种选择x 的方法，皆能使φ(x) 为真”的这个概念来的。
若一个公式不包含自由变量，即为一个句子，则一开始的变量赋值不会影影其真值。换句话说，一个句子根据M及 为真，当且仅当这个句子根据M 及其他的变量赋值 为真。
还有第二种常见的做法可以定义真值，而且不需要依靠变量赋值函数。给定一个解释M，首先将一组常数符号加至标识之中，每一个在M中的论域的元素对应一个常数符号：称对每个域论中的元素d，都会固定有一个常数符号cd。如此，解释就会被扩展至能使每一新的常数符号被赋予至其对应的论域元素上。现在可语法性地定义量化公式的真值如下：
存在量化。公式 根据M 为真，若存在某些在论域中的d，使得 为真。这里， 是用cd 取代每个φ 内以自由变量出现的x所得到的公式。
全称量化。公式 根据M 为真，若对每个论域中的d，根据M 的 皆为真。
这个做法对所有的句子会给出和使用变量赋值的做法一样的真值。
有效性、可满足性及逻辑结论
参见：可满足性
若句子φ 在一给定解释M 下为真，则称M 满足 φ，标记为。一个句子称为可满足的，若存在一些解释使其为真。
具自由变量的公式的可满足性就较为复杂了，因为只用解释并无法决定此类公式的真值。一个常见的惯例是称一个具自由变量的公式在一个解释下为可满足的，若不论如何将论域中的个体赋予其自由变量，这个公式皆为真。这等价于称公式为可从足的，当且仅当其全称闭包为可满足的。
一个公式是逻辑有效的（或简单称为有效的），若在每一个解释之下皆为真。此类的公式和命题逻辑中的重言式扮演着相似的角色。
一个公式φ 是公式ψ的逻辑结论，若每个使得ψ 为真的解释皆会使得φ 为真。在此一状况下，称φ 被ψ 逻辑蕴涵着。
代数化
另一种赋予一阶逻辑语义的方法可经由抽象代数处理。这种方法是将命题逻辑的林登鲍姆-塔斯基代数扩展而成。有如下几种类型：
圆柱代数，由阿尔弗雷德·塔斯基和其同事提出；
多元代数，由保罗·哈尔莫斯提出。
谓词函子逻辑，主要是基于威拉德·范·奥曼·奎因的工作成果。
这些代数都是纯粹扩展两元素布尔代数而成的格。
塔斯基和葛范德于1987年证明，没有超过包在三个以上的量化内的原子句子的部份一阶逻辑，其表示力和关系代数相同。上述部份一阶逻辑令人十分地感到有兴趣，因为它已足够表示皮亚诺算术和公理化集合论，包括典型的ZFC。他们亦证明了，具有简单有序对的一阶逻辑和具有两个有序的投影函数的关系代数等价。
一阶理论、模型及基本类
另见：一阶理论列表
一阶理论是由在一特定一阶标识内的一组公理所组成的。公理所组成的集合通常是有限的或递归可枚举的，此类的理论称为是有效的。有些作者要求理论也要包括所有由公理导出的逻辑结论。
满足给定理论内的所有句子的一阶结构称为此理论的模型。基本类是由所有满足特定理论的结构所组成的集合。这些类是类型论里的研究主题。
许多理论都有一个预期解释，即一个在研究理论时会在意的某种模型。例如，皮亚诺公理的预期解释是由一般的自然数和其一般的运算所组成的。不过，勒文海姆–斯科伦定理证明，大多数的一阶理论也都会有其他的非标准模型。
一个理论是相容的，若不可能由这个理论的公理中证明出矛盾来。一个理论是完备的，若对每个其标识内的公式，此公式或公式的否定会是个由理论公理导出的逻辑结论。哥德尔不完备定理证明，有效的一阶理论只要它强到足以蕴涵自然数的理论，即无法同时是相容且完备的。
空论域
上述定义需要任何一个解释的论域均为非空集合。但在如自由逻辑之中，设定空论域是被允许的。更甚之，若代数结构的类包含一个空结构（如空偏序集），当允许空论域时，这个类只能是一阶逻辑中的一个基本类，不然就要将空结构由类中移除。
不过，空论域存在着一些难点：
许多常见的推理规则只在论域被要求是非空时才为有效的。一个例子为，当x 不是 内的自由变量时，会蕰涵。这个用来将公式写成前束范式的规则在非空论域中是可靠的，但在允许空论域时则是不可靠的。
在使用变量赋值函数的解释中，真值的定义不能和空论域一起运作，因为不存在范围为空的变量赋值函数。（相似地，也无法将解释赋予上常数符号。）在甚至是原子公式的真值可被定义之前，都必须选定一个变量赋值函数。然后一个句子的真值即可在任一个变量赋值之下定义出其真值，且可证明其真值不依选定的赋值而变。这个做法在赋值函数不存在时不能运作；除非将其改成配上空论域。
因此，若空论域是被允许的，通常也必须被视成特例。不过，大多数的作家会简单地将空论域由定义中排除。
代换
设 t是项。φ(x)是可能包含x作为自由变量的公式。
φ(t)可定义为把自由变量x替代为t的结果，但前提是必须没有任何t在φ(x)中是约束的。
若非如此，则x替代成t之前，必须先把φ中的约束变量，改为不同于t的符号。
例如把公式φ(x)假定为∀y:y ≤ x（"x是极大的"）。
若用t代换x，则φ(t)即∀y:y ≤ t就表示t是极大的。
这里举个错误的例子，若在φ(x)中含有约束变量y的状况下，不去修改φ(x)中含有约束变量y，直接把x代换成y，代换结果如下
∀y:y ≤ y
如此一来即成为跟φ(x)意义完全不同的公式。
正确的演算方法为先把φ(x)中的约束变量用到y的地方改成不同于y的符号，好比z
即把 ∀y:y ≤ x 改成 ∀z:z ≤ x，这两命题的意义一致。
再把x代换成y，即为 ∀z:z ≤ y
所以 φ(y) 表示 ∀z:z ≤ y，而不是 ∀y:y ≤ y
忘记这个条件是声名狼籍的犯错误原因。
推理规则
肯定前件充当推理的唯一规则。
叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为
如果，则
这里的Z(x)假定表示谓词演算的一个已证明的定理，而∀xZ(x)是它针对于变量x的闭包。谓词字母Z可以被任何谓词字母所替代。
公理
对于任何理论，知道公理的集合是否可用算法生成，或是否存在算法确定合式公式为公理，是很有价值的。
如果存在生成所有公理的算法，则公理的集合被称为递归可枚举的。
如果存在算法在有限步骤后确定一个公式是否是公理，则公理的集合被称为递归的或“可判定的”。在这种情况下，你还可以构造一个算法来生成所有的公理：这个算法简单的（随着长度增长）一个接一个的生成所有可能的公式，而算法对每个公式确定它是否是个公理。
一阶逻辑的公理总是可判定的。但是在一阶理论中非逻辑公式就不必需如此。
量词公理
下列四个公理是谓词演算的特征：
PRED-1:
PRED-2:
PRED-3:
PRED-4:
它们实际上是公理模式：表达式W表示对于其中任何wff，x不是自由的；而表达式Z（x）表示对于任何wff带有额外的约定，即Z（t）表示把Z（x）中的所有x替代为项t的结果。
等式和它的公理
在一阶逻辑中对使用等式（或恒等式）有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果，区别主要在术语上。
对等式的最常见的约定是把等号包括为基本逻辑符号，并向一阶逻辑增加等式的公理。等式公理是
x = x
x = y → f(...,x,...) = f(...,y,...)对于任何函数f
x = y →（P(...,x,...) → P(...,y,...)）对于任何关系P（包括 = 自身）
其次常见的约定是把等号包括为理论的关系之一，并向这个理论的公理增加等式的公理。在实际中这是同前面约定最难分辨的，除了在没有等式概念的不常见情况下。公理是一样的，唯一的区别是把它叫做逻辑公理还是这个理论的公理。
在没有函数和有有限数目个关系的理论中，有可能以关系的方式定义等式，通过定义两个项s和t是相等的，如果任何关系通过把s改变为t 在任何讨论下都没有改变。例如，在带有一个关系∈的集合论中，我们可以定义s = t为∀x (s ∈ x ↔ t ∈ x) ∧ ∀x (x ∈ s ↔ x ∈ t)的缩写。这个等式定义接着自动的满足了关于等式的公理。
在某些理论中有可能给出特别的等式定义。例如，在带有一个关系 ≤的偏序的理论中，我们可以定义s = t为s ≤ t ∧ t ≤ s的缩写。
谓词演算
谓词演算是命题演算的扩展，它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件来定义（可以有很多不同的方式），则谓词演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说，谓词演算采用的公理有：
来自命题演算的所有重言式（命题变量被替代为公式）。
上面给出的量词公理。
上面给出的等式公理，如果等式被认为是逻辑概念的话。
一个句子被定义为是在一阶逻辑中可证明的，如果可以通过从谓词演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。
如果我们有一个理论T（在某些语言中叫做公理的陈述的集合），则一个句子φ被定义为是在理论T中可证明的，如果
a ∧ b ∧ ... → φ
在一阶逻辑中对于理论T的某个公理a, b,...的有限集合是可证明的。
可证明性的一个明显问题是它好像非常特别：我们采用了显然随机的公理和推理规则的搜集，不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理确保这实际上不是问题：这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是，在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义（尽管在不同的可证明性的定义下证明的长度可能有巨大差别）。
有很多不同（但等价）的方式来定义可证明性。前面的演算是"希尔伯特风格"演算的一个典型例子，它有许多不同的公理但只有非常少的推理规则。"根岑风格"谓词演算有非常少的公理但有许多推理规则。
文法上说谓词演算在现存的命题演算上增加了“谓词-主词结构”和量词。主词是给定的个体群组（集合）的一个成员的名字，而谓词是在这个群组上的关系，一元谓词在哲学中称为性质，在数学中称为指示函数，在数理逻辑中称为布尔值函数。
一阶逻辑的元逻辑定理
下面列出了一些重要的元逻辑定理。
不像命题演算，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程，判定P是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）
有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式P, P是可证明的。
一元谓词逻辑（就是说，谓词只有一个参数的谓词逻辑）是可判定的。
转换自然语言到一阶逻辑
用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。 [4]
一阶逻辑的限制
所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。
难于表达if-then-else
太奇怪了，（如典型定义的）带有等式的FOL不包含或允许定义if-then-else谓词或函数if(c,a,b)，这里的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，谓词和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。
在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。[5] 谓词if(c,a,b)如果重写为就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况谓词叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这里的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。[6] 其他人进一步扩展FOL使得函数和谓词可以在任何位置接受项和公式二者。
类型（种类）
除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 [7]，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 [8]。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。
单一参数谓词可以用来在合适的地方实现类型的概念。例如:
，
谓词Man(x)可以被认为是一类“类型断言”（就是说，x必须是男人）。 谓词还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如:
(“存在既是男人又是人类的事物”)。
容易写成，但这将等价与(“存在不是男人的事物或者存在是人类的事物”)，这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如:
(“对于所有x，如果x是男人，则x是哺乳动物)。
难于刻画有限性或可数性
图可及性不能表达
很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用谓词逻辑完全表达。换句话说，没有谓词逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）谓词符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。[9]
