形式化大数数学（1.2-Veblen函数）一 (5-2)

Φ : (Ord → Ord) → Ord → Ord → Ord

Φ F = rec F fixpt (λ φ[_] → jump λ β → lim λ n → φ[ n ] β)

注意 极限步的跳出操作是反直觉的一步. 从通常的定义式反推不难发现这里需要跳出. 仔细分析二元Veblen函数的序性质才能更好的理解这里跳出的动机, 具体可以参看 Agda大序数(9) 二元Veblen函数. 这里只需简单的理解为是为了更好的性质和更高的增长率就行了.

定义 二元Veblen函数

φ：＝Φ λα，ωα

φ : Ord → Ord → Ord

φ = Φ (ω ^_)

我们习惯将最后一个参数之前的所有参数都写成下标.

例 由定义, 以下等式成立.

φ₀＝λα，ωα

φ₁＝ε

φ₂＝ζ

φ₃＝η

φ-0 : φ 0 ≡ ω ^_

φ-0 = refl

φ-1 : φ 1 ≡ ε

φ-1 = refl

φ-2 : φ 2 ≡ ζ

φ-2 = refl

φ-3 : φ 3 ≡ η

φ-3 = refl

定理 对于第一个参数为后继和极限的情况, 由定义, 有以下等式成立.

φα⁺＝fixpt φα

φₗᵢₘ f＝jump λα，lim λn，φ f ₙ α

φ-suc : φ (suc α) ≡ fixpt (φ α)

φ-suc = refl

φ-lim : φ (lim f) ≡ jump λ α → lim λ n → φ (f n) α

φ-lim = refl

为了对jump 的行为有更加直观的感受, 对第一个参数为极限的情况, 我们对第二个参数再次分成零, 后继和极限的情况进行讨论, 有如下等式成立.

φₗᵢₘ f0＝lim λn，φ f ₙ 0

φₗᵢₘ f(β⁺)＝lim λn，φ f ₙ (φlim f β)⁺

φₗᵢₘ f(lim g)＝lim λn，φₗᵢₘ f (g n)

φ-lim-0 : φ (lim f) 0 ≡ lim λ n → φ (f n) 0

φ-lim-0 = refl

φ-lim-suc : φ (lim f) (suc β) ≡ lim λ n → φ (f n) (suc (φ (lim f) β))

φ-lim-suc = refl

φ-lim-lim : φ (lim f) (lim g) ≡ lim λ n → φ (lim f) (g n)

φ-lim-lim = refl

很快, 我们来到了二元Veblen函数的能力极限.

定义 对函数 λα，φα 0 取不动点枚举, 得到的函数称为 Γ.

Γ：＝fixpt λα，φα 0

Γ : Ord → Ord

Γ = fixpt λ α → φ α 0

例 最小的 Γ 数是

Γ₀＝φφφφ…0 0 0 0

Γ-0 : Γ 0 ≡ iterω (λ α → φ α 0) 0

Γ-0 = refl

没有什么能阻止我们继续取不动点枚举. 将Γ 看作新的 λα，ωα， 我们可以得到所谓第二代 ε，ζ，η 函数, 分别记作 ·ε，·ζ，·η.

·ε＝fixpt Γ

·ζ＝fixpt ·ε

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。