数理逻辑.md

数理逻辑与数学分析

本笔记适用于北京大学 信息与计算科学 数理逻辑课程，教学课件可在网络上搜索“北京大学 信息与计算科学 数理逻辑”找到，如讲义0。参考教材：Logic for Mathematicians, by Hamilton A G, Cambridge University Press 和 Introduction to Mathematical Logic, by Mendelson E, CRC Press。

还有一个博客园的专栏：https://www.cnblogs.com/minor-second/category/2057764.html

本课程课件也被山东大学C-Fair项目人工智能本科班级使用。

命题

具有真假意义的判断性或陈述性的语句称为 命题 (Proposition)，或称语句(Statement)。

真值：命题的真假意义称为命题的 真值 (Truth Value)。

逻辑推理

当前提的真蕴涵结论的真时，称前提和结论之间有可推导性，即前提蕴涵结论。

推理之正确，取决于前提的真蕴含结论的真。

形式语言（Propositional Language）

语义涉及符号和符号表达式的意义，语法涉及符号和符号表达式的形式结构。语义是具体的，语法相反是普遍的。因此对形式系统的研究，主要研究的是语法的成立，语法的成立可以使得证明可以被机械地检验。

复合命题

由简单命题通过逻辑运算符连接而成的命题称为 复合命题 (Compound Proposition)。

连结词：非、与、或、蕴涵、等价。

连结词	符号	名称
非 A (not A)	$\neg A$或者 $\sim A$	否定(Negation)
A 与 B (A and B)	$A \land B$	合取(Conjunction)
A 或 B (A or B)	$A \lor B$	析取(Disjunction)
A 蕴涵 B (A implies B)	$A \to B$	蕴涵(Material Implication)
A 当且仅当 B (A if and only if B)	$A \leftrightarrow B$	等值于(Equivalence)

命题变元：表示命题的符号。用小写字母（可加下标）表示。

辅助符：用于表示复合命题的符号，如括号。

真值函数和真值表

$\neg p$ 的真值函数为 $f(p) = \neg p$。

$p$	$\neg p$
T	F
F	T

对应真值函数(Bool 函数):

$$f^\sim : {T, F} \mapsto {T, F}$$ $$f^\sim(T) = F, f^\sim(F) = T$$

$p \land q$ 的真值函数为 $f(p, q) = p \land q$。

$p$	$q$	$p \land q$
T	T	T
T	F	F
F	T	F
F	F	F

对应真值函数(Bool 函数):

$$ f^\land : {T, F} \times {T, F} \mapsto {T, F} $$

$$ f^\land(T, T) = T, f^\land(T, F) = F, f^\land(F, T) = F, f^\land(F, F) = F $$

$p \lor q$ 的真值函数为 $f(p, q) = p \lor q$。

$p$	$q$	$p \lor q$
T	T	T
T	F	T
F	T	T
F	F	F

对应真值函数(Bool 函数):

$$ f^\lor : {T, F} \times {T, F} \mapsto {T, F} $$

$$ f^\lor(T, T) = T, f^\lor(T, F) = T, f^\lor(F, T) = T, f^\lor(F, F) = F $$

$p \to q$ 的真值函数为 $f(p, q) = p \to q$。

$p$	$q$	$p \to q$
T	T	T
T	F	F
F	T	T
F	F	T

$p$的真蕴涵$q$的真，不要求$p$的假有任何结论；排除$p$的真有$q$的假的情况，其他情况都是真。

举个例子:

• 如果明天太阳走西边升起，那么 1+1=3。(真，因为前提假，结论无论真假都是真)
• 如果明天太阳走东边升起，那么 1+1=2。(真，因为前提真，结论真)
• 如果明天太阳走西边升起，那么 1+1=2。(真，因为前提假，结论无论真假都是真)

$p \leftrightarrow q$ 的真值函数为 $f(p, q) = p \leftrightarrow q$。

$p$	$q$	$p \leftrightarrow q$
T	T	T
T	F	F
F	T	F
F	F	T

技术性符号（如括号）是没有必要的。可以把中置运算符写成前置或后置运算符，如 $p \land q$ 可以写成 $\land p q$，连接符按照 $\sim$、$\land$、$\lor$、$\leftrightarrow$、$\to$ 的优先级降序。

命题形式

否定式、合取式、析取式、蕴涵式、等值式

如：$((p\land q)\to (\sim (q \lor r)))$，简略写法：

$$ p \land q \to \sim( q \lor r) $$

$$ P \land q \to \sim . q \lor r $$

这个式子里面的$.$是技术符号，取代掉了括号，表示$q\lor r$是$\sim$的参数。

