> I don’t really know how to work with the definition of ordinal arithmetic in terms of successors and limits.
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.
How do you go from these definitions of ordinal arithmetic by transfinite recursion to mechanical rules for arithmetic on the cantor normal form / deriving the needed algebraic identities? It seems very non obvious to me, although certainly must be very obvious to many. I would like a reference if you have one.
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 frequency illusion is funny—I just learned about the ordinals and now I’m seeing articles pop up about them everywhere.
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.
> 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
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.
Regarding 1), I meant bizarre to non-mathematicians. Most people are familiar with arithmetic and perhaps even geometry proofs, but not so much with proofs that involve ordinals and multiple levels of infinity. That such a simple program requires more than (Peano) arithmetic to prove statements about its behavior seems very unintuitive, at least to me.
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.
inf(1)
wow! ordinals are way cooler mathematical objects than i thought! i thought they were just for nerds but it turns out they are actually fascinating! what a mathematical rollercoaster!
Yea, I think it's a very neat structure. The typical presentation of the general concept of ordinals as an aspect of set theory hides a more down to earth cute algorithmic thing.
Surreal arithmetic is much nicer than ordinal arithmetic, it is commutative for example. I've always thought that a surreal number library supporting infinite numbers would be useful. Surreal numbers include ordinals but a lot more, they are the largest totally ordered field.
The main "software" application I'm aware of is a connection to termination checking (whether a program actually finishes). This is in turn connected to automated complexity analysis, which is a more refined answer about how long a program takes to finish.
This is a couple steps removed from all that.
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.
I guess... math programs...? Proof generators? I've been working with some mathematical code recently and read (skimmed) this whole thing, and I didn't come away with any ideas. There is a link to a resource on "ordinal algebra", but it's lacking the obvious appeal of quaternions and octonions. Commenting in the hope that my ignorance inspires an insightful correction from someone who knows more Math than I do!
Take any problem where the naturals are a good conceptual fit, and there probably exists an alternate reality where you didn't have enough power to push back on insane design decisions, and in that reality ordinals are a good fit. The features you're likely to care about include (a) being able to reference an abstract entity instead of the thing itself (like an auto-incrementing database index referring to the knowledge atom in question) and (b) caring about some sort of ordering on those things (else you'd use uuids or some similar abomination and move on with your life).
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.
This reminds me a bit of splittable random number generators [1], which are useful for monte carlo methods with fork-join parallelism. Perhaps ordinals would be the non-random version of that? But then again, it seems like ordinals couldn’t be a fixed-size datatype like a float, so why not use dotted paths as strings?
The things you gain compared to a string-based API are
(a) Potentially some space efficiency. They can't be fixed-size, but they can absolutely be a small number of varints (the standard zig-zag encoded 7 bits per byte with a high-bit signalling more data would be fine, or since everything in sight is unsigned you could skip the zig-zag).
(b) An intrinsic notion of order that is almost definitely correct. When the standard dictionary order suffices (actually a bit tricky with strings, starting with upper/lower-case and quickly devolving into questions of what an upper-case emoji is, but assume ASCII for the sake of argument), strings are probably a better conceptual fit. You'll struggle with the path-based approach when the number of dots changes though, when you have some concerns ordered monotonically one direction and others ordered the other way, when you need a notion of enough space to _always_ be able to slot an intermediate value in, ...
About (3) ordinary working programmers expect their type checkers to just work. But that's very similar to how ordinary working programmers expect their priority queue libraries and their data base indices to just work, too.
What on Earth is happening at the end of this article? I feel like I'm reading an AI-generated text from a pre-GPT-2 model. For instance:
"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...?
Is this some kind of AI poisoning? This would be a kind of way to protect somewhat against web scraping LLMs using content. Include sections of gibberish for them to train themselves on and reduce accuracy.
Don't worry, training is protected by the Glory of the Commons -- any intentional linguistic sabotage by an individual would be a tiny drop in the bucket.
It is as finished as it's going to be. I may write about the ordinals again, maybe I'll reuse pieces, but I won't be improving this particular page except with the occasional addendum.
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.