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

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

相关小说

沐心归尘 连载中
沐心归尘
岑夏仲月
死去多年的混沌时代前最强者沐汐突然重生为人,并遇到无心的尘归,二人一见钟情,那么接下来会发生什么呢?
8.8万字6个月前
凡人修仙恋 连载中
凡人修仙恋
夜风花
这个是第一次写,写不好大家可以不看,
0.2万字5个月前
巷来巷往 连载中
巷来巷往
139***084_7062947698
3.0万字4个月前
山茶花的思念 连载中
山茶花的思念
在上不是南北~
0.7万字3个月前
五行传奇 连载中
五行传奇
柒茉_
这个嘛……剧透?打咩!想知道内容就进来看看叭~(灵感来源于小学时和好朋友玩的角色扮演小游戏~)
2.3万字2个月前
禁止觊觎貌美向导 连载中
禁止觊觎貌美向导
谢家小螃蟹
朝九晚六的打工牛马安暖暖一朝穿越来到哨向世界,这里向哨比例达到1:900000,白塔向导数量告急,圣所三番四次搜寻向导。安暖暖只想贯彻咸鱼生......
11.1万字1个月前