Ordinal definability—how did Gödel do it?

Gödel proposed the concept of ordinal definability well before the reflection theorem of Lévy and Montague existed. How did he do it?

Kurt Gödel introduced the concept of ordinal definability in 1946, making key claims about it and insightful predictions. Meanwhile, almost all our current understanding of this idea is founded upon the reflection theorem of Lévy and Montague, which did not appear until 1960. How did Gödel do it?

Kurt Gödel, CC BY 4.0, via Wikimedia Commons

This is the historical conundrum of ordinal definability, which I should like to consider in this essay.

Welcome to this series of essays on the topic of ordinal definability, which can be found in the ordinal-definability tag. The essays are adapted from a longer, more technical work currently in progress with myself and Bokai Yao on the topic of what we call the Contingent HOD Dichotomy. That paper is currently still in progress and will be released soon.

Let’s get into it.