Agda大序数(8) ε层级, ζ层级, η层级

交流Q群: 893531731
目录: NonWellFormed.html
本文源码: Epsilon.lagda.md
高亮渲染: Epsilon.html

{-# OPTIONS --without-K --safe --experimental-lossy-unification #-}
{-# OPTIONS --no-qualified-instances #-}

module NonWellFormed.Epsilon where

前置

open import NonWellFormed.Ordinal
open NonWellFormed.Ordinal.≤-Reasoning
open import NonWellFormed.WellFormed hiding (wf⇒wf)
open import NonWellFormed.Function using (normal; wf-preserving; zero-increasing; suc-increasing)
open import NonWellFormed.Recursion using (rec_from_by_)
open import NonWellFormed.Arithmetic
open import NonWellFormed.Tetration using (_^^ω; _^^ω[_]; ^^≈^^[]ω; ^^-stuck; ^-^^[]-comm)
open import NonWellFormed.Fixpoint

open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

引理

本小节统一列出本章所需关于 ω ^_ 的一些平凡的引理.

ω^-normal : normal (ω ^_)
ω^-normal = ^-normal ω

ω^-wfp : wf-preserving (ω ^_)
ω^-wfp = ^-wfp ω-wellFormed

ω^-zero-incr : zero-increasing (ω ^_)
ω^-zero-incr =        begin-strict
  zero                <⟨ <s ⟩
  ⌜  ⌝               ≡⟨⟩
  ω ^ zero            ∎

ω^-suc-incr : suc-increasing (ω ^_)
ω^-suc-incr α with ≡z⊎>z α
... | inj₁ refl =     begin-strict
  ⌜  ⌝               <⟨ n<ω ⟩
  ω                   ≈˘⟨ ^-identityʳ ω ⟩
  ω ^ ⌜  ⌝           ∎
... | inj₂ α>0 =      begin-strict
  suc α               ≤⟨ +-monoʳ-≤ α (<⇒s≤ α>0) ⟩
  α + α               ≈˘⟨ α*2≈α+α α ⟩
  α * ⌜  ⌝           <⟨ *-monoʳ-< α ⦃ α>0 ⦄ (n<ω {}) ⟩
  α * ω               ≤⟨ *-monoˡ-≤ ω (^-incrˡ-≤ α ω) ⟩
  ω ^ α * ω           ∎

ε层级

ε 定义为对函数 ω ^_ 的不动点的枚举. 由于 ω ^_ 是序数嵌入, 所以 ε 也是序数嵌入, 且对任意 α 有 ω ^ ε α ≈ ε α.

ε : Ord → Ord
ε = (ω ^_) ′

ε-normal : normal ε
ε-normal = ′-normal ω^-normal

ε-fp : ∀ α → ε α isFixpointOf (ω ^_)
ε-fp α = ′-fp ω^-normal α

由 ω ^_ 以及 _′ 的相关引理可证 ε 保良构.

ε-wfp : wf-preserving ε
ε-wfp = ′-wfp ω^-normal ω^-zero-incr ω^-suc-incr ω^-wfp

ε zero 是无穷层的 ω 指数塔.

ε_{0} = ω^{ω^{.^{.^{.^{ω}}}}}

ε₀ : ε zero ≈ ω ^^ω
ε₀ =                  begin-equality
  ε zero              ≈˘⟨ ε-fp zero ⟩
  ω ^ ω ^^ω[ zero ]   ≈⟨ ^-^^[]-comm ω zero ω ⟩
  ω ^^ω[ ω ^ zero ]   ≡⟨⟩
  ω ^^ω[ ⌜  ⌝ ]      ≈˘⟨ ^^≈^^[]ω ω ⌜  ⌝ n≤ω ⦃ ≤-refl ⦄ ⟩
  ω ^^ω               ∎

后继的情况:

ε_{α+1} = ω^{ω^{.^{.^{.^{ε_{α}+1}}}}}

_ : ∀ α → ε (suc α) ≡ ω ^^ω[ suc (ε α) ]
_ = λ α → refl

极限的情况:

ε_{γ} = \sup \{ε_{γ[0]},ε_{γ[1]},ε_{γ[2]},...\}

_ : ∀ f → ε (lim f) ≡ lim (λ n → ε (f n))
_ = λ f → refl

ε 的另一种表示

可以证明对任意良构 α 有 ε (suc α) ≈ ε α ^^ ω.

ζ层级

由于 ε 是序数嵌入, 它也存在不动点, 这些不动点组成了 ζ层级, 且 ζ 也是序数嵌入.

ζ : Ord → Ord
ζ = ε ′

ζ-normal : normal ζ
ζ-normal = ′-normal ε-normal

对任意 α 有 ε (ζ α) ≈ ζ α.

ζ-fp : ∀ α → ζ α isFixpointOf ε
ζ-fp α = ′-fp ε-normal α

ζ 保良构.

ε-zero-incr : zero-increasing ε
ε-zero-incr = ′-zero-incr ω^-zero-incr

ε-suc-incr : suc-increasing ε
ε-suc-incr = ′-suc-incr ω^-normal ω^-suc-incr

ζ-wfp : wf-preserving ζ
ζ-wfp = ′-wfp ε-normal ε-zero-incr ε-suc-incr ε-wfp

ζ_0 = ε_{ε_{._{._{ε_0}}}}

_ : ζ zero ≡ ε ⋱ zero
_ = refl

ζ_{α+1} = ε_{ε_{._{._{{ζ_α}+1}}}}

_ : ∀ α → ζ (suc α) ≡ ε ⋱ suc (ζ α)
_ = λ α → refl

ζ_{γ} = \sup \{ζ_{γ[0]},ζ_{γ[1]},ζ_{γ[2]},...\}

_ : ∀ f → ζ (lim f) ≡ lim (λ n → ζ (f n))
_ = λ f → refl

η层级

由于 ζ 是序数嵌入, 它也存在不动点, 这些不动点组成了 η层级, 且 η 也是序数嵌入.

η : Ord → Ord
η = ζ ′

η-normal : normal η
η-normal = ′-normal ζ-normal

对任意 α 有 ζ (η α) ≈ η α.

η-fp : ∀ α → η α isFixpointOf ζ
η-fp α = ′-fp ζ-normal α

η 的保良构.

ζ-zero-incr : zero-increasing ζ
ζ-zero-incr = ′-zero-incr ε-zero-incr

ζ-suc-incr : suc-increasing ζ
ζ-suc-incr = ′-suc-incr ε-normal ε-suc-incr

η-wfp : wf-preserving η
η-wfp = ′-wfp ζ-normal ζ-zero-incr ζ-suc-incr ζ-wfp

η_0 = ζ_{ζ_{._{._{ζ_0}}}}

_ : η zero ≡ ζ ⋱ zero
_ = refl

η_{α+1} = ζ_{ζ_{._{._{{ζ_α}+1}}}}

_ : ∀ α → η (suc α) ≡ ζ ⋱ suc (η α)
_ = λ α → refl

η_{γ} = \sup \{η_{γ[0]},η_{γ[1]},η_{γ[2]},...\}

_ : ∀ f → η (lim f) ≡ lim (λ n → η (f n))
_ = λ f → refl

符号是有限的, 不可能这样一直命名下去. 但是, 将 ω ^_, ε, ζ, η 分别看作第0, 1, 2, 3层级, 可以将其推广到任意序数层级, 从而得到著名的 Veblen 函数, 我们将在下一章介绍.