一阶逻辑

一阶逻辑是使用于数学、哲学、语言学及计算机科学中的一种形式系统，也可以称为：一阶断言演算、低端断言演算、量化理论或谓词逻辑。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑包含量词。

高阶逻辑和一阶逻辑不同之处在于，高阶逻辑的断言符号可以有断言符号或函数符号当做引数，且容许断言量词或函数量词。在一阶逻辑的语义中，断言被解释为关系。而高阶逻辑的语义里，断言则会被解释为集合的集合。

在通常的语义下，一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）的。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。

一阶逻辑是数学基础中很重要的一部分。许多常见的公理系统，如一阶皮亚诺公理、冯诺依曼-博内斯-哥德尔集合论和策梅洛-弗兰克尔集合论都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数大小，因根据勒文海姆–斯科伦定理和康托尔定理，可以构造出一种“病态”集合论模型，使整个模型可数，但模型内却会觉得自己有“不可数集”。类似地，可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为斯科伦悖论。但一阶的直觉主义逻辑里，勒文海姆–斯科伦定理不可证明，故不会有以上之现象。

简介

基本符号

命题逻辑顾名思义，会将“苏格拉底是哲学家”、“帕雷托是哲学家”之类直观上有真有假的叙述简记为 $p$ 及 $q$ （也就是有真有假的命题），然后讨论 $\neg p$（非p）、$p\Rightarrow q$（若p则q）、$p\wedge q$（p且q）与$p\vee q$（p或q）之间的推理关系。

但一阶逻辑尝试从一些比较基础的词汇去建构“句子”，比如说，可用符号 ${\text{Phil}}(x)$ 代表 “ x 是哲学家”，也就是赋予断言符号“${\text{Phil}}(x)$ ”语义的解释。这个解释默认一个“所有人类的群体”（也就是下面标准语义一节会说到的论域），并将变量 $x$ 对应为自群体中取出来的某人。

以此类推，断言符号可以包含一个以上的变量。例如：可以将 ${\text{Cp}}(x,\,y)$ 解释为“ x 与 y 是夫妻”。

一阶逻辑类似于命题逻辑，可以将断言符号与 $\neg$（非）、$\Rightarrow$（则）、$\wedge$（且）和 $\vee$（或）组成更复杂的叙述，例如：把断言符号 ${\text{Schol}}(x)$ 解释成“ $x$ 是学者”，那“若 x 为哲学家，则 x 为学者”可表示为：

${\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)\,$

但相较之下，一阶逻辑又加入了描述“所有”与“存在”的量词，比如说“对所有 x ，若 x 为哲学家，则 x 为学者”可记为：

$\forall x[{\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)]$

也就是自左方开始阅读，将 $\forall x$ 解释成“对所有 x 有…”。$\forall$ 这个符号被称为全称量词。

而对于“有 x 是哲学家”这一叙述，一阶逻辑则引入另一种量词：

$\exists x[{\text{Phil}}(x)]$

也就是自左方开始阅读，将 $\exists x$ 解释成“存在 $x$ 使…”。$\exists$ 这个符号被称为存在量词。

顺带一提“并非所有 x 不是哲学家”等价于“有 x 是哲学家”；且“不存在 x 不是学者”也等价于“所有的 x 是学者”。所以可以用“否定”和“全称量词”来组合出“存在量词”。换句话说，可作以下的符号定义（${\mathcal {A}}$ 代表一段“叙述”）：

$\exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]$

相等

一阶逻辑也考虑到“相等”这个概念在叙述中的重要性，例如想表达“若所有$x$是哲学家，那$x$的长子也会是哲学家”，可先把 ${\text{Son}}(x)$ 解释为 “ x 的长子”，那么这段叙述可记为：

$\forall x{\text{Phil}}(x)\Rightarrow {\text{Phil}}[{\text{Son}}(x)]$

换句话说，${\text{Son}}(x)$ 被解释成“与 $x$ 有特定且唯一对应关系”的某对象（被称为函数符号）。换句话话说，只要“$x$就是$y$”，那“$x$的长子也会是$y$的长子”。换句话说：

$(x=y)\Rightarrow [{\text{Son}}(x)={\text{Son}}(y)]$

这些性质被一阶逻辑视为“理所当然”。

类似地，叙述中也有一些“不变的实体”，如苏格拉底，表示这些“实体”的符号被称为常数符号。例如将 $s$ 解释为苏格拉底，那“苏格拉底为哲学家”就可以写成：

${\text{Phil}}(s)$

所谓的“不变”隐含的代表：

“苏格拉底就是苏格拉底”

“对所有x，对所有y，如果x就是苏格拉底，且y就是苏格拉底，那x就是y”

换句话说

$(s=s)$

$\forall x\forall y\{[(x=s)\wedge (y=s)]\Rightarrow (x=y)\}$

这两个性质也被一阶逻辑视为“理所当然”。

形式理论

一阶逻辑的形式理论可分成几个部分：

1. 语法：决定哪些符号组合是合式公式。（直观上的“文法无误的叙述”）
2. 推理规则：由合式公式符号组合出新合式公式的规则（直观上的“推理”）
3. 公理：一套合式公式（直观上的基本假设）

基本符号

一套理论能容许多少符号，取决于人类能运用物理定律来塑造多少符号，但目前无法确知宇宙是不是有限，或是以可无限制地分割。虽然所有的公理化集合论都以量词的形式隐晦的承认跟自然数一样多的无穷（如ZF集合论的无穷公理），甚至以这样的可数无穷为基础，去建构出不可数的实数，但将抽象的理论对应到现实时，还是需要回答物理上有没有可数或不可数的无穷。所以谨慎起见，如果没有特别申明的话，以下各种类符号的数目上限都是有限的。

逻辑符号

一阶逻辑通常拥有以下的符号：

1. 量化符号 $\forall$ 及 $\exists$
   • 某些作者会把 $\exists$ 符号定义为 $\exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]$，如此便只需要 $\forall$ 做为基础符号。
2. 逻辑联结词：以下为可能的表示符号（关于波兰表示法下的逻辑连接词，请参见逻辑运算的波兰记法）：
   • 否定： $\neg$ 或 $\sim$ 或－
   • 条件：$\Rightarrow$ 或 $\rightarrow$ 或 $\supset$
   • 且：$\land$ 或 $\&$
   • 或：$\lor$ 或 ||
   • 双条件：$\Leftrightarrow$ 或 $\leftrightarrow$
   • 某些作者会作如下的符号定义：

   ${\mathcal {A}}\wedge {\mathcal {B}}:=\neg ({\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})),$

   ${\mathcal {A}}\vee {\mathcal {B}}:=(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}},$

   ${\mathcal {A}}\Leftrightarrow {\mathcal {B}}:=({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}}),$

   如此一来只需要否定和条件做为基础符号。

3. 标点符号：括号、逗号及其他，依作者的喜好有所不同。
   • 为了更有效的将括号做配对，通常还会采用大括号{ }跟中括号[ ]。
4. 至多跟自然数一样多的变量，通常标记为英文字母末端的小写字母x、y、z、…，也常会使用下标（或上标、上下标兼有）来区别不同的变量：x₀、x₁、x₂、…（特别注意c有时候会被当成常数符号而引起混淆）。
5. 等式符号：$=$
   • 有作者会因为语义上对“相等”的不同解释，而将等式符号视为双元断言符号、甚至是某种合式公式的简写。
6. 符号相等：$\asymp$
   • 某些作者会额外采用这个符号来表示符号识别上的等同以便与等式符号作区别。

并非所有的符号都不可或缺的，像谢费尔竖线“$|$”（或异或）可以用来定义量词以外的所有逻辑符号，换句话说：

符号定义 — 
$(\neg {\mathcal {A}}):=({\mathcal {A}}|{\mathcal {A}})$

$({\mathcal {A}}\Rightarrow {\mathcal {B}}):={\mathcal {A}}|({\mathcal {B}}|{\mathcal {B}})$

$({\mathcal {A}}\wedge {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {B}})|({\mathcal {A}}|{\mathcal {B}})\,]$

$({\mathcal {A}}\vee {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {A}})|({\mathcal {B}}|{\mathcal {B}})\,]$

另外，一些作者不区分语义解释和形式理论，所以会将表示真值的符号纳入形式理论里，也就是说，用 T 、Vpq 或 $\top$ 来表示“真”，并用 F 、 Opq 或 $\bot$ 来表示“假”。

断言符号

“他们两人是夫妻”，是一个关于两个“对象”的断言，而“他是人”、“三点共线”则表明断言容许一个或者多个对象。所以对于自然数 $n$ 、$j$ 约定：

$A_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})$

为一阶逻辑的合法词汇。它在直观上表示一个有 $n$ 个“对象”的断言，称为 $n$ 元断言符号。下标的自然数 $j$ 只是拿来和其他同为 $n$ 元的断言符号作区别。

实用上只要有申明，不至于和其他词汇引起混淆的话，可以用任意的形式简写一个断言符号。如：公理化集合论里的双元断言符号 $A_{1}^{2}(x,\,y)$ 也可以表示为 $x\in y$ 。

函数符号

“物体的颜色”、“夫妻的长子”这种断言说明了一组对象所唯一对应的对象。但不同的夫妻有不同的长子；不同的物体有不同的颜色。据此，形式上对于自然数 $n$ 、$j$ 约定：

$f_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})$

为一阶逻辑的合法词汇，直观上表示 $n$ 个“对象”所对应到的东西，称它为 $n$ 元函数符号。需要特别注意，这种“唯一对应”的直观想法，必须配上关于“等式”的性质（详见下面的等式定理章节），才能在形式理论中被实现。

与断言符号一样，只要不引起混淆，就可以用任何的形式简写函数符号。如：公理化集合论里的 $x\cup y$ 是依据并集公理而定义的新函数符号（请参见下面函数符号与唯一性章节），也可以冗长的表记为 $f_{j}^{2}(x,\,y)$ 。

常数符号

“刻度0”、“原点”、“苏格拉底”是直观上＂唯一不变＂的对象。据此，对自然数 $j$ 约定

$c_{j}$

为一阶逻辑的合法词汇，直观上表示一个“唯一不变”的对象，称为常数符号。同样的。“常数的不变性”需配上等式的性质（详见下面等式定理）才能被实现。

为了不和变量的表记混淆，常数符号一样可以用任何的形式简写，如公理化集合论里的 $\varnothing$ 是根据空集公理和函数符号与唯一性，而定义的新常数符号。亦可冗长的表示为 $c_{j}$ 。

语法

和自然语言（如英语）不同，一阶逻辑的语言以明确的递归定义判断一个给定的词汇是否合法。大致上来说，一阶逻辑以“项”代表讨论的对象，而对“项”的断言组成了最基本的原子（合式）公式；而原子公式和逻辑符号组成了更复杂的合式公式（也就是“叙述”）。

