Definition of the ordinal rank of sentences of the natural number structure.

Question

Let our structure be $(\mathbb{N};+,\cdot,0,1)$. I want to define the ordinal rank of a sentence regarding this structure. Informally, the ordinal rank is the number of steps you need to either verify or refute the sentence. For example, sentences with no variables get a rank of $0$. A sentence like $(\exists x) x = x$ gets a rank of $1$, because, since $0 = 0$, and $0$ is the first natural number, we only need $1$ step to verify the sentence. A sentence like $(\exists x)x=1$ gets a rank of $2$, because $1$ is the second natural number. A sentence like $(\forall x)x=x$ gets a rank of $\omega$, because you need $\omega$ steps to verify it. A sentence like $(\forall x)(\forall y)x+y=y+x$ gets a rank of $\omega^2$, because you need $\omega^2$ steps to verify it. I hope these examples have made it clear what I am talking about. So, my question is, what is the formal definition of the ordinal rank of a sentence regarding the structure $(\mathbb{N};+,\cdot,0,1)$? And, has this notion appeared in some book or paper?

Answer 1

I think this formalizes what you're looking for, to every formula $\phi$ we assign an ordinal $\textrm{rank}(\phi)$:

• For a quantifier-free formula $\phi(z_0,\ldots,z_k)$, let $\textrm{rank}(\phi(z_0,\ldots,z_k))=1$.
• For a formula $\phi$ of the form $\exists(y<x)\psi(y,z_0,\ldots,z_k)$, let $\textrm{rank}(\phi)$ be $\sum_{y=0}^{\textrm{min}(a,x)}\textrm{rank}(\psi(y,z_0,\ldots,z_k))$, where $a$ is the least natural number such that $\psi(a,z_0,\ldots,z_k)$ (intuitively "total number of computation steps to verify the $\psi(y,z_0,\ldots,z_k)$, stopping either when you hit $y=a$ or find an example $y$".)
• For a formula $\phi$ of the form $\forall(y<x)\psi(x,z_0,\ldots,z_k)$, let $\textrm{rank}(\phi)=\sum_{y=0}^x\textrm{rank}(\psi(y,z_0,\ldots,z_k))$ (intuitively "total number of computation steps to verify each $\psi(y,z_0,\ldots,z_k)$".)
• For a formula $\phi$ of the form $\exists y,\psi(y,z_0,\ldots,z_k)$, let $\textrm{rank}(\phi)$ be $\sum_{y=0}^a\textrm{rank}(\psi(y,z_0,\ldots,z_k))$, where $a$ is the least natural number such that $\psi(a,z_0,\ldots,z_k)$ (intuitively "total number of computation steps to verify the $\psi(y,z_0,\ldots,z_k)$, hitting $y=a$ and then stopping".) If there is no such $a$, let $\textrm{rank}(\phi)=\textrm{rank}(\forall y,\lnot\psi(y,z_0,\ldots,z_k))$.
• For a formula $\phi$ of the form $\forall y,\psi(y,z_0,\ldots,z_k)$, let $\textrm{rank}(\phi)$ be the ordinal $\textrm{sup}\{\sum_{y=0}^x\textrm{rank}(\psi(y,z_0,\ldots,z_k))\mid x\in\mathbb N\}$ (intuitively "$\sum_{y=0}^\omega\textrm{rank}(\psi(y,z_0\ldots,z_k))$".)

For example, the rank of each formula $\exists y(x+1=y)$ for any natural $x$ should be $x+2$, because the rank of each $x+1=y$ is 1, and we sum from $y=0$ until we find the example $y=x+1$ and then stop - overall this should put the rank of $\forall x\exists y(x+1=y)$ at $\omega$ as you want. About any issues with a formula being an input of a function to the ordinals, $\textrm{rank}$ can be thought of as a function from naturals to ordinals via Godel-coding.

This is not that pretty of a definition, but I think it works. At first I tried ordering satisfying assignments of the formula lexicographically, in my opinion this was more elegant, but that didn't work. Nevertheless, this kind of idea reminds me a bit of the definition of $<_L$, a well-order on Godel's constructible universe $L$ of sets. It's not exactly the same idea, in the definition of $<_L$ we are ordering the sets by which formulae define them, instead of ordering formulae by which sequences of naturals satisfy them. I think part of the reason this ordering doesn't show up in theoretical computer science is because dovetailing takes the spotlight - calculations can be multi-threaded and weaved together in the way Noah Schweber mentioned in order to achieve the same computation, with computation steps ordered only in order type $\omega$. This allows us to achieve smaller ordinals, which TCS may find more central.