一阶逻辑 是使用于数学 、哲学 、语言学 及电脑科学 中的一种形式系统 ，也可以称为：一阶断言演算 、低端断言演算 、量化理论 或谓词逻辑 。一阶逻辑和命题逻辑 的不同之处在于，一阶逻辑包含量词 。
高端逻辑 和一阶逻辑不同之处在于，高端逻辑的断言符号可以有断言符号或函数符号当做引数，且容许断言量词或函数量词[1] 语义 中，断言被解释为关系 。而高端逻辑的语义里，断言则会被解释为集合的集合。
在通常的语义下，一阶逻辑是可靠 （所有可证的叙述皆为真）且完备 （所有为真的叙述皆可证）。虽然一阶逻辑的逻辑归结 只是半可判定性 的，但还是有许多用于一阶逻辑上的自动定理证明 。一阶逻辑也符合一些使其能通过证明论 分析的元逻辑 定理，如勒文海姆–斯科伦定理 及紧致性定理 。
一阶逻辑是数学基础 中很重要的一部分。许多常见的公理系统，如一阶皮亚诺公理 、冯诺伊曼-博内斯-哥德尔集合论 和策梅洛-弗兰克尔集合论 都是一阶理论。然而，一阶定理并没有能力去完整描述及范畴性地 （“唯一地”）刻划如自然数 或实数 之类无限的概念。这些结构的公理系统可以由如二阶逻辑 之类更强的逻辑来获取。
简介 以下通俗的介绍一阶逻辑。
在命题逻辑里，“苏格拉底是哲学家”、“帕雷托是哲学家”只能简单标记为
p
{\displaystyle p}
q
{\displaystyle q}
而在一阶逻辑，我们先将符号
Phil
(
x
)
{\displaystyle \text{Phil}(x)}
x
{\displaystyle x}
s
{\displaystyle s}
b
{\displaystyle b}
Phil
(
s
)
{\displaystyle \text{Phil}(s)}
p
{\displaystyle p}
Phil
(
b
)
{\displaystyle \text{Phil}(b)}
q
{\displaystyle q}
断言符号 “
Phil
(
x
)
{\displaystyle \text{Phil}(x)}
语义的解释 ，而这个解释默认一个“所有人类的群体”(也就是我们一阶逻辑语义的论域 )，将变量
x
{\displaystyle x}
事实上断言符号可以包含不只一个的变量，比如说我们可以把
Cp
(
x
,
y
)
{\displaystyle \text{Cp}(x,\,y)}
x 与y 是夫妻”，这样
Cp
(
s
,
y
)
{\displaystyle \text{Cp}(s,\,y)}
就可以解释为“苏格拉底和y 是夫妻”。
进一步的，断言符号和变量还可以和逻辑符号组合成更复杂的叙述。例如将断言符号
Schol
(
x
)
{\displaystyle \text{Schol}(x)}
x
{\displaystyle x}
x 为哲学家，则x 为学者”可以表示为
Phil
(
x
)
⇒
Schol
(
x
)
{\displaystyle \text{Phil}(x)\Rightarrow \text{Schol}(x) \,}
而“对所有x ，若x 为哲学家，则x 为学者”之类的叙述，我们写为
∀
x
(
Phil
(
x
)
⇒
Schol
(
x
)
)
{\displaystyle \forall x ( \text{Phil}(x) \Rightarrow \text{Schol}(x))}
也就是自左方开始阅读，以
∀
x
{\displaystyle \forall x}
x ”；将叙述理解为“对所有的x ，
∀
x
{\displaystyle \forall x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
全称量词
但全称量词直观上，会有“若所有x 是哲学家，那x 的长子也会是哲学家”这样的叙述，为此我们将
Son
(
x
)
{\displaystyle \text{Son}(x)}
x 的长子”，这样前面的叙述可以写为
∀
x
Phil
(
x
)
⇒
Phil
[
Son
(
x
)
]
{\displaystyle \forall x \text{Phil}(x) \Rightarrow \text{Phil}[\text{Son}(x)]}
这种解释为成与
x
{\displaystyle x}
函数符号 。而事实上这段直观为真的叙述，经过适当的扩展以后就是一阶逻辑其中的一条公理 。
而对于“有x 是哲学家”，我们引入另一种量词而表记为：
∃
x
(
Phil
(
x
)
)
{\displaystyle \exists x ( \text{Phil}(x))}
自左方开始阅读，以
∃
x
{\displaystyle \exists x}
x ”；也就是解释为“有x 使
∃
x
{\displaystyle \exists x}
∃
x
{\displaystyle \exists x}
x
{\displaystyle x}
存在量词 。全称量词和存在量词一起被简称为量词
而直观上，“并非所有x 不是哲学家”，和“有x 是哲学家”是等价的；且“并非有x 不是学者”也跟“所有的x 是学者”在直观上也是等价的。所以只要有“否定”这个逻辑概念，那一阶逻辑就只需要一种量词。据此，并且为了使逻辑公理的叙述更加简洁，一般会以全称量词 为基础，作以下的符号定义(
¬
{\displaystyle \neg}
A
{\displaystyle \mathcal{A}}
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
{\displaystyle \exists x \mathcal{A}:=\neg[\forall x (\neg\mathcal{A})]}
而将存在量词定义为全称量词的衍伸符号。
在通常的一阶逻辑语义解释 上，需要一个量词所提及对象所组成的非空集合，称为论域 。例如，
∃
x
Phil
(
x
)
{\displaystyle \exists x \text{Phil}(x)}
集合论 基础，但一般的严谨的公理化集合论 都是以一阶逻辑的语言来叙述（如策梅洛-弗兰克尔集合论 ）。这不免让一阶逻辑语义沦为"具有集合论公理的一阶逻辑理论的一套元定理 "，用来有效的检验一段"叙述"(合式公式 )是否为这个一阶逻辑理论的定理 。
形式理论 一阶逻辑的形式理论 可分成几个部分：
语法 ：决定哪些符号组合是合法表示式 。推理规则：一种针对合式公式的符号组合规则(对应于直观上的"推理")
公理：一套合式公式(对应于直观理解上，一个理论的基本假设。逻辑公理缩小形式系统与直观逻辑的差距。) 语法 基本词汇 一套理论到底能容许多少符号，取决于人类以物理定律 的手段能塑造和容下多少的符号。但以目前所知是无法确知宇宙是不是有限，或是是否可无限制分割。虽然所有的公理化集合论 都以量词的形式隐晦的承认无穷的存在(如ZF集合论的无穷公理 )，甚至以这样自然数 意义上的无穷为基础，去建构出不可数 的实数。但将之对应到现实，还是会遇到同样的物理问题。
谨慎起见，以下各种类的符号没有特别声明，数量将会是有限个。
逻辑符号 词汇表中存在若干个逻辑符号，通常包括：
量化符号
∀
{\displaystyle \forall}
∃
{\displaystyle \exists}
某些作者[2]
∃
{\displaystyle \exists}
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
,
{\displaystyle \exists x\mathcal{A}:= \neg[\forall x(\neg\mathcal{A})],}
如此只需要
∀
{\displaystyle \forall}
逻辑联结词 ：以下为可能的表示符号，而波兰表示法下的逻辑连接词请参见逻辑运算的波兰记法
否定 ：
¬
{\displaystyle \neg}
∼
{\displaystyle \sim}
条件 ：
⇒
{\displaystyle \Rightarrow}
→
{\displaystyle \rightarrow}
⊃
{\displaystyle \supset}
且 ：
∧
{\displaystyle \land}
&
{\displaystyle \&}
或 ：
∨
{\displaystyle \lor}
|| 双条件 ：
⇔
{\displaystyle \Leftrightarrow}
↔
{\displaystyle \harr}
某些作者[3]
A
∧
B
:=
¬
(
A
⇒
(
¬
B
)
)
,
{\displaystyle \mathcal{A}\wedge\mathcal{B}:=\neg(\mathcal{A}\Rightarrow(\neg\mathcal{B})),}
A
∨
B
:=
(
¬
A
)
⇒
B
,
{\displaystyle \mathcal{A}\vee\mathcal{B}:=(\neg\mathcal{A})\Rightarrow\mathcal{B},}
A
⇔
B
:=
(
A
⇒
B
)
∧
(
B
⇒
A
)
,
{\displaystyle \mathcal{A}\Leftrightarrow\mathcal{B}:=(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A}),}
如此一来只需要否定 和条件 作为基础符号。 标点符号：括号、逗号及其他，依作者的喜好有所不同。
为了更有效的将括号做配对，通常还会采用大括号{ } 跟中括号[ ] 。
至多跟自然数 一样多的变量 ，通常标记为英文字母末端的小写字母x 、y 、z 、…，也常会使用下标（或上标、上下标兼有）来区别不同的变量：x 0 、x 1 、x 2 、…。(特别注意c有时候会被当成常数符号而引起混淆)
等式符号：
=
{\displaystyle =}
有作者会因为语义上解释"相等"的不同，而将等式符号视为双元断言符号、甚至是某类合式公式的简写。详见下面的“等式”一节。
符号相等：
≍
{\displaystyle \asymp}
为了将词汇于符号识别上为等同 和等式符号做区隔，某些作者[4] 注意并非所有的符号都需要，比如说比较极端的理论，因谢费尔竖线 (或异或 )的布尔代数 完备性使得所有不含量词的逻辑公理可以以谢费尔竖线表述，而大幅减少基础的逻辑联结词。
另外，一些作者并没有将语义学 和形式理论 划分清楚，而会将真值常数纳入符号的一环；用T、Vpq 或
⊤
{\displaystyle \top}
pq 或
⊥
{\displaystyle \bot}
断言符号 “他们两人是夫妻”，代表一个关于两个"对象"的断言，而“他是人”、“三点共线”显示了断言是容许一个──甚至多个对象，所以对于自然数
n
{\displaystyle n}
j
{\displaystyle j}
A
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle A^n_j(x_1,\,x_2,\,...,\,x_n)}
为一阶逻辑的合法词汇，它在直观上表示一个有
n
{\displaystyle n}
n
{\displaystyle n}
元断言符号 。下标的自然数
j
{\displaystyle j}
n
{\displaystyle n}
实用上只要有申明，不至于和其他词汇引起混淆的话，我们可以用任意的形式简写一个断言符号，如公理化集合论 里的
x
∈
y
{\displaystyle x\in y}
A
1
2
(
x
,
y
)
{\displaystyle A^2_1(x,\,y)}
函数符号 “物体的颜色”、“夫妻的长子”说明了一列对象所唯一 对应的对象。但不同的夫妻有不同的长子；不同的物体有不同的颜色，所以对于自然数
n
{\displaystyle n}
j
{\displaystyle j}
f
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle f^n_j(x_1,\,x_2,\,...,\,x_n)}
为一阶逻辑的合法词汇，它在直观上表示
n
{\displaystyle n}
n
{\displaystyle n}
元函数符号 。但特别注意这种＂唯一对应＂的直观想法，必须要有量词的公理配上下面“等号”的章节以后，才能被实现。
就像断言符号，不引起混淆的话我们可以用任何的形式简写函数符号，如公理化集合论 里的
x
∪
y
{\displaystyle x\cup y}
并集公理 而定义的新函数符号(请参见下面“函数符号与唯一性”的章节)，也可以冗长的表记为
f
j
2
(
x
,
y
)
{\displaystyle f^2_j(x,\,y)}
常数符号 “刻度0”、“原点”、“苏格拉底 ”这种(至少在作者的)直观上"唯一不变"的对象，使我们对自然数
j
{\displaystyle j}
c
j
{\displaystyle c_j}
为一阶逻辑的合法词汇，它在直观上表示一个"唯一不变"的对象。称为常数符号 ，同样的"常数的不变"要等到下面“等号”的章节才能被实现。
为了不和变量的表记混淆，常数符号一样可以用任何的形式简写，如公理化集合论 里的
∅
{\displaystyle \varnothing}
空集公理 和“函数符号与唯一性”的章节，而定义的新常数符号。亦可冗长的表示为
c
j
{\displaystyle c_j}
形成规则 和自然语言(如英语 )不同，一阶逻辑的语言以明确的递归定义判断一个给定的词汇是否合法。大致上来说，一阶逻辑以“项”代表讨论的对象，而对“项”的断言组成了最基本的原子(合式)公式 合式公式 (也就是"叙述")。
项 “那对夫妻的长子的职业”、“
(
x
+
y
)
×
z
{\displaystyle (x+y)\times z}
x
∪
∅
{\displaystyle x\cup\varnothing}
项 为：
变量 和常数 是项。若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_1,\,....,\,T_n}
f
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle f^n_j(T_1,\,....,\,T_n)}
项只能透过以上两点，于有限步骤内置构出来。 我们习惯用大写的西方字母(如英文 字母、希伯来 字母、希腊字母 )代表项，如果变量不得不采用大写字母，而跟会项引起混淆的话，需额外规定分辨的办法。
原子公式 为了比较简洁的规定什么是合式公式 ，我们先规定原子公式 为：（若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_1,\,....,\,T_n}
A
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle A^n_j(T_1,\,....,\,T_n)}
这样的形式。
公式 一阶逻辑的合式公式
w
f
{\displaystyle wf}
原子公式为公式。(美观起见，在原子公式外面包一层括弧也是公式)
若
A
{\displaystyle \mathcal{A}}
(
¬
A
)
{\displaystyle (\neg\mathcal{A})}
若
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
⇒
B
)
{\displaystyle (\mathcal{A}\Rightarrow\mathcal{B})}
若
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
(
∀
x
A
)
{\displaystyle (\forall x\mathcal{A})}
(
∀
x
)
A
:=
∀
x
A
{\displaystyle (\forall x)\mathcal{A}:=\forall x\mathcal{A}}
合式公式只能透过以上四点，于有限步骤内置构出来。 另外成对的中括弧跟大括弧，符号识别上我们视为成对的小括弧。我们习惯以草书的大写西方字母 为公式的代号。
举例来说，
{
(
∀
y
)
A
1
2
[
x
,
f
1
1
(
y
)
]
}
{\displaystyle \{(\forall y)A^2_1[x,\,f^1_1(y)]\}}
是公式而
∀
x
x
⇒
{\displaystyle \forall x\, x \Rightarrow}
则不是公式。
而接下来我们只要对任意公式
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
x
{\displaystyle x}
(
A
∧
B
)
:=
{
¬
[
A
⇒
(
¬
B
)
]
}
{\displaystyle (\mathcal{A}\wedge\mathcal{B}):=\{\neg[\mathcal{A}\Rightarrow(\neg\mathcal{B})]\}}
(
A
∨
B
)
:=
[
(
¬
A
)
⇒
B
]
{\displaystyle (\mathcal{A}\vee\mathcal{B}):=[(\neg\mathcal{A})\Rightarrow\mathcal{B}]}
(
A
⇔
B
)
:=
[
(
A
⇒
B
)
∧
(
B
⇒
A
)
]
{\displaystyle (\mathcal{A}\Leftrightarrow\mathcal{B}):=[(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A})]}
(
∃
x
A
)
:=
{
¬
[
∀
x
(
¬
A
)
]
}
{\displaystyle (\exists x\mathcal{A}):=\{\neg[\forall x(\neg\mathcal{A})]\}}
(
∃
x
)
A
:=
∃
x
A
{\displaystyle (\exists x)\mathcal{A}:=\exists x\mathcal{A}}
这样所有的逻辑连接词与量词就纳入了合式公式的规范。
施用 所谓的施用 /作用 ，是以下公式形式的口语说法：(其中
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
¬
A
)
{\displaystyle (\neg\mathcal{A})}
¬
{\displaystyle \neg}
A
{\displaystyle \mathcal{A}}
(
A
⇒
B
)
{\displaystyle (\mathcal{A}\Rightarrow\mathcal{B})}
⇒
{\displaystyle \Rightarrow}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
∧
B
)
{\displaystyle (\mathcal{A}\wedge\mathcal{B})}
∧
{\displaystyle \wedge}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
∨
B
)
{\displaystyle (\mathcal{A}\vee\mathcal{B})}
∨
{\displaystyle \vee}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
⇔
B
)
{\displaystyle (\mathcal{A}\Leftrightarrow\mathcal{B})}
⇔
{\displaystyle \Leftrightarrow}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
∀
x
A
)
{\displaystyle (\forall x\mathcal{A})}
∀
x
{\displaystyle \forall x}
A
{\displaystyle \mathcal{A}}
(
∃
x
A
)
{\displaystyle (\exists x\mathcal{A})}
∃
x
{\displaystyle \exists x}
A
{\displaystyle \mathcal{A}}
就好似运算符作用在它们身上。
自由变量和约束变量 量词所施用的公式被称为量词的范围 (scope)。同一个变量在公式一般来说不只出现一次，若变量
x
{\displaystyle x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
不自由 /被约束的
x
{\displaystyle x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
自由的
x
{\displaystyle x}
例如，对于公式：
(
∀
x
)
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
{\displaystyle (\forall x)[A^1_1(x)\Rightarrow A^1_2(y)]}
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
{\displaystyle [A^1_1(x)\Rightarrow A^1_2(y)]}
∀
x
{\displaystyle \forall x}
A
1
1
{\displaystyle A^1_1}
x
{\displaystyle x}
A
2
1
{\displaystyle A^1_2}
y
{\displaystyle y}
说
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
封闭公式/句子
括弧的简写 括弧是为了保证语义解释符合预期，但太多的括弧书写不易，为此我们规定以下的"重构法"(反过来就是"简写法")，从表面上不合法的一串符号找出作者原来想表达的公式：
若整串符号的括弧不成对，直接视为无法重构 。
以
¬
,
∧
,
∨
,
∀
,
∃
,
⇒
,
⇔
{\displaystyle \lnot,\,\land,\,\lor,\,\forall,\,\exists,\,\Rightarrow,\,\Leftrightarrow}
相邻的逻辑连接词或量词无法决定施用顺序的话，以右边为先。
重构施用的顺序，以被成对括弧包住的部分为优先施用，其次才是落单的断言符号。 举例来说
¬
[
∀
x
A
1
1
(
x
)
]
⇒
∃
x
¬
A
2
1
(
x
)
{\displaystyle \lnot [\forall x A^1_1(x)] \Rightarrow \exists x \lnot A^1_2(x)}
的重构过程如下
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
∃
x
[
¬
A
2
1
(
x
)
]
{\displaystyle \{\lnot [\forall x A^1_1(x)]\} \Rightarrow \exists x [\lnot A^1_2(x)]}
¬
{\displaystyle \lnot}
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
{\displaystyle \{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\}}
∃
{\displaystyle \exists}
{
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
}
{\displaystyle \{\{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\}\}}
⇒
{\displaystyle \Rightarrow}
可以被重构为公式的一串符号，我们宽松的认定为"合式公式"。(最明显的例子就是合式公式最外层的括弧可以"省略")
波兰表示法 波兰表示法 将逻辑连接词前置于被施用的公式 而非传统的中间。如果沿用以上的"施用顺序"，这个表示法允许舍弃所有括弧。如公式
∀
x
∀
y
{
A
1
1
[
f
1
1
(
x
)
]
⇒
¬
{
A
1
1
(
x
)
⇒
A
1
3
[
f
1
1
(
y
)
,
x
,
z
]
}
}
{\displaystyle \forall x\forall y\{A^1_1[f^1_1(x)]\Rightarrow\neg\{A^1_1(x)\Rightarrow A^3_1[f^1_1(y),x,z]\}\}}
的波兰表示法为
∀
x
∀
y
⇒
A
1
1
f
1
1
x
¬
⇒
A
1
1
x
A
1
3
f
1
1
y
x
z
{\displaystyle \forall x\forall y\Rightarrow A^1_1 f^1_1 x\neg\Rightarrow A^1_1 x A^3_1 f^1_1 y x z}
推理规则 对于公式
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
A
⇒
B
{\displaystyle \mathcal{A}\Rightarrow\mathcal{B}}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
直观意义非常明显，就是p =>q 且p 可以推出q 。
公理 逻辑公理 如果
B
{\displaystyle \mathcal{B}}
C
{\displaystyle \mathcal{C}}
D
{\displaystyle \mathcal{D}}
(A1)
B
⇒
(
C
⇒
B
)
{\displaystyle \mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{B})}
(A2)
[
B
⇒
(
C
⇒
D
)
]
⇒
[
(
B
⇒
C
)
⇒
(
B
⇒
D
)
]
{\displaystyle [\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{D})]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{D})]}
(A3)
[
(
¬
B
)
⇒
(
¬
C
)
]
⇒
[
(
¬
B
⇒
C
)
⇒
B
]
{\displaystyle [(\neg\mathcal{B})\Rightarrow(\neg\mathcal{C})]\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow\mathcal{B}]}
都是公理。
它们实际上是公理模式 ，代表着"无限多"条的公理。
量词公理 以下的
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
C
{\displaystyle \mathcal{C}}
(A4)
T
{\displaystyle T}
t
{\displaystyle t}
T
{\displaystyle T}
B
{\displaystyle \mathcal{B}}
∀
t
{\displaystyle \forall t}
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
T
{\displaystyle T}
x
{\displaystyle x}
[
(
∀
x
)
B
(
x
)
]
⇒
[
B
(
T
)
]
{\displaystyle [(\forall x)\mathcal{B}(x)]\Rightarrow[\mathcal{B}(T)]}
为公理
其中
B
(
T
)
{\displaystyle \mathcal{B}(T)}
B
{\displaystyle \mathcal{B}}
x
{\displaystyle x}
T
{\displaystyle T}
(A5)如果
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
B
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[\mathcal{B}\Rightarrow(\forall x\mathcal{C})]}
为公理 (A6)
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
(
∀
x
B
)
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[(\forall x\mathcal{B})\Rightarrow(\forall x\mathcal{C})]}
(A7) 若
B
{\displaystyle \mathcal{B}}
(
∀
x
)
B
{\displaystyle (\forall x)\mathcal{B}}
也是公理。 它们实际上是公理模式 。
定理与证明 以下介绍一些理解公理所需的基本用语和符号
在一阶逻辑理论
L
{\displaystyle \mathcal{L}}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
C
n
{\displaystyle \mathcal{C}_n}
A
{\displaystyle \mathcal{A}}
C
1
{\displaystyle \mathcal{C}_1}
L
{\displaystyle \mathcal{L}}
若
1
<
k
<
n
{\displaystyle 1 < k < n}
C
k
{\displaystyle \mathcal{C}_k}
C
k
{\displaystyle \mathcal{C}_k}
L
{\displaystyle \mathcal{L}}
存在
i
,
j
<
k
{\displaystyle i,\,j < k}
C
i
{\displaystyle \mathcal{C}_i}
(
C
j
⇒
C
k
)
{\displaystyle (\mathcal{C}_j\Rightarrow\mathcal{C}_k)}
而口语上会称公式
A
{\displaystyle \mathcal{A}}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
L
{\displaystyle \mathcal{L}}
定理 (theorem)。而这列
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
例如定理
⊢
L
B
⇒
B
{\displaystyle \vdash_{\mathcal{L}}\mathcal{B}\Rightarrow\mathcal{B}}
C
1
{\displaystyle \mathcal{C}_1}
{
B
⇒
[
(
B
⇒
B
)
⇒
B
]
}
⇒
{
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
}
{\displaystyle \{\mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]\}\Rightarrow\{[\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})\}}
C
2
{\displaystyle \mathcal{C}_2}
B
⇒
[
(
B
⇒
B
)
⇒
B
]
{\displaystyle \mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]}
C
3
{\displaystyle \mathcal{C}_3}
B
⇒
(
B
⇒
B
)
{\displaystyle \mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})}
C
4
{\displaystyle \mathcal{C}_4}
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
{\displaystyle [\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})}
C
1
{\displaystyle \mathcal{C}_1}
C
2
{\displaystyle \mathcal{C}_2}
C
5
{\displaystyle \mathcal{C}_5}
B
⇒
B
{\displaystyle \mathcal{B}\Rightarrow\mathcal{B}}
C
4
{\displaystyle \mathcal{C}_4}
C
3
{\displaystyle \mathcal{C}_3}
直观上的证明，总是会有一些"前提假设"，对此，若我们以
Γ
{\displaystyle \Gamma}
Γ
⊢
L
A
{\displaystyle \Gamma\vdash_{\mathcal{L}}\mathcal{A}}
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
C
n
{\displaystyle \mathcal{C}_n}
A
{\displaystyle \mathcal{A}}
若
k
<
n
{\displaystyle k < n}
C
k
{\displaystyle \mathcal{C}_k}
C
k
{\displaystyle \mathcal{C}_k}
L
{\displaystyle \mathcal{L}}
C
k
{\displaystyle \mathcal{C}_k}
Γ
{\displaystyle \Gamma}
存在
i
,
j
<
k
{\displaystyle i,\,j < k}
C
i
{\displaystyle \mathcal{C}_i}
(
C
j
⇒
C
k
)
{\displaystyle (\mathcal{C}_j\Rightarrow\mathcal{C}_k)}
这样我们称
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
Γ
{\displaystyle \Gamma}
A
{\displaystyle \mathcal{A}}
若要特别凸显
Γ
{\displaystyle \Gamma}
B
{\displaystyle \mathcal{B}}
Γ
,
B
⊢
L
A
{\displaystyle \Gamma,\,\mathcal{B}\vdash_{\mathcal{L}}\mathcal{A}}
Γ
{\displaystyle \Gamma}
B
1
,
.
.
.
,
B
n
{\displaystyle \mathcal{B}_1,...,\mathcal{B}_n}
B
1
,
.
.
.
,
B
n
⊢
L
A
{\displaystyle \mathcal{B}_1,...,\mathcal{B}_n\vdash_{\mathcal{L}}\mathcal{A}}
以上的记号，在引用哪个理论很显然的情况下，
⊢
L
{\displaystyle \vdash_{\mathcal{L}}}
L
{\displaystyle \mathcal{L}}
从公理(A1)和(A2)会得出一条很直观的元定理：
一阶逻辑理论
L
{\displaystyle \mathcal{L}}
Γ
,
B
⊢
L
C
{\displaystyle \Gamma,\mathcal{B}\vdash_{\mathcal{L}}\mathcal{C}}
Γ
⊢
L
B
⇒
C
{\displaystyle \Gamma\vdash_{\mathcal{L}}\mathcal{B}\Rightarrow\mathcal{C}}
等式和它的公理 在一阶逻辑中对使用等式（或恒等式）有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果，区别主要在术语上。
对等式的最常见的约定是把等号包括为基本逻辑符号，并向一阶逻辑增加等式的公理。等式公理是 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 的缩写。 语义 一阶语言的解释 会对语言内的所有非逻辑常数赋予上意义，同时也决定能指明量化范围的论域 。其结果为，每个项都会被赋予其代表的组件，每个句子也都会被赋予上一个真值。这样，解释即对语言内的项及公式提供了语义。研究形式语言的解释的学科称为形式语义学 。
论域D 是由某种类型的“对象”所组成的非空集合。直观上来看，一阶公式是有关这些对象的叙述。例如，
∃
x
P
(
x
)
{\displaystyle \exists x P(x)}
x ，能使得指涉此对象的断言P 为真。论域即是此类考量的对象的集合，例如可取D 为整数的集合。
函数符号的解释是函数。举例来说，若论域由整数所组成，则一个2元的函数符号f 能解释为给出其参数之和的函数。换句话说，符号f 和在此解释下为加法的函数I(f) 是相关连的。
常数符号的解释是一个从单元素集合D 0 映射至D 的函数，也可简单视为是D 内的一个对象。例如，一个解释可将值
I
(
c
)
=
10
{\displaystyle I(c)=10}
c
{\displaystyle c}
n 元断言符号的解释是由论域中的元素所组成的n 对有序集。这意味着，给定一个解释、一个断言符号及论域中的n 个元素，则可依给定的解释判断这些元素的断言是否为真。例如，一个2元断言符号P 的解释I(P) 可以是一对整数，能使得第一个整数小于第二个整数。依据这个解释，断言P 在其第一个参数小于第二个参数时为真。
一阶结构 指定一个解释的最常见方法是指定一个结构 （或称做模型 ，见下文）。结构包括一个由论域及标识内的非逻辑项的解释I 所组成的非空集合。这个解释自身是个函数：
每个n 元函数符号f 都会赋予一个从
D
n
{\displaystyle D^n}
D
{\displaystyle D}
I(f) 。特别地是，每个标识内的常数符号都会被赋予论域中的一个个体。
每个n 元断言符号P 都会赋予一个在
D
n
{\displaystyle D^n}
I(P) （或等价地说，一个从
D
n
{\displaystyle D^n}
{
t
r
u
e
,
f
a
l
s
e
}
{\displaystyle \{true,false\}}
D 上的布尔值函数 所解释。 真值的赋值 一个公式由给定的解释及将论域中的元素与每个变量相关连的变量赋值 μ来决定为真或为假。需要变量赋值的原因是为了给予具自由变量的公式（如
y
=
x
{\displaystyle y = x}
x 和y 是否标记着相同的个体。
首先，变量赋值μ可以扩展到语言内的所有项，使每个项都能映射至论域中的单一元素。下列的规则被用来得到赋值：
变量 。每个变量x 皆可得到μ(x )。函数 。给定一组项
t
1
,
…
,
t
n
{\displaystyle t_1, \ldots, t_n}
d
1
,
…
,
d
n
{\displaystyle d_1, \ldots, d_n}
n 元函数符号f ，则项
f
(
t
1
,
…
,
t
n
)
{\displaystyle f(t_1, \ldots, t_n)}
(
I
(
f
)
)
(
d
1
,
…
,
d
n
)
{\displaystyle (I(f))(d_1,\ldots,d_n)}
再来，每个公式皆可赋予一个真值。用来得到赋值的递归性定义称为T-模式 。
原子公式（1） 。公式
P
(
t
1
,
…
,
t
n
)
{\displaystyle P(t_1,\ldots,t_n)}
⟨
v
1
,
…
,
v
n
⟩
∈
I
(
P
)
{\displaystyle \langle v_1,\ldots,v_n \rangle \in I(P)}
v
1
,
…
,
v
n
{\displaystyle v_1,\ldots,v_n}
t
1
,
…
,
t
n
{\displaystyle t_1,\ldots,t_n}
I
(
P
)
{\displaystyle I(P)}
P
{\displaystyle P}
原子公式（2） 。公式
t
1
=
t
2
{\displaystyle t_1 = t_2}
t
1
{\displaystyle t_1}
t
2
{\displaystyle t_2}
逻辑联结词 。
¬
ϕ
{\displaystyle \neg \phi}
ϕ
→
ψ
{\displaystyle \phi \rightarrow \psi}
真值表 （如命题逻辑一般）来赋值的。存在量化 。公式
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
M 和变量赋值μ为真，若存在一个只和μ在对x 的赋值上有所不同的变量赋值μ'，能使得φ根据解释M 和变量赋值μ'为真。此一形式定义是由“
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
x 的方法，使得φ(x )为真”的这个概念来的。全称量化 。公式
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
M 和变量赋值μ为真，若φ(x )根据每个只和μ在对x 的赋值上有所不同的变量赋值μ'及解释M 为真。此一形式定义是由“
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
x 的方法，皆能使φ(x )为真”的这个概念来的。若一个公式不包含自由变量，即为一个句子，则一开始的变量赋值不会影响其真值。换句话说，一个句子根据M 及
μ
{\displaystyle \mu}
M 及其他的变量赋值
μ
′
{\displaystyle \mu'}
还有第二种常见的做法可以定义真值，而且不需要依靠变量赋值函数。给定一个解释M ，首先将一组常数符号加至标识之中，每一个在M 中的论域的元素对应一个常数符号：称对每个域论中的元素d ，都会固定有一个常数符号c d
存在量化 。公式
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
M 为真，若存在某些在论域中的d ，使得
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
c d x 所得到的公式。全称量化 。公式
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
M 为真，若对每个论域中的d ，根据M 的
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
这个做法对所有的句子会给出和使用变量赋值的做法一样的真值。
有效性、可满足性及逻辑结论 若句子φ在一给定解释M 下为真，则称M 满足 φ，标记为
M
⊨
ϕ
{\displaystyle M \vDash \phi}
可满足的 ，若存在某个解释使其为真。
具自由变量的公式的可满足性就较为复杂了，因为只用解释并无法决定此类公式的真值。一个常见的惯例是称一个具自由变量的公式在一个解释下为可满足的，若不论如何将论域中的个体赋予其自由变量，这个公式皆为真。这等价于称公式为可从足的，当且仅当其全称闭包 为可满足的。
一个公式是逻辑有效的 （或简单称为有效的 ），若在每一个解释之下皆为真。此类的公式和命题逻辑中的重言式 扮演着相似的角色。
一个公式φ是公式ψ的逻辑结论 ，若每个使得ψ为真的解释皆会使得φ为真。在此一状况下，称φ被ψ逻辑蕴涵着。
代数化 另一种赋予一阶逻辑语义的方法可经由抽象代数 处理。这种方法是将命题逻辑的林登鲍姆-塔斯基代数 扩展而成。有如下几种类型：
这些代数 都是纯粹扩展两元素布尔代数 而成的格 。
塔斯基和葛范德于1987年证明，没有超过包在三个以上的量化内的原子句子 的部分一阶逻辑，其表示力和关系代数 相同。上述部分一阶逻辑令人十分地感到有兴趣，因为它已足够表示皮亚诺算术 和公理化集合论 ，包括典型的ZFC 。他们亦证明了，具有简单有序对 的一阶逻辑和具有两个有序的投影函数 的关系代数等价。
一阶理论、模型及基本类 一阶理论 公理 所组成的。公理所组成的集合通常是有限的或递归可枚举 的，此类的理论称为是有效的 。有些作者要求理论也要包括所有由公理导出的逻辑结论。
满足给定理论内的所有句子的一阶结构称为此理论的模型 。基本类 是由所有满足特定理论的结构所组成的集合。这些类是类型论 里的研究主题。
许多理论都有一个预期解释 ，即一个在研究理论时会在意的某种模型。例如，皮亚诺公理 的预期解释 是由一般的自然数 和其一般的运算所组成的。不过，勒文海姆–斯科伦定理证明，大多数的一阶理论也都会有其他的非标准模型 。
一个理论是兼容的 完备的 哥德尔不完备定理 证明，有效的一阶理论只要它强到足以蕴涵自然数的理论，即无法同时是兼容且完备的。
空论域 上述定义需要任何一个解释的论域均为非空集合。但在如自由逻辑 之中，设置空论域是被允许的。更甚之，若代数结构的类包含一个空结构（如空偏序集 ），当允许空论域时，这个类只能是一阶逻辑中的一个基本类，不然就要将空结构由类中移除。
不过，空论域存在着一些难点：
许多常见的推理规则只在论域被要求是非空时才为有效的。一个例子为，当x 不是
ϕ
{\displaystyle \phi \,}
ϕ
∨
∃
x
ψ
{\displaystyle \phi \lor \exists x \psi}
∃
x
(
ϕ
∨
ψ
)
{\displaystyle \exists x (\phi \lor \psi)}
前束范型 的规则在非空论域中是可靠的，但在允许空论域时则是不可靠的。
在使用变量赋值函数的解释中，真值的定义不能和空论域一起运作，因为不存在范围为空的变量赋值函数。（相似地，也无法将解释赋予上常数符号。）在甚至是原子公式的真值可被定义之前，都必须选定一个变量赋值函数。然后一个句子的真值即可在任一个变量赋值之下定义出其真值，且可证明其真值不依选定的赋值而变。这个做法在赋值函数不存在时不能运作；除非将其改成配上空论域。 因此，若空论域是被允许的，通常也必须被视成特例。不过，大多数的作家会简单地将空论域由定义中排除。
常用的定理 断言演算是命题演算 的扩展，它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统 。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件 来定义（可以有很多不同的方式），则断言演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说，断言演算采用的公理有：
来自命题演算的所有重言式（命题变量被替代为公式）。
上面给出的量词公理。
上面给出的等式公理，如果等式被认为是逻辑概念的话。 一个句子被定义为是在一阶逻辑中可证明 的，如果可以通过从断言演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。
如果我们有一个理论T （在某些语言中叫做公理的陈述的集合），则一个句子φ被定义为是在理论T 中可证明 的，如果
a ∧ b ∧ ... → φ在一阶逻辑中对于理论T 的某个公理a , b ,...的有限集合是可证明的。
可证明性的一个明显问题是它好像非常特别：我们采用了显然随机的公理和推理规则的搜集，不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理 确保这实际上不是问题：这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是，在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义（尽管在不同的可证明性的定义下证明的长度可能有巨大差别）。
有很多不同（但等价）的方式来定义可证明性。前面的演算是"希尔伯特风格 "演算的一个典型例子，它有许多不同的公理但只有非常少的推理规则。"根岑风格" 断言演算有非常少的公理但有许多推理规则。
文法上说断言演算在现存的命题演算上增加了“断言-主词结构”和量词 。主词是给定的个体群组（集合 ）的一个成员的名字，而断言 是在这个群组上的关系 ，一元断言在哲学中称为性质 ，在数学中称为指示函数 ，在数理逻辑 中称为布尔值函数 。
可证明的恒等式
¬
∀
x
P
(
x
)
⇔
∃
x
¬
P
(
x
)
{\displaystyle \neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)}
¬
∃
x
P
(
x
)
⇔
∀
x
¬
P
(
x
)
{\displaystyle \neg \exists x P(x) \Leftrightarrow \forall x \neg P(x)}
∀
x
∀
y
P
(
x
,
y
)
⇔
∀
y
∀
x
P
(
x
,
y
)
{\displaystyle \forall x \forall y P(x,y) \Leftrightarrow \forall y \forall x P(x,y)}
∃
x
∃
y
P
(
x
,
y
)
⇔
∃
y
∃
x
P
(
x
,
y
)
{\displaystyle \exists x \exists y P(x,y) \Leftrightarrow \exists y \exists x P(x,y)}
∀
x
P
(
x
)
∧
∀
x
Q
(
x
)
⇔
∀
x
(
P
(
x
)
∧
Q
(
x
)
)
{\displaystyle \forall x P(x) \land \forall x Q(x) \Leftrightarrow \forall x (P(x) \land Q(x)) }
∃
x
P
(
x
)
∨
∃
x
Q
(
x
)
⇔
∃
x
(
P
(
x
)
∨
Q
(
x
)
)
{\displaystyle \exists x P(x) \lor \exists x Q(x) \Leftrightarrow \exists x (P(x) \lor Q(x)) }
可能增加的推理规则
∃
x
∀
y
P
(
x
,
y
)
⇒
∀
y
∃
x
P
(
x
,
y
)
{\displaystyle \exists x \forall y P(x,y) \Rightarrow \forall y \exists x P(x,y)}
∀
x
P
(
x
)
∨
∀
x
Q
(
x
)
⇒
∀
x
(
P
(
x
)
∨
Q
(
x
)
)
{\displaystyle \forall x P(x) \lor \forall x Q(x) \Rightarrow \forall x (P(x) \lor Q(x)) }
∃
x
(
P
(
x
)
∧
Q
(
x
)
)
⇒
∃
x
P
(
x
)
∧
∃
x
Q
(
x
)
{\displaystyle \exists x (P(x) \land Q(x)) \Rightarrow \exists x P(x) \land \exists x Q(x)}
∃
x
P
(
x
)
∧
∀
x
Q
(
x
)
⇒
∃
x
(
P
(
x
)
∧
Q
(
x
)
)
{\displaystyle \exists x P(x) \land \forall x Q(x) \Rightarrow \exists x (P(x) \land Q(x)) }
一阶逻辑的元定理 下面列出了一些重要的元逻辑定理。
不像命题演算 ，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程 ，判定P是否有效，（参见停机问题 ）。（结论独立的来自于邱奇 和图灵 。）
有效性 的判定问题是半可判定的。按哥德尔完备性定理 所展示的，对于任何有效的 公式P, P是可证明的。一元断言逻辑 （就是说，断言只有一个参数的断言逻辑）是可判定的。转换自然语言到一阶逻辑 用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，
p
∨
q
{\displaystyle p \lor q}
[5]
一阶逻辑的限制 所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。
难于表达if-then-else 带有等式的FOL不包含或允许定义if-then-else断言或函数if（c,a,b），这里的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，断言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数电脑程序的基础。
在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。[6]
(
c
∧
a
)
∨
(
¬
c
∧
b
)
{\displaystyle (c \wedge a) \lor (\neg c \wedge b)}
[7]
类型（种类） 除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。
某些人争辩说缺乏类型是巨大优点
[8] [9]
单一参数断言可以用来在合适的地方实现类型的概念。例如：
∀
x
(
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
)
{\displaystyle \forall x (Man(x) \rightarrow Mortal(x))}
断言Man(x)可以被认为是一类“类型断言”（就是说，x必须是男人）。
断言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：
∃
x
(
M
a
n
(
x
)
∧
M
o
r
t
a
l
(
x
)
)
{\displaystyle \exists x (Man(x) \wedge Mortal(x))}
容易写成
∃
x
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
{\displaystyle \exists x Man(x) \rightarrow Mortal(x)}
∃
x
¬
M
a
n
(
x
)
∨
∃
x
M
o
r
t
a
l
(
x
)
{\displaystyle \exists x \neg Man(x) \lor \exists x Mortal(x)}
∀
x
(
M
a
n
(
x
)
→
M
a
m
m
a
l
(
x
)
)
{\displaystyle \forall x (Man(x) \rightarrow Mammal(x))}
难于刻画模型大小 从Löwenheim–Skolem定理 得出在一阶逻辑中不可能刻画有限性或可数性。若一阶理论有任意大的模型，则也有无穷大的模型，所以说不能刻划有限性。[10] :1 而若理论有某个无穷基数大小的模型，则也必有任意更大的模型，所以不能刻划可数性。[11] :45 另一个例子，是无法用一阶语言将实数系 公理化，因为不论用何种一阶理论描述，既然该理论有实数系此种无穷模型（大小为
2
ℵ
0
{\displaystyle 2^{\aleph_0}}
2
2
ℵ
0
{\displaystyle 2^{2^{\aleph_0}}}
上确界 性质一项，它声称实数的所有有界的、非空集合都有上确界 。一阶逻辑祗能对元素量化，但此公理中，要对模型的全部子集量化，这就需要二阶逻辑 了。[12] :30
图可及性不能表达 很多情况可以被建模为节点和有向连接（边）的图 。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用断言逻辑完全表达。换句话说，没有断言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）断言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。[13]
参考文献 引用
↑ Mendelson, Elliott. Introduction to Mathematical Logic. Van Nostrand Reinhold. 1964: 56. ↑ Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.48 ISBN 978-1482237726
↑ Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.29 ISBN 978-1482237726
↑ Stephen Cole Kleene Introduction to Metamathematics , p.252 ISBN 978-0923891572
↑ Suber, Peter, Translation Tips , [2007-09-20 ] ↑ Otter Example if.in , [2007-09-21 ] ↑
Manna, Zohar, Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company: 77–147, 1974, ISBN 0-07-039910-7
↑ Leslie Lamport, Lawrence C. Paulson.
Should Your Specification Language Be Typed?
ACM Transactions on Programming Languages and Systems.
1998.
http://citeseer.ist.psu.edu/71125.html
↑ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
↑ Mahesh Viswanathan. Finite Model Theory (PDF) . ↑ David Marker. Model Theory: An Introduction. Graduate Texts in Mathematics 217 . Springer. 2002. ↑ Johnstone, P. T. Notes on logic and set theory. Cambridge University Press . 1987. doi:10.1017/CBO9781139172066 ↑
Huth, Michael; Ryan, Mark, Logic in Computer Science, 2nd edition: 138–139, 2004, ISBN 0-521-54310-X
来源 外部链接 参见
背景
分主题
应用
相关主题
人物
关键的语义网组织
标准
语法及支持技术
模式、本体和规则
语义标注
公共词表