真值指派

对一个命题中的所含变元分别赋予 T 或 F，称为一组真值指派。

可满足性：如果一个命题中的某个真值指派使得命题为真，则称这命题是可满足的。

SAT 问题（Satisfiability Problem）：判断一个命题是否可满足的问题——寻找一个多项式时间内对一个命题寻找满足的真值指派。

重言式和矛盾式

对于任意一组真值指派，命题都为真的命题称为 重言式 (Tautology)。

对于任意一组真值指派，命题都为假的命题称为 矛盾式 (Contradiction，inconsistent)。

例子：

• $p \lor q$ 是可满足的。（当$p=T, q=F$时，$p \lor q = T$）
• $p \lor \sim p$ 是重言式。
• $p \land \sim p$ 是矛盾式。
• $(\sim p \to q) \to ((\sim p \to \sim q) \to p)$ 是重言式。

逻辑隐含和逻辑等价

如果$A \to B$是重言式，则称$A$逻辑蕴含$B$，记作$A \models B$。

如果$A \leftrightarrow B$是重言式，则称$A$逻辑等价于$B$，记作$A \equiv B$。

操作和替换

命题 1：设$A$和$B$是两个命题，$A$和$A\to B$都是重言式，则$B$是重言式。

设$A$是含有变元$p_1, p_2, \cdots, p_n$组成的命题形式，$A_1, A_2, \cdots, A_n$是任意的命题形式，$A_{p_1, p_2, \cdots, p_n / A_1, A_2, \cdots, A_n}$表示把$A$中的$p_1, p_2, \cdots, p_n$分别替换为$A_1, A_2, \cdots, A_n$得到的命题形式。

命题 2：设$A$是一个命题，$A$是重言式，$A_{p_1, p_2, \cdots, p_n / A_1, A_2, \cdots, A_n}$也是重言式。

这个命题是说，如果$A$是重言式，那么$A$中的任意变元替换后的命题也是重言式。举个具体例子，$p \lor q$是重言式，其中$p$是一个变元，那么$p \lor q$中的$p$替换为$A$，$A \lor q$也是重言式。或者更具体一些，$p_1, p_2, \cdots, p_n \to (太阳会落山)$，此处的$p_1, p_2, \cdots, p_n$是任何一个命题，都不影响这个命题是重言式。

一个含有变元的重言式，他的每个变元可以任意替换为一个命题形式，得到的命题形式也是重言式。

命题 3：

$$ \begin{aligned} \sim(A \land B) &\equiv \sim A \lor \sim B \\ \sim(A \lor B) &\equiv \sim A \land \sim B \\ \end{aligned} $$

这个也称为德摩根定律。

结合律和交换律

$$ \begin{aligned} A \land (B \land C) &\equiv (A \land B) \land C \\ A \lor (B \lor C) &\equiv (A \lor B) \lor C \\ A \land B &\equiv B \land A \\ A \lor B &\equiv B \lor A \\ \end{aligned} $$

所以，在这个时候可以把所有的括号去掉，因为不同的括号组合不影响结果。

命题 4：

设$A_1$ 是含有命题形式$A$ 的命题形式，$B_1(A_{1, A/B})$ 是用命题形式 $B$ 替换 $A$ 得到的命题形式，若$A$与$B$等值，则$B_1$与$A_1$逻辑等价。

受限命题形式

受限命题形式是仅含有符号$\land$、$\lor$、$\sim$ 的命题形式。

命题 5：

设$A$是受限命题形式，$A^*$ 是通过如下形式得到的受限命题形式：

1. 互换$\land$和$\lor$；
2. 用$\sim p$替换$A$中的所有变元$p$；

则$A^*$与$\sim A$逻辑等价。

这个命题的证明可以使用数学归纳法。

推论（De Morgan 定律）：

令$P_1, P_2, \cdots, P_n$是命题变元，$A$是受限命题形式，则：

$$ \bigwedge\limits_{i=1}^n(\sim P_i) \equiv\sim (\bigvee \limits_{i=1}^n P_i) $$

一些常见的定律

