Is the theory of $(\operatorname{Ord}, <)$ decidable?

Question

Over a sufficiently strong second-order theory (such as Morse-Kelley set theory), it's possible to define the truth of all first-order formulae in the language of sets. This allows us to construct the set of true sentences about the structure $(\operatorname{Ord}, <)$, where $\operatorname{Ord}$ denotes the class of all ordinals. My question is as stated in the title: is there a decision procedure for this set of sentences?

According to this answer which cites a paper I couldn't understand, the structure $(\mathbf{Ord}, <)$ is elementarily equivalent to the structure $(\omega^\omega, <)$, hence my question is equivalent to asking whether the theory of $(\omega^\omega, <)$ is decidable. I scanned the paper they cited, but it didn't seem to answer my question.

---

I strongly suspect that the theory is decidable, and in particular there's a conservative extension which I think permits quantifier elimination, but I wasn't able to assemble a proof. This extension works by defining a sequence of operations via recursion in the metatheory. Define the function $\alpha+\omega^0 = \min\{\beta : \alpha<\beta\}$, and then for each standard numeral $n$ we define the following function. $$\alpha + \omega^{n+1} = \min\{\beta>\alpha :\forall(\gamma<\beta), \gamma+\omega^n<\beta\}$$

It's not hard to prove that, in the standard model of ordinals, these functions do what their names suggest they do. In this extended language, the "constant terms" are any expression formed by repeatedly applying the various $+\omega^n$ functions, starting from $0$. Given any constant term $T$ and variable $\alpha$, we define the expression $\alpha+T$ to denote the term identical to $T$ but where the $0$ in $T$ is replaced by $\alpha$. This means, for example, that $\alpha+0=\alpha$ by definition, and $\alpha+(0+\omega^n) = \alpha+\omega^n$. For convenience, we also define the constant symbols $\omega^n = 0+\omega^n$, which is unambiguous due to the previous observation. Using this notation, we define the following relation for each constant term $T$. $$\alpha \sim T \iff \exists \beta, \alpha = \beta+T$$

I believe that extending our language with the above relations and functions will enable quantifier elimination, but I couldn't figure it out. I was able to show that, for any quantifier-free formula $\psi$ expressed using only $<$, the formula $\exists \alpha, \psi$ can be reduced to a quantifier-free formula using only $<$ and the $+1$ function. I think it's possible to eliminate a second quantifier by introducing the $+\omega$ operation and the $\sim T$ relations for finite constants $T$, but it was too complicated for me to formalize it. Ideally this would give way to some pattern which lets us eliminate all quantifiers, at which point there's a simple decision procedure for the quantifier-free sentences. I couldn't figure out the quantifier elimination, though.

Answer 1

$\def\ord{\mathrm{Ord}}$Doner, Mostowski, and Tarski, The elementary theory of well-ordering – a metamathematical study (in: Logic Colloquium ’77, A. Macintyre, L. Pacholski, and J. Paris (eds.), North-Holland, 1978, pp. 1–54) prove a quantifier elimination result for the first-order theory of well orders using definable predicates similar to what you propose. It implies that the extension of the theory with axioms expressing that multiples of $\omega^k$ are cofinal for every fixed $k\in\mathbb N$ is complete and decidable, and therefore it coincides with the theory of either $(\ord,<)$ or $(\omega^\omega,<)$, or $(\omega^\omega\cdot\gamma,<)$ for any $\gamma>0$ for that matter.

For the record, a complete list of axioms of $\operatorname{Th}(\ord,<)$ is: $$\begin{align*} &\neg(x<x),\\ &x<y\land y<z\to x<z,\\ &x<y\lor x=y\lor y<x,\\ &\exists z\:\forall x\:z\le x,\\ &\exists y\:\bigl(y\le x\land\lambda_k(y)\land\forall z\:(z\le x\land\lambda_k(z)\to z\le y)\bigr),\\ &\exists y\:\bigl(x<y\land\lambda_k(y)\land\forall z\:(x<z\land\lambda_k(z)\to y\le z)\bigr) \end{align*}$$ for each $k\ge0$, where, as usual, free variables are assumed universally quantified in front, $x\le y$ stands for $x<y\lor x=y$ (or: $\neg(y<x)$ if you prefer), and the $\lambda_k$ are the following formulas that define multiples of $\omega^k$: $$\begin{align*} \lambda_0(x)&\equiv\top,\\ \lambda_{k+1}(x)&\equiv\forall y\:\bigl(y<x\to\exists z\:(y<z\land z<x\land\lambda_k(z))\bigr). \end{align*}$$

Btw, this all holds in plain ZF; it is not necessary to use MK. The point is that as another consequence of the quantifier elimination result, one can also define a satisfaction predicate for arbitrary formulas over $(\ord,<)$, and prove it obeys the usual Tarski conditions (such a predicate is then necessarily unique). In fact, structures of the form $(\omega^\omega\cdot\gamma,<)$ for $\gamma>0$ form an elementary chain, thus we can simply define $(\ord,<)\models\phi(\vec\alpha)$ as $\exists\gamma\in\ord\,(\vec\alpha<\omega^\omega\cdot\gamma\land(\omega^\omega\cdot\gamma,<)\models\phi(\vec\alpha))$ for any formula $\phi$ and $\vec\alpha\in\ord$. This gives “the theory of $(\mathrm{Ord},<)$” a well-defined meaning already in ZF.