数学联邦政治世界观
超小超大

形式化大数数学(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

数学联邦政治世界观提示您:看后求收藏(笔尖小说网http://www.bjxsw.cc),接着再看更方便。

相关小说

蚊子 连载中
蚊子
巟无
oc一号世界观而已
0.5万字9个月前
小刘的发疯日常 连载中
小刘的发疯日常
紫薯LO
神神经经,没有烦恼!啊啊啊啊!
0.5万字5个月前
梦境丶 连载中
梦境丶
女青丶
死后意外进入梦境世界为了再次见到父母她开启了收集情感值的冒险以为事情会顺利进行可梦境背后好像有一个人在监视着一切……
1.0万字3个月前
mbti:多重世界 连载中
mbti:多重世界
星辰梦呓
华倩怜(isfp)在一次上课走神后,意外发现了自己居然拥有异能,更重要的是,这居然跟她失踪了十几年的母亲有关…时空穿越器的出现,让华倩怜来到......
12.0万字2个月前
盗笔综合 连载中
盗笔综合
别让心爱的玫瑰凋落
小哥吴邪他们从西王母宫回来后的一些事情。
0.1万字1个月前
当时间和暗物质交错 连载中
当时间和暗物质交错
QC烔
叶罗丽仙境中,时间和暗物质的关系有微妙的联结。
0.2万字1个月前