• 无矛盾律：$\sim (p \land \sim p)$ 就是说，$p$ 和 $\sim p$ 不能同时为真。
• 排中律：$p \lor \sim p$ 就是说，$p$ 和 $\sim p$ 至少有一个为真。
• 双重否定律：$\sim \sim p \equiv p$ 就是说，两次否定等于肯定。
• 同幂律：$p \equiv p \land p \equiv p \lor p$ 就是说，一个命题等于自己的合取和析取。
• 赎出律：$(A \land B )\to C \equiv A \to (B \to C)$ 就是说，如果 C 是由 A 和 B 共同决定的，那么 A 决定 B 决定 C，A 是真的的话，B 是真的的话，C 就是真的。
• 换位率：$A \to B \equiv \sim B \to \sim A$
• 交换律：$A \land B \equiv B \land A$，$A \lor B \equiv B \lor A$
• 结合律：$(A \land B) \land C \equiv A \land (B \land C)$，$(A \lor B) \lor C \equiv A \lor (B \lor C)$
• 分配律：$A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$，$A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$

范式

一个文字（Literal）是一个变元$p$（称为正文字）或者一个变元的否定 $\sim p$ （称为负文字）。（1.3.4）

一个基本合取式（Elementary Conjunctive Form）是一个或多个文字的合取，其又称为子句（Clause）。如：$p \land \sim q \land r$。（1.3.3）

任一真值函数$F$都会对应于一个受限的命题形式$A$，即可反向构造一个命题形式$A$，使得$A$的真值函数与$F$相同。（1.3.5）

推论：任一非矛盾的命题形式都与一个形为$\bigvee\limits_{i=1}^n (\bigwedge\limits_{j=1}^{m_i} L_{ij})$的受限命题形式逻辑等价，其中$L_{ij}$是文字。这个式子称为析取范式（Disjunctive Normal Form，DNF）。（1.3.6）

任一非重言式的命题形式都与一个形为$\bigwedge\limits_{i=1}^n (\bigvee\limits_{j=1}^{m_i} L_{ij})$的受限命题形式逻辑等价，其中$L_{ij}$是文字。这个式子称为合取范式（Conjunctive Normal Form，CNF）。（1.3.7）

连接符的完备集

连接符的完备集$S$是指，用$S$中的连接符可以构造出所有的命题形式。

由(1.3.5)可知，${\land, \lor, \sim}$是一个完备集。

可以证明，${\land, \sim}$, ${\lor, \sim}$, ${\to, \sim}$ 都是完备集。

定义 1.4.1：

与非：$A | B \equiv \sim (\sim A \land \sim B)$

或非：$A \downarrow B \equiv \sim A \land \sim B$

异或：$A \oplus B \equiv (A \land \sim B) \lor (\sim A \land B)$ 或者$p \oplus q = p + q \mod 2$

可以证明，${|},{\downarrow}$ 都是完备集。

连接符完备集只含一个连接符，命题形式的表达比较长且复杂。

推理的有效性

推理是从一些判断推出另一个判断的思维过程，推出的判断称为结论（Conclusion），推理的前提称为前提（Premise）。

演绎推理（Deductive Reasoning）：从一系列基本前提出发，通过一定的推理规则推出结论的过程，所可能推出的结论是不可废除的。

归纳推理（Inductive Reasoning）：从一系列特殊的个别事实出发，推出一般性的结论，所得结论是有可能废除的。

推理形式，又称形式推理，是命题形式的一个有限序列，最后一个命题 形式是结论，其它的命题形式为前提。

一个有效（Valid）的推理形式是指，如果前提都为真，则结论也为真。

有效的推理形式

分离规则或三段论(Modus Ponens, MP)

$$ \begin{aligned} A \to B \\ A \\ \hline B \end{aligned} $$

逆分离规则(Modus Tollens)

$$ \begin{aligned} \sim B \\ A \to B \\ \hline \sim A \end{aligned} $$

假言三段论(Hypothetical Syllogism, HS)

$$ \begin{aligned} A \to B \\ B \to C \\ \hline A \to C \end{aligned} $$

析取三段论(Disjunctive Syllogism)

$$ \begin{aligned} A \lor B \\ \sim A \\ \hline B \end{aligned} $$

归谬法(Argumentum ad Absurdum)

$$ \begin{aligned} A \to B \\ \sim B \\ \hline \sim A \end{aligned} $$

引入规则(Introduction)

$$ \begin{aligned} A \\ \hline A \lor B \end{aligned} $$

$$ \begin{aligned} A \\ B \\ \hline A \land B \end{aligned} $$

消去规则(Elimination)

$$ \begin{aligned} A \land B \\ \hline A \end{aligned} $$

有效推理和逻辑隐含

推理形式$A_1, A_2, \cdots, A_n; \therefore B$是有效的，当且仅当$A_1 \land A_2 \land \cdots \land A_n \to B$是重言式。(1.5.0)

模型

对于任何一个命题形式$A$，如果存在一个真值指派$v$，使得$A$为真，则称这个真值指派是$A$的一个模型(Model)，或者说$v$满足$A$，$v \models A$。(1.5.1)

