一阶逻辑

在命题逻辑里，“苏格拉底是哲学家”、“帕雷托是哲学家”只能简单标记为 ${\displaystyle p}$  及 ${\displaystyle q}$  。

而一阶逻辑先设符号 ${\displaystyle {\text{Phil}}(x)}$  意为 “ x 是哲学家”，然后以 ${\displaystyle s}$  代表苏格拉底、 ${\displaystyle b}$  代表帕雷托，则 ${\displaystyle {\text{Phil}}(s)}$  对应 ${\displaystyle p}$  ； ${\displaystyle {\text{Phil}}(b)}$  对应 ${\displaystyle q}$  。也就是赋予断言符号“${\displaystyle {\text{Phil}}(x)}$  ”语义的解释。这个解释默认一个“所有人类的群体”（也就是语义解释的论域），并将变量 ${\displaystyle x}$  解释为自群体中取出来的某人。

断言符号可以包含一个以上的变量。例如：设 ${\displaystyle {\text{Cp}}(x,\,y)}$  意为“ x 与 y 是夫妻”，则 ${\textstyle {\text{Cp}}(s,\,y)}$  意为“苏格拉底和 y 是夫妻”。

一阶逻辑和命题逻辑相同，断言符号和变量还能与逻辑符号组成更复杂的叙述。例如：设断言符号 ${\displaystyle {\text{Schol}}(x)}$  意为 ${\displaystyle x}$  是学者。则“若 x 为哲学家，则 x 为学者”可表示为：

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

而“对所有 x ，若 x 为哲学家，则 x 为学者”则记为：

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

也就是自左方开始阅读，以 ${\displaystyle \forall x}$  表示“对于所有 x ”，可以将之理解为“对于所有 x ， ${\displaystyle \forall x}$  右方的叙述为真。”其中，${\displaystyle \forall x}$  这个符号被称为 ${\displaystyle x}$  的全称量词。

直观上有“若所有x是哲学家，那x的长子也会是哲学家”这样“合理”的叙述。若设 ${\displaystyle {\text{Son}}(x)}$  意为 “ x 的长子”，那么这段“合理”叙述可记为：

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

${\displaystyle \Rightarrow }$  表示“与 ${\displaystyle x}$  有唯一对应的那个对象”，被称为函数符号。这段直观为真的叙述，经过适当的扩展以后就是一阶逻辑其中的一条公理。

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

${\displaystyle \exists x({\text{Phil}}(x))}$ 

自左方开始阅读，以 ${\displaystyle \exists x}$  代表“存在 x ”，可以将之理解为“有 x 使 ${\displaystyle \exists x}$  右方的叙述为真”。其中，${\displaystyle \exists x}$  被称为 ${\displaystyle x}$  的存在量词。全称量词和存在量词一起被简称为量词。

直观上，“并非所有 x 不是哲学家”，和“有 x 是哲学家”是等价的；且“不存在 x 不是学者”也与“所有的 x 是学者”等价。所以只要有“否定”这个逻辑概念，那么一阶逻辑就能以全称量词为基础，作以下的符号定义（ ${\displaystyle \neg }$  解释为 “否定”， 而 ${\displaystyle {\mathcal {A}}}$  代表一段＂叙述＂）：

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

由此，存在量词被定义为全称量词的衍伸。

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

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

基本符号

一套理论能容许多少符号，取决于人类根据物理定律能塑造多少符号。但以目前无法确知宇宙是不是有限，或是是否可无限制分割。虽然所有的公理化集合论都以量词的形式隐晦的承认无穷的存在（如ZF集合论的无穷公理），甚至以这样自然数意义上的无穷为基础，去建构出不可数的实数。但将之对应到现实，还是会回到同样的物理问题。

谨慎起见，以下各种类的符号没有特别声明，数量将会是有限个。

逻辑符号

词汇表中存在若干个逻辑符号，通常包括：

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

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

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

   ${\displaystyle {\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. 等式符号：${\displaystyle =}$ 
   • 有作者会因为语义上对“相等”的不同解释，而将等式符号视为双元断言符号、甚至是某种合式公式的简写。
6. 符号相等：${\displaystyle \asymp }$ 
   • 为了将符号识别上区别等同和等式符号，某些作者^[5]会额外采用这个符号。

注意：并非所有的符号都是必需的。比如，在比较极端的情况中，因为谢费尔竖线（或异或）的布尔代数完备性使得所有不含量词的逻辑公理都可以用谢费尔竖线表述，而大幅减少基础的逻辑联结词。

另外，一些作者并没有将语义学和形式理论划分清楚，而会将真值常数纳入符号的一环：用 T 、Vpq 或 ${\displaystyle \top }$  来表示“真”，并用 F 、 Opq 或 ${\displaystyle \bot }$  来表示“假”。

断言符号

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

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

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

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

函数符号

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

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

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

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

常数符号

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

${\displaystyle c_{j}}$ 

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

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

语法

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

项

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

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

原子公式

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

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

这样的形式。

公式

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

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

举例来说，

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

是公式而

${\displaystyle \forall x\,x\Rightarrow }$ 

则不是公式。

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

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

施用

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

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

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

自由变量和约束变量

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

例如，对于公式：

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

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

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

括弧的简写

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

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

举例来说

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

的重构过程如下

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

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

波兰表示法

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

${\displaystyle \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]\}\}}$ 

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

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

${\displaystyle \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律

对于公式 ${\displaystyle {\mathcal {A}}}$  和 ${\displaystyle {\mathcal {B}}}$ ：

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

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

公理

逻辑公理

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

量词公理

以下的 ${\displaystyle x}$  为任意变量， ${\displaystyle {\mathcal {B}}}$  、 ${\displaystyle {\mathcal {C}}}$  为任意公式。

它们实际上是公理模式。

等式和它的公理

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

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

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

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

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

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

项的取值

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

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

或较直观的符号

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

来表示。

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

真假的赋值

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

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

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

的${\displaystyle m}$  元有序对子集合。

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

更进一步的来说

代数化语义

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

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

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

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

空论域

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

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

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

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

定理与证明

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

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

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

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

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

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

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

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

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

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

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

演绎元定理

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

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

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

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

否定

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

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

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

实质条件

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