- --without-K and --safe
- Ready for googology function such as fast growing hierarchy
- Literate agda script (but in Chinese) and html5 rendering
- Inductive definition of Brouwer ordinal
- Inductive definition of non-strict order
_≤_ - Equality
_≈_and strict order_<_are defined by_≤_ - Partial ordering of
_≤_and strict ordering of_<_is proved - No total ordering, but that's fine
- Well formed (WF) ordinals are those constructed hereditarily by strictly increasing sequence
- WF of finite ordinals and
ωis proved
- Common properties of ordinal functions are defined
- Definition of normal function is adapted for constructive setup
- General form of ordianl recursive function is defined and its properties are proved
_+_,_*_and_^_are defined by recursion and their WF preserving properties are proved- Association law, distribution law, etc
- We show that tetration is no-go since
α ^^ suc ω ≈ α ^^ ωand, moreover,α ^^ β ≈ α ^^ ωforallβ ≥ ω
- Infinite iteration
_⋱_is defined - If
Fis normal thenF ⋱ αis a fixed point not less thanα - Recursion of
F ⋱_ ∘ sucis the fixed point yielding function ofF, writtenF ′ - We proved that higher order function
_′is normal-preserving and wf-preserving-preserving
- Trivial examples of fixed point
- ε function is defined as
(ω ^_) ′ - We have
ε (suc α) ≡ ω ^^[ suc (ε α) ] ωforallα - ζ is defined as
ε ′and η asζ ′ ε,ζ,η, ... are all normal and WF preserving
- We proved
ε (suc α) ≈ ε α ^^ ωforall WFα
- Veblen function
φ α βis defined - We show that
φis normal, monotonic, congruence and wf-preserving - Γ₀ is defined as
(λ α → φ α zero) ⋱ zero
There is also a well formed version of most of the above in src/WellFormed. From Γ₀ on, there will be only the well formed version.