令 $\Gamma$ 是一个命题形式的集合，如果存在一个真值指派$v$，使得$\Gamma = {A_1, A_2, \cdots, A_n}$，$v \models A_i$，则称$v$是$\Gamma$的一个模型。

令 $\Gamma$ 是一个命题形式集，$A$是任意命题形式，则当且仅当$\Gamma \models A$，对于$\Gamma$的任意模型$v$，$v \models A$。称为$\Gamma$ 蕴含（Entail） $A$。(1.5.2)

推理形式$A_1, A_2, \cdots, A_n; \therefore B$是有效的，当且仅当$|A_1 \land A_2 \land \cdots \land A_n| \models B$是重言式。(1.5.3)

形式系统

形式推演和符号演算

Leibniz 提出了形式推演的思想，要求建立的关于推导的演算，形式推演的正确性是能够机械地检验的，一种精确的、普遍适用的科学语言，一种推理的演算，能够用计算来解决辩论和意见不一致的问题。

形式系统，又称为演绎系统（符号计算，calculus），指使用符号，并且有关符号的一切行为和性质完全由给定的规则集来确定，而不依赖于符号特定的意义和具体的性质。

形式系统$L$是命题（逻辑）演算，命题逻辑是在命题语言$L_0$基础上的形式化推演系统。

形式系统的要素

描述一个形式系统，需要以下几个要素：

• 形式语言$L_0$，其包含一个字符（Symbol）集合$S$，一个由字符组成的有限字符串集合，称为公式（well-formed formula，wff）集。
• 公理（Axiom）：是形式系统的基础，是一组合取公式。
• 推理规则（Inference Rule），其可以把一个合取公式$A$作为某些合取公式$A_1, A_2, \cdots A_n$的直接后承（Immediate Successor, Consequence）而推出。

形式系统的定义（L）

命题演算形式系统$L$：

• 一个符号集：$\sim$, $\land$, $\lor$, $\to$, $\leftrightarrow$, $p_1, p_2, \cdots$
• 一个公式集，要求：
  • $p_1, p_2, \cdots$是公式
  • 如果$A$是公式，则$\sim A$是公式
  • 如果$A$和$B$是公式，则$(A \land B)$, $(A \lor B)$, $(A \to B)$, $(A \leftrightarrow B)$是公式
  • 所有的公式都是由上述规则生成的
• 一组公理（Axiom），通过三组公理模式（Schema）定义，对于任意的公式$A, B, C$：
  • $A \to (B \to A)$
  • $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
  • $(\sim B \to \sim A) \to (A \to B)$
• 一组推理规则（Inference Rule）：
  • Modus Ponens（分离规则）：$A \to B, A \therefore B$

公理化方法

形式系统$L$是一个公理系统。对于一个公理系统，其中的公理是没有经过证明但是视为显然、符合直觉的，被当作演绎的起点。

公理系统是证明论（Proof Theory）的一种系统（也就是说证明论还有其他的系统）

历史上第一个公理系统是 Euclid 的几何公理系统，其形式系统最早由 Hilbert 提出。

证明论

证明

在形式系统$L$中的一个形式证明是指，通过一个公式序列$A_1, A_2, \cdots, A_n$，其中每一个$A_i$是$L$中的一个公理，或者可由此序列中位于前面的两个公式作为应用分离规则的直接后承而得，则称为$L$中$A_n$的一个证明，$A_n$称为$L$中的一个定理（Theorem）。

令$\Gamma$是$L$中的公式集，$L$中的公式序列$A_1, A_2, \cdots, A_n$满足，对于每一个$A_i$，以下之一成立：

• $A_i$是$L$中的一个公理
• $A_i \in \Gamma$
• $A_i$是由序列中位于前面的两个公式作为应用分离规则的直接后承而得

则$A_n$称为从$\Gamma$可演绎的（Deducible），或称为$L$中$\Gamma$的一个后承，记作 $\Gamma \vdash A_n$。若$A$为$\Gamma$ 的某个演绎的最后一项，则称$\Gamma$推出$A$，记作$\Gamma \vdash _LA$或者$\Gamma \vdash A$。

由于$L$中的一个定理是从空集可演绎的，所以记作 $\emptyset \vdash A$，$\vdash A$。这其实是一种情况，在每一个公理系统里面都会有一些东西，他实际上不需要任何一个公理，他就是对的，说的就是这些情况；而其他的一些定理，他们会基于一些公理而推导产生。

$\vdash$是一个元语言的符号，就是说，这是关于形式语言$L$的一个断言。

演绎定理

