TON记号：修订间差异

←上一编辑下一编辑→

可视化wikitext

2026年6月23日 (二) 15:24的版本

合法表达式

常量包含 $0, Ω_{n}$ 。

常量是合法表达式；
如果 $a$ 和 $b$ 是合法表达式，那么 $C (a, b)$ 是合法表达式。

后缀形式

对于一个合法表达式，我们删去它其中的所有 $,$ 与 $()$ ，并反转整个字符串，即为该表达式的后缀形式。

比较

对于两个合法表达式，它们的大小关系等同于它们的后缀形式在字典序上的大小关系（我们认为 $C < 0 < Ω_{n}$ ）。

标准表达式

常量是合法表达式；
C(a,b)是标准表达式当且仅当：
- $a, b$ 是标准表达式；
- 如果 $b$ 能表示成 $C (c, d)$ 的形式，则 $a \leq c$ ；
- 对于不同的版本，还有一些额外的条件，我们一般称其为 built-from-below 条件。

为了检查 built-from-below 条件，我们需要遍历某些表达式的语法树，为此，我们需要一些辅助定义：

位于不同位置的同类型的项被认为是不同的；
对于一个表达式 $C (a, b)$ ，我们称 $a$ 和 $b$ 是 $C (a, b)$ 的子项，记作 $a, b ⊑ C (a, b)$ ；
我们称a是b的真子项（记作 $a ⊏ b$ ），当且仅当 $a ⊑ b \land a \neq b$ 。

与序数的关系

TON 中的标准表达式和序数一一对应。具体的，对于一个标准表达式 $a$ ，如果有一系列小于它的表达式 $b_{1}, b_{2} \dots$ ，则 $a$ 对应的序数为 $b_{1}, b_{2} \dots$ 对应的序数的上确界。

性质

$C (a, b) > b$ ；
$C (a, b)$ 对 $a, b$ 都单调递增，且对 $a$ 连续；
$C (a, b) = b + ω^{a}$ 当且仅当 $C (a, b) \geq a$ 。

变种

以下判定条件中涉及到的项 $x$ 默认满足 $x ⊑ a$ 。

Built-from-below 风格

有三种 built-from-below 风格：Degrees of Reflection 风格，标准风格与 Iteration 风格（从弱到强排序）。

Degrees of Reflection 风格

为了检查 $C (a, b)$ 是否标准，built-from-below 条件为 $a ≺ C (a, b)$ ，其定义为：

$\forall x \forall y ⊏ x (x < y < Ω \Rightarrow \exists z ⊒ y (z < Ω \land (z ⊐ x \lor z < C (a, b))))$

Degrees of Reflection（DR）仅由 Degrees of Reflection 风格判定标准表达式。

标准风格

为了检查 $C (a, b)$ 是否标准，built-from-below 条件为 $a ≺_{n} C (a, b)$ ，其定义为：

$a ≺_{0} b \Leftrightarrow a < b$ ；
$a ≺_{m + 1} b \Leftrightarrow \forall x (x > a \Rightarrow \exists y ⊒ x (y ≺_{m} b))$ 。

Main Ordinal Notation System（M）是一系列系统，仅由标准风格判定标准表达式，其中的n可任取 $\geq 1$ 的自然数，分别对应不同的系统。

Iteration 风格

