[FOM] A computational approach to the countable ordinals

[Paul Budnik]

I have always been sceptical of completed infinite totalities in set 
theory. At the same time I consider questions like "Does a computer have 
an infinite number of outputs?" to be objectively true or false. This 
led me to the idea that the only mathematical questions that are 
objectively true or false are those logically determined by a 
recursively enumerable sequence of events. This includes most of 
standard mathematics, but excludes questions like the continuum 
hypothesis. I published a philosophical paper about this, What is 
Mathematics About?  (http://www.mtnmath.com/pom.html), in Paul Ernest's 
online journal.

This philosophy has led me to suspect that a computational approach to 
the ordinal numbers can ultimately go beyond the recursive ordinals 
provably definable in ZF. Writing code to define an expandable notation 
system allows one to do computer experiments on notations systems that 
are not otherwise possible.  It also helps immensely in keeping track of 
all the details. I have put some effort into this project starting with 
the Veblen hierarchy and its generalizations.  I have two questions for 
this group.

Have there been other attempts to write code for ordinal notations as a 
research tool to create stronger notations systems? I know this has been 
done to support automated proofs.

I have reached a point where the best way to proceed seems to be to use 
ordinals greater than the Church Kleene ordinal to generalize the 
functional hierarchies used to construct recursive ordinal notations. I 
know the countable admissible ordinals have been used to construct 
recursive ordinal notations using collapsing functions. but I wonder if 
anything like I am suggesting has been attempted?

Paul Budnik