若$\Gamma \cup {A} \vdash B$，则$\Gamma \vdash A \to B$。(2.7)

逆：若$\Gamma \vdash A \to B$，则$\Gamma \cup {A} \vdash B$。(2.8)

推论：对于任何公式$A, B, C$有：

$$ A \to B, B \to C \vdash A \to C $$

一致性、平凡性和单调性

公式集 $\Gamma$ 是一致的（Consistent），如果$\Gamma$中不存在一个公式$A$，使得$\Gamma \vdash A$和$\Gamma \vdash \sim A$。

公式集 $\Gamma$ 是平凡的（Trivial），如果$\left\lbrace A, \sim A \right\rbrace \subseteq \Gamma$，则任何公式$B$满足$\Gamma \vdash B$。

公式集 $\Gamma$ 是单调的（Monotonic），对于$\Gamma \subseteq \Gamma'$，对于任意公式$A$，如果$\Gamma \vdash A$，则$\Gamma' \vdash A$。

一个公式集$L_0$的公式集$\Gamma$ 是极大一致（Maximally Consistent, MC），如果$\Gamma$是一致的，而且不存在一个一致的公式集$\Gamma'$，使得$\Gamma \subset \Gamma'$。这个集合称为极大一致子集（Maximally Consistent Subset, MCS）。

极大一致的充要条件：当且仅当每个公式$A $，$A \in \Gamma$ 或者 $\sim A \in \Gamma$。

极大一致推理$\vdash_{MCS}$：$\Gamma\vdash_{MCS} A$，当且仅当$MCS(\Gamma) \vdash A$。

证明论下的其他系统

• 公理系统（Hilbert 系统）：公理是不可证的，推理规则是分离规则。
• 自然演绎系统（Gentzen 系统）：公理是不可证的，推理规则是分离规则和引入规则。
• 表系统（Tableaux）：公理是不可证的，推理规则是分离规则和消去规则。

由于上文提及到的连接符的完备性问题，只要有一个完备的连接符，就可以构建一套完备的形式系统。

完全性和可靠性

完全性（completeness）：$\Gamma \vdash A \Leftarrow \Gamma \models A$。

可靠性（soundness）：$\Gamma \vdash A \Rightarrow \Gamma \models A$。

对于这个事情具体的解释，对于一个命题语言$L_0$，其分为语法和语义。二者具有同构关系：

• 语法，包括了符号集（如$\sim$, $\land$, $\lor$, $\to$, $\leftrightarrow$, $p_1, p_2, \cdots$）和公式集(wfs)。
• 语义，就是命题形式和真值函数。

需要验证一个证明是否是有效的，可以使用赋值的办法去验证；但是语法的正确性可以让一个证明可以被机械地检验正确性，就是说这个语法成立那么他一定是正确的。

对于$L_0$的一个形式系统$L$，在语法上，证明论$L \vdash A$基于的是一组公理和推理规则，就是说这个推导是在逻辑上的，而在语义上，$L \models A$是基于真值函数的，就是说这个推导是在指派上的。这二者的统一性要求一个命题演算（形式系统）是完全的和可靠的。

赋值

$L$的一个赋值是一个函数$v$，将$L$中的每个命题变元映射到${T, F}$的一个值。其中要求任意其中的公式满足：

• $v(A) \neq v(\sim A)$
• $v(A \to B) = F$ 当且仅当 $v(A) = T$ 且 $v(B) = F$

模型

上文已经给出了模型的定义。在赋值的角度，也就是说对于$v(A) = T$，则$v$满足$A$，$v$是$A$的模型，$v\models_L A$简称 $v\models A$。

重言式就是对于任意的$v$，$v\models A$，记作$\models_L A$，简称$\models A$。

一个重言式，其对于命题语言是不变的，也就是说，如果一个重言式是真的，那么在任何的命题语言下，这个重言式都是真的。

可靠性定理

$L$中的每一个定理都是一个重言式。

作为推论就是，若$\vdash A$则$\models A$，任何一个与生俱来的定理都是一个重言式。

一致性定理

$L$的一个扩充（extension）就是对于$L$中公理组的修改（包括引入新的定理）而得到的一个新的形式系统。这个定义言下之意就是，一个公理系统他的扩充和他甚至可以没有共同的公理，因为可以全部修改掉。

$L$的一个扩充是一致的，就是要求不允许存在一个$A$，使得$\sim A$和$A$同时是定理。

一致性定理就是说，$L$本身是一致的。这个可以通过反证法证明。这里需要注意的是，这个一致性是指的在$L$内具有一致性，是绝对一致性。可以理解为，在某些其他的扩充中，可能会有一些不一致的地方，但是在$L$内永远是自洽的。

