有限模型论/预备知识

一阶逻辑 (FO)

维基百科在 一阶逻辑 中有相关信息

我们在这里只对 FO 做一个非常粗略的总结。可以在 FO 中找到介绍。

语法

语法只是关于符号序列。FO 的字母表包括

变量 $x_{0},x_{1},x_{2},...$
逻辑连接词： $\neg$ , $\land$
量词： $\exists$
等式： $\equiv$
括号：), (
n 元关系符号，对于没有或多个 n>0，例如 R(., .)
常数符号（没有或多个）

括号的处理方式是“通常”的，在此不再做进一步的正式描述。

对于给定的符号集 S，变量和常数符号被称为 S-项。

S-表达式通过以下规则的多次应用得到

$t_{1}\equiv t_{2}$ 是一个表达式
$Rt_{1}...t_{n}$ 是一个表达式，对于 n 元关系符号 R
$\neg \varphi ,\varphi _{1}\land \varphi _{2}$ 是表达式
$\exists _{x}\varphi$ 是一个表达式

其中 $t_{.}$ 是一个项， $\varphi _{.}$ 是一个表达式。

因此，可以定义 OR、IMPLICATION、EQUIVALENCE 等的附加连接词，以及 FOR ALL 量词。

语义

语义通过三个步骤为语言添加意义

首先，它定义了逻辑符号（连接词和量词）的含义（这在 FO 中始终成立），
其次，它将关系符号和常数符号映射到给定实体集上的实际关系和常数（这通常由主题定义，例如分析或统计），以及
第三，它将自由变量（未绑定到量词）映射到实体（通常由问题定义，例如求解方程）。

首先，我们假设逻辑符号 $\neg ,\land ,...,\exists$ 具有通常的含义。

其次，S-结构是 (A, a) 的一对，

一个非空集 A，即宇宙，和
从 S 到 a 的映射，使得
- 每个 n 元关系符号都被映射到 A 上的 n 元关系，并且
- 每个常数符号都被映射到 A 的一个元素

一个解释是，一对 $({\mathfrak {A}},\beta )$ ，其中 ${\mathfrak {A}}$ = (A, a) 是一个 S 结构，并且 $\beta$ 是一个将所有自由变量映射到 A 中的一个元素的映射。

如果一个解释是对一组 S 表达式 $\Phi$ （ ${\mathfrak {I}}\vDash \Phi$ ）的 **模型**，当且仅当以下所有条件成立：

${\mathfrak {I}}(t_{1})={\mathfrak {I}}(t_{1})$ ，对于 ${\mathfrak {I}}\vDash t_{1}\equiv t_{2}$
$R^{n}{\mathfrak {I}}(t_{1}),...,{\mathfrak {I}}(t_{n})$ ，对于 ${\mathfrak {I}}\vDash Rt_{1}...t_{n}$
不 ${\mathfrak {I}}\vDash \varphi$ ，对于 ${\mathfrak {I}}\vDash \neg \varphi$
${\mathfrak {I}}\vDash \varphi _{0})$ 并且 ${\mathfrak {I}}\vDash \varphi _{1})$ ，对于 ${\mathfrak {I}}\vDash \varphi _{0}\land \varphi _{1}$
存在一个 $a\in A$ 使得 ${\mathfrak {I}}\vDash \varphi (a)$ ，对于 ${\mathfrak {I}}\vDash \exists _{x}\varphi (x)$

游戏

维基百科在 博弈论 中有相关信息

一个游戏由以下内容描述：

它的玩家（>1）
它的规则，即谁在何时玩以及允许做什么
它的可能结果和收益。

更正式地说，它是一个元组 (P, T, m, u)，其中

P（玩家）是一个集合，其中 |P| = n > 1
T 是一个在节点集上的图，形成一个分类法，即 T 是一棵具有指定根节点的树。叶子被称为终结节点 T，所有其他节点都是决策节点 D。这描述了可能的移动序列。
m 是从 D 到 P 的映射，它表示在哪个点谁应该移动。
u 是一组映射 u_i（每个玩家 i 一个），从 T 到有序集合 U，它给出每个玩家在每个终结节点的收益。

我们在这里以及在下面假设每个玩家都拥有完美信息（因此以上定义是不完整的），即所有玩家到目前为止的所有移动，我们不考虑随机移动。关于规则和玩家的常识是默认假设的。以上称为博弈的扩展形式表示。其他形式，如规范形式表示，对这个做了简化假设（例如，关于信息）并使用策略的概念而不是单一移动。

注意不同的移动会导致相同的“位置”，即一个位置可以在一个博弈树中被表示多次。并且，相同的收益对于不同的玩家可以有不同的意义。

结构上的同构

同态

同构

来回方法

由于以下原因，计算一个集合可能会变得很混乱

以非自然顺序计算事物
多次计算元素

...

方法

固定基础集的枚举（无重复）

{\begin{matrix}A&=&\{\,a_{1},a_{2},a_{3},\dots \,\},\\\\B&=&\{\,b_{1},b_{2},b_{3},\dots \,\}.\end{matrix}}

现在我们构造一个 A 和 B 之间的一一对应关系，它是严格递增的。最初 A 中的成员没有与 B 中的任何成员配对。

(1) 令 i 为最小的索引，使得 a_i 还没有与 B 中的任何成员配对。令 j 为最小的索引，使得 b_j 还没有与 A 中的任何成员配对并且 a_i 可以与 b_j 配对，符合配对必须严格递增的要求。将 a_i 与 b_j 配对。

(2) 令 j 为最小的索引，使得 b_j 还没有与 A 中的任何成员配对。令 i 为最小的索引，使得 a_i 还没有与 B 中的任何成员配对并且 b_j 可以与 a_i 配对，符合配对必须严格递增的要求。将 b_j 与 a_i 配对。

(3) 返回步骤(1)。

仍然需要检查步骤(1)和(2)中要求的选择是否可以根据要求实际进行。以步骤(1)为例

如果 A 中已经有与 B 中的 b_p 和 b_q 分别对应的 a_p 和 a_q，使得 $a_{p}<a_{i}<a_{q}$ 并且 $b_{p}<b_{q}$ ，我们使用密度在 b_p 和 b_q 之间选择 b_j。否则，我们使用 B 既没有最大值也没有最小值的事实来选择合适的较大或较小元素。在步骤(2)中做出的选择是双重可能的。最后，构造在可数的许多步骤之后结束，因为 A 和 B是可数无穷的。注意我们必须使用所有先决条件。

如果我们只迭代步骤(1)，而不是来回迭代，那么生成的配对将无法双射。