项

“那对夫妻的长子的职业”、“$(x+y)\times z$”、“$x\cup \varnothing$”代表变量可以与函数符号组成更一般的对象。据此形式，递归地规定一类合法词汇——项为：

递归定义 — 

1. 变量和常数是项。
2. 若 $T_{1},\,....,\,T_{n}$ 全都是项，那么 $f_{j}^{n}(T_{1},\,....,\,T_{n})$ 也是项。
3. 项只能通过以上两点，于有限步骤内置构出来。

习惯上以大写的西方字母（如英文字母、希伯来字母、希腊字母）代表项，如果变量不得不采用大写字母，而可能跟项引起混淆的话，需额外规定分辨的办法。

原子公式

为了比较简洁地规定什么是合式公式，先规定原子公式为：（若 $T_{1},\,....,\,T_{n}$ 是项）

$A_{j}^{n}(T_{1},\,....,\,T_{n})$

这样的形式。

公式

一阶逻辑的合式公式（简称公式或 $wf$ ）以下面的规则递归地定义：

递归定义 — 

1. 原子公式为公式。（美观起见，在原子公式外面包一层括弧也是公式）
2. 若 ${\mathcal {A}}$ 为公式，则 $(\neg {\mathcal {A}})$ 为公式。
3. 若 ${\mathcal {A}}$ 与 ${\mathcal {B}}$ 为公式，则 $({\mathcal {A}}\Rightarrow {\mathcal {B}})$ 为公式。
4. 若 ${\mathcal {A}}$ 为公式， $x$ 为任意变量，则 $(\forall x{\mathcal {A}})$ 为公式。 （美观起见 $(\forall x){\mathcal {A}}:=\forall x{\mathcal {A}}$，也就是里面的量词有无外包括弧都是公式）
5. 合式公式只能通过以上四点，于有限步骤内置构出来。

另外成对的中括弧跟大括弧，符号识别上视为成对的小括弧，而草书的大写西方字母为公式的代号。

举例来说，

$\{(\forall y)A_{1}^{2}[x,\,f_{1}^{1}(y)]\}$

是公式而

$\forall x\,x\Rightarrow$

则不是公式。

而接下来只要对任意公式${\mathcal {A}}$ 、 ${\mathcal {B}}$ 与变量 $x$，做以下符号定义

符号定义 — 
$({\mathcal {A}}\wedge {\mathcal {B}}):=\{\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]\}$

$({\mathcal {A}}\vee {\mathcal {B}}):=[(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]$

$({\mathcal {A}}\Leftrightarrow {\mathcal {B}}):=[({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}})]$

$(\exists x{\mathcal {A}}):=\{\neg [\forall x(\neg {\mathcal {A}})]\}$ （同样美观起见 $(\exists x){\mathcal {A}}:=\exists x{\mathcal {A}}$）

这样所有的逻辑连接词与量词就纳入了合式公式的规范。

施用

所谓的施用/作用，是以下公式形式的口语说法：（其中 ${\mathcal {A}}$ 与 ${\mathcal {B}}$ 都是公式）

• $(\neg {\mathcal {A}})$ 称为 $\neg$ 施用于 ${\mathcal {A}}$ 上。
• $({\mathcal {A}}\Rightarrow {\mathcal {B}})$ 称为 $\Rightarrow$ 施用于 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
• $({\mathcal {A}}\wedge {\mathcal {B}})$ 称为 $\wedge$ 施用于 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
• $({\mathcal {A}}\vee {\mathcal {B}})$ 称为 $\vee$ 施用于 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
• $({\mathcal {A}}\Leftrightarrow {\mathcal {B}})$ 称为 $\Leftrightarrow$ 施用于 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
• $(\forall x{\mathcal {A}})$ 称为 $\forall x$ 施用于 ${\mathcal {A}}$ 上。
• $(\exists x{\mathcal {A}})$ 称为 $\exists x$ 施用于 ${\mathcal {A}}$ 上。

就类似于运算符作用在它们身上。

自由变量和约束变量

量词所施用的公式被称为量词的范围（scope）。同一个变量在公式一般来说不只出现一次，若变量 $x$ 出现在 $\forall x$ 的范围内，称这样出现的 $x$ 为不自由/被约束的 $x$ （not free/bounded）；反过来说，不出现在 $\forall x$ 的范围内的某个 $x$ 被称为自由的 $x$。

例如，对于公式：

$\{(\forall x)[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]\}$

$[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]$ 就是量词 $\forall x$ 的范围；而 $A_{1}^{1}(x)$ 里的 $x$ 就是不自由的；反之 $A_{2}^{1}(y)$ 里的 $y$ 就是自由的。

说 $x$ 于公式 ${\mathcal {A}}$ 完全自由，意为于 ${\mathcal {A}}$ 出现的 $x$ 都是自由的；反之，说 $x$ 于公式 ${\mathcal {A}}$ 完全不自由/完全被约束，意为 ${\mathcal {A}}$ 内根本没有 $x$ ，或是 ${\mathcal {A}}$ 内没有自由的 $x$ 。若 ${\mathcal {A}}$ 内所有的变量都完全不自由，${\mathcal {A}}$ 特称为封闭公式/句子（closed formula/sentence）。

括弧的简写

括弧是为了保证语义解释符合预期，但太多的括弧书写不易，为此规定以下的“重构法”（反过来就是“简写法”），从表面上不合法的一串符号找出作者原来想表达的公式：

• 若整串符号的括弧不成对，直接视为无法重构。
• 以$\lnot ,\,\land ,\,\lor ,\,\forall ,\,\exists ,\,\Rightarrow ,\,\Leftrightarrow$（左至右）的施用顺序重构括弧。
• 相邻的逻辑连接词或量词无法决定施用顺序的话，以右边为先。
• 重构施用的顺序，以被成对括弧包住的部分为优先施用，其次才是落单的断言符号。

举例来说

$\lnot [\forall xA_{1}^{1}(x)]\Rightarrow \exists x\lnot A_{2}^{1}(x)$

的重构过程如下

1. $\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)]$ （优先施用 $\lnot$）
2. $\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}$ （施用 $\exists$）
3. $\{\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}\}$ （最后施用 $\Rightarrow$）

可以被重构为公式的一串符号则宽松的认定为“合式公式”。（最明显的例子就是合式公式最外层的括弧可以省略）

波兰表示法

波兰表示法将逻辑连接词前置于被施用的公式而非传统的中间。如果沿用以上的＂施用顺序＂，这个表示法允许舍弃所有括弧。如公式

$\forall x\forall y\{A_{1}^{1}[f_{1}^{1}(x)]\Rightarrow \neg \{A_{1}^{1}(x)\Rightarrow A_{1}^{3}[f_{1}^{1}(y),x,z]\}\}$

转成波兰表示法的过程如下

$\forall x\forall y\Rightarrow A_{1}^{1}f_{1}^{1}x\neg \Rightarrow A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz$ （转成波兰表示法的顺序）

$\Pi x\Pi y{\text{C}}A_{1}^{1}f_{1}^{1}x{\text{N}}{\text{C}}A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz$ （逻辑链接词的符号变换）

推理规则

一阶逻辑通常只有以下的推理规则（因为将普遍化视为推理规则会有不直观的限制）

MP律 — 对于公式 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 有

${\mathcal {A}}\Rightarrow {\mathcal {B}}$ 和 ${\mathcal {A}}$ 组合出 ${\mathcal {B}}$。

直观意义非常明显，就是p=>q且p可以推出q。

在只以谢费尔竖线“$|$”为基础逻辑连接词的公理系统里，MP律会被改写成

修改的MP律 — 对于公式 ${\mathcal {A}}$ 、${\mathcal {B}}$ 和 ${\mathcal {C}}$ 有 ${\mathcal {A}}|({\mathcal {C}}|{\mathcal {B}})$ 和 ${\mathcal {A}}$ 组合出 ${\mathcal {B}}$。

公理

逻辑公理

公理 — 如果${\mathcal {B}}$、${\mathcal {C}}$、${\mathcal {D}}$都是公式，则：

• （A1） ${\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})$
• （A2） $[{\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {D}})]\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {D}})]$
• （A3） $[(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})]\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow {\mathcal {B}}]$

都是公理。

它们实际上是公理模式，代表着“跟自然数一样多”条的公理。

在有（A1）与（A2）的前提下，（A3）等价于以下的公理模式：（证明请参见下面否定一节。）

（T1） — $[\,(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})\,]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$

另外，在只以谢费尔竖线“$|$”为基础逻辑连接词的公理系统里，上面三条公理模式等价于下面这条公理模式：

公理 — 如果 ${\mathcal {B}}$、${\mathcal {C}}$、${\mathcal {D}}$ 、${\mathcal {E}}$ 和 ${\mathcal {F}}$ 都是公式，则：

• $[\,{\mathcal {B}}|({\mathcal {C}}|{\mathcal {D}})\,]|{\big \{}\,[\,{\mathcal {E}}|({\mathcal {E}}|{\mathcal {E}})\,]|\{\,({\mathcal {F}}|{\mathcal {C}})|[\,({\mathcal {B}}|{\mathcal {F}})|({\mathcal {B}}|{\mathcal {F}})\,]\,\}\,{\big \}}$

都是公理。

量词公理

公理 — $x$ 为任意变量， ${\mathcal {B}}$ 、 ${\mathcal {C}}$ 为任意公式，则

• （A4） $T$ 是一个项， $t$ 为 $T$ 中出现的任意变量；若 ${\mathcal {B}}$ 里，自由的 $x$ 都不在 $\forall t$ 的范围里（这样取代成 $T$ 时才不会被 $\forall t$ 约束），则

$(\forall x){\mathcal {B}}\Rightarrow {\mathcal {B}}(T)$

为公理

其中 ${\mathcal {B}}(T)$ 代表把 ${\mathcal {B}}$ 里自由的 $x$ 都替换成 $T$ 所得到的新公式。

• （A5）如果 $x$ 在 ${\mathcal {B}}$ 里完全被约束，则

