What is the least order type of this set?

Question

Working in ZFC - Infinity, lets say that there exists two sets $A, B$ that are nonempty and mutually disjoint, and $A$ is well ordered by relation $<^A$, and $B$ is well ordered by relation $<^B$. Now an initial segment $A^-$ of $A$ is defined as a subset of $A$ that is closed under $<^A$, and similarly define initial segments of $B$. Of course $A,B$ are initial segments of themselves. Now let $A$ be isomorphic to some proper $B^-$, that is: $$\exists f (f: A \to B^- \land \\ f \text{ is bijective } \land \\\forall x,y \in A [x <^A y \leftrightarrow f(x) <^B f(y)])$$

Now I want to coin a sort of definitional equivalence between subsets of $A$ and subsets of $B$, so we say that a subset $S^A$ of $A$ that is definable after a formula $\phi^A$ whose variables range over $A \cup P(A)$ and that uses $=,\in, <^A$ relation symbols is definitionally equivalent to a subset $S^B$ that is definable after the formula $\phi^B$ which is the formula obtained from $\phi^B$ by replacing every occurrence of the $A$ symbol by the symbol $B$, and all of its variables are taken to range over $B \cup P(B)$, examples are the set which only contain the initial element of $A$ with respect to $<^A$, this is definitially equivalent to the set that only contain the initial element of $B$ with respect to $<^B$; another example is $A$ and $B$ themselves, they are definitially equivalent after formula $\forall x (x \in X \leftrightarrow x \in A)$.

Now comes the question: if we say that for any formula $\phi$ if $A^-$ is definable after $\phi$ and its definitional equivalent is isomorphic to it, then $A^- \neq A$ that is: there is an element of $A$ such that all elements of $A^-$ has the relation $<^A$ to; then:

what's the least possible order type of set $A$?

Answer 1

Rephrasing to use more standard terminology, you're looking at second-order-definable subsets of ordinals. Specifically, say that $(\alpha,\beta)$ is a good pair if $\alpha<\beta$ and for every second-order formula $\varphi$ we have $$\varphi^\alpha\cong\varphi^\beta\implies \varphi^\alpha\not=\alpha.$$

(Note that replacing "$\not=$" with "$\not\cong$" in the right hand side won't lead to a different notion, since we can take collapses in a second-order-definable manner.) The following shows that good pairs have to be ridiculously large:

Suppose there is a second-order sentence $\theta$ such that $\theta$ pins down $\alpha$ (that is, $\mathcal{A}\models\theta$ iff $\mathcal{A}\cong\alpha$). Then there is no $\beta$ such that $(\alpha,\beta)$ is a good pair.

Put another way:

Let $\sigma$ be the least ordinal not pinned down by a second-order sentence. If $(\alpha,\beta)$ is a good pair then $\sigma<\alpha$.

Proof: Fix such an $\alpha,\theta$. Consider the second-order formula $\hat{\theta}(x)\equiv$ "No initial segment below $x$ satisfies $\theta$." We have $\hat{\theta}^\beta=\alpha$ for all $\beta\ge \alpha$. $\quad\Box$

And $\sigma$ is gigantic. Specifically, we have:

Proposition. Suppose $T$ is any computable (or indeed projective) first-order theory in the language of set theory such that some level of $L$ satisfies $T$. Letting $\alpha_T=\min\{\alpha: L_\alpha\models T\}$, we then have $\sigma>\alpha_T$.

And from this we get:

Corollary. Suppose $T$ is a computable (or indeed projective) first-order theory in the language of set theory such that $T$ has a transitive model. Then $\sigma$ is greater than the shortest height of a transitive model of $T$.

So, for example, $\sigma$ is greater than the minimal height of a transitive model of ZFC + "There is a proper class of supercompacts," assuming there are transitive models of the latter in the first place.

Proof of corollary. Apply the Proposition to $T'=$ ZFC+ "$T$ has a transitive model" and use Shoenfield absoluteness to say that $T'$ holds in some level of $L$ if $T$ has a transitive model in $V$. $\quad\Box$

Proof of proposition. By Condensation we know $\alpha_T<\omega_1^L$. The key fact now is that the set of $\alpha<\omega_1$ such that $L_\alpha$ is pointwise-definable is cofinal in $\omega_1^L$. If $\beta<\alpha_T$, let $\gamma$ be the smallest ordinal $>\alpha_T$ such that $L_\gamma$ is a pointwise-definable model of ZFC+V=L and let $\varphi^{L_\gamma}=\{\beta\}$. Then $\beta$ is the unique ordinal $\gamma$ such that there is a pointwise-definable model $M$ of ZFC+V=L satisfying "$\alpha_T$ exists and there is no pointwise-definable level of $L$ satisfying $ZFC$ of height $>\alpha_T$" such that $\varphi^M\cong\gamma$. Since WLOG $\beta$ is infinite, and all the structures we're considering are countable by Condensation, we can talk about existence of such structures in $\beta$ in a second-order way ("There is a family of relations on me such that ..."). $\quad\Box$

---

On the other hand, we do at least get that $\sigma<\omega_1$. This raises the natural question:

Is there a good pair $(\alpha,\beta)$ with $\alpha$ countable?

The answer to this is yes: by a straightforward counting argument, there is some $\alpha<\omega_1$ such that no subset of $\omega_1$ of ordertype $\alpha$ is second-order definable in $\omega_1$. Then $(\alpha,\omega_1)$ forms a good pair.

This, in turn, raises one last natural question:

Is there a good pair $(\alpha,\beta)$ with $\beta$ countable?

The pigeonhole principle trick in the previous bulletpoint doesn't work here. Moreover, note that $\omega_1$ is pinned down by a second-order sentence, so we're not going to find a "sufficiently $\omega_1$-like" ordinal to just trivially reflect the argument above.

I don't immediately have an answer to this question.