为了检查 $C (a, b)$ 是否标准，我们需要找出 $a$ 的语法树中所有极长的 $< Ω$ 的子项 $a^{'}$ （即找出所有 $a^{'}$ 满足 $\forall x ⊐ a^{'} (x \geq Ω)$ ），然后，我们按以下步骤对每个求出对应的：

将中的改成；
将改写成前缀形式（直接删去所有和）；
删去对应的左侧的全部内容，并在左侧添加使表达式合法；
将重新改写回一般形式。
对所有形如的项，如果，就将其替换为，一直替换到没有这样的项；
执行完 1~5 步后，将现在的记作；
记为初始的和的最长公共后缀（前缀形式下）；
则为最大的自然数使得的前缀形式形如。

该风格的 built-from-below 条件为对所有，都有，其定义如下：

；
。

Iteration of n-built from below (variation without 4b)（I）仅由 Iteration 风格判定标准表达式。

Passthrough

Passthrough 有三种类型：无 passthrough，-passthrough 与 -passthrough（从弱到强排序）。

-passthrough

-passthrough 可以和 Iteration 风格组合，这就是 Iteration of n-built from below（IBP）。的定义和无 passthrough 的情况一样，但 built-from-below 条件不同：为检查是否标准，该风格的 built-from-below 条件为对所有，都有，其定义如下：

我们定义辅助函数：，下同；
；
。

passthrough 也可以和 Degrees of Reflection 风格组合，这就是 Built-from-below with Passthrough（BP）。其定义和其他变种有较大不同，见下：

合法表达式：

是合法表达式；
如果是合法表达式，则是合法表达式。

比较：

是最小的表达式。当且仅当。

标准表达式：

是标准表达式；
是标准表达式当且仅当：
- 是标准表达式；
- 如果可以表示成的形式，则；
- 该系统的 built-from-below 条件为：，其中的定义为。

passthrough 不能和标准风格组合。

-passthrough

-passthrough 可以和 Iteration 风格组合，这就是 Iteration of n-built from below (Possible extension)（IP）。其定义几乎与 IBP 一样，除了 built-from-below 条件，它变成了对所有，都有。

passthrough 也可以和 Degrees of Reflection 风格组合，这就是 Degrees of Reflection with Passthrough（DRP）。为检查是否标准，built-from-below 条件为，其定义为

passthrough 还可以和标准风格组合，这就是 Main ordinal notation system (Passthrough extension)（MP）。和 Main ordinal notation system 类似，它也是一系列系统的组合。我们需要确定一个的自然数，则 built-from-below 条件为，其定义为

；
。

反射配置

反射配置从底层重新定义了 built-from-below 条件。

语法

在反射配置下的 TON 中，表达式会出现一个新的符号。其余部分和普通的 TON 一样。

比较和普通的 TON 类似，我们认为。

定义

反射配置由两个项来定义，记作。以下是反射配置的一个递归定义：

；
；
我们设，则：
- 若：；
- 若：；
- 若且：；
- 若且：。

反射配置可以和 Degrees of Reflection 风格组合（即 Reflection configuration version of Degrees of Reflection（DRC））。为了检查是否标准，其 built-from-below 条件为：

我们定义为满足的项，如果不存在这样的，则；
对于项，我们定义。

反射配置也可以和带 Passthrough 的 Degrees of Reflection 风格组合（即 Reflection configuration version of Degrees of Reflection with Passthrough（DRPC），注意这里不分 -passthrough 和 -passthrough）。为了检查是否标准，其 built-from-below 条件为：

反射配置可以和标准风格（与 -passthrough）组合，同样的，它是一系列记号的组合。你需要确定一个自然数，则为了检查是否标准，反射配置和标准风格的组合（即 Reflection configuration version of Main Ordinal Notation System（MC））的 built-from-below 条件为，而反射配置和带 -passthrough 的标准风格的组合（即 Reflection configuration version of Main ordinal notation system (Passthrough extension)（MPC））的 built-from-below 条件为。的定义如下：

；
；
我们定义为满足的项，如果不存在这样的，则；
；
我们称，当且仅当；
我们称，当且仅当。

@@ 第24行： / 第24行： @@
 * 位于不同位置的同类型的项被认为是不同的；
 * 对于一个表达式<math>C(a,b)</math>，我们称<math>a</math>和<math>b</math>是<math>C(a,b)</math>的子项，记作<math>a,b\sqsubseteq C(a,b)</math>；
-* 我们称a是b的真子项（记作<math>a\sqsubset b</math>），当且仅当<math>a\sqsubseteq b\land a\neq b</math>。
+* 我们称a是b的真子项（记作<math>a\sqsubset b</math>），当且仅当<math>a\sqsubseteq b\and a\neq b</math>。
 == 与序数的关系 ==
@@ 第44行： / 第44行： @@
 为了检查<math>C(a,b)</math>是否标准，built-from-below 条件为<math>a\prec C(a,b)</math>，其定义为：
-<math>\forall x\forall y\sqsubset x(x<y<\Omega\Rightarrow</math>
+<math>\forall x\forall y\sqsubset x(x<y<\Omega\Rightarrow\exists z\sqsupseteq y(z<\Omega\and(z\sqsupset x\or z<C(a,b))))</math>
 Degrees of Reflection（DR）仅由 Degrees of Reflection 风格判定标准表达式。
 ==== 标准风格 ====
-为了检查  是否标准，built-from-below 条件为 ，其定义为：
+为了检查<math>C(a,b)</math>是否标准，built-from-below 条件为<math>a\prec_nC(a,b)</math>，其定义为：
-* ；
+* <math>a\prec_0b\Leftrightarrow a<b</math>；
-* 。
+* <math>a\prec_{m+1}b\Leftrightarrow\forall x(x>a\Rightarrow\exists y\sqsupseteq x(y\prec_mb))</math>。
-Main Ordinal Notation System（M）是一系列系统，仅由标准风格判定标准表达式，其中的  可任取  的自然数，分别对应不同的系统。
+Main Ordinal Notation System（M）是一系列系统，仅由标准风格判定标准表达式，其中的n可任取<math>\geq1</math>的自然数，分别对应不同的系统。
 ==== Iteration 风格 ====
-为了检查  是否标准，我们需要找出  的语法树中所有极长的  的子项 （即，找出所有  满足 ），然后，我们按以下步骤对每个  求出对应的 ：
+为了检查<math>C(a,b)</math>是否标准，我们需要找出<math>a</math>的语法树中所有极长的<math><\Omega</math>的子项<math>a'</math>（即找出所有<math>a'</math>满足<math>\forall x\sqsupset a'(x\geq\Omega)</math>），然后，我们按以下步骤对每个  求出对应的 ：
 # 将  中的  改成 ；