$[(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [{\mathcal {B}}\Rightarrow (\forall x{\mathcal {C}})]$

为公理

• （A6） $[(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [(\forall x{\mathcal {B}})\Rightarrow (\forall x{\mathcal {C}})]$ 为公理
• （A7） 若 ${\mathcal {B}}$ 是公理， $x$ 是任意变量，则

$(\forall x){\mathcal {B}}$

也是公理。

它们实际上也是公理模式。

等式和它的公理

根据不同作者的看法，甚至是理论本身的需求，“等式”在形式理论里可能是断言符号或是一段公式（如 a 等于 b 可定义为对所有的 x ， x 属于 a 等价于 x 属于 b ）。而如何刻划直观上“等式的性质”，有一开始就将“等式的性质”视为公理（模式），但也有视为元定理的另一套处理方法，以下暂且以公理模式的方式处理。以元定理处理的方法会在等式定理详述。

公理 — $(x=y)$ 是一段变量 $x$ 、 $y$ 完全自由，且型式完全被确定的公式 ${\mathcal {E}}(x,\,y)$ 的简写。要求：

• （E1） $(\forall x)(x=x)$ 为公理。
• （E2） 若在公式 ${\mathcal {A}}$ 中自由的 $x$ 都不在 $\forall y$ 的范围内，以${\mathcal {A}}_{y}$ 代表 ${\mathcal {A}}$ 某些（而非全部）自由的 $x$ 被取代成 $y$ 而成的新公式，则

$(\forall x)(\forall y)[(x=y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})]$

为公理。

事实上这两个公理模式也确保了函数符号“唯一对应”和常数符号的“唯一性”，但证明这些性质需要一些元定理，简便起见合并于下面的等式定理一节讲述。

标准语义

一阶逻辑的标准语义源于波兰逻辑学家阿尔弗雷德·塔斯基所著《On the Concept of Truth in Formal Languages》。根据上面语法一节，公式是由原子公式递归地添加逻辑链接词而来的，而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确，就要规定项的取值，然后检验这样的取值会不会落在断言符号所对应的关系里。由此延伸出所有公式的“真假值“。

也就是一套一阶逻辑的语义解释，要包含

1. 变量取值的论域
2. 如何解释函数符号（为论域中的某个函数）与常数符号（为论域中的某特定元素），以便从特定的变量取值得出项的取值。
3. 如何将断言符号与论域里的某关系做对应。

通常一套解释方法（简称为解释）会以代号 $M$ 表示。

项的取值

量词的解释需要指明变量取值范围的论域——也就是一个集合 $D$ 。而变量可能跟自然数一样多，换句话说，所有变量在论域 $D$ 取的值可以依序以自然数标下标——也就是一个在 $D$ 取值的数列。如果以 $x_{1},\,x_{2},\,x_{3},\,\cdots$ 的代号（不一定是变量本身的表示符号）来枚举变量，那么从 $D$ 的某套变量取值就以

$\left\langle a_{k}\right\rangle _{k\in \mathbb {N} }$

或较直观的符号

$\left\langle a_{1},\,a_{2},\,a_{3},\,\cdots \right\rangle$

来表示。

一套解释 $M$ 会将 $n$ 元函数符号 $f_{i}^{n}$ 解释成某个 ${(f_{i}^{n})}^{M}:D^{n}\to D$ 的 $n$ 元函数；而常数符号 $c_{l}$ 解释成特定的 ${c_{l}}^{M}\in D$ （亦称为 $c_{l}$ 的取值为 ${c_{l}}^{M}$），这样就可以用上面语法一节定义项的方式，递归地规定项的取值：

元定义 — 在解释 $M$ 下的某套变量取值下，一列项 $T_{1},\,\cdots ,\,T_{n}$ 的取值分别为 ${T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M}$，则这套变量取值下，项 $f_{i}^{n}(T_{1},\,\cdots ,\,T_{n})$ 的取值规定为

${(f_{i}^{n})}^{M}({T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M})$

真假的赋值

直观上要解释关系最直接的方法，就是枚举所有符合关系的对象；例如如果想说明夫妻关系，可以枚举所有（老公, 老婆）的双元有序对，但并非所有的人类有序对都会在这个关系中。

以此为基础，若以 $D^{m}$ 代表所有以 $m$ 个 $D$ 中的元素构成的 $m$ 元有序对的集合（也就是 $m$ 元笛卡尔积） ，那一套解释 $M$ 会将 $m$ 元断言符号 $A_{j}^{m}$ 解释为一个

${(A_{j}^{m})}^{M}\subseteq D^{m}$

的$m$ 元有序对子集合。

这样就可以依据语法的递归定义，以下面的规则对每条公式赋予真值。（这种赋值方式称为T-模式，取名于逻辑学家阿尔弗雷德·塔斯基）

元定义 — 在一套解释 $M$ 下：

• 在一套特定的变量取值下，一列项 $T_{1},\,\cdots ,\,T_{m}$ 的取值为 ${T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M}$ ，那 $A_{j}^{m}(T_{1},\,\cdots ,\,T_{m})$ 为真定义为

$({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\in {(A_{j}^{m})}^{M}$

反之

$({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\notin {(A_{j}^{m})}^{M}$

则定义为假。

• 在一套特定的变量取值下，“$(\neg {\mathcal {B}})$ 为真” 等价于 “${\mathcal {B}}$ 为假”。
• 在一套特定的变量取值下，$({\mathcal {B}}\Rightarrow {\mathcal {C}})$ 为真，意为“ ${\mathcal {B}}$ 为假或是 ${\mathcal {C}}$ 为真。” （p=>q为假只有p为真且q为假的状况）
• 在变量取值 $\left\langle a_{k}\right\rangle _{k\in \mathbb {N} }$ 下，$(\forall x_{i}{\mathcal {B}})$ 为真，意为“对所有的 $d\in D$ ， ${\mathcal {B}}$ 于变量取值 $\left\langle a_{1},\,\cdots ,\,a_{i-1},\,d,\,a_{i+1},\,\cdots \right\rangle$ 下为真”。（也就是把变量 $x_{i}$ 的取值换为论域的任意元素仍然为真）

更进一步的来说

元定义 — #在一套解释 $M$ 下，不管怎么样的变量取值，公式 ${\mathcal {B}}$ 都为真，则称为 $M$ 下 ${\mathcal {B}}$ 为真，以符号 $M\vDash {\mathcal {B}}$ 简记。若没有变量取值可以满足 ${\mathcal {B}}$ ，则称 $M$ 下 ${\mathcal {B}}$ 为假。

1. 若任意解释下公式 ${\mathcal {B}}$ 都为真，称 ${\mathcal {B}}$ 为逻辑有效的（logically valid） （类似于命题逻辑的恒真式）
2. 若一阶逻辑理论 ${\mathcal {L}}$ 的公理都于 $M$ 为真，称解释 $M$ 为 ${\mathcal {L}}$ 之模型（model）

代数化语义

另一种一阶逻辑语义的方法可经由命题逻辑的林登鲍姆-塔斯基代数扩展而成。有如下几种类型：

• 圆柱代数，由阿尔弗雷德·塔斯基和其同事提出；
• 多元代数，由保罗·哈尔莫斯提出。
• 断言函子逻辑，主要是基于威拉德·范·奥曼·奎因的工作成果。

这些代数都是纯粹扩展两元素布尔代数而成的格。

塔斯基和葛范德于1987年证明，没有超过包在三个以上的量化内的原子句子的部分一阶逻辑，其表示力和关系代数相同。上述部分一阶逻辑令人十分地感到有兴趣，因为它已足够表示皮亚诺算术和公理化集合论，包括典型的ZFC。他们亦证明了，具有简单有序对的一阶逻辑和具有两个有序的投影函数的关系代数等价。

空论域

主条目：空论域

上述的语义解释都要求论域为非空集合。但在如自由逻辑之中，设置空论域是被允许的。甚至代数结构的类包含一个空结构（如空偏序集），当允许空论域时，这个类只能是一阶逻辑中的一个基本类，不然就要将空结构由类中移除。

不过，空论域存在着一些难点：

• 许多常见的推理规则只在论域被要求是非空时才为有效的。一个例子为，当x不是$\phi \,$内的自由变量时，$\phi \lor \exists x\psi$会蕰涵$\exists x(\phi \lor \psi )$。这个用来将公式写成前束范型的规则在非空论域中是可靠的，但在允许空论域时则是不可靠的。
• 在使用变量赋值函数的解释中，真值的定义不能和空论域一起运作，因为不存在范围为空的变量赋值函数。（相似地，也无法将解释赋予上常数符号。）在甚至是原子公式的真值可被定义之前，都必须选定一个变量赋值函数。然后一个句子的真值即可在任一个变量赋值之下定义出其真值，且可证明其真值不依选定的赋值而变。这个做法在赋值函数不存在时不能运作；除非将其改成配上空论域。

因此，若空论域是被允许的，通常也必须被视成特例。不过，大多数的作家会简单地将空论域由定义中排除。

常用的推理性质

定理与证明

以下介绍一些基本用语和符号

元定义 — 在一阶逻辑理论 ${\mathcal {L}}$ 下， $\vdash _{\mathcal {L}}{\mathcal {A}}$ 代表有一列公式 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 满足：

1. ${\mathcal {C}}_{n}$ 符号识别上为 ${\mathcal {A}}$。
2. 所有的 ${\mathcal {C}}_{k}$有下列两种可能情况

• ${\mathcal {C}}_{k}$ 为 ${\mathcal {L}}$ 的公理。
• 存在 $i,\,j<k$使得 ${\mathcal {C}}_{i}$ 为 $({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k})$ （也就是由前面的公式以MP律组合出来）

口语上会称公式 ${\mathcal {A}}$ （或 $\vdash _{\mathcal {L}}{\mathcal {A}}$ ） 为 ${\mathcal {L}}$ 下的定理（theorem）。而这列${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 会称为$\vdash _{\mathcal {L}}{\mathcal {A}}$ 的证明。

例如定理$(I)$ $\vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {B}}$ 的证明：

证明 — 

${\mathcal {C}}_{1}$：$\{{\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}})\}$ （公理A2）

${\mathcal {C}}_{2}$：${\mathcal {B}}\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]$ （公理A1）

${\mathcal {C}}_{3}$：${\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})$ （公理A1）

${\mathcal {C}}_{4}$：$[{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})$ （${\mathcal {C}}_{1}$和${\mathcal {C}}_{2}$加上MP律）

${\mathcal {C}}_{5}$：${\mathcal {B}}\Rightarrow {\mathcal {B}}$ （${\mathcal {C}}_{4}$和${\mathcal {C}}_{3}$加上MP律）

以上其实是蕴含了无限多定理的元定理的证明(因为没有给出合式公式的明确形式)。方便起见，这种元定理还是会称为定理并以同样的形式来表达。

直观上的证明，总是会有一些“前提假设”，对此，若以 $\Gamma$ 代表一列有限数目的公式，那

元定义 — $\Gamma \vdash _{\mathcal {L}}{\mathcal {A}}$ 代表有一列公式 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 满足：

1. ${\mathcal {C}}_{n}$ 符号识别上为 ${\mathcal {A}}$。
2. 所有的 ${\mathcal {C}}_{k}$ 有下列三种可能情况

• ${\mathcal {C}}_{k}$ 为 ${\mathcal {L}}$ 的公理。
• ${\mathcal {C}}_{k}$ 为 $\Gamma$ 中的其中一条公式。
• 存在 $i,\,j<k$使得 ${\mathcal {C}}_{i}$ 为 $({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k})$ （也就是由前面的公式以MP律组合出来）

这样称 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 为在前提 $\Gamma$ 下， ${\mathcal {A}}$ 的证明；或是说 ${\mathcal {A}}$ 是 $\Gamma$ 的推论结果。

若要特别凸显 $\Gamma$ 里的一条＂前提条件＂ ${\mathcal {B}}$ 对＂证明过程＂的重要性，可以用 $\Gamma ,\,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {A}}$ 的符号去特别凸显。若 $\Gamma$ 里的公式枚举出来有 ${\mathcal {B}}_{1},...,{\mathcal {B}}_{n}$ ，那亦可表示为

${\mathcal {B}}_{1},...,{\mathcal {B}}_{n}\vdash _{\mathcal {L}}{\mathcal {A}}$

证明过程没有被引用的公式尽可能不写出来。另一方面从以上对于证明定义可以发现，依怎样的顺序枚举前提条件，对于证明本身是不会有任何影响的。

本节所介绍的符号，在引用哪个理论很显然的情况下，$\vdash _{\mathcal {L}}$ 的下标${\mathcal {L}}$ 可以省略。

实际的证明常常会＂引用＂别的（元）定理，严格来说，就是照抄（元）定理的证明过程，然后作一些修改使符号一致。为了节省证明的篇幅，引用时只会单单列出配合引用（元）定理所得出的公式（形式），并在后面注明引用的（元）定理代号。

演绎元定理

从公理（A1）和（A2）会得出不但直观且实用的演绎元定理：

元定理 — 
一阶逻辑理论 ${\mathcal {L}}$ 下，若有 $\Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}$ ，则有 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}$