那么对于$L$的一个扩充$L*$，其一致当且仅当存在一个不是定理的公式$A$。

$L*$是$L$的一个扩充，存在一个赋值，使得$L*$的每个定理都为T。

完全性定理

若$A$是一个公式且是重言式，则$\vdash_L A$。可以使用反证法，即$\sim A$存在于$L$但是$\sim A$不是重言式，其赋值不可能为T。

作为推论，若$\models A$则$\vdash A$。

那么可靠性和完全性定理，$\models A$当且仅当$\vdash A$。

对于一个公式，存在一种方式可以判定其为定理。

一些其他内容

• 线路模型（数字电路和布尔代数）
• 命题逻辑的完全性定理证明（Kalmar，1935）
• 直觉主义命题逻辑

模型论

谓词和量词

对于一个推导，如果只有命题逻辑的话，许多的逻辑不能成立。

先定义主谓结构。一个简单命题，用大写字母表示谓词，小写字母表示主词；而复合命题，就是简单命题的细化结果。

全称量词和存在量词，$\forall x P(x)$ 和 $\exists x P(x)$，这里的$x$是变元。对于用量词开始的命题中使用的变元，其称为约束变元，否则称为自由变元。

比如，1+x=2，可以表示为$E(f(1, x), 2)$，其中$f$是一个函数（加法），$E$是一个关系（相等）。这里的$x$是自由变元。

自由变元因为是自由的，所以不能指派真值，而应该通过上下文确定。

$\forall x A(x)$ 和 $\exists x A(x)$ 分别表示存在或者任意的对象满足$A$性质。然后还可以写成$\forall x A(X) \to B(x)$，这个就是一个命题，对于任意满足$A$的$x$，都满足$B$。

同时，我们也可以意识到，不存在就是任意都不，存在就是不是任意都不，也就是说，$\forall x \sim A(x)$ 和 $\sim \exists x A(x)$ 是等价的。

一阶语言

一阶（谓词）语言（演算）（First Order predicate Logic, FOL）是一个在$L$上扩充的更复杂的形式系统。一阶语言的字符表：

• 变元：$x, y, z, x_1, x_2, \cdots$
• 常元：$a, b, c, a_1, a_2, \cdots$
• 谓词符：$A^1_1 A^2_1 A^1_2 \cdots$
• 函项符：$f^1_1 f^2_1 f^1_2 \cdots$
• 技术性符号，如括号和逗号等
• 连接符：$\sim, \to$
• 量词符：$\forall$

其中对于谓词和函项，上标表示元数。比如说一个二元函数，可以表示为$f^2$。

非逻辑符号有的时候使用字符串来表示。函项通常小驼峰，谓词通常大驼峰。

一个一阶语言$L$的字符表是上述的一个子集。

一个$L$-字符的有限（可为空）序列，称为$L$-字符串。对于字符串有几个概念，包括初始段、结束段、子段……不赘述。有两种$L$-串：项和公式。

项是，变元、常元和通过其中函数项产生的新项，递归定义。

可以将一个项解释为一个对象。函数，作用于项，项具有一些属性，并且可以对其做出某些判定。

常元是一个特殊的项，其可以视为函数项的特殊情况，就是一个没有参数的函数。

闭项是不含有变元的项，所有的变元都通过函项符产生；含有变元的项称为开项。

项$t$的度$det(t)$是$t$中的函项符的个数。

原子公式：对于一个谓词符$A^n$和$n$个项$t_1, t_2, \cdots, t_n$，$A^n(t_1, t_2, \cdots, t_n)$是一个原子公式。

合式公式是，所有的原子公式，以及他们通过连接符产生的公式。

命题符就是零元谓词符。$L_0$是一阶语言的一个子集，其只包含命题符。公式$A$的复杂度是指，其中的$\sim$次数乘以1加上$\to$次数乘以2。

为了方便起见，可以利用$\land, \lor, \leftrightarrow$等符号来更简洁地表示一些复杂的逻辑。这本质其实是一样的，可以看作是语法糖。分析含有这些符号的公式的复杂度时，可以将其转换为不含这些符号的公式。

举个例子，我们知道群的定义如下：如果对于一个非空的集合$G$，存在一个运算符$\cdot$，使得对于任意的$a, b, c \in G$，有：

1. 封闭性：$\forall a, b \in G, a \cdot b \in G$
2. 结合律：$\forall a, b, c \in G, (a \cdot b) \cdot c = a \cdot (b \cdot c)$
3. 单位元：$\exists e \in G, \forall a \in G, a \cdot e = e \cdot a = a$
4. 逆元：$\forall a \in G, \exists b \in G, a \cdot b = b \cdot a = e$

