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

定义 三元Veblen函数

φ：＝Φ Bin. φ

φ : Ord → Ord → Ord → Ord

φ = Φ Bin.φ

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

φ₀＝Bin. φ

φ₁，₀＝Γ

φ₁，₁＝·ε

φ₁，₂＝·ζ

φ₁，₃＝·η

φ₁＝·φ

φ₂，₀＝·Γ

φ₂，₁＝··ε

φ₂，₂＝··ζ

φ₂，₃＝··η

φ₂＝··φ

φ₃，₀＝··Γ

φ-0 : φ 0 ≡ Bin.φ

φ-0 = refl

φ-1-0 : φ 1 0 ≡ Γ

φ-1-0 = refl

φ-1-1 : φ 1 1 ≡ ε̇

φ-1-1 = refl

φ-1-2 : φ 1 2 ≡ ζ̇

φ-1-2 = refl

φ-1-3 : φ 1 3 ≡ η̇

φ-1-3 = refl

φ-1 : φ 1 ≡ φ̇

φ-1 = refl

φ-2-0 : φ 2 0 ≡ Γ̇

φ-2-0 = refl

φ-2-1 : φ 2 1 ≡ ε̈

φ-2-1 = refl

φ-2-2 : φ 2 2 ≡ ζ̈

φ-2-2 = refl

φ-2-3 : φ 2 3 ≡ η̈

φ-2-3 = refl

φ-2 : φ 2 ≡ φ̈

φ-2 = refl

φ-3-0 : φ 3 0 ≡ Γ̈

φ-3-0 = refl

定理 对于第一个参数为后继的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

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

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

φα⁺，ₗᵢₘ g＝jump λγ，lim λn，φα⁺，g n γ

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

φ-suc-0 = refl

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

φ-suc-suc = refl

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

φ-suc-lim = refl

定理 对于第一个参数为极限的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

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

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

φα⁺，ₗᵢₘ g＝jump λγ，lim λn，φα⁺，g ₙ γ

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

φ-suc-0 = refl

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

φ-suc-suc = refl

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

φ-suc-lim = refl

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