证明

（注意这是元逻辑下的证明）： 假设 ${\mathcal {C}}_{1},{\mathcal {C}}_{2},....,{\mathcal {C}}_{n}$ 为条件所说 ${\mathcal {C}}$ 的证明，如果 ${\mathcal {C}}_{1}$ 是$\Gamma$ 里的公式或 ${\mathcal {L}}$ 的公理，那根据（A1） $\vdash {\mathcal {C}}_{1}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}_{1})$ 所以由MP律有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{1}$ 若 ${\mathcal {C}}_{1}$ 是 ${\mathcal {B}}$，那因为 $\vdash {\mathcal {B}}\Rightarrow {\mathcal {B}}$ 所以有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{1}$ 至此${\mathcal {C}}_{1}$的部分证明完毕。 接下来要用归纳法；假设对 $i<k$ 都有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{i}$ 。 若${\mathcal {C}}_{k}$ 是公理、或从 $\Gamma$ 来的、或是根本就是 ${\mathcal {B}}$，仿造上面 ${\mathcal {C}}_{1}$ 的部分就有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{k}$ 剩下没考虑的状况是由MP律组合出 ${\mathcal {C}}_{k}$ 的状况，也就是有 $l,m<k$ 使${\mathcal {C}}_{m}$ 是 ${\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k}$。 由公理A2有 $\vdash [{\mathcal {B}}\Rightarrow ({\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k})]\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {C}}_{l})\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}_{k})]$ 套用归纳法的假设，加上MP律，就会发现 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{k}$ 如此可以一路归纳到 ${\mathcal {C}}_{n}$ 也就是 ${\mathcal {C}}$ 的情况，故元定理得证。$\Box$

因为 $\Gamma$ 代表的是有限条公式，所以透过演绎元定理可以将证明过程必要的前提条件递归地移到 $\vdash$ 后，直到不需要任何前提为止；然后由MP律可以知道，若有 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}$ ，则有 $\Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}$，如此一来透过演绎元定理搬到推论结果的合式公式，也可以任意的搬回来。所以 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}$ 等价于某定理 $\vdash _{\mathcal {L}}{\mathcal {C}}$ 。因此也会将 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}$ 称为一个定理。

而从演绎元定理和MP律，会有以下直观且实用的元定理

元定理 — 
（D1） ${\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}$

（D2） ${\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}$

以下如果需要将引用的定理以演绎元定理进行＂搬移＂，会省略掉搬移的过程并在搬移后得到的结果后标注（D）。如果引用以上的（D1）和（D2）也会省略过程，单有结果和代号标注。

否定

以下的证明会分成使用（A3）的部分跟将公理（A3）取代为（T1）的部分，用以证明两者的等价性。

（DNe） Double negation, elimination — 
$\vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$

证明（使用A3）

（1）$(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}]$ （A3） （2）$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （I） （3）$(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}$ （D2 with 1, 2） （4）$\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1） （5）$\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

证明（使用T1）

（1）$\neg \neg {\mathcal {A}}\Rightarrow (\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1） （2）$\neg \neg {\mathcal {A}}$ （Hyp） （3）$\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 1） （4）$\neg {\mathcal {A}}\Rightarrow \neg \neg \neg {\mathcal {A}}$ （MP with 3, T1） （5）$\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （MP with 4, T1） （6）${\mathcal {A}}$ （MP with 2, 5）

（DNi） Double negation, introduction — 
$\vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$

证明（使用A3）

（1）$(\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}]$ （A3） （2）$(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}$ （MP with DNe, 1） （3）${\mathcal {A}}\Rightarrow (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})$ （A1） （4）${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 2,3）

证明（使用T1）
（1）$\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （DNe） （2）${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 1, T1）

上面两定理表达了双否定推理上等价于于原公式，引用两者任一会都以（DN）简写。

（T1） Transposition-1 — 
$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}$

证明（使用A3）

（1）$(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}]$ （A3） （2）$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （Hyp） （3）$(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}$ （MP with 1, 2） （4）${\mathcal {B}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （A1） （5）${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

（T2） Transposition-2 — 
${\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$

证明（使用T1）

（1）$\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$ （DN） （2）${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （Hyp） （3）$\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D with 1, 2） （4）${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （DN） （5）$\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 3,4） （6）$(\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （T1, D） （7）$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （MP with 5, 6）

注意到（T2）的证明引用了（T1）+（DN），但之前已经证明了（A1）+（A2）+（A3）可以推出（T1）；还有（A1）+（A2）+（T1）也可以推出（DN），所以注明使用（T1）即可。

以上二定理说明 ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ 推理上等价于 $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ ，引用这两个定理中任一都以（T）表示。

至此，已经可以证明（A1）+（A2）+（T1）可以推出（A3）：

（T1）可推出（A3）的证明

由MP律显然有 $\neg {\mathcal {B}},\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {B}}$ （1）$\neg {\mathcal {B}}\Rightarrow [\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}\,]$ （对上面的定理使用两次演绎元定理） （2）$\neg {\mathcal {B}}\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$（D1 with 1, T2） （3）$(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$（MP with A2, 2） （4）$\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})$（MP with I, 3） （5）$(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}$（MP with T1, 4） （6）$(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})$（Hyp） （7）$\neg {\mathcal {B}}\Rightarrow {\mathcal {C}}$（Hyp） （8）$\neg {\mathcal {C}}\Rightarrow \neg \neg {\mathcal {B}}$（MP with T2, 7） （9）$\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {B}}$（D1 with 6, 8） （10）$\neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$（D1 with DN, 9） （11）${\mathcal {B}}$（MP with 5, 10）

所以综合以上所述，在有（A1）+（A2）的前提下，公理（T1）等价于公理（A3）。

由（T）可以得到类似于公理（A3）的定理

（A3'） — 
${\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}$

证明

（1）$(\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]$ （A3） （2）$(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})$ （T, D） （3）$\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp） （4）$\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 3） （5）$(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}$ （MP with 1, 4） （6）$({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （T, D） （7）${\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp） （8）$\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 6, 7） （9）${\mathcal {B}}$ （MP with 5, 8）

实质条件

以下的定理重现了实质条件的直观理解。

（M0）material condition — 
$\neg {\mathcal {A}},{\mathcal {A}}\vdash {\mathcal {B}}$

（也就是$\neg {\mathcal {A}}\vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}$）

证明

（1）$\neg {\mathcal {A}}$ （Hyp） （2）${\mathcal {A}}$ （Hyp） （3）$(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}]$ （A3） （4）$\neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （A1） （5）$\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 4, 1） （6）${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})$ （A1） （7）$\neg {\mathcal {B}}\Rightarrow {\mathcal {A}}$ （MP with 6, 2） （8）$(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}$ （MP with 3,5） （9）${\mathcal {B}}$ （MP with 8,7）

（M1）material condition — 
${\mathcal {A}},\neg {\mathcal {B}}\vdash \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$

证明

首先注意到${\mathcal {A}},{\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}$ （MP） （1）${\mathcal {A}}\Rightarrow [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]$ （0, D） （2）$[({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\Rightarrow \{\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\}$ （T） （3）${\mathcal {A}}$ （Hyp） （4）$({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}$ （MP with 1, 3） （5）$\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]$ （MP with 2, 4） （6）$\neg {\mathcal {B}}$ （Hyp） （7）$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （MP 5, 6）

（M2）material condition — 
$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash \neg {\mathcal {B}}$

证明

（1）${\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （A1） （2）$[{\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})\}$ （T） （3）$[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})$ （MP with 1, 2） （4）$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp） （5）$\neg {\mathcal {B}}$ （MP with 3, 4）

（M3）material condition — 
$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {A}}$

证明

（1）$\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （M0, D） （2）$[\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})\}$ （T） （3）$[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})$ （MP with 1, 2） （4）$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp） （5）$\neg \neg {\mathcal {A}}$ （MP with 3,4） （6）${\mathcal {A}}$ （MP with 5, DN）

反证法

（C1）Proof by Contradiction — 
${\mathcal {A}}\Rightarrow \neg {\mathcal {B}},{\mathcal {B}}\vdash \neg {\mathcal {A}}$

