phi(a,b,c) = (x -> w^x) ( c b a )
( 0 1 2 )
Small Veblen ordinal = (x -> w^x) ( 1 )
( w )
See https://core.ac.uk/download/pdf/33091421.pdf for more information.
We start with the large Veblen ordinal (LVO) which is the least fixed point of the function α↦φ(1_α), φ(1_α) representing the application of φ with transfinitely many variables with 1 at position α and 0 anywhere else. Then we consider a function F which enumerates the fixed points of α↦φ(1_α). So we have LVO = F(0). The next fixed point F(1) is the limit of LVO+1,φ(1_LVO+1),φ(1_φ(1_LVO+1)),...
Then we can consider the fixed points of the function F and define a function G which enumerates these fixed points, then a function H which enumerates the fixed points of G, and so on.
This construction is similar to ϵ which enumerates the fixed points of α↦ωα, ζ which enumerates the fixed points of ϵ, η which enumerates the fixed points of ζ.*
Like we have defined :Then φ′α(β) can be written as a binary function φ′(α,β) which can be generalized to finitely many variables like φ′(α,β,γ) and transfinitely many variables like φ′(1ω).
Then we can consider the fixed points of the function α↦φ′(1α) and define a function φ′′0 which enumerates these fixed points.
The same way we can define φ′′′, φ′′′′, ...
We can then introduce a new notation :
Then we can go on with for example the fixed points of α↦Φα(1α) or something like that ...
There is another way to express this construction, using Veblen functions indiced by the function used for φ0.
There are different conventions for φ0(x), like ωx or ϵx. We can write explicitely the convention chosen for φ0 by writing "φf(α,β)" for "φα(β) with function f used for φ0". With this notation we have:
Then we generalize the binary function φf(α,β) to finitely many variables: for example φ_f(1,0,α)=(1+α)th common fixed point of the function ξ↦φ(ξ,0) ( see https://en.wikipedia.org/wiki/Veblen_function ) and to infinitely many variables with a finite number of them different from 0, for example φ_f(1_ω).
Then we can define new φ functions by taking for φ0 the function ξ↦φ_f(1_ξ) and define functions φ_ξ↦φ_f(1_ξ) with 2 variables, with finitely many variables and with transfinitely many variables.
To make a correspondence with my previous construction, if f is the function ξ↦ω^ξ, then φ_f(α,β) corresponds to what I wrote φ_α(β), and φ_ξ↦φf(1ξ)(α,β) to φ′_α(β).
If we define the function S by S(f)(ξ)=φ_f(1_ξ), then φ_ξ↦φf(1ξ) can be written φ_S(f). We can then consider φ_S(S(f)) and so on.
Given an ordinal α, we can iterate transfinitely "α times" the application of S to an initial function f0, for example f0(ξ)=ω^ξ, to obtain a function which I will write S^α(f0). We can use this function to define a function φ_S^α(f0) which permits to construct big ordinals.
We must verify that this function really permits to get greater and greater ordinals and does not get stucked in a loop, perhaps by verifying it is "fruitful" or "helpful" in the sense of http://www.cs.man.ac.uk/~hsimmons/TEMP/OrdNotes.pdf : "An ordinal function f∈Ord' is fruitful if it is inflationary, monotone, continuous, and big. Let Fruit be the class of fruitful functions. An ordinal function h∈Ord' is helpful if it is strictly inflationary, monotone, and strictly big. Let Help be the class of helpful functions."
If it is the case and if this construction is correct, there is probably a correspondence with the notations using ordinal collapsing functions, but for the moment I don't see how to establish it.
And after ? The next step could perhaps start by enumerating the fixed points of a function like ξ↦φ_S^ξ(1_ξ) or something like that ...
Notation of Harold SimmonsFix f z = f^w(z+1) = H f (suc z) = least fixed point of f which is > z Next = Fix [w^*] = "next epsilon_a" [0] h = Fix (a → h^a 0) [1] H h = Fix (a → H^a h 0) [2] H h g = Fix (a → H^a h g 0) or [0] h = Fix (a → h^a w) [1] H h = Fix (a → H^a h w) [2] H h g = Fix (a → H^a h g w) … Delta[0] = w Delta[1] = Next w = epsilon 0 Delta[2] = [0] Next w = least v with v = Next^v w = zeta 0 Veb f z = (Fix f)^(1+z) 0 = (1+z)th fixed point of f Enm h a = h^(1+a) 0 Veb = Enm o Fix ; [0] = Fix o Enm Fix o Veb = Fix o Enm o Fix = [0] o Fix Fix o Veb^a = [0]^a o Fix Delta[3] = [1] [0] Next w = least v with v = [0]^v Next w = Gamma 0 Delta[4] = [2] [1] [0] Next w = least v with v = [1]^v [0] Next w = large Veblen ordinal …Correspondence with Veblen function
epsilon_a = phi(1,a) = Next^(1+a) 0 = Next^(1+a) w zeta_0 = phi(2,0) = least fixed point of (x → epsilon_x) = Fix (x → epsilon_x) 0 = Fix (x → Next^(1+x) 0] 0 = Fix (x → Next^x 0) 0 = [0] Next 0 Next fixed point : zeta_1 = phi(2,1) = Fix (x → Next^x 0) ([0] Next 0) = [0] Next ([0] Next 0) = ([0] Next)^2 0 zeta_a = phi(2,a) = ([0] Next)^(1+a) 0 eta_0 = phi(3,0) = Fix (x → zeta_x) 0 = Fix (x → ([0] Next)^(1+x) 0) 0 = Fix (x → ([0] Next)^x 0) 0 = [0] ([0] Next) 0 = [0]^2 Next 0 eta_a = phi(3,a) = ([0]^2 Next)^(1+a) 0 phi(1+b,a) = ([0]^b Next)^(1+a) 0 Gamma_0 = phi(1,0,0) = least fixed point of x → phi(x,0) = Fix (x → phi(x,0)) 0 = Fix (x → [0]^x Next 0) 0 = [1] [0] Next 0 phi(c,b,a) = ([0]^b (([1] [0])^c Next))^(1+a) 0 phi(d,c,b,a) = ([0]^b (([1] [0])^c (([1]^2 [0])^d Next)))^(1+a) 0 Small Veblen ordinal = [1]^w [0] Next 0 Large Veblen ordinal = [2] [1] [0] Next 0 = [2] [1] [0] Next wSee also http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/FromBelow.pdf.
Large Veblen ordinal = [2...0] Next 0 Bachmann-Howard ordinal = [w...0] Next 0 [1] [w...0] Next 0 = [w+1...0] Next 0 Fix (x → [x...0] Next 0) 0Variant
Replace a → w^a by suc N = Fix suc [0] N 0 = Fix (x → N^x 0) 0 = lim 1, N^1 0 = w, N^w 0 = w*w = w^2, N^w^2 0 = w*w^2 = w^3, ... = w^w [0]^2 N 0 = [0] ([0] N) 0 = Fix (x → ([0] N)^x 0) 0 = lim 1, [0] N 0 = w^w, ... = w^w^2 [0]^a N 0 = w^w^a [1] [0] N a = Fix (x → [0]^x N 0) a = lim a+1, [0]^(a+1) N 0 = w^w^(a+1), ... = Next a [1] [0] N = Next ([0]^b ([1] [0] N))^(1+a) = phi(1+b,a)
An ordinal collapsing function is a function which, when applied to an uncountable ordinal, gives a countable ordinal.
The general idea is to define a set of ordinals C(a) or C(a,b) where a and b are ordinals, which contains all ordinals that can be built using an initial set of ordinals and some operations or functions, and then define psi(a) or psi(a,b) as the smallest ordinal which is not in C(a) or C(a,b), or the least ordinal which is greater than than all countable ordinals of C(a) or C(a,b).
Different ordinal collapsing functions are described here : http://googology.wikia.com/wiki/Ordinal_notation
An example of ordinal collapsing function : Madore's psi
This ordinal collapsing function is described in https://en.wikipedia.org/wiki/Ordinal_collapsing_function and http://quibb.blogspot.fr/2012/03/infinity-impredicative-ordinals.html.
The definition of this function uses the ordinal Omega which is the least uncountable ordinal.
C(a) is the set of all ordinals constructible using only 0, 1, w, Omega and addition, multiplication, exponentiation, and the function psi (which will be defined later) restricted to ordinals smaller than a.
psi(a) is the smallest ordinal not in C(a).
The smallest ordinal not in C(0) is the limit of w, w^w, w^w^w, ... which is ε0, so psi(0) = epsilon_0.
More generally, psi(a) = epsilon_a for all a < zeta_0, psi(a) = zeta_0 for zeta_0 <= a <= Omega, and psi(Omega+a) = epsilon_(zeta_0+a) for a <= zeta_1.
The limit psi(epsilon_(Omega+1)) of psi(Omega), psi(Omega^Omega), psi(Omega^Omega^Omega), ... is the Bachmann-Howard ordinal.
Some examples of fundamental sequences (FS) are :
To distinguish between the different Veblen functions, let us call φF the Veblen function with finitely many variables, and φT the Veblen function with transfinitely many variables.
φF is a function which, when applied to a list of countable ordinals, gives a countable ordinal. A list of countable ordinals can be seen as a function which, when applied to a natural number, gives a countable ordinal, with the restriction that the result differs from 0 for finitely many integers. If we denote ω the set of natural numbers and Ω the set of countable ordinals, then this can be written : φF:(ω→Ω)→Ω. If we replace α→β by β^α, we get Ω^Ω^ω, and if we apply ψ to it, we get ψ(Ω^Ω^ω), which is the small Veblen ordinal, the least ordinal that cannot be reached using φF.
For φT, the position of a variable is represented by a countable ordinal instead of a natural number, also with the restriction that finitely many variables differ from 0, so we have φT:(Ω→Ω)→Ω. If we replace α→β by β^α, we get Ω^Ω^Ω, and if we apply ψ to it, we get ψ(Ω^Ω^Ω), which is the large Veblen ordinal, the least ordinal that cannot be reached using
If we extrapolate this correspondence, we can define a generalization of the Veblen function whose limit would be ψ(Ω^Ω^Ω^Ω), and the "position" of a variable would be a function which gives a countable ordinal when applied to a countable ordinal, and so on, up to the Howard ordinal, which is the limit of ψ(Ω),ψ(Ω^Ω),ψ(Ω^Ω^Ω),...
θ function
This is another collapsing function.
θ function is a binary function. It’s defined as follows:
It means that, θ(α,β) is the (1+β)-th ordinal such that it cannot be built from ordinals less than it by addition, applying θ(δ,_) where δ < α and getting an uncountable cardinal.
It seems that θ(a,b) = φ(a,b) below Gamma_0, making θ function an extension of φ function. Even θ(Gamma_0,b) = φ(Gamma_0,b) is true.
Other important values :
See https://stepstowardinfinity.wordpress.com/2015/05/04/ordinal2/ for more information.
Taranovsky's C
Taranovsky's C is also a collapsing function.
C(a,b) is the least element above b that has degree >= a.
Definition: A degree for a well-ordered set S is a binary relation on S such that
In other terms : Let ηη be an ordinal, and let 0S and let Ld(a,b) be the statement that aa is a limit of ordinals c such that (c,b)∈D. Let D be the following binary relation over η:
For ordinals in the standard representation written in the postfix form, the comparison is done in the lexicographical order where 'C' < '0' < 'Ω': For example, C(C(0,0),0) < C(Ω, 0) because 000CC < 0ΩC. (This does not hold for non-standard representations of ordinals.)
The fundamental sequences of Taranovsky’s notation can be easily defined.[3] Let L(α) be the amount of C’s in standard representation of α, then α[n]=max{β|β<α∧L(β)≤L(α)+n}.
Here is a summary of the system by Taranovsky (see https://cs.nyu.edu/pipermail/fom/2012-March/016349.html) :
Examples of representations of some ordinals (where W = W1) :
See http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm and https://stepstowardinfinity.wordpress.com/2015/06/22/ordinal3/ for more information.
Ordinal trees
See http://www.madore.org/~david/math/ordtrees.pdf and http://journals.openedition.org/philosophiascientiae/pdf/402.
The order on finite rooted trees is recursively defined as follows: a tree A is less than a tree B, written A < B,
iff :
- either there is some child (=immediate subtree) B' of B such that A <= B',
- or
the following two conditions hold: every child A' of A satisfies A'
< B, and the list of children of A is lexicographically less than
the list of children of B for the order < (with the leftmost
children having the most weight, i.e., either B has more children than
A, or if A' and B' are the leftmost children on which they differ then
A' < B').
This is a well-order.
Combinatory or RHS0 notation
This method is based on combinatory logic and lambda calculus formalism.
Intuitively, the method consists in :
a = R1 H suc 0 b = R1 H (R1 H suc) 0 s = R1 H z = suc f x = x 0 [suc->R1 H,0->suc] a = R1 H (R1 H) suc c = f ([suc->R1 H,0->suc] a) = R1 H (R1 H) suc 0With the following rules :
| Basic notation | Formula | Limit | Extension | Correspondence with basic notation | Crossing beyond limit |
| Cantor | cantor(a,b)=b+w^a | least a = cantor(a,0) = w^a = epsilon_0 | Taranovsky | C(a,b) = b+w^a iff C(a,b) >= a | C(W,0) = epsilon_0 |
| Epsilon | epsilon_a | least a = epsilon_a = zeta_0 | Madore's psi | psi(a) = epsilon_a for all a < zeta_0 | psi(W) = zeta_0 |
| Binary Veblen | phi_a(b) or phi(a,b) | least a = phi(a,0) = Gamma_0 | theta | theta(a,b) = phi(a,b) below Gamma_0 | theta(W,0) = Gamma_0 |
| Name | limit of Veblen | Simmons | Madore's psi | theta | Taranovsky |
| Gamma_0 | phi_a(b) or phi(a,b) | [1] [0] Next w | psi(W^W) | theta(W,0) | C(W^2,0) |
| Small Veblen | finitely many variables phi(a_n,...,a_0) | psi(W^W^w) | theta(W^w,0) | C(W^w,0) | |
| Large Veblen | transfinitely many variables phi | [2] [1] [0] Next w | psi(W^W^W) | theta(W^W,0) | C(W^W,0) |
| Bachmann Howard | extension of phi : T = T -> W phi(a1:...:an,b1:...:bn,...) | limit of ... [3] [2] [1] [0] Next w | psi(epsilon_(W+1)) = limit of psi(W^W^...^W) | theta(epsilon_(W+1),0) | C(C(W_2,W),0) |
| Name | Symbol | Properties | Algebraic | Veblen function | Simmons notation | Madore's psi | Taranovsky's | Ordinal tree | Combinatory |
| Zero | 0 | Smallest ordinal | 0 | 0 | () | 0 | |||
| One | 1 | 1 | C(0,0) = 0+w^0 | (()) | suc 0 | ||||
| Two | 2 | 2 | C(0,1) = C(0,C(0,0)) = 1+w^0 | ((())) | suc (suc 0) | ||||
| omega | w | Smallest infinite ordinal | w | w | C(1,0) = 0+w^1 | (()()) | H suc 0 = r w suc 0 = L [r * suc 0] = [[L [r * *** **]]] suc 0 |
||
| w+1 | C(0,w) = w+w^0 | ((()())) | suc (H suc 0) | ||||||
| w+2 | C(0,w+1) | (((()()))) | suc (suc (H suc 0)) | ||||||
| w*2 | C(1,w) = w+w^1 | (()(())) | H suc (H suc 0) | ||||||
| w*3 | C(1,w*2) = w*2+w^1 | (()((()))) | H suc (H suc (H suc 0)) | ||||||
| w^2 | C(2,0) = 0+w^2 | (()(()())) | H (H suc) 0 | ||||||
| w^3 | C(3,0) = 0+w^3 | (()(()(()()))) | H (H (H suc)) 0 | ||||||
| w^w | C(w,0) = 0+w^w | ((())()) | H H suc 0 | ||||||
| w^w^w | C(w^w,0) = 0+w^w^w | ((()())()) | H H H suc 0 | ||||||
| epsilon 0 | limit of w^w^...^w | phi(1,0) | Next 0 = Next w | psi(0) | C(W,0) | (()()()) | R1 H suc 0 = H <H> I suc 0 = r w <r w> I suc 0 = [r w <*> I] (r w) suc 0 with R1 = [ H (CI *) I ] = [H <*> I] = tuple 1 [H * I] or \f (H (\g (g f)) (\x x)) in lambda calculus |
||
| epsilon 1 | epsilon 0 ^ ... ^ epsilon 0 | phi(1,1) | Next (Next 0) = Next^2 0 | psi(1) | C(W,C(W,0)) | (()()(())) | R1 (R1 H) suc 0 | ||
| epsilon 2 | phi(1,2) | Next^3 0 | psi(2) | C(W,C(W,C(W,0))) | (()()((()))) | R1 (R1 (R1 H)) suc 0 | |||
| epsilon w | phi(1,w) | Next^w 0 | psi(w) | C(C(0,W),0) | (()()(()())) | H R1 H suc 0 | |||
| epsilon epsilon 0 | phi(1,phi(1,0)) | psi(psi(0)) | C(W+epsilon_0,0) | (()()(()()())) | R1 H R1 H suc 0 | ||||
| zeta 0 | phi(2,0) | [0] Next 0 = [0] Next w | psi(W) | C(C(W,W),0) = C(W*2,0) with W*2 = C(W,W) | (()(())()) | R(2...1) H suc 0 = R2 R1 H suc 0 = [[r w <**,*> I]] [r w <*> I] (r w) suc 0 with R2 = [[ H (B (CI *) (CI **)) I ]] = [[ H <**,*> I ]] = tuple 2 [H * I] |
|||
| eta 0 | phi(3,0) | [0]^2 Next 0 | psi(W^2) | C(W*3,0) with W*3 = C(W,C(W,W)) | (()((()))()) | R2 (R2 R1) H suc 0 | Feferman-Schütte | Gamma 0 | phi(1,0,0) | [1] [0] Next 0 = [1] [0] Next w | psi(W^W) | C(C(W*2,W),0) = C(W^2,0) with W² = C(W*2,0) | ((())()()) |
R(3...1) H suc 0 = R3 R2 R1 H suc 0 with R3 = [[[H(B(CI *)(B(CI **)(CI ***)))I]]] = [[[ H <***,**,*> I ]]] = tuple 3 [H * I] |
| phi(1,0,1) | ([1] [0] Next)^2 0 | psi(W^W*2) | ((())()(())) | R3 R2 R1 (R3 R2 R1 H) suc 0 | |||||
| Gamma w | phi(1,0,w) | ([1] [0] Next)^w 0 | psi(W^W*w) | C(W^2+1,0) | ((())()(()())) | H (R3 R3 R1) H suc 0 | |||
| phi(1,0,Gamma 0) | psi(W^W*Gamma 0) | ((())()((())()())) | R1 H (R3 R2 R1) H suc 0 | ||||||
| phi(1,1,0) | [0] ([1] [0] Next) 0 | psi(W^(W+1)) | ((())(())()) | R2 (R3 R2 R1) H suc 0 | |||||
| phi(1,2,0) | [0]^2 ([1] [0] Next) 0 | psi(W^(W+2)) | ((())((()))()) | R2 (R2 (R3 R2 R1)) H suc 0 | |||||
| phi(2,0,0) | ([1] [0])^2 Next 0 | psi(W^(W*2)) | (((()))()()) | R3 R2 (R3 R2 R1) H suc 0 | |||||
| phi(3,0,0) | ([1] [0])^3 Next 0 | psi(W^(W*3)) | ((((())))()()) | R3 R2 (R3 R2 (R3 R2 R1))) H suc 0 | |||||
| Ackermann | phi(1,0,0,0) | [1]^2 [0] Next 0 | psi(W^W^2) | (()()()()) | R3 (R3 R2) R1 H suc 0 | ||||
| phi(1,0,0,0,0) | [1]^3 [0] Next 0 | psi(W^W^3) | (()()()()()) | R3 (R3 (R3 R2)) R1 H suc 0 | |||||
| small Veblen | limit of phi(1,0,...,0) | [1]^w [0] Next 0 | psi(W^W^w) | C(W^w,0) | no representation for a>=small Veblen ordinal |
H R3 R2 R1 H suc 0 | |||
| large Veblen | phi(W^W,0) | [2] [1] [0] Next 0 = [2] [1] [0] Next w | psi(W^W^W) | C(W^W,0) | R4 R3 R2 R1 H suc 0 | ||||
| Bachmann-Howard | phi(epsilon (W+1),0) with epsilon(W+1)=W^...^W |
Limit of ... [3] [2] [1] [0] Next w | psi(epsilon(W+1)) | C(C(W2,W),0) | Rw...1 H suc 0 | ||||
| Takeuti-Feferman-Buchholz |
psi(epsilon W(w)+1) |
H [R*...1 H suc 0] 0 ? |
|||||||
| Church-Kleene | wCK1 | Smallest non recursive ordinal | |||||||
| W or w1 | Smallest uncountable ordinal |
Inductive ordinal : Type := | Zero : ordinal | Succ : ordinal -> ordinal | Limit : (nat -> ordinal) -> ordinal. Fixpoint iter (a:Type) (f:a->a) (n:nat) (x:a) : a := match n with | O => x | S p => iter a f p (f x) end. Definition OpLim (F:nat->ordinal->ordinal) (a:ordinal) : ordinal := Limit (fun n => F n a). Definition OpItw (f:ordinal->ordinal) : ordinal->ordinal := OpLim (iter _ f). Fixpoint cantor (a:ordinal) (c:ordinal) : ordinal := match c with | Zero => Succ a | Succ b => OpItw (fun x => cantor x b) a | Limit f => Limit (fun n => cantor a (f n)) end. Fixpoint Nabla (f:ordinal->ordinal) (b:ordinal) : ordinal := match b with | Zero => f Zero | Succ a => f (Succ (Nabla f a)) | Limit h => Limit (fun n => Nabla f (h n)) end. Definition deriv (f:ordinal->ordinal) : ordinal->ordinal := Nabla (OpItw f). Fixpoint veblen (b:ordinal) : ordinal->ordinal := match b with | Zero => Nabla (OpLim (iter _ (cantor Zero))) | Succ a => Nabla (OpLim (iter _ (veblen a))) | Limit f => Nabla (OpLim (fun n => veblen (f n))) end. Definition veb (a:ordinal) : ordinal := veblen a Zero. Definition epsilon0 : ordinal := veb Zero. Definition Gamma0 : ordinal := Limit (fun n => iter _ veb n Zero). Check epsilon0. Check Gamma0.
module ordi where data nat : Set where O : nat S : nat -> nat data ordinal : Set where Zero : ordinal Succ : ordinal -> ordinal Limit : (nat -> ordinal) -> ordinal iter : (a : Set) (f : a -> a) (n : nat) (x : a) -> a iter a f O x = x iter a f (S p) x = iter a f p (f x) OpLim : (nat -> ordinal -> ordinal) -> ordinal -> ordinal OpLim F a = Limit (\n -> F n a) OpItw : (ordinal -> ordinal) -> ordinal -> ordinal OpItw f = OpLim (iter _ f) cantor : ordinal -> ordinal -> ordinal cantor a Zero = Succ a cantor a (Succ b) = OpItw (\x -> cantor x b) a cantor a (Limit f) = Limit (\n -> cantor a (f n)) Nabla : (ordinal -> ordinal) -> ordinal -> ordinal Nabla f Zero = f Zero Nabla f (Succ a) = f (Succ (Nabla f a)) Nabla f (Limit h) = Limit (\n -> Nabla f (h n)) deriv : (ordinal -> ordinal) -> ordinal -> ordinal deriv f = Nabla (OpItw f) veblen : ordinal -> ordinal -> ordinal veblen Zero = Nabla (OpLim (iter _ (cantor Zero))) veblen (Succ a) = Nabla (OpLim (iter _ (veblen a))) veblen (Limit f) = Nabla (OpLim (\n -> veblen (f n))) veb : ordinal -> ordinal veb a = veblen a Zero epsilon0 : ordinal epsilon0 = veb Zero Gamma0 : ordinal Gamma0 = Limit (\n -> iter _ veb n Zero)
{-
A definition of the large Veblen ordinal in Agda
by Jacques Bailhache, March 2016
See https://en.wikipedia.org/wiki/Veblen_function
(1) phi(a)=w**a for a single variable,
(2) phi(0,an-1,...,a0)=phi(an-1,...,a0), and
(3) for a>0, c->phi(an,...,ai+1,a,0,...,0,c) is the function enumerating the common fixed points of the functions
x->phi(an,...,ai+1,b,x,0,...,0) for all b<a.
(4) Let a be a transfinite sequence of ordinals (i.e., an ordinal function with finite support) which ends in zero
(i.e., such that a0=0), and let a[0->c] denote the same function where the final 0 has been replaced by c.
Then c->phi(a[0->c]) is defined as the function enumerating the common fixed points of all functions x->phi(b)
where b ranges over all sequences which are obtained by decreasing the smallest-indexed nonzero value of a
and replacing some smaller-indexed value with the indeterminate x (i.e., b=a[i0->z,i->x] meaning that
for the smallest index i0 such that ai0 is nonzero the latter has been replaced by some value z<ai0
and that for some smaller index i<i0, the value ai=0 has been replaced with x).
-}
module LargeVeblen where
data Nat : Set where
O : Nat
1+ : Nat -> Nat
data Ord : Set where
Zero : Ord
Suc : Ord -> Ord
Lim : (Nat -> Ord) -> Ord
-- rpt n f x = f^n(x)
rpt : {t : Set} -> Nat -> (t -> t) -> t -> t
rpt O f x = x
rpt (1+ n) f x = rpt n f (f x)
-- smallest fixed point of f greater than x, limit of x, f x, f (f x), ...
fix : (Ord -> Ord) -> Ord -> Ord
fix f x = Lim (\n -> rpt n f x)
w = fix Suc Zero -- not a fixed point in this case !
-- cantor a b = b + w^a
cantor : Ord -> Ord -> Ord
cantor Zero a = Suc a
cantor (Suc b) a = fix (cantor b) a
cantor (Lim f) a = Lim (\n -> cantor (f n) a)
-- phi0 a = w^a
phi0 : Ord -> Ord
phi0 a = cantor a Zero
-- Another possibility is to use phi'0 instead of phi0 in the definition of phi,
-- this gives a phi function which grows slower
phi'0 : Ord -> Ord
phi'0 Zero = Suc Zero
phi'0 (Suc a) = Suc (phi'0 a)
phi'0 (Lim f) = Lim (\n -> phi'0 (f n))
-- Associative list of ordinals
infixr 40 _=>_&_
data OrdAList : Set where
Zeros : OrdAList
_=>_&_ : Ord -> Ord -> OrdAList -> OrdAList
-- Usage : phi al, where al is the associative list of couples index => value ordered by increasing values,
-- absent indexes corresponding to Zero values
phi : OrdAList -> Ord
phi Zeros = phi0 Zero -- (1) phi(0) = w**0 = 1
phi (Zero => a & Zeros) = phi0 a -- (1) phi(a) = w**a
phi ( k => Zero & al) = phi al -- eliminate unnecessary Zero value
phi (Zero => a & k => Zero & al) = phi (Zero => a & al) -- idem
phi (Zero => a & Zero => b & al) = phi (Zero => a & al) -- should not appear but necessary for completeness
phi (Zero => Lim f & al) = Lim (\n -> phi (Zero => f n & al)) -- canonical treatment of limit
phi ( Suc k => Suc b & al) = fix (\x -> phi (k => x & Suc k => b & al)) Zero -- (3) least fixed point
phi (Zero => Suc a & Suc k => Suc b & al) = fix (\x -> phi (k => x & Suc k => b & al)) (Suc (phi (Zero => a & Suc k => Suc b & al))) -- (3) following fixed points
phi ( Suc k => Lim f & al) = Lim (\n -> phi (Suc k => f n & al)) -- idem
phi (Zero => Suc a & Suc k => Lim f & al) = Lim (\n -> phi (k => Suc (phi (Zero => a & Suc k => Lim f & al)) & Suc k => f n & al)) -- idem
phi ( Lim f => Suc b & al) = Lim (\n -> phi (f n => (Suc Zero) & Lim f => b & al))
phi (Zero => Suc a & Lim f => Suc b & al) = Lim (\n -> phi (f n => phi (Zero => a & Lim f => Suc b & al) & Lim f => b & al))
phi ( Lim f => Lim g & al) = Lim (\n -> phi (Lim f => g n & al))
phi (Zero => Suc a & Lim f => Lim g & al) = Lim (\n -> phi (f n => phi (Zero => a & Lim f => Lim g & al) & Lim f => g n & al))
SmallVeblen = phi (w => Suc Zero & Zeros)
LargeVeblen = fix (\x -> phi (x => Suc Zero & Zeros)) (Suc Zero)
{-
Normally it should terminate because the parameter of phi lexicographically decreases, but Agda is not clever enough to see it,
so it must be called with no termination check option :
$ agda -I --no-termination-check LargeVeblen.agda
_
____ | |
/ __ \ | |
| |__| |___ __| | ___
| __ / _ \/ _ |/ __\ Agda Interactive
| | |/ /_\ \/_| / /_| \
|_| |\___ /____\_____/ Type :? for help.
__/ /
\__/
The interactive mode is no longer supported. Don't complain if it doesn't work.
Checking LargeVeblen (/perso/ord/LargeVeblen.agda).
Finished LargeVeblen.
Main> phi Zeros
Suc Zero
Main> phi (Zero => Suc Zero & Zeros)
Lim (λ n → rpt n (λ a → Suc a) Zero)
Main> phi (Zero => Suc (Suc Zero) & Zeros)
Lim
(λ n → rpt n (λ a → Lim (λ n₁ → rpt n₁ (λ a₁ → Suc a₁) a)) Zero)
Main> phi (Suc Zero => Suc Zero & Zeros)
Lim
(λ n →
rpt n (λ x → phi (Zero => x & Suc Zero => Zero & Zeros)) Zero)
Main>
-}
Simmons hierarchy in Haskell module Simmons where -- Natural numbers data Nat = ZeroN | SucN Nat -- Ordinals data Ord = Zero | Suc Ord | Lim (Nat -> Ord) -- Ordinal corresponding to a given natural ordOfNat ZeroN = Zero ordOfNat (SucN n) = Suc (ordOfNat n) -- omega w = Lim ordOfNat lim0 s = Lim s lim1 f x = lim0 (\n -> f n x) lim2 f x = lim1 (\n -> f n x) -- this does not work : -- lim ZeroN s = Lim s -- lim (SucN p) f = \x -> lim p (\n -> f n x) -- f^a(x) fpower0 f Zero x = x fpower0 f (Suc a) x = f (fpower0 f a x) fpower0 f (Lim s) x = Lim (\n -> fpower0 f (s n) x) fpower l f Zero x = x fpower l f (Suc a) x = f (fpower l f a x) fpower l f (Lim s) x = l (\n -> fpower l f (s n) x) -- fix f z = least fixed point of f which is > z fix f z = fpower lim0 f w (Suc z) -- Lim (\n -> fpower0 f (ordOfNat n) (Suc z)) -- cantor b a = a + w^b cantor Zero a = Suc a cantor (Suc b) a = fix (cantor b) a cantor (Lim s) a = Lim (\n -> cantor (s n) a) -- expw a = w^a expw a = cantor a Zero -- next a = least epsilon_b > a next = fix expw -- [0] simmons0 h = fix (\a -> fpower lim0 h a Zero) -- [1] simmons1 h1 h0 = fix (\a -> fpower lim1 h1 a h0 Zero) -- [2] simmons2 h2 h1 h0 = fix (\a -> fpower lim2 h2 a h1 h0 Zero) -- Large Veblen ordinal lvo = simmons2 simmons1 simmons0 next w $ hugs __ __ __ __ ____ ___ _________________________________________ || || || || || || ||__ Hugs 98: Based on the Haskell 98 standard ||___|| ||__|| ||__|| __|| Copyright (c) 1994-2005 ||---|| ___|| World Wide Web: http://haskell.org/hugs || || Bugs: http://hackage.haskell.org/trac/hugs || || Version: September 2006 _________________________________________ Haskell 98 mode: Restart with command line option -98 to enable extensions Type :? for help Hugs> :load simmons Simmons> lvo ERROR - Cannot find "show" function for: *** Expression : lvo *** Of type : Ord Simmons>Simmons hierarchy in Symbolic Lambda Calculus
LET I ^x x LET Y [[* *] ['* (* *)]] LET zeron ^z ^s z LET sucn ^n ^z ^s (s n) LET zero ^z ^s ^l z LET suc ^a ^z ^s ^l (s a) LET lim ^f ^z ^s ^l (l f) LET insert ^x ^t ^f (t (f x)) LET tuple (Y ^r ^n ^f : n (f I) : ^p ^x : r p : ^t : f : insert x t) LET ordOfNat (Y ^r ^n : n zero : ^p : suc : r p) LET w (lim ordOfNat) LET lim0 lim LET lim1 ^f ^x (lim0 : ^n : f n x) LET lim2 ^f ^x (lim1 : ^n : f n x) LET limn (Y ^r ^p : p lim : ^q ^f ^x : r q : ^n : f n x) LET fpower (Y ^r ^l ^f ^a ^x : a x (^b : f : r l f b x) (^s : lim : ^n : r l f (s n) x)) LET fix ^f ^z (fpower lim0 f w : suc z) LET cantor (Y ^r ^b ^a : b (suc a) (^p : fix (r p) a) (^s : lim : ^n : r (s n) a)) LET expw ^a (cantor a zero) LET next (fix expw) LET simmons0 ^h (fix ^a : fpower lim0 h a zero) LET simmons1 ^h1 ^h0 (fix ^a : fpower lim1 h1 a h0 zero) LET simmons2 ^h2 ^h1 ^h0 (fix ^a : fpower lim2 h2 a h1 h0 zero) LET simmonsn ^n ^h (tuple n : ^t : fix ^a : t (fpower (limn n) a) zero) LET lvo (simmons2 simmons1 simmons0 next w) LET tupleSimmons (Y ^r ^n : n I ^p : insert (simmonsn p) : r p) LET delta ^n (tupleSimmons n I next w) LET howard (lim delta) howardSymbolic Lambda Calculus in Haskell
module Collapsing where -- Natural numbers data Nat = ZeroN | SucN Nat -- Ordinals data Ord = Zero | Suc Ord | Lim (Nat -> Ord) | Ext (Ord -> Ord) -- Ordinal corresponding to a given natural ordOfNat ZeroN = Zero ordOfNat (SucN n) = Suc (ordOfNat n) -- omega w = Lim ordOfNat -- plus a b = b + a plus Zero b = b plus (Suc a) b = Suc (plus a b) plus (Lim s) b = Lim (\n -> plus (s n) b) plus (Ext f) b = Ext (\x -> plus (f x) b) lim0 s = Lim s iter f ZeroN a = a iter f (SucN p) a = iter f p (f a) opLim f a = Lim (\n -> f n a) opItw f = opLim (iter f) -- cantor a b = a + w^b cantor a Zero = Suc a cantor a (Suc b) = opItw (\x -> cantor x b) a cantor a (Lim s) = Lim (\n -> cantor a (s n)) cantor a (Ext f) = Ext (\x -> cantor a (f x)) -- expw a = w^a expw = cantor Zero nabla f Zero = f Zero nabla f (Suc a) = f (Suc (nabla f a)) nabla f (Lim s) = Lim (\n -> nabla f (s n)) nabla f (Ext g) = Ext (\x -> nabla f (g x)) deriv f = nabla (opItw f) veblen Zero = nabla (opLim (iter (cantor Zero))) veblen (Suc a) = nabla (opLim (iter (veblen a))) veblen (Lim s) = nabla (opLim (\n -> veblen (s n))) veblen (Ext f) = \a -> Ext (\x -> veblen (f x) a) epsilon = veblen Zero fix f z = opItw f (Suc z) next = fix expw -- Omega o = Ext (\x -> x) -- Omega*2 o2 = Ext (\x -> plus x o) psi Zero = epsilon Zero psi (Suc a) = next (psi a) psi (Lim s) = Lim (\n -> psi (s n)) psi (Ext f) = psi (opItw (\a -> f (psi a)) Zero)
module Taranovsky where -- Natural numbers data Nat = ZeroN | SucN Nat -- Ordinals data Ord = Zero | Suc Ord | Lim (Nat -> Ord) | Ext (Ord -> Ord) -- Ordinal corresponding to a given natural ordOfNat ZeroN = Zero ordOfNat (SucN n) = Suc (ordOfNat n) -- omega w = Lim ordOfNat -- plus a b = b + a plus Zero b = b plus (Suc a) b = Suc (plus a b) plus (Lim s) b = Lim (\n -> plus (s n) b) plus (Ext f) b = Ext (\x -> plus (f x) b) lim0 s = Lim s iter f ZeroN a = a iter f (SucN p) a = iter f p (f a) opLim f a = Lim (\n -> f n a) opItw f = opLim (iter f) -- Taranovsky's C(b,a) = generalization of a + w^b tc Zero a = Suc a tc (Suc b) a = opItw (tc b) a tc (Lim s) a = Lim (\n -> tc (s n) a) -- tc (Ext f) a = Ext (\x -> tc (f x) a) tc (Ext f) a = opItw (\x -> tc (f x) a) Zero -- tc (Ext f) a = tc (opItw (\x -> f (tc x a)) Zero) a epsilon_0 = tc (Ext (\x -> x)) Zero bho = tc (tc (Ext (\x -> x)) (Ext (\x -> x))) Zero
Example :
C(W,0) = tc (Ext I) Zero = opItw (\x -> tc x Zero) Zero = H [C(*,0)] 0
= lim 0, C(0,0)=0+w^0=1, C(1,0)=0+w^1=w, C(w,0)=0+w^w=w^w, ...
= epsilon_0
Links
A tutorial overview of ordinal notations
Tutorial introduction to ordinal numbers in French by David Madore
Petit guide bordélique de quelques ordinaux intéressants by David Madore
Pointless Gigantic List of Infinite Numbers
Sbiis Saibian's !!! FORBIDDEN LIST !!! of Infinite Numbers
Professor Quibb's Infinity Series Portal
Ordinal notation
Traveling to the infinity
A short introduction to Ordinal Notations by Harold Simmons
A survey on ordinal notations around the Bachmann-Howard ordinal by Wilfried Buchholz
Ordinal Notation by Dmytro Taranovsky
Higher Order Set Theory with Reflective Cardinals by Dmytro Taranovsky
The Realm of Ordinal Analysis by Michael Rathjen
Connecting the Two Worlds: Well-partial-orders and Ordinal Notation Systems by Jeroen Van der Meeren
Veblen function on Wikipedia
Continuous increasing functions of finite and transfinite ordinals by
Oswald Veblen
Ordinal collapsing function on Wikipedia
Buchholz psi functions on Wikipedia
Ordinal trees
Large Countable Ordinals by John Baez
Part 1
Part 2
Part 3
Mind blown: the fast growing hierarchy for laymen — aka enormous numbers
Sbiis Saibian's Large Number Site
Extremely Large Numbers (videos)
My number is bigger !
Metatheory and Reflection in Theorem Proving: A Survey and Critique by John Harrison
Penrose's Gödelian argument by Solomon Feferman
Systems of logic based on ordinals by Alan Turing
Coq documentation
Agda documentation