Ordinals do show up in the well foundedness check of definitions in ACL2, which is a common lisp interactive proof assistant with applications to software verification.
Both of these, while software, are somewhat niche. I'm not aware of a non formal methods / verification software context the ordinals would show up, but I'd love to hear it if so.
For some spitballed examples:
1. You can get low-contention, globally unique database keys for "free" by allowing ordinal indices. Management commands like creating a table instance on a given cluster node give that table instance a unique id through some scheme involving adding infinite ordinals, and that table instance is then able to assign guaranteed unique ids ad infinitum. The sort order on keys naturally clusters time-correlated data per table, which is a hugely desirable property when reasoning about the distributed behemoth you're creating (more applicable to the DB author perhaps than an end user).
2. Priority queues are often a good start for a sequence of tasks you'd like to accomplish. Start with the idea that older things should finish first. We'll add bigger and bigger "low priority" numbers to new tasks. Continue to find that you actually have different task types, and "Bob the ML engineer" has zero access to the TPUs, the general public has mid-priority access through Colab, and Sundar has infinite priority; if he wants to dabble in ML then all the real work needs to pause. And so on. As you add more levels of order to "the next thing that should run," the system gets substantially more complicated. God forbid you need a higher priority and there are none left. Starting in some infinite middle of a stream of ordinals gives you the power to handle all that garbage without much thought. Your task queue can be pretty generic and just care about ordinal arithmetic, not the to/from steps for creating those ordinals.
1a. The database index idea is probably not usable in the real world for perf reasons, but when object counts are in the low billions you have a lot more flexibility. Imagine a VCS using ordinal arithmetic to give you perfect information just from the id of the chain of branching and commits that led you to where you are (in structure, obviously not grabbing the metadata like commit messages while magically not hitting disk).
3. Not a "working programmer" concern, but type checking, SAT solving, theorem proving, ..., tend to be fairly deeply connected. The idea of using ordinals to track and analyze recursive calls has been around for awhile. Similar techniques, even when not explicitly ported to those other domains yet, are likely to end up there eventually IMO.
[1] https://docs.oracle.com/en/java/javase/17/docs/api/java.base...
"Order summation. Disjoint sum of underling sets and the sayeverything in Right is greater than everything in Left. This shows the composition of two prcoesses is terminating.
Lexiocgraphic product. Tuple of underlying sets. Nesting of two terminating properties is terminating. How do I square that this feels like two nested for loops with lex being part of ackermann termination also?"
I thought this was an article, and then it turned into a bunch of word salad esque personal notes...?
I recommend the technique.
- It is actually the part that is the most valuable for me to refer to, since the actual content of the post I understand well by the time I write it.
- It has generated the most conversations, since people are more interested in pipping up about an unsolved problem than a solved one.
- It helps me edit since tossing stuff back there helps me more ruthlessly delete without the irrevocable loss of some paragraph I kind of liked.
- It gets it out there. Perfection is the enemy of the good.
It’s only mentioned briefly in a footnote in the article, but one of the most mind-blowing concepts related to ordinals is called the Goldstein sequences.
These are basically sequences that start at an arbitrary natural number n and follow some simple rules (like the Collatz conjecture) to go from one item in a Goodstein sequence to the next. Much like the sequences in the Collatz conjecture, the Goodstein sequences can reach incredibly (extraordinarily) high numbers before eventually coming back down and terminating at zero. However, unlike the Collatz conjecture, the statement that all Goodstein sequences eventually terminate at zero for any starting value n has been proven.
But here’s the remarkable part: the proof that all sequences eventually terminate requires axioms “beyond” what you think of as involved in standard arithmetic. Specifically, we require the ordinals and transfinite induction to prove that all sequences terminate (i.e., there is a proof that Peano Arithmetic cannot prove that all sequences terminate; ZFC can however).
What this means is that you can create an extraordinarily tiny Turing machine (or a Python script that’s about 10 lines of code) whose halting behavior requires these bizarre axioms that most non-mathematicians have never heard of to prove. That is just nuts to me for some reason.
Two comments:
(1) How can it be that we need bizarre axioms if ZFC can prove it? Or is it just that we know of a "direct" proof using bizarre axioms, but not one in ZFC? Isn't proving that a proof exists in ZFC enough to consider it proven in ZFC?
(2) This is related to the reason why BusyBeaver(4) was easy to prove, BusyBeaver(5) only known recently, and BusyBeaver(745) is known to be independent of ZFC. For any set of axioms, there's some n and q where BusyBeaver(n) == q is true but not able to be proven in those axioms. Weird stuff starts happening once you get n large enough to encode the axioms themselves in the turing machine.
2) Yeah that’s actually how I discovered Goodstein sequences. I saw some post on HN about tiny Turing machines that halt iff ZFC is consistent and wanted to learn more.
"These number do no have commutative multiplication."
However, I do note the unauthorized use of "cute" - outrageous!
What a shame... I think the dude is overcomplicating stuff just by not understanding this.
As an analogy, the naturals are the closure of 0 being a natural number, and to each natural number, having a function that gives you another number not in the set, as the "next" natural number (called the successor of that original number).
The class of ordinals are just the closure of having 0 be an ordinal, and to each *set* of ordinals being able to get the "next" ordinal, (i.e. the smallest ordinal that comes (not necessarily immediately) after all elements in the set). Then omega is the "next" ordinal wrt the natural numbers (aka finite ordinals), and that's what's meant by a limit ordinal, defined by exclusion, as not the "next" ordinal of any set of ordinals that has a maximum element (the natural numbers have no maximum element, but the natural numbers and omega together have omega as the maximum element); the "next" ordinal of a set that has a maximum element is equally the "next" ordinal of the set containing just that maximum element, and we can do a +1, just as with natural numbers, hence we call it successor ordinal.
I think a deficiency of my post is that I didn't go into much of what the ordinals are, but I think a strength is that it is all quite mechanical.
The only library I know of that supports infinite surreal numbers is CGSuite, you can see its hierarchy here: https://github.com/aaron-siegel/cgsuite/blob/e909ab8bc330e39...