证明
（1）$({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow (\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （T, D） （2）${\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （Hyp） （3）$\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 1, 2） （4）${\mathcal {B}}$ （Hyp） （5）$\neg \neg {\mathcal {B}}$ （MP with DN, 4） （6）$\neg {\mathcal {A}}$ （MP with 3, 5）

（C2）Proof by Contradiction — 
$\neg {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}$

逻辑与和逻辑或

且与或的交换性

以下为逻辑与的交换性

元定理 — 
$\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow ({\mathcal {B}}\wedge {\mathcal {A}})$

证明

（1）$({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （C1, D） （2）$[({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]\}$ （T, D） （3）$[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]$ （MP with 1,2）

类似的，（C2）正是逻辑或的交换性：

元定理 — 
${\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {B}}\vee {\mathcal {A}}$ （C2, D）

且与或的直观意义

＂且＂的直观意义是实质条件元定理的直接结果

（AND）Intuitive meaning of And — 
${\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}$ （M1）

${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}$ （M3）

${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}$ （M2）

从（AND）和 $\Leftrightarrow$ 的符号定义可知，$\vdash {\mathcal {B}}\Leftrightarrow {\mathcal {C}}$ 的证明可以拆成两部分；习惯上会以“（ $\Rightarrow$ ） ”标示 $\vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}$ 部分的证明，而“（ $\Leftarrow$ ） ”标示 $\vdash {\mathcal {C}}\Rightarrow {\mathcal {B}}$ 部分的证明。

类似的，＂或＂的直观意义是（M0）跟（D）的直截结果

（OR）Intuitive meaning of OR — 
${\mathcal {A}}\vdash {\mathcal {A}}\vee {\mathcal {B}}$ （M0, DN）

${\mathcal {B}}\vdash {\mathcal {A}}\vee {\mathcal {B}}$ （A1, D）

${\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {A}}\vdash {\mathcal {B}}$ （D）

${\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}$ （交换性, D）

以下的定理则是（A3'）的直截结果

（DisJ）Disjunction — 
${\mathcal {A}}\Rightarrow {\mathcal {C}},{\mathcal {B}}\Rightarrow {\mathcal {C}},{\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {C}}$

证明
（1） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp） （2） ${\mathcal {B}}\Rightarrow {\mathcal {C}}$ （Hyp） （3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 1, 2） （4） ${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （Hyp） （5） ${\mathcal {C}}$ （A3' with 3, 4）

且与或的结合律

对于＂且＂，展开符号定义后，可以从直观意义轻松地得到

（ASO-AND）Associativity of AND — 
$\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\wedge {\mathcal {C}}$

＂或＂也有类似的性质

（ASO-OR）Associativity of OR — 
$\vdash {\mathcal {A}}\vee ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\vee {\mathcal {C}}$

且与或的分配律

＂且＂和＂或＂之间还有分配律

（DIS-1）Distribution — 
$\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})$

证明

（$\Rightarrow$） （1）${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$ （Hyp） （2）${\mathcal {A}}$ （MP with 1, AND） （3）$\neg {\mathcal {B}}\Rightarrow {\mathcal {C}}$ （MP with 1, AND） （4）$\neg \neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （Hyp） （5）${\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （MP with 4, DN） （6）${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 3, 5） （7）${\mathcal {C}}$ （MP with 2, 5） （8）${\mathcal {A}}\wedge {\mathcal {C}}$ （MP twice with 2, 7, AND） 也就是 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg ({\mathcal {A}}\wedge {\mathcal {B}})\vdash {\mathcal {A}}\wedge {\mathcal {C}}$ 再套用（D）就会得到 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})$ （$\Leftarrow$） （1）$\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}\wedge {\mathcal {C}}$ （Hyp） （2）$\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}$ （D1 with 1, AND） （3）$\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}$ （D1 with 1, AND） （4）$\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})$ （MP with 2, C2） （5）$\neg {\mathcal {C}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})$ （MP with 3, C2） （6）$\neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （D1 with 4, AND） （7）$\neg {\mathcal {C}}\Rightarrow {\mathcal {B}}$ （D1 with 4, AND） （8）${\mathcal {A}}$ （A3' with 6, I） （9）${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$ （MP twice with 7, 8, AND） 也就是 $({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$

（DIS-2）Distribution — 
$\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$

证明

（$\Rightarrow$） （1）$\neg {\mathcal {A}}\Rightarrow ({\mathcal {B}}\wedge {\mathcal {C}})$（Hyp） （2）$\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （D1 with 1, AND） （3）$\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 1, AND） （4）$({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$（MP twice with 2, 3,AND） 也就是 ${\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\vdash ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$ （$\Leftarrow$） （1）$(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge (\neg {\mathcal {A}}\Rightarrow {\mathcal {C}})$ （Hyp） （2）$\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （MP with 1, AND） （3）$\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （MP with 1, AND） （4）$\neg {\mathcal {A}}$ （Hyp） （5）${\mathcal {B}}$ （MP with 2,4） （6）${\mathcal {C}}$ （MP with 3,4） （7）${\mathcal {B}}\wedge {\mathcal {C}}$ （MP twice with 5, 6, AND） 也就是 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg {\mathcal {A}}\vdash {\mathcal {B}}\wedge {\mathcal {C}}$ 再使用一次推论元定理会得到 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})$

德摩根定律

以下的元定理的名字来自于英国逻辑学家奥古斯塔斯·德摩根。

De Morgan I — 
$\vdash [\neg ({\mathcal {A}}\wedge {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\vee (\neg {\mathcal {B}})]$

证明

（$\Rightarrow$） （1）$\neg \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]$ （Hyp） （2）${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （MP with 1, DN） （3）$\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （DN） （4）$\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （D1 with 2, 3） （$\Leftarrow$） （1）$\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （Hyp） （2）${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （DN） （3）${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （D1 with 1, 2） （4）$\neg \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]$ （MP with DN, 3）

De Morgan II — 
$\vdash [\neg ({\mathcal {A}}\vee {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})]$

证明
（$\Rightarrow$） （1）$\neg (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp） （2）$\neg {\mathcal {A}}$ （MP with M2, 1） （3）$\neg {\mathcal {B}}$ （MP with M3, 1） （4）$(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})$ （AND with 2, 3） （$\Leftarrow$） （1）$\neg {\mathcal {A}}$ （Hyp） （2）$\neg {\mathcal {B}}$ （Hyp） （3）$\neg (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （M1）

普遍化元定理

公理模式（A7）可以稍加延伸成以下的元定理

定理的普遍化 — 

对任意变量 $x$ ，若 $\vdash {\mathcal {B}}$ 则有 $\vdash (\forall x){\mathcal {B}}$。

证明

假设${\mathcal {C}}_{1},{\mathcal {C}}_{2},....,{\mathcal {C}}_{n}$ 就是 ${\mathcal {B}}$的证明，那 ${\mathcal {C}}_{1}$一定是公理，根据（A7）可以得到 $\vdash (\forall x){\mathcal {C}}_{1}$ 若对 $i<k$ 都有 $\vdash (\forall x){\mathcal {C}}_{i}$ ，如果 ${\mathcal {C}}_{k}$ 是公理的话显然 $\vdash (\forall x){\mathcal {C}}_{k}$ 。 若有 $l,m<k$ 使得 ${\mathcal {C}}_{m}:{\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k}$ 那根据归纳法的假设跟（A6）有 $\vdash (\forall x){\mathcal {C}}_{l}\Rightarrow (\forall x){\mathcal {C}}_{k}$ 上式配上 $\vdash (\forall x){\mathcal {C}}_{l}$ 就可以得到 $\vdash (\forall x){\mathcal {C}}_{k}$ 以此归纳到${\mathcal {C}}_{n}$ 也就是 ${\mathcal {B}}$，故本元定理得证。$\Box$

更进一步，有以下元定里

（GEN） — 
在 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}$ 里变量 $x$ 都完全被约束，若

${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash {\mathcal {B}}$

则有

${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash (\forall x){\mathcal {B}}$

证明

以下对前提条件的数量 $n$ 做归纳。 若 $n=1$，根据前提有 ${\mathcal {A}}_{1}\vdash {\mathcal {B}}$ 以（D）将 ${\mathcal {A}}_{1}$ 往前搬，再套用定理的普遍化，会得到 $\vdash (\forall x)({\mathcal {A}}_{1}\Rightarrow {\mathcal {B}})$ 再根据（A5）和MP律，就可以得到 $\vdash {\mathcal {A}}_{1}\Rightarrow (\forall x){\mathcal {B}}$ 也就是本元定理要求的结果。 现在假设 $n<k$ 的情况下元定理会成立。元定理的前提条件根据（D）可以写为 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash {\mathcal {A}}_{k}\Rightarrow {\mathcal {B}}$ 则根据归纳法的假设 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash (\forall x)({\mathcal {A}}_{k}\Rightarrow {\mathcal {B}})$ 上式配上（A5），本元定理在 $n=k$ 的情况就可以得到证明，故本元定理得证。$\Box$

（GEN）可以稍加修饰，以套用在含有存在量词的公式上

（GENe） — 

若变量 $x$ 在 $\Gamma$ 的公式和 ${\mathcal {C}}$ 里都完全被约束则

（1） 若 $\Gamma \vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}$ 则 $\Gamma \vdash (\exists x){\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}$

（2） 若 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}$ 则 $\Gamma \vdash (\exists x){\mathcal {B}}\Rightarrow {\mathcal {C}}$

等价代换

以下的定理，说明两条“等价”的公式可以互相代换

（Equv）Equivalence of WF — 
$\Gamma$ 代表一群公式，若公式 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 满足：

$\Gamma \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}$

则对变量 $x$ 和任意公式 ${\mathcal {C}}$ ：

1. $\Gamma \vdash (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})$
2. $\Gamma \vdash ({\mathcal {C}}\Rightarrow {\mathcal {A}})\Leftrightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})$
3. $\Gamma \vdash ({\mathcal {A}}\Rightarrow {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$
4. 变量 $x$ 于 $\Gamma$ 完全被约束 ，则

$\Gamma \vdash (\forall x){\mathcal {A}}\Leftrightarrow (\forall x){\mathcal {B}}$

证明

以下的证明都会用到这三条公式： (a) ${\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ （from $\Gamma$） (b) ${\mathcal {A}}\Rightarrow {\mathcal {B}}$ （MP with AND, a） (c) ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （MP with AND, a） 1. (1) $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})$ （MP with T, b） (2) $(\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})$ （MP with T, c） (3) $(\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})$ （AND with 3, 5） 2. ($\Rightarrow$) (1) ${\mathcal {C}}\Rightarrow {\mathcal {A}}$（Hyp） (2) ${\mathcal {C}}\Rightarrow {\mathcal {B}}$（D1 with 1, b） ($\Leftarrow$) (1) ${\mathcal {C}}\Rightarrow {\mathcal {B}}$（Hyp） (2) ${\mathcal {C}}\Rightarrow {\mathcal {A}}$（D1 with 1, c） 3. ($\Rightarrow$) (1) ${\mathcal {A}}\Rightarrow {\mathcal {C}}$（Hyp） (2) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})$（MP with T, 1） (3) $(\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})$（MP with T, c） (4) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})$（D1 with 2, 3） (5) ${\mathcal {B}}\Rightarrow {\mathcal {C}}$（MP with T, 4） ($\Leftarrow$) (1) ${\mathcal {B}}\Rightarrow {\mathcal {C}}$（Hyp） (2) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})$（MP with T, 1） (3) $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})$（MP with T, b） (4) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})$（D1 with 2, 3） (5) ${\mathcal {A}}\Rightarrow {\mathcal {C}}$（MP with T, 4） 4. ($\Rightarrow$) (1)$(\forall x)({\mathcal {A}}\Rightarrow {\mathcal {B}})$（GEN with $x$, a） (2)$(\forall x){\mathcal {A}}\Rightarrow (\forall x){\mathcal {B}}$（MP with A6 , 1） ($\Leftarrow$) (1)$(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {A}})$（GEN with $x$, c） (2)$(\forall x){\mathcal {B}}\Rightarrow (\forall x){\mathcal {A}}$（MP with A6 , 1）

