There's a (fairly basic) fact I want to use in a paper I'm writing; it's not entirely trivial, so I don't feel comfortable just stating the result and moving on, but I don't have a citation for it. Can anyone provide a reference? (I'd be willing to include it if I thought it was new, but it's the sort of thing that at least feels like folklore.) I've put the proof below for those interested.


The result is a kind of $\Sigma^1\_1$ bounding claim (although the proof I have doesn't actually use $\Sigma^1\_1$ bounding); namely, that from a $\Sigma^1\_1$ description of an ordinal relative to some structure, I can pass to a computable description of a possibly longer ordinal relative to that same structure.


Formally, the result is:


**Suppose** we have


* a countable structure (in a finite (or at worst computable) language) $\mathfrak{A}$,
* a $\Sigma^1\_1$ formula $\varphi(x, X)=\exists Y\psi(x, X, Y)$, and
* an ordinal $\alpha$,


such that $\varphi$ defines a copy of $\alpha$ uniformly from any copy of $\mathfrak{A}$; more precisely, such that whenever $A$ is a structure with domain $\omega$ which is isomorphic to $\mathfrak{A}$ (below: *$\omega$-copy*), $\varphi(x, A)$ defines a well-ordering of $\omega$ of ordertype $\alpha$.


**Then** there is some $e\in\omega$ and some ordinal $\beta\ge\alpha$ such that for each $\omega$-copy $A$ of $\mathfrak{A}$, $\Phi\_e^A\cong\beta$.


EDIT: In fact, from the proof we get a slightly stronger result - that if there is a $\Sigma^1\_1$ formula which defines an ordinal when fed any copy of $\mathfrak{A}$, then there is some ordinal uniformly computable from copies of $\mathfrak{A}$ which is greater than any of the ordinals the above formula can produce from any copy of $\mathfrak{A}$. (This is not quite a trivial application of $\Sigma^1\_1$-bounding, because of the word "uniformly": $\Sigma^1\_1$-bounding does give us that there is an ordinal $\alpha$ which is computable in each copy of $\mathfrak{A}$ and appropriately large, but it does not give a *uniform* computation of $\alpha$ from arbitrary copies of $\mathfrak{A}$.)




---


Proof: First, terminology. For $k\in\omega$, a *$k$-shuffle* is a bijection $f: A\rightarrow B$ for some $A, B\subset\omega$ with $\vert A\vert=\vert B\vert=2k$ and $\{0, ..., k-1\}\subset A\cap B$. The point is that if $\sigma\_i$ are $i$-shuffles for $i\in\omega$ and $s\_0\subset s\_1\subset...$, the map $\bigcup s\_i$ is in fact a permutation of $\omega$. *This is basically the back-and-forth condition.*


Now given an $\omega$-copy $A$ of $\mathfrak{A}$, we build a tree $T\_A$ as follows. We'll then convert this into a well-founded tree $S\_A$, and let $\beta$ be the Kleene-Brouwer order of that tree. *The trees in question are not defined as sets of finite strings of natural numbers; but to take the Kleene-Brouwer order of a tree, we need an appropriate lateral ordering on the nodes, coming from a well-ordering of the "symbols." So fix in the background some appropriate way of viewing the trees below as subsets of $\omega^{<\omega}$.*


$T\_A$ is defined as follows. A node of length $k$ on $T\_A$ is a four-tuple $(s, l, w, n)$ such that:


* $s$ is a $k$-shuffle (which builds part of a possibly-different $\omega$-copy $B$ from the $\omega$-copy $A$)
* $l$ is a finite linear order with domain $\{0, 1, ..., k-1\}$ (which describes the node's guess as to the ordering of the copy of $\alpha$ built by the copy of $\mathfrak{A}$ our shuffle produces from $A$)
* $w\in\omega^k$ (which is a partial witness to the correctness of $l$ above)
* $p\in\omega^k$ (which isn't doing anything except to "pad out" the tree, to guarantee that $S\_A$ embeds into $S\_B$ for any pair of $\omega$-copies $A, B$; I don't think this is necessary but it clears out a possible problem), and
* $w$ has *not* been seen at stage $k$ to fail to be a witness to $l\subset\varphi(-, s(A))$. *Note that by the Normal Form Theorem, we may take the matrix $\psi$ of $\varphi$ to be $\Pi^0\_1$ so this makes sense; even if it were higher arithmetic, we could still make this work by having our node contain "more data" - specific guesses about the relevant witnesses.*


The ordering on $T\_A$ is the obvious one. Note that $T\_A$ is uniformly computable from $A$.


Now we build a well-founded tree $S\_A$ associated to the (very ill-founded) tree $T\_A$. Namely, a node on $S\_A$ of length $n$ is a sequence of pairs $\langle \sigma\_i, \tau\_i\rangle\_{i<n}$ such that


* $\sigma\_i=(s\_i, l\_i, w\_i, p\_i)$ is a node on $T\_A$ with $\sigma\_0<\sigma\_1<...$, and
* $\tau\_i$ is a descending sequence in $l\_i$ of length $i$.


Note that $S\_A$ is again uniformly computable from $A$, and that $S\_A$ is wellfounded since any infinite path would represent an infinite descending sequence in the copy of $\alpha$ built from the relevant copy of $A$. Finally, let $\beta\_A$ be the ordertype of the Kleene-Brouwer ordering of $S\_A$.


Because of the padding coordinate $p$, it's easy to see that $S\_A$ embeds into $S\_B$ for any two $\omega$-copies $A, B$ of $\mathfrak{A}$; so $\beta\_A=\beta\_B=\beta$. And the tree of descending sequences in $\alpha$ embeds into $S\_A$, so $\beta\ge\alpha$. Since taking Kleene-Brouwer orderings is computable, we're done. $\quad\Box$


*It should be clear at this point why I don't want to include the proof - it's a bit lengthy but doesn't really involve anything non-easy.*


*It's only borderline relevant, but I've added the "descriptive set theory" tag because of the tangential connection to $\Sigma^1\_1$ bounding; I could see this result being stated in a descriptive set theory paper on the more model-theoretic side.*



Reference request: a version of $\Sigma^1_1$ bounding for structures
After asking around for a while, it appears that there is no prior reference for this fact. I'm posting and accepting this answer to move this question off the unanswered list. That said, if anyone does later find a reference for this, please post it as an answer - I'll accept it and delete this one.


*(I've made this CW since I don't really think reputation gain for inactivity-made-explicit is appropriate.)*


