[list][*]

基础：一个全局的、离散的时间轴 t : T。

[*]

判断：核心的判断不再是 a : A （a是A类型的项），而是 a @ t : A （在时间t，a被生成并属于类型A）。或者更进一步，是 R ⊢ a @ t : A （规则R在时间t输出了a，并将其归入类型A）。

[*]

类型形成规则：类型本身的形成也是时间相关的。
A @ t Type 表示类型A在时间t已经形成。
A -> B 这个函数类型，只能在时间 t > max(t_A, t_B) 之后形成，其中 t_A 和 t_B 是A和B形成的时间。

[*]

无限：引入一个“未来模态” ◇。◇P 表示“在未来的某个时间，命题P为真”。那么“潜在无限”就可以表述为 ∀n:ℕ, ◇(∃m:ℕ, m > n)。我们永远不断言一个完成了的无限集合 ℕ 的存在，只断言其无限的可能性。

[/list]

这是一个富有生产力的“谬论”

思想实验绝非荒谬。它是一个：

[list=1][*]

批判性的工具：它强迫我们重新审视数学中那些我们视为理所当然的“自明真理”（如无限、连续），并追问它们的认知和物理根源。

[*]

建构性的蓝图：它为开发更适合描述计算、认知和物理过程的数学基础提供了一个极具启发性的蓝图。在人工智能、复杂系统建模和量子引力理论中，这种“过程本体论”的数学可能比静态的集合论更有用。

[*]

哲学的深化：它将“时间”和“生成”带入了数学的本体论讨论，这是一个非常深刻的哲学推进。

[/list]