这些定理通常是混合使用，以达到“等价代换”的结果，例如，考虑到“逻辑与”是以下的符号定义：

$({\mathcal {A}}\wedge {\mathcal {C}}):=\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]$

那如果假设 $\vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ ，就有：

• $\vdash [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]$
• $\vdash \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow \{\neg [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]\}$

换句话说，从“ $\vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ ”可以得到“ $\vdash ({\mathcal {A}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\wedge {\mathcal {C}})$”，直观上相当于，把 ${\mathcal {A}}$ 都代换成 ${\mathcal {B}}$ 则两式等价。日后像这样递归地套用上述定理来得到“代换则某两式等价”，都简单地以“引用（Equv）”来表示这段实际的推演过程。

量词的可交换性

由普遍化，很容易证明以下关于＂交换性＂的定理

元定理 — 
（1） $(\forall x)(\forall y){\mathcal {A}}\vdash (\forall y)(\forall x){\mathcal {A}}$

（2） $(\exists x)(\exists y){\mathcal {A}}\vdash (\exists y)(\exists x){\mathcal {A}}$

（3） $(\exists x)(\forall y){\mathcal {A}}\vdash (\forall y)(\exists x){\mathcal {A}}$

注意最后（3）一般来说是不能反向的，只要想到＂对每个 $a$，都有一个数（也就是 $-a$ ），使 $a+(-a)=0$＂，但是任取一个 $a$ 的数 $(-a)$ 和任意的数 $b$ ， $b+(-a)$ 并不一定会为零。

量词的简写

数学中常常有 ＂对所有 $\epsilon >0$ 有...＂，或是 ＂存在 $\delta >0$ 使的...＂。而两句话比较清晰，接近一阶逻辑语言的说法是 ＂对所有 $\epsilon$ ，只要 $\epsilon >0$ 则...＂ 与 ＂存在 $\delta$ ， $\delta >0$ 且...＂。“大于”直观上是一个二元关系，也就是说，在公理化集合论里对应于一条 $\epsilon$ （ 或 $\delta$ ） 在里面完全自由的合式公式。据此，可做以下的符号定义

符号定义 — 
如果变量 $x$ 和 $y$ 都于合式公式 ${\mathcal {A}}(x,\,y)$ 里完全自由，那

$[\,\forall {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\forall x)[\,{\mathcal {A}}(x,\,y)\Rightarrow {\mathcal {B}}\,]$

$[\,\exists {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\exists x)[\,{\mathcal {A}}(x,\,y)\wedge {\mathcal {B}}\,]$

但直观上也会说 ＂对所有 $n>0$ 和 $m>0$ 有...＂，这样连续，带有条件的全称量词也是有＂交换性＂的。 为了讨论这个问题，首先需要一些前置的定理

（abb） — 
$\vdash [{\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Leftrightarrow [({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}]$

证明

（$\Rightarrow$） ${\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}$ 注意到 （AND） ${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}$ （AND） ${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}$ 所以 ${\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}),\,{\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {C}}$ 再套上演绎元定理就可以得证。$\Box$ （$\Leftarrow$） $({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}\vdash {\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$ 注意到 （AND） ${\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}$ 所以 $({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}},\,{\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {C}}$ 再套上演绎元定理就可以得证。$\Box$

这样就可以证明以下定理

元定理 — 
如果变量 $x$ 和 $y$ 都于合式公式 ${\mathcal {A}}(x,\,y)$ 和 ${\mathcal {B}}(x,\,y)$ 里完全自由，若项 $T$ 里没有 $y$ 那

$\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow \forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {C}}\}$

证明

（$\Rightarrow$） $[\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\vdash \forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}$ （1）$(\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （Hyp） （2）${\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with 1, A4） （3）${\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （D1 with 2, A4） （4）$[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {C}}$ （MP with abb, 3） （5）$\forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {B}}\}$ （GEN with 4 twice） （$\Leftarrow$） $\forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}$ （1）$\forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}$ （Hyp） （2）$[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}$ （MP with 2, A4 twice） （3）${\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with abb, 2） （4）$(\forall y)\{\,{\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （GEN with 3） （5）${\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with A5, 4） （6）$(\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （GEN with 5）

如果再加上 ＂项 $S$ 里没有 $x$ ＂ 那就是 ＂对所有 $n>0$ 和 $m>0$ 有...＂，也就是以上所讨论的情况了。以这个定理配上全称量词本身的交换性定理，那这句话就可以等价的说成 ＂对所有 $m$ 和 $n$ 若 $n>0$ 且 $m>0$ 则...＂，所以根据＂且＂的可交换性，可以进一步的说成 ＂对所有 $m>0$ 和 $n>0$ 有...＂，所以连续带有条件的全称量词是＂可交换的＂。也就是说

元定理 — 
如果变量 $x$ 和 $y$ 都于合式公式 ${\mathcal {A}}(x,\,y)$ 和 ${\mathcal {B}}(x,\,y)$ 里完全自由，若项 $T$ 里没有 $y$ ，且项 $S$ 里没有 $x$ 则

$\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow [\,\forall {\mathcal {B}}(y,\,S)\,][\,\forall {\mathcal {A}}(x,\,T)\,]{\mathcal {C}}$

但对于带条件的存在量词，首先可以得到以下非等价的定理。

元定理 — 
$(\exists x)(\exists y)({\mathcal {A}}\wedge {\mathcal {B}}\wedge {\mathcal {C}})\vdash (\exists x)[\,{\mathcal {A}}\wedge (\exists y)({\mathcal {B}}\wedge {\mathcal {C}})\,]$

这是因为一般来说， $(\exists y){\mathcal {D}}$ 不总是能推出 ${\mathcal {D}}$ 。虽说如此，只要对公式做出一些限制，就会有以下交换的直观定理：

（Ce）－Commutativity of existential quantification — 
若变量 $x$ 于公式 ${\mathcal {Q}}$ 完全被约束，且 ${\mathcal {R}}$ 是另外一条公式，则：

$\vdash (\exists x)({\mathcal {R}}\wedge {\mathcal {\mathcal {Q}}})\Leftrightarrow [(\exists x)({\mathcal {R}})\wedge {\mathcal {Q}})]$

证明

($\Rightarrow$) (1) ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})$ (Hyp) (2) ${\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})$ (D1 with 1 and A4) 换句话说 ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash {\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})$ 这样使用(GEN)有 ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash (\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]$ 这样对上式使用(De Morgan)和(T)就有 $\vdash (\exists x)({\mathcal {R}}\wedge {\mathcal {\mathcal {Q}}})\Rightarrow [(\exists x)({\mathcal {R}})\wedge {\mathcal {Q}})]$ ($\Leftarrow$) (1) $(\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]\Rightarrow [{\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})]$ (A5) (2) $(\forall x)[(\neg {\mathcal {Q}})\vee (\neg {\mathcal {R}})]\Rightarrow [(\neg {\mathcal {Q}})\vee (\forall x)(\neg {\mathcal {R}})]$ ( $\vee$ 的定义) (3) $(\forall x)[\neg ({\mathcal {Q}}\wedge {\mathcal {R}})]\Rightarrow \{\neg [({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\}$ (MP with 2, De Morgan) (4) $[({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\Rightarrow (\exists x)({\mathcal {Q}}\wedge {\mathcal {R}})$ (MP with 3, T)

也就是直观上，“存在x使得 x>0 且 y>0”与“y>0 且存在x使得 x>0”是一样的意思。

等式定理

一般来说，等式 $(x=y)$ 会被视为某个合式公式 ${\mathcal {E}}(x,\,y)$ 的简写。若使用元定理的形式刻划等式的性质，会作如下的定义

元定义 — 
说一阶逻辑理论 ${\mathcal {L}}$ 带相等符号 ${\mathcal {E}}(x,\,y)$ 意为（ $x_{1},\,\cdots ,\,x_{n}$ 、 $x$ 和 $y$ 都是 ${\mathcal {L}}$ 的任意变量）

• 除了变量 $x$ 和 $y$ 于 ${\mathcal {E}}(x,\,y)$ 是完全自由外其他变量都完全被约束
• （E1） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,x)$ 。
• （E2'） ${\mathcal {B}}(x,\,x)$ 为 ${\mathcal {L}}$ 内不含函数符号与常数符号的原子公式 ，$x$ 若以 ${\mathcal {B}}(x,\,y)$ 表示 ${\mathcal {B}}(x,\,x)$ 内某一个 $x$ 被取代成 $y$ 而成的新公式，则有

$\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]$

• （E2＂） 若以 $f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})$ 代表项 $f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})$ 里的 $x_{k}$ 被取代成 $y$ 而成的新项，则有

$\vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]$

• （E3） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(y,\,x)$ 。

并在这种状况下，规定 $(x=y)$ 为 ${\mathcal {E}}(x,\,y)$ 的简写。

上面的定义符合函数符号直观上的＂唯一对应＂。为了证明常数符号的＂唯一性＂，需要以下元定理

元定理 — 
说一阶逻辑理论 ${\mathcal {L}}$ 带相等符号 ${\mathcal {E}}(x,\,y)$ ，等同于要求：

• ${\mathcal {E}}(x,\,y)$ 除了变量 $x$ 和 $y$ 于 ${\mathcal {E}}(x,\,y)$ 是完全自由外其他变量都完全被约束。
• 符合（E1）。
• （E2） 对于任意变量 $x$ 和 $y$，若在公式 ${\mathcal {A}}$ 中自由的 $y$ 都不在 $\forall x$ 的范围内。若以${\mathcal {A}}_{y}$ 代表 ${\mathcal {A}}$ 某些自由的 $x$ 被取代成 $y$ 而成的新公式，则

$\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})$

证明

