Google 翻译生成的粗略草稿，质量较低。术语依照术语表，但句子可能有误；之后会由仔细的译文取代。

1. 项与关系

1. 符号与组合

数学理论$\mathscr{T}$[^1]的*符号*如下：

(1) 逻辑符号[^2]：$\square$、$\tau$、$\vee$、$\neg$。 (2) 字母。

我们所说的字母是指大写和小写罗马字母，带或不带重音符号。因此 $A$、$A'$、$A''$、$A'''$、... 是字母。在文本的任何地方都可以引入除先前论证中出现的字母之外的字母。

(3) 具体标志，取决于所考虑的理论。

在集合论中，我们将仅使用以下三个特定符号：$=$、$\in$、$\supset$。

$\mathscr{T}$中的*集合*是一系列$\mathscr{T}$的符号写在一个另一个旁边；除字母外，某些符号可以通过线上方的条线连接到对，称为*链接*。 \*对于例，在集合论中，其中$\in$是一个特定的符号，

是一个程序集。\*

单独使用组合会给印刷者和读者带来难以克服的困难。因此，当前文本使用缩写符号（特别是普通语音的字），而不使用属于至形式数学。此类符号的引入就是*定义*的目的。它们的使用“对于理论来说并不是必不可少的”，并且常常会导致混乱，而只有对主题有一定的熟悉程度才能使读者避免这种混乱。

例

2. 代换判据

形式数学包含仅明确写为组合。然而，即使使用缩写符号，严格按照这个原理发展数学也会导致推理的链条非常长。为此，我们应建立与不确定的组合相关的判据；这些判据中的每一个都将一次性描述对这些组合进行确定的序列操作的最终结果。因此，这些判据对于理论来说并不是必不可少的；他们对元数学的辩护属于。

元数学本身的发展在实践中需要使用缩写符号，其中一些已经被指出。大多数这些符号也用于数学中。

我们将使用以下判据，称为 代换判据 ：

CS1。令$A$和$B$为组合，并令$x$和$x'$为字母。如果$x'$没有出现在$A$中，则$(B|x)A$与$(B|x')(x'|x)A$相同。

CS2。令$A$、$B$和$C$为组合，并令$x$和$y$为不同的字母[^3]。如果$y$没有出现在$B$中，则$(B|x)(C|y)A$等同于

其中 $C'$ 是集合 $(B|x)C$。

CS3。 设$A$为集合，$x$和$x'$为字母。如果 $x'$ 没有出现在 $A$ 中，则 $\tau_x(A)$ 与 $\tau_{x'}(A')$ 相同，其中 $A'$ 是程序集 $(x'|x)\,A$。

