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

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

相关小说

团宠:有五个不熟悉的哥哥怎么办? 连载中
团宠:有五个不熟悉的哥哥怎么办?
悦雪风吟
作为一个身体不好的小孩子,爸妈为了让她养好身体,带她回到了山上的奶奶家,与奶奶父母一起生活,彼时大哥已经完全有能力接管公司,父母便安心照顾她......
1.2万字5个月前
穿成电竞文里的菜鸡小炮灰 连载中
穿成电竞文里的菜鸡小炮灰
哒布吉呀
#年度MVP选手林宿雨穿书了#(双男主)(文中三观不代表作者三观,真的真的真的!)1林宿雨在带领自家俱乐部取得中国赛区的冠军,还没有享受冠军......
9.4万字4个月前
美:天选之人 连载中
美:天选之人
操控者
不许转载抄袭,模仿@操控者(模仿J.K罗琳的哈利波特)。角色已拟人前面的正在修改中,正文持续更新中
0.9万字3个月前
穿成反派大小姐后我躺赢了 连载中
穿成反派大小姐后我躺赢了
空花亦落果
常年排行垫底的系统菁菁被前辈扔到了反派大师姐身边,任务竞是阻止她崩坏位面!!菁菁欲死无泪,战战兢兢的跟着这个暴躁大师姐走过一个又一个位面。本......
1.7万字2个月前
萌萌传 连载中
萌萌传
像老鹰一样123
《这样唱好美》中的女歌手,苏诗丁,唱得歌,比如《杀破狼》,唱得声音很玄空,清脆悦耳,小艳听了也说好听,撒撒听了说摇头,那我问他:“你喜欢什么......
61.9万字1个月前
生活里的生活 连载中
生活里的生活
大森林狂想曲
未来的潮流趋势,谁也不知道,科技是永恒的话题
6.4万字1个月前