（$\Rightarrow$） 从（E1）+（E2'）+（E2＂）+（E3）推出（E2）的过程分成几个阶段推广（E2'） （1）含有常数符号的原子公式 取 $c_{j}$ 为任意常数符号。目标是证明：对一段含常数符号 $c_{j}$ 但不含任何函数符号的原子公式 ${\mathcal {B}}(x,\,x,\,c_{j})$ ，若 ${\mathcal {B}}(x,\,y,\,c_{j})$ 表 ${\mathcal {B}}(x,\,x,\,c_{j})$ 里某一个 $x$ 被取代为 $y$ 的新公式，则 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]$ （a） （a）证明过程如下： 取一个不曾在 ${\mathcal {B}}(x,\,y,\,c_{j})$ 出现的变量 $z$。若以 ${\mathcal {B}}(x,\,x,\,z)$ 表示 ${\mathcal {B}}(x,\,x,\,c_{j})$ 内的 $c_{j}$ 都被取代成 $z$ 的新公式，将之带入 （E2'）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]$ 对上式，以变量 $z$ 取（GEN）有 $\vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}$ （b） 但从（A4）有 $\vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}\Rightarrow \{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]\}$ 这样上式就可以与（b）式取MP，就会有（a）。 （2）含有任意项的原子公式 对一列项 $T_{1},\,\cdots ,\,T_{m}$ ，若以 $S$ 代表项 $T_{k}$ 里的一个 $x$ 被取代成 $y$ 而成的新项，那这样可以用 $A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})$ 代表 $A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})$ 的 $T_{k}$ 被取代成 $S$ 所构成的新公式。那现在的目标是证明 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})\Rightarrow A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})]$ （c） 但根据（A4）和（GEN），只需要证明 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]$ （c'） 就足够了。更进一步的，由下面两定理可以推出（c'） $\vdash _{\mathcal {L}}{\mathcal {E}}(z,\,z^{\prime })\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z,\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z^{\prime },\,x_{k+1},\,\cdots ,\,x_{m})]$ （d） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)$ （e） 也就是对（c）以变量 $z$ 和 $z^{\prime }$ 连续两次使用（GEN），然后连续两次与（A4）以MP律配合会得到 $\vdash _{\mathcal {L}}{\mathcal {E}}(T_{k},\,S)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]$ 然后将上式与（e）带入（D1）就有（c'）。但事实上（d）就是（E2'）的特殊状况，所以接下来只需要从（E2＂）证明（e），为此根据项的递归定义，以对项 $T_{k}$ 里有的函数符号数量做归纳： 函数符号数量为零的时候，（e）有两种状况（其中 $c_{j}$ 为任意常数符号） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(x,\,y)$ （e0） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(c_{j},\,c_{j})$ （e0'） （e0）就只是（I）故显然成立；另一方面，对（E1）使用（GEN）然后与（A4）配合就会有 $\vdash _{\mathcal {L}}{\mathcal {E}}(c_{j},\,c_{j})$ 故与（A1）配合就会有（e0'），至此函数符号数量为零情况的（e）已被证明。 若 $T_{k}$ 内函数符号数量为 $l$ 个，事实上会有一列函数符号数量小于 $l$ 的项 $S_{1},\,\cdots ,\,S_{n}$ ，而有 $T_{k}:f_{i}^{n}(S_{1},\,\cdots ,\,S_{n})$ 若以 ${S_{r}}^{\prime }$ 代表 $S_{r}$ 中的某个 $x$ 被取代成 $y$ 而成的新项，那这就是 $T_{k}$ 取代成新项 $S$ 的详细过程，那归纳法的前提就是 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })$ 那对（E2＂）使用 $n$ 次（GEN），然后同样与（A4）以MP律配合 $n$ 次有 $\vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}[f_{i}^{n}(S_{1},\,\cdots ,\,S_{r},\,\cdots ,\,S_{n}),\,f_{i}^{n}(S_{1},\,\cdots ,\,{S_{r}}^{\prime },\,\cdots ,\,S_{n})]$ 也就是 $\vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}(T_{k},\,S)$ 故将上式与归纳前提套入（D1）就会有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)$ 至此（e）已被归纳法证明。 （3）任意的公式 为了将（E2'）从任意原子公式推广到任意公式，根据语法对公式的递归定义，要分别对公式里的量词和逻辑连接词的数量做归纳。 假设 ${\mathcal {B}}(x,\,x)$ 为不含逻辑连接词的任意公式： ${\mathcal {B}}(x,\,x)$ 没有量词的情况就只是（c）而已，故成立。 若假设对于量词数量为 $l$ 的 ${\mathcal {B}}(x,\,x)$ 有（ ${\mathcal {B}}(x,\,y)$ 代表 ${\mathcal {B}}(x,\,x)$ 内某个自由的 $x$ 被取代成 $y$ 所成的新公式） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]$ 首先注意到新增量词的时候，不可以取 $\forall x$ 或是 $\forall y$ ，否则上面的自由取代就会完全被破坏。故取个不是 $x$ 也不是 $y$ 的任意变量 $z$ ，对上式使用（GEN），然后与（A6）、（A5）配合使用MP律有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\forall z{\mathcal {B}}(x,\,x)\Rightarrow \forall z{\mathcal {B}}(x,\,y)]$ 上式也就是量词数量为 $l+1$ 的状况，而把（E2'）推广到了不含逻辑连接词的任意公式上。 接下来对不含“ $\Rightarrow$ ”的任意公式里的“ $\neg$ ”的数量做归纳： “ $\neg$ ”的数量为零的情况刚刚已经证明，不再赘述。 假设“ $\neg$ ”的数量为 $l$ ，没有“ $\Rightarrow$ ”的公式下（E2'）都对，那对“ $\neg$ ”的数量为 $l$ 的 ${\mathcal {B}}(x,\,x)$ 有（特别注意到推广的（E2'）也可以将 ${\mathcal {B}}(x,\,y)$ 里唯一的$y$ 取代成 $x$） $\vdash _{\mathcal {L}}{\mathcal {E}}(y,\,x)\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]$ （f） 那根据（T）有 $\vdash _{\mathcal {L}}[{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]$ （g） 这样对（f）和（g）套用（D1），结果再和（E3）套用（D1）一次就有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]$ （f） 上式也就“ $\neg$ ”的数量为 $l+1$ 的情况，故把（E2'）推广到了仅不含“ $\Rightarrow$ ”的任意公式上。 为了要推广到任意的公式上，我要要对“ $\Rightarrow$ ”的数量做归纳： “ $\Rightarrow$ ”的数量为零的情况刚刚已经证明，不再赘述。 假设“ $\Rightarrow$ ”的数量小于 $l$ 的公式下（E2'）都对，那对但数量合起来为 $l$ 的 ${\mathcal {B}}(x,\,x)$ 与 ${\mathcal {C}}(x,\,x)$ 就会满足 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]$ （*） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]$ （**） 考虑到（D1）有 ${\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x),\,{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)$ ${\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x),\,{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)$ 那配上（*）与（**）就有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]\}$ $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {C}}(x,\,x)]\}$ 上两式就是所有“ $\Rightarrow$ ”的数量为 $l+1$ 的情况，故把（E2'）推广到了任意公式。 最后，取代 $n+1$ 个 $x$ 的状况，就是取代 $n$ 后再取代一次。所以可以由归纳法，从推广后的（E2'）推出（E2） （ $\Leftarrow$ ） 首先（E2'）显然只是（E2）的特例；要得到（E2＂）只要注意到由（E2）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow \{{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]\}$ 然后对（E1）使用（GEN）再配合（A4）使用MP律有 $\vdash _{\mathcal {L}}{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]$ 所以对上面两式套用（D2）就有（E2＂）。 至于（E3），注意到由（E2）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {E}}(x,\,x)\Rightarrow {\mathcal {E}}(y,\,x)]$ 那这样对上式和（E1）套用（D2）就有（E3）

从上面可以得知，如果等式符号仅仅为断言符号，那等式和它的公理一节的等式公理模式，是等价于本节的（E1）+（E2'）+（E2＂）。

由上面的元定理，对带有等式符号的 ${\mathcal {L}}$ 可以证明以下的等式性质

元定理 — 
若 $T$ 、 $S$ 与 $R$ 为 ${\mathcal {L}}$ 的任意项，则有

• $\vdash _{\mathcal {L}}T=T$
• $\vdash _{\mathcal {L}}(T=S)\Rightarrow (S=T)$
• $\vdash _{\mathcal {L}}(S=T)\Rightarrow [(S=R)\Rightarrow (T=R)]$

证明提示：

• （E1）+（GEN）+（A4）。
• 将 $(x=x)$ 带入（E2）后使用（D2），然后套用两次（GEN）+（A4）即可。
• 注意到从（E2）有 $\vdash _{\mathcal {L}}(x=y)\Rightarrow [(x=z)\Rightarrow (y=z)]$，然后套用三次（GEN）+（A4）即可。

对任意常数符号 $c$ ，上列元定理确保了

$\vdash _{\mathcal {L}}(c=c)$

$(x=c),\,(y=c)\vdash _{\mathcal {L}}(x=y)$

也就是常数符号的＂唯一性＂。

函数符号与唯一性

唯一性

数学讨论中，常常唯一存在某个符合特定条件的数，像是“存在唯一的实数 $s\in \mathbb {R}$ 使的对所有的实数 $r\in \mathbb {R}$ ， $r+s=r$ ”；更精确地来说，这句话的意思是：

“存在 $s\in \mathbb {R}$ 使的对所有的实数 $r\in \mathbb {R}$ ， $r+s=r$”且“对所有的 $s^{\prime },\,s\in \mathbb {R}$ 和所有 $r\in \mathbb {R}$，若 $r+s=r$ 且 $r+s^{\prime }=r$ 则 $s=s^{\prime }$ ”

这样一般来说，可以对任意变量 $x$ 和合式公式 ${\mathcal {B}}(x)$ 做以下的符号定义：

符号定义 — 
$\exists !x{\mathcal {B}}(x):=\exists x{\mathcal {B}}(x)\wedge (\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]$

（其中 $y$ 必须是展开以上定义时首次出现的变量； ${\mathcal {B}}(y)$ 是将 ${\mathcal {B}}(x)$ 内自由的 $x$ 都取代成 $y$ 所形成的新公式。）

注意到要能定义唯一性，一阶逻辑理论一定要带有等号。

新旧理论的等效条件

上节所提到的例子，实际上就是所谓的实数 $0$ ，但常数符号不能凭空从理论中冒出来，所以仔细来说，“定义实数 $0$ ”的过程应该是在原来的理论添加新的常数符号“ $0$ ”与以下的公理：

“对所有的实数 $r\in \mathbb {R}$ 有 $r+0=r$ ”

这样的话，“ $r>0$”就是一条含有新常数符号的叙述，它应等价于：