对于单位元，可以用如下方式表述：

• $a_1$代表单位元
• $A^2_1$代表相等
• $f^1_1$代表一个求逆元的运算
• $f^2_1$代表一个二元运算

$A^2_1(f^2_1(x_1, f^1_1(x_1)), a_1)$可以表示$a_1$是单位元。

一个$L$-串的权重指的是，变元加-1，n-元函项符和谓词符加n-1，量词符加1，$\sim$加0，$\to$加1。

每一个项具有权重-1，每一个$t$初始子段的权重非负，且每一个公式的权重是唯一确定的。

在公式$\forall xA(x)$中，$A$称为$x$的辖域（Scope）。当这个公式在$B$作为子公式出现的时候，辖域内的变元是约束变元，否则是自由变元。

项替换。对于所有的自由变元，其都可替换。而且替换不应该带来和原式子里面的约束变元冲突的情况。对于具体的替换法则就不赘述了，总之就是，不能替换之后和原来的约束变元冲突，也不能替换约束变元。要考虑变元的名字和作用域。

解释

语义确定一个公式的解释，但是因为这个公式中的某些非逻辑符号依赖于不同的场景可能有不同的意思，因此不能一次性确定所有的含义。那么就引入一个语义抽象的概念，他把这个世界抽象出一系列对象，对于一个谓词符，这些对象会有或者没有对应的这个属性（就是满足或者不满足），并根据这个而赋值为T或者F。FOL假设这就是所有的关于非逻辑符的解释，也因而可以确定了公式的真值。（Tarski，1934）概念化，对象和其之间的关系。

对于一个$L$的解释$I$，由如下组成：

• 一个非空的集合（$I$的论域$D_I$）
• 不同元素（个体集${\bar a,\bar b,\bar c, \cdots}$）
• 一个在$D_I$上的函项集合
• 一个在$D_I$上的关系集合

一阶语言里，对于变元的量词所指的对象在论域中；在某些情况下他并不是，比如如果量词可以解释为某些对象之间的关系，即开始指代谓词了，那么这个语言就称为二阶语言；类似地还有三阶语言等等。比如，每个非空的自然数集都有一个最小的元素，我们这个“自然数集”包含了这些元素，需要判断“元素是最小的”这个谓词，“集合里面存在”这个谓词，因此是一个高阶的语言。

对于一个字符串，可以代入不同的解释，然后其真假才能确定，并且可以不一样。

满足

对于一个解释$I$，其上的一个赋值是从$L$上的项到论域$D_I$的映射$v$。

变元赋值$u: {x_1, x_2, \cdots} \to D_I$。就是给里面每个变元指派一个元素作为其解释。对于一个解释，可以有多个赋值。这个很显然。如果有两个赋值满足除了$x_i$外的一切变元赋值都相同（严格意义上是等效），那么这两个赋值是i-等值的。

满足

$I$的一个赋值$u$满足$A$，记作$I, u \models A$，或者$I, v \models A[u]$，其中$u$是对应的变元赋值。简写成$I \models A$，其就是满足所有的原子公式为真，并且逻辑的关系也都为真。

如果不满足，记作$I \not\models A$。

替换

简单来说就是，对于其中每一个自由变元$x_i$，i-等值的赋值之间可以互相替换。

模型

对于一个公式$A$，如果一个解释$I$的每一个赋值都为真，那么$I$使得$A$为真，是$A$的一个模型，记作$I \models A$。

对于一个含有自由变元的命题，其不真也不假；并且对于不同的解释，一个命题可以是真的或者假的。但是如果$\sim A$是真，那么$A$是假的。

在一个解释中，如果$A$和$(A\to B)$都为真，那么$B$为真。$I \models A$当且仅当$\forall x_1, x_2, \cdots, x_n, I \models A$，其中$x_1, x_2, \cdots, x_n$是$A$中的自由变元。

对于一个公式，假如存在一个赋值$v$满足$(\exists x_i)A$，那么一定存在一个i-等值赋值$v'$满足$A$。

$L$中的一个重言式，其任何一个解释都为真。其实这个也很显然，就是说，一个重言式中的某一部分，可以用一些其他的方式表述，比如“函数的连续性”可以表述为“不存在间断点”，那么，可导一定连续也就可以表述为存在导数的函数一定不会有间断点。

一个没有自由变元的公式称为闭公式。一个闭公式的真假是确定的，因为其不依赖于上下文。即是说，$I \models A$或者$I \models \sim A$。