CS4。 令$A$和$B$为组合，并让$x$和$y$为不同的字母。如果 $x$ 没有出现在 $B$ 中，则 $(B|y)\tau_xA$ 与 $\tau_x(A')$ 相同，其中 $A'$ 是程序集 $(B|y)\,A$。

CS5。 令$A$、$B$、$C$为组合，并令$x$为字母。 组合 $(C|x)(\neg A)$、$(C|x)(\vee AB)$、$(C|x)(\Rightarrow AB)$、$(C|x)(sAB)$（其中$s$为特定符号）分别与$\neg A'$、$\vee A'B'$、$\Rightarrow A'B'$、$sA'B'$相同，其中$A'$、$B'$分别为$(C|x)\,A$、$(C|x)\,B$。

作为例，让我们表示CS2验证的原理。比较将我们从 $A$ 到 $(B|x)(C|y)\,A$ 的运算与将我们从 $A$ 到 $(C|y)(B|x)\,A$ 的运算。在每个运算中，$A$中出现的且与$x$和$y$不同的符号没有改变。在$A$中出现$x$的每个地方，我们都必须在第一个运算中用$B$替换$x$；对于第一个运算，这一点很明显，而对于第二个$y$，它没有出现在$B$中。最后，在$A$中出现$y$的每个地方，第一个运算包含在替换中，$C$代表$y$，然后在$x$出现在$C$中的每个地方，$B$代表$x$；但很明显，这与替换 $y$ 是一样的，无论它出现在 $A$ 中，还是程序集 $(B|x)\,C$。

3. 形成性构造

理论的一些具体标志称为“关系性”，其他则称为“实质性”。每个特定的标志都与自然数相关联，称为 权 （实际上总是数 2）。

¶ 如果一个程序集以 $\tau$ 开头，或以实数符号开头，或由单个字母组成，则称该程序集属于 first 类；否则它是*第二个类*。

¶ $\mathscr{T}$ 理论中的*形成性构造* 是组合的序列，它具有以下性质：对于序列的每个组件$A$，满足以下条件之一：

(a) $A$ 是一个字母。

(b) 在序列中存在第二个类的集合$B$，其位于$A$之前，使得$A$是$\neg B$。

(c) 第二个类（无论是否不同）有两个组合、$B$和$C$，位于$A$之前，使得$A$是$\vee BC$。

(d) 在 $A$ 之前存在第二个类的集合 $B$，以及字母 $x$，使得 $A$ 为 $\tau_x(B)$。

(e) $\mathscr{T}$ 中存在权 $n$ [^4] 的特定符号$s$，以及第一个类的$n$ 组合 $A_1,A_2,\ldots,A_n$，位于 $A$ 之前，使得$A$ 是 $sA_1A_2\ldots A_n$。

出现在 $\mathscr{T}$ 的构成构造中的第一个类的组合（分别为第二个类）在 $\mathscr{T}$ 中称为项（分别为关系）。

4. 形成性判据

CF1。如果$A$和$B$在理论$\mathscr{T}$中是关系，则$\vee AB$在$\mathscr{T}$中是关系。

考虑两个形成的构造（在$\mathscr{T}$中），其中一个包含$A$，另一个$B$。考虑通过先写入第一个构造的组合，然后写入第二个构造的组合，最后写入$\vee AB$来获得组合的序列。由于$A$和$B$属于第二个类，所以立即验证这个序列是$\mathscr{T}$的构成构造。集合$\vee AB$是第二个类的集合，因此它是$\mathscr{T}$中的关系。

以下三个判据的建立方式类似：

CF2。如果$A$在理论$\mathscr{T}$中是关系，则$\neg A$在$\mathscr{T}$中是关系。

CF3。如果$A$在理论$\mathscr{T}$中是关系，并且如果$x$是字母，那么$\tau_x(A)$在$\mathscr{T}$中是项。

CF4。如果 $A_1$、$A_2$、...、$A_n$ 是理论 $\mathscr{T}$ 中的项，并且如果 $s$ 是 $\mathscr{T}$ 中权 $n$ 的关系（或实数）符号，则$sA_1A_2...A_n$ 是$\mathscr{T}$ 中的关系（分别为项）。

这些判据立即意味着以下内容：

CF5。如果$A$和$B$在理论$\mathscr{T}$中是关系，则$\Longrightarrow AB$在$\mathscr{T}$中是关系。

CF6。令$A_1$、$A_2$、...、$A_n$为理​​论$\mathscr{T}$中的形成构造，并令$x$和$y$为字母。假设$y$没有出现在任何$A_i$中。那么$(y|x) A_1$、$(y|x) A_2$、...、$(y|x) A_n$ 是$\mathscr{T}$ 中的构成构造。

为了证明 CF6，令 $A_i'$ 为集合 $(y|x)A_i$。如果$A_i$是一个字母，那么$A_i'$也是一个字母。如果$A_i$属于形式$\neg A_j$，其中$A_j$是构造中位于$A_i$之前的第二个类的集合，则$A_i'$与CS5中的$\neg A_j'$相同，并且$A_j'$是组装第二个类。如果$A_i$是形式$\vee A_jA_k$或$sA_{j_1}A_{j_2}\ldots A_{j_m}$，推理是类似的，$s$是$\mathscr{T}$的特定符号。如果最终$A_i$是形式$\tau_z(A_j)$，其中$A_j$是构造中位于$A_i$之前的第二个类的集合，则需要考虑多种情况：

(a) $z$ 是一个不同于 $x$ 和 $y$ 的字母。那么$A_i'$与CS4中的$\tau_z(A_j')$相同，$A_j'$是第二个类的集合。

(b) $z$ 与 $x$ 相同。那么$A_i$不等于包含$x$，因此$A_i'$与$A_i$相同，也就是说与$\tau_x(A_j)$相同；由于$y$没有出现在$A_j$中，所以$\tau_x(A_j)$与CS3中的$\tau_y(A_j)$相同。

(c) $z$ 与$y$ 相同。那么$A_i$就是集合$\tau A_j$，因为$y$没有出现在$A_j$中；因此$A_i'$是$\tau A_j'$的集合，即$\tau_u(A_j')$，其中$u$是$A_j'$中没有出现的字母。

CF7。 在理论$\mathscr{T}$中，令$A$为关系（分别为项），并令$x$和$y$为字母。那么 $(y|x)A$ 就是 $\mathscr{T}$ 中的关系（或项）。

令 $A_1,A_2,\ldots,A_n$ 为形成构造，其中出现$A$。我们将逐步证明，如果$A_i$是关系（分别是项），那么$(y|x)A_i$（我们用$A_i'$表示）也是关系（分别是项）。假设这个点已经为$A_1,A_2,\ldots,A_{i-1}$成立；让我们证明$A_i$。如果$A_i$是一个字母，那么$A_i'$也是一个字母。如果构造中$A_i$位于关系$A_j$之前，使得$A_i$等于$\neg A_j$，则$A_i'$与CS5中的$\neg A_j'$相同，并且$\neg A_j'$与CF2中的关系相同。如果 $A_i$ 前面有关系 $A_j,A_k$，使得 $A_i$ 是 $\vee A_jA_k$，或者如果 $A_i$ 前面有项 $A_{j_1},\ldots,A_{j_m}$，使得 $A_i$ 是 $sA_{j_1}\cdots A_{j_m}$，则参数类似，其中$s$是权$m$的$\mathscr{T}$的特定符号。最后，如果$A_i$前面是关系$A_j$，使得$A_i$是$\tau_z(A_j)$，则需要考虑多种情况：

(a) $z$ 不同于 $x$ 和 $y$。那么$A_i'$与CS4中的$\tau_z(A_j')$相同，并且我们已经知道$A_j'$是关系；因而，根据 CF3，$A_i$ 为项。

