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

形式化大数数学(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),接着再看更方便。

相关小说

黑爷求别痞 连载中
黑爷求别痞
如素的风
黑爷身份:神秘莫测的传奇人物,拥有强大的实力和不可深测的背景。性格:冷酷而潇洒,不羁中透露出几分温柔与宠溺。他看似玩世不恭,实则内心深藏不露......
2.2万字6个月前
青山不知语(红线) 连载中
青山不知语(红线)
鱼头煲鸡汤
原以为自己是没有父亲的,结果等自己母亲死了才知道母亲谈了一个异世界的人,被接回去的时候才知道,自己还有一个姐姐,但这个姐姐很不喜欢她。可以说......
3.5万字5个月前
十二星座:与你共存 连载中
十二星座:与你共存
柒染qire
地方叫尔晴洛漓簇使,那里的人培养十二星座,可有一天,一个名叫泫雅的,带领了一群黑衣人闯入了尔晴洛漓簇。她们拿走了族中最珍贵的伊克斯宝石,它是......
2.5万字5个月前
什么时候才能当主角 连载中
什么时候才能当主角
到处随逛
穿越剧情,星越祈穿越到各个剧情中,填各种的坑,填完之后还要带队友做业务,呵呵,不过越来越爽是怎么回事?
0.9万字4个月前
时钟妤你 连载中
时钟妤你
沈噫予
茫茫人海与你相遇,这是真正的幸运
0.2万字2个月前
恋爱的九九八十一面 连载中
恋爱的九九八十一面
春敬惊
有虐男师徒恋正常恋爱与笔下角色相恋...你想看的脑洞它都有
2.1万字1个月前