形式化大数数学（1.2-Veblen函数）二

定义 四元Veblen函数‬

φ：＝Φ Tri. φ

φ : Ord → Ord → Ord → Ord → Ord

φ = Φ Tri.φ

例 第一个参数从无效到刚开始生效, 由定义, 有以下等式成立.

φ₀＝Tri. φ

φ₁，₀，₀＝fixpt λα，Tri. φα，₀ 0

φ-0 : φ 0 ≡ Tri.φ

φ-0 = refl

φ-1-0-0 : φ 1 0 0 ≡ fixpt (λ α → Tri.φ α 0 0)

φ-1-0-0 = refl

定理 中间两个参数为零, 讨论第一个参数为后继和极限的情况, 由定义, 有以下等式成立.

φα⁺，₀，₀＝fixpt λβ，φα，ᵦ，₀ 0

φₗᵢₘ f，₀，₀＝jump λβ，lim λn，φ f ₙ，ᵦ，₀ 0

φ-suc-0-0 : φ (suc α) 0 0 ≡ fixpt λ β → φ α β 0 0

φ-suc-0-0 = refl

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

φ-lim-0-0 = refl

定理 将 φα 看作一个固定的函数, 类似地, 有以下等式成立.

φα，ᵦ⁺，₀＝fixpt λᵧ，φα，ᵦ，ᵧ 0

φα，ₗᵢₘ g，₀＝jump λᵧ，lim λn，φα，g ₙ，ᵧ 0

φ-α-suc-0 : φ α (suc β) 0 ≡ fixpt λ γ → φ α β γ 0

φ-α-suc-0 {α = zero} = refl

φ-α-suc-0 {α = suc _} = refl

φ-α-suc-0 {α = lim f} = refl

φ-α-lim-0 : φ α (lim g) 0 ≡ jump λ γ → lim λ n → φ α (g n) γ 0

φ-α-lim-0 {α = zero} = refl

φ-α-lim-0 {α = suc _} = refl

φ-α-lim-0 {α = lim f} = refl

定理 将 φα，ᵦ 看作一个固定的函数, 类似地, 有以下等式成立.

φα，ᵦ，ᵧ⁺＝fixpt φα，ᵦ，ᵧ

φα，ᵦ，ₗᵢₘ ₕ＝jump λδ，lim λn，φα，ᵦ，ₕ ₙ δ

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

φ-α-β-suc {α = zero} {β = zero} = refl

φ-α-β-suc {α = zero} {β = suc _} = refl

φ-α-β-suc {α = zero} {β = lim _} = refl

φ-α-β-suc {α = suc _} {β = zero} = refl

φ-α-β-suc {α = suc _} {β = suc _} = refl

φ-α-β-suc {α = suc _} {β = lim _} = refl

φ-α-β-suc {α = lim _} {β = zero} = refl

φ-α-β-suc {α = lim _} {β = suc _} = refl

φ-α-β-suc {α = lim _} {β = lim _} = refl

φ-α-β-lim : φ α β (lim h) ≡ jump λ δ → lim λ n → φ α β (h n) δ

φ-α-β-lim {α = zero} {β = zero} = refl

φ-α-β-lim {α = zero} {β = suc _} = refl

φ-α-β-lim {α = zero} {β = lim _} = refl

φ-α-β-lim {α = suc _} {β = zero} = refl

φ-α-β-lim {α = suc _} {β = suc _} = refl

φ-α-β-lim {α = suc _} {β = lim _} = refl

φ-α-β-lim {α = lim _} {β = zero} = refl

φ-α-β-lim {α = lim _} {β = suc _} = refl

φ-α-β-lim {α = lim _} {β = lim _} = refl

例 一个很大的大数：

ₒₒₘ₂：＝fφΓ₀，₀，₀ (0) (99)

oom₂ = FGH.f (QuaternaryVeblen.φ (BinaryVeblen.Γ 0) 0 0 0) 99

本文使用 WPL/s 发布 @GitHub