有效

对于一个公式$A$，如果在$L$下每一个解释都为真，那么他就是逻辑有效的；否则就是逻辑无效的。

为了证明一个公式的有效性，需要枚举所有的解释下的所有的赋值，然后验证其是否为真；而为了证明一个公式的无效性，只需要找到一个解释下的一个赋值使其为假。

所有的重言式都是有效的，但是反之不然。

蕴含关系和逻辑等价

如果$A$的所有模型都是$B$的模型（满足$A$的所有解释都满足$B$），那么$A$蕴含$B$，记作$A \models_K B$，简写为$A \models B$。

如果$A \models B$且$B \models A$，那么$A$和$B$是逻辑等价的，记作$A \equiv B$。

如果$A \models_L B$，那么$A \models_K B$。重言等价则逻辑等价。（一个是PL的概念，一个是FOL的概念）

斯特伦式

简单来说就是，如果有一个公式$\exists x B$，出现在一系列的全称量词的变元辖域内，那么可以删除掉$\exists x$，并且把$x_i$用一个含有其他变元的函项替换，这个替换他的项称为斯特伦项。若其不出现在全称量词的变元辖域内，那么可以用一个新的常元替换，这个常元称为斯特伦常元。

这个过程称为斯特伦化。这个公式称为斯特伦式。

一个例子，对于“人有一个心脏”这个句子，可以这么写：

$$ \forall x.Person(x) \to \exists y.Heart(y) \land Has(x, y) \\ \forall x.Person(x) \to Heart(h(x)) \land Has(x, h(x)) $$

他的目的就是消去量词。

一个公式矛盾当且仅当其斯特伦式是矛盾的。

证明论

回顾一个形式系统的 11 个规则：

• 自反：$A \vdash A$
• 增加前提：若$\Gamma \vdash A$则$\Gamma, B \vdash A$
• 否定消去（归谬）：若$\Gamma, A \vdash B$且$\Gamma, A \vdash \sim B$，则$\Gamma \vdash \sim A$
• 蕴含消去：若$\Gamma \vdash A \to B$且$\Gamma \vdash A$，则$\Gamma \vdash B$
• 蕴含引入：若$\Gamma, A \vdash B$，则$\Gamma \vdash A \to B$
• 合取消去：若$\Gamma \vdash A \land B$，则$\Gamma \vdash A$和$\Gamma \vdash B$
• 合取引入：若$\Gamma \vdash A$和$\Gamma \vdash B$，则$\Gamma \vdash A \land B$
• 析取消去：若$\Gamma \vdash A \lor B$且$\Gamma, A \vdash C$且$\Gamma, B \vdash C$，则$\Gamma \vdash C$
• 析取引入：若$\Gamma \vdash A$，则$\Gamma \vdash A \lor B$和$\Gamma \vdash B \lor A$
• 等价消去：若$\Gamma \vdash A \leftrightarrow B$，则$\Gamma \vdash A \to B$和$\Gamma \vdash B \to A$
• 等价引入：若$\Gamma, A \vdash B$且$\Gamma, B \vdash A$，则$\Gamma \vdash A \leftrightarrow B$

形式推演系统

利用谓词间的各种等值关系和蕴含关系，从一些谓词公式可以推导出另一些谓词公式，这就是一阶谓词的推理。

在一阶谓词中仍然是重言式的蕴含式为推理定律。包括如下几种：

• 代换实例，类似于合取消去和析取引入
• $\sim \exists x A \Leftrightarrow \forall x \sim A$
• 量词分配定律： $$ \forall xA(x) \lor \forall xB(x) \Rightarrow \forall x(A(x) \lor B(x)) \ \exists x(A(x) \land B(x)) \Rightarrow \exists xA(x) \land \exists xB(x) \ \forall x (A(x) \to B(x)) \Rightarrow \forall xA(x) \to \forall xB(x) \ \exists x(A(x) \to B(x)) \Rightarrow \exists xA(x) \to \exists xB(x) $$

加上如下四条：

• 全称量词消去（UI, Universal Instantiation）：$\forall xA(x) \vdash A(t)$，其中$t$是一个项
• 全称量词引入（UG, Universal Generalization）：$A(t) \vdash \forall xA(x)$
• 存在量词引入（EG, Existential Generalization）：$A(t) \vdash \exists xA(x)$
• 存在量词消去（EI, Existential Instantiation）：$\exists xA(x) \vdash A(t)$，其中$t$是一个项（而不是一个变元）

谓词演算

谓词演算指的是形式系统$K_L$，其不固定一个指定的$L$。