Ordinal Exponentiation Levy Hierarchy

It is a standard exercise (see Jech's "Set Theory" Exercise 13.8) to prove that ordinal addition and multiplication are $$\Delta_1$$ expressible functions. The proof for addition comes from noting that $$\alpha+\beta$$ is order isomorphic to the disjoint union $$(\{1\}\times \alpha)\cup (\{2\}\times \beta)$$ under the lexicographical order (and everything after the "order isomorphic" part is all $$\Delta_0$$ expressible). Similarly $$\alpha\cdot \beta$$ is order isomorphic to the direct product $$\beta\times \alpha$$ under the lexicographical order.

It was surprised to see that ordinal exponentiation was not listed in the exercise. After a serious google search, the only reference I could find was a wiki article that claimed ordinal exponentiation was indeed $$\Delta_1$$. I couldn't make the same argument work here, since the corresponding order structure for $$\alpha^\beta$$ is the set $$\{f:\beta\to \alpha\,|\, f\text{ has finite support}\}$$ and I couldn't find an easy way to express this set in a $$\Sigma_1$$ way.

Is ordinal exponentiation $$\Sigma_1$$? If so, how does the proof go? (Hopefully I didn't miss an easy argument!)

(This also raised the question in my mind of whether or not, given $$X$$, the set of finite subsets of $$X$$ is $$\Sigma_1$$. I'd like to know the answer to that as well.)

Added: If I didn't make any mistakes, ordinal exponentiation is $$\Delta_1$$ if and only if that finite support set above is $$\Delta_1$$ definable. Thus, in principle, there should be an easy way to get a $$\Sigma_1$$ definition of that set. This seems surprising to me.

• A (nonempty) set $A$ is finite iff there is a surjection from some successor ordinal not above any limit ordinal. Dec 18 '18 at 20:45
• I'd prove all these facts (for addition, multiplication, and exponentiation) by invoking the fact that the class of $\Delta_1$ functions is closed under recursion over ordinals. This ought to be in, for example, Barwise's book "Admissible Sets and Structures". Dec 18 '18 at 21:21
• @NoahSchweber If we could get the full set $\{f:\beta\to\alpha\}$ in a $\Sigma_1$ way, then adding the finite support condition would be easy (as finiteness is $\Delta_1$). Do you see an easy way to get that full set of functions (using ordinals $\alpha,\beta$ as parameters)? Or were you thinking of some other argument? Dec 18 '18 at 22:48
• @AndreasBlass If you have a reference, I'd appreciate it. I've thought about using Lemma 13.12 from Jech's "Set Theory" but couldn't quite get the argument to work out. Dec 18 '18 at 22:49

First, I claim that one can express in $$\Delta_1$$ form the following property of $$\alpha,\gamma, g$$, which I'll abbreviate as $$P(\alpha,\gamma,g)$$: $$\alpha$$ and $$\gamma$$ are ordinals, $$g$$ is a function with domain $$\gamma$$, and, for each $$\beta<\gamma$$, $$g(\beta)$$ is the set of finitely supported functions $$f:\beta\to\alpha$$. Being an ordinal and being a function with a specified domain are easily $$\Delta_1$$, so the problem is to specify the values $$g(\beta)$$. But this can be done by saying that $$g(0)=\{\varnothing\}$$, that the elements of $$g(\beta+1)$$ are exactly the things of the form $$f\cup\{\langle\beta,\xi\rangle\}$$ with $$f\in g(\beta)$$ and $$\xi<\alpha$$ (for each $$\beta+1<\gamma$$), and that, for all limit ordinals $$\lambda<\gamma$$, the elements of $$g(\lambda)$$ are exactly the things of the form $$f\cup((\lambda-\beta)\times\{0\})$$ with $$\beta<\lambda$$ and $$f\in g(\beta)$$.
Once we have this $$\Delta_1$$ definition of $$P$$, we can express "$$x$$ is the set of finitely supported functions $$\beta\to\alpha$$" by saying "there exists $$g$$ such that $$P(\alpha,\beta+1,g)$$ and $$g(\beta=x)$$." Except for "there exists $$g$$", everything here is $$\Delta_1$$, so the whole statement is $$\Sigma_1$$.
The same idea, for converting a recursive definition to an explicit definition, can be used to support my earlier comment about using the recursive definitions of addition, multiplication, and exponentiation to show that these are $$\Delta_1$$-definable. One says, for example, that $$\alpha^\beta=\theta$$ iff there is a function $$g$$ with domain $$\beta+1$$ satisfying the inductive clauses for the definition of exponentiation and $$g(\beta)=\theta$$. That's a $$\Sigma_1$$ definition and, since exponentiation is provably total, $$\Delta_1$$-definability follows. (As far as I know, the idea of converting recursive definitions to explicit ones goes back to Dedekind.)