(b) $z$ 与 $x$ 相同。那么 $A_i$ 不等于包含 $x$，因而 $A_i'$ 与 $A_i$ 相同，因此是项。

(c) $z$ 与$y$ 相同。然后令$u$为一个字母，与$x$和$y$都不同，它不会出现在$A_1,A_2,\ldots,A_j$中。通过CF6，组合$(u|y)A_1,\ldots,(u|y)A_j$的序列（我们用$A_1'',\ldots,A_j''$表示）构成了$\mathscr{T}$中的构成构造。由于$y$不再出现在这个新的构造中，$(y|x)A_1'',\ldots,(y|x)A_j''$是CF6形成的构造，所以$(y|x)A_j''$是$\mathscr{T}$中的关系；因而 $\tau_u((y|x)A_j'')$ 是 $\mathscr{T}$ 的项。但是这个项与CS4的$(y|x)\tau_u(A_j'')$相同，因此与CS3的$(y|x)\tau_y(A_j)$相同，因此与$A_i$相同。

CF8。令$\mathscr{T}$中的$A$为关系（或项），令$x$为字母，$\mathscr{T}$中的$T$项。那么$(T|x)A$在$\mathscr{T}$中就是关系（分别是项）。

令 $A_1, A_2, \ldots, A_n$ 为形成构造，其中出现$A$。令 $x_1, x_2, \ldots, x_p$ 为$T$ 中出现的不同字母。让我们将每个字母$x_i$与一个字母$x_i'$关联起来，与每个字母$x_1, \ldots, x_p$和$A_1, \ldots, A_n$中出现的字母不同，这样字母$x_1', \ldots, x_p'$都是不同的。大会

CF7 为项 $T'$，$(T|x)A$ 与

通过应用CS1。因而，只要证明 $(T'|x)\,A$ 是关系（或项）即可；在其他字中，我们可以假设从现在起$T$中出现的字母不会出现在$A_1, \ldots, A_n$中。

¶ 我们将逐步证明，如果$A_t$是关系（分别是项），那么$(T|x)\,A_t$（我们将用$A_t'$表示）是关系（分别是项）。假设对于$A_1,A_2,\ldots,A_{i-1}$这个点已经成立，让我们对$A_i$证明它。如果$A_i$是一个字母，那么$A_i'$要么是同一个字母，要么是$T$，因此项。如果$A_i$是形式$\neg A_j$，其中$A_j$是关系，在构造中它在$A_i$之前，那么$A_i$与CS5中的$\neg A_j'$相同，并且我们已经知道$A_j'$是关系，因而 $A_i'$ 通过 CF2 等于关系。如果 $A_i$ 是形式 $\vee A_jA_k$ 或 $sA_{j_1}\ldots A_{j_m}$，证明是类似的。最后，如果$A_i$是形式$\tau_z(A_j)$，其中$A_j$是关系，并且在构造中先于$A_i$，则需要考虑多种情况：

(a) $z$ 不同于$x$ 以及$T$ 中出现的字母。那么$A_i'$与CS4中的$\tau_z(A_j')$相同，并且我们已经知道$A_j'$是关系；因此CF3 $A_i'$ 是项。

(b) $z$ 与$x$ 相同。那么 $A_i$ 不会包含 $x$，因而 $A_i'$ 与 $A_i$ 相同，因此是项。

(c) $z$ 出现在 $T$ 中。那么$z$不会出现在$A_j$中，因而$A_i'$与$\tau A_j'$相同；因而 $A_i'$ 与 $\tau A_j'$ 相同。现在，我们已经知道$A_j'$是关系，$\tau A_j'$与$\tau_u(A_j)$相同，其中$u$是$A_j$中没有出现的字母；由CF3可知$A_i'$是项。

直观上，如果$\mathscr{T}$中$A$是关系，我们可以将其视为表达对象$x$的性质，断言$(B|x)\,A$相当于说，对象$B$有这个性质。如果$A$在$\mathscr{T}$中是项，则它表示一个对象在某种程度上依赖于$x$表示的对象； 项$(B|x)\,A$表示当我们将$x$作为对象$B$时，对象$A$会变成什么。

习题

参见习题为 § 1。

[^1]: The meaning of this expression will become clear as the chapter progresses. [^2]: For the intuitive meanings of these signs, see no. 3, Remark. [^3]: In accordance with what was said in no. 1, the phrase “$x$ and $y$ are distinct letters” is an abuse of language: it means that $x$ and $y$ denote distinct letters in the assemblies under consideration. [^4]: As was said above, it would be possible, for the development of present-day mathematical theories, to limit our consideration to specific signs of weight 2, and consequently to avoid using the expression “natural number $n$” in the definition of a formative construction.