存在 $s\in \mathbb {R}$ 使“$r>s$ 且对所有的 $x\in \mathbb {R}$ ， $x+s=x$”

也就是说，添加“ $0$ ”创造了一套新理论，新理论的每条新叙述会对应到旧理论的某条旧叙述，且照理来说，新的对旧的也会对，反之亦然。

更一般的来说，如果新的一阶逻辑理论，是在旧的理论增添一些新符号跟新公理（并额外要求新符号与旧公理兼容），那为了让新旧理论等效，对于任意新理论的合式公式 ${\mathcal {C}}$ ，都要有某条相应的旧理论公式 ${\mathcal {C}}^{\prime }$ 满足以下条件：

新旧理论的等价条件 — 
（ $\vdash _{o}$ 代表旧理论可以推出； $\vdash _{n}$ 代表新理论可以推出。）

（1）若 ${\mathcal {C}}$ 本来就内含在旧理论里，则 ${\mathcal {C}}^{\prime }$ 就是 ${\mathcal {C}}$ 。

（2）$\vdash _{n}{\mathcal {C}}^{\prime }\Leftrightarrow {\mathcal {C}}$

（3）若 $\vdash _{n}{\mathcal {C}}$ ，则有 $\vdash _{o}{\mathcal {C}}^{\prime }$ 。

从条件（2）事实上就可以推出“若 $\vdash _{o}{\mathcal {C}}^{\prime }$ ，则有 $\vdash _{n}{\mathcal {C}}$ ”，因为 $\vdash _{o}{\mathcal {C}}^{\prime }$ 的话， 新理论只是扩张旧理论而没改变旧理论固有的定理，所以有 $\vdash _{n}{\mathcal {C}}^{\prime }$ ，但这样根据条件（2）跟MP律就会有 $\vdash _{n}{\mathcal {C}}$。所以条件（2）事实上是比“旧的对那新的也对”强的条件，但在之后的推导上（2）会比较方便。

预备定理

在以严谨的方式实践以上提及的直观动机前，需要一个预备定理

元定理 — 
变量 $x$ 在和合式公式 ${\mathcal {B}}(x)$ 与 ${\mathcal {C}}(x)$ 完全自由，则有

（Aux）$\exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Leftrightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$

证明

（$\Rightarrow$） $\exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Rightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ 以下取一个不曾出现的变量 $y$ 展开唯一性的定义 （1）$(\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]$ （Hyp） （2）${\mathcal {B}}(y)$ （Hyp） （3）${\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ （Hyp） （4）${\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)$ （MP with A4, 1） （5）${\mathcal {B}}(x)$ （MP with AND, 3） （6）${\mathcal {B}}(x)\wedge {\mathcal {B}}(y)$ （MP twice with AND, 2, 5） （7）$(x=y)$ （MP with 4, 6） （8）$(x=y)\Rightarrow [\,{\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)\,]$ （E2） （9）${\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)$ （MP with 7, 8） （10）${\mathcal {C}}(x)$ （MP with AND, 3） （11）${\mathcal {C}}(y)$ （MP with 9, 10） 这样根据（AND）和 (D1) 有 $\exists x!{\mathcal {B}}(x),\,{\mathcal {B}}(y),\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,\vdash \,{\mathcal {C}}(y)$ 那这样先使用（D）把 ${\mathcal {B}}(y)$ 移到左边，并对变量 $x$ 使用（GENe）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)$ 那这样再对变量 $y$ 使用（GEN）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists y[\,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)\,]$ 再使用（A4）把右侧的变量 $y$ 替换成 $x$ ，再对 $x$ 使用（GEN）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists x[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ 所以根据（D），本部分得证。 （$\Leftarrow$） $\exists !{\mathcal {B}}(x)\vdash (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]\Rightarrow (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ （1）$(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ （Hyp） （2）${\mathcal {B}}(x)$ （Hyp） （3）${\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)$ （MP with A4, 1） （4）${\mathcal {C}}(x)$ （MP with 2, 3） （4）${\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ （MP twice with AND, 2, 4） 也就是说 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,{\mathcal {B}}(x)\,\vdash \,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ 对变量 $x$ 使用（GENe）有 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ 这样根据（AND）和 (D1) 有 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists !x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ 所以根据（D），本部分得证。

新理论的假设

一般来说，如果变量 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$ 在 ${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ 完全自由，且旧理论里有：

（$U$）$\vdash _{o}\exists !x{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$

那所谓的新理论，就是添加一个函数符号 $f_{k}^{n}$ 和以下的新公理：

（$U^{\prime }$）${\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$

如果仅仅是：

$\vdash _{o}\exists !x{\mathcal {B}}(x)$

的话，添加的是常数符号 $c_{k}$ 与以下的新公理：

（$U$）${\mathcal {B}}(c_{k})$

添加常数符号的情况可视为添加函数符号情况的特例，因为常数符号可以视为“零变量”的函数符号。

但不管如何，还需假设 $f_{k}^{n}$ 和新理论的逻辑公理、量词公理兼容，也就是所有公理模式须涵盖内含 $f_{k}^{n}$ 的项。特别像是（A4）这种将自由变量代换成项的公理模式，也就是说，若项 $T$ 内含 $f_{k}^{n}$ ，且公式 ${\mathcal {D}}(x)$ 内自由的 $x$ 都不在 $T$ 的变量的量词范围内，那

$\forall x{\mathcal {D}}(x)\Rightarrow {\mathcal {D}}(T)$

仍然是新理论的公理。

另外还需要考虑到 $f_{k}^{n}$ 与等号的兼容性（换句话说，新理论仍须是带等号的一阶逻辑理论），这样的话，考虑到上面等式定理所述的条件（E2''），需额外假设：

新理论的额外假设 — 
对任何介于 $1$ 与 $n$ 的下标 $k$ 和变量 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$

$(t_{k}=x)\Rightarrow [\,f_{k}^{n}(t_{1},\,\ldots ,\,t_{k},\,\ldots ,\,t_{n})=f_{k}^{n}(t_{1},\,\ldots ,\,x,\,\ldots ,\,t_{n})\,]$

是公理 （若是添加常数符号的特例，就不须额外假设以上的公理）

这样就有以下直观的定理

元定理 — 
对变量 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$ 有

（E）$\vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Leftrightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)$

证明

（$\Rightarrow$） $\vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （1）$(y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,]$ （E2） （2）$(\forall y)\{(y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\,]\}$ （GEN with 1, $y$） （3）$[\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow \{\,{\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,\}$ （MP with A4, 2） （4）$[\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （D2 with $U^{\prime }$, 3） （$\Leftarrow$） $\vdash _{n}{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （1）$\forall x\forall y\{\,[\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\,]\Rightarrow (x=y)\,\}$ （MP with AND and $U$） （2）$\forall x{\big \{}\,\{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,{\big \}}$ （A4 with 1 and $y$） （3）$\{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （A4 with 2 and $x$） （4）${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （Hyp） （5）${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （AND with $U$ and 4） （6）$x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})$ （MP with 3 and 5）

换句话说，“ $s=0$ ”在新理论里等价于 “对所有的实数 $r\in \mathbb {R}$ ， $r+s=r$”。

一阶逻辑的元定理

下面列出了一些重要的元逻辑定理。

1. 不像命题演算，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程，判定P是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）
2. 有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式P, P是可证明的。
3. 一元断言逻辑（就是说，断言只有一个参数的断言逻辑）是可判定的。

转换自然语言到一阶逻辑

用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，$p\lor q$意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。

一阶逻辑的限制

所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。

难于表达if-then-else

带有等式的FOL不包含或允许定义if-then-else断言或函数if（c,a,b），这里的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，断言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。

在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。 断言if（c,a,b）如果重写为$(c\wedge a)\lor (\neg c\wedge b)$就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况断言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这里的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。 其他人进一步扩展FOL使得函数和断言可以在任何位置接受项和公式二者。

类型（种类）

除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 ，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。

单一参数断言可以用来在合适的地方实现类型的概念。例如：

$\forall x(Man(x)\rightarrow Mortal(x))$，

断言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。 断言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：

$\exists x(Man(x)\wedge Mortal(x))$（“存在既是男人又是人类的事物”）。

容易写成$\exists xMan(x)\rightarrow Mortal(x)$，但这将等价与$\exists x\neg Man(x)\lor \exists xMortal(x)$（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：

$\forall x(Man(x)\rightarrow Mammal(x))$（“对于所有x，如果x是男人，则x是哺乳动物）。

难于刻画模型大小

主条目：二阶逻辑

从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。若一阶理论有任意有限大的模型，则也有无穷大的模型，所以说不能刻划有限性。而若理论有某个无穷基数大小的模型，则也必有任意更大的模型，所以不能刻划可数性。另一个例子，是无法用一阶语言将实数系公理化，因为不论用何种一阶理论描述，既然该理论有实数系此种无穷模型（大小为$2^{\aleph _{0}}$），所以必有比实数系更大（比如$2^{2^{\aleph _{0}}}$）的另一个模型，从而该理论不是（唯一地）刻划实数系的性质。实数系满足的公理中，有上确界性质一项，它声称实数的所有有界的、非空集合都有上确界。一阶逻辑祗能对元素量化，但此公理中，要对模型的全部子集量化，这就需要二阶逻辑了。

图可及性不能表达

很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用断言逻辑完全表达。换句话说，没有断言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）断言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。

参见

• 真值表
• 逻辑等价
• 逻辑条件
• 逻辑与非
• 逻辑或非
• 数理逻辑
• 零阶逻辑
• 一阶语言
• 二阶逻辑
• 布尔函数
• 推理规则列表
• 哥德尔完备性定理
• 哥德尔不完备定理

参考文献

来源

• Jon Barwise and John Etchemendy，2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
• David Hilbert and Wilhelm Ackermann 1950. Principles of Theoretical Logic（English translation）. Chelsea. The 1928 first German edition was titled Grundzüge der theoretischen Logik.
• Wilfrid Hodges, 2001, "Classical Logic I: First Order Logic", in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

外部链接

• Stanford Encyclopedia of Philosophy：＂Classical Logic（页面存档备份，存于互联网档案馆） -- by Stewart Shapiro. Covers syntax, model theory, and metatheory for first order logic in the natural deduction style.
• forall x: an introduction to formal logic（页面存档备份，存于互联网档案馆）, by P.D. Magnus, covers formal semantics and proof theory for first-order logic.
• Metamath（页面存档备份，存于互联网档案馆）：an ongoing online project to reconstruct mathematics as a huge first order theory, using first order logic and the axiomatic set theory ZFC. Principia Mathematica modernized and done right.
• Podnieks, Karl. Introduction to mathematical logic.（页面存档备份，存于互联网档案馆）