Roughly speaking, given a set-sized logic $\mathcal{L}$ let $\mathcal{L}'$ be gotten by adding to $\mathcal{L}$ the ability to quantify over $\mathcal{L}$-definable relations. (The details are a bit tedious, so I've put the rigorous definition at the end of this question.) Note that $\mathcal{L}'$ is always strictly stronger than $\mathcal{L}$: let $\kappa$ be some cardinal greater than the set of $\mathcal{L}$-formulas in the language $\{<\}$, and consider the least $\mathcal{L}$-undefinable element of the structure $(\kappa;<)$. We can iterate this jump operation up to any ordinal $\alpha$ by taking unions at limit stages as usual (since we're not worrying about syntax there is no "notation"-flavored issue) to get $\mathcal{L}^{(\alpha)}$. Even iterating through all the ordinals makes sense; call the result $\mathcal{L}^{(\infty)}$.
I'm interested in pinning down $\mathsf{FOL}^{(\infty)}$. Here's what I know so far:
-
$\mathsf{FOL}^{(\infty)}$ is (always up to expressive strength) a sublogic of $\mathcal{L}_{\infty,\omega}^L=\mathcal{L}_{\infty,\omega}\cap L$. More generally, if $M$ is an inner model and $\mathcal{L}$ is a set-sized sublogic of $\mathcal{L}_{\infty,\omega}^M$ which is appropriately definable in $M$, then $\mathcal{L}'\subseteq\mathcal{L}^M_{\infty,\omega}$ as well.
-
$\mathsf{FOL}^{(\infty)}$ is strictly weaker than $\mathcal{L}_{\infty,\omega}^L$: if $(r_i)_{i\in\omega}$ are sufficiently mutually Cohen generic (say, generic over a countable elementary submodel of $L_{\omega_1}$), then the $\{<,\in\}$-structures $\omega\sqcup\{r_{2i}:i\in\omega\}$ and $\omega\sqcup\{r_{2i+1}: i\in\omega\}$ are $\mathsf{FOL}^{(\infty)}$-equivalent but not $\mathcal{L}_{\infty,\omega}^L$-equivalent.
-
The argument of the previous bulletpoint implies that the $\mathsf{FOL}^{(\infty)}$-definable relations on $(\omega;<)$ fall well short of the constructible ones. On the other hand, it's also easy to see that they reach well past the hyperarithmetic: the $\mathsf{FOL}^{(\omega_1^{CK})}$-definable relations are exactly the hyperarithmetic ones, and $\mathcal{O}$ is then $\mathsf{FOL}^{(\omega_1^{CK}+1)}$-definable since a computable linear order is a well-order iff it supports a hyperarithmetic jump sequence.
-
Finally, despite its clear weaknesses, for every countable structure $\mathfrak{A}$ the automorphism orbit relation on elements (or $n$-tuples for fixed $n$) of $\mathfrak{A}$ is $\mathsf{FOL}^{(\infty)}$-definable (this is just Scott's argument).
My main question is whether there is a better description of this logic as a whole:
Question 1: Is there a snappier description of $\mathsf{FOL}^{(\infty)}$?
The definition of $\mathsf{FOL}^{(\infty)}$ is "bottom-up" (a more snappy version: it's the smallest possibly-class-sized logic containing $\mathsf{FOL}$ and containing $\mathcal{L}'$ whenever $\mathcal{L}$ is a set-sized logic it contains). I would be especially be interested in a "top-down" definition, such as "the largest logic containing $\mathsf{FOL}$ with [tameness properties]." Lindstrom's theorem is one motivating example of such a definition, but there are others – e.g. Barwise's analysis of $\mathcal{L}_{\infty,\omega}$.
My secondary question, for which I at least have a conjecture, is about its arithmetic power specifically:
Question 2: What are the $\mathsf{FOL}^{(\infty)}$-definable relations on the naturals?
My guess is that these are exactly the relations in $L_{\beta_0}$, where ${\beta_0}$ is the smallest "gap ordinal" (= such that $L_{\beta_0}\cap\mathbb{R}=L_{\beta_0+1}\cap\mathbb{R}$). This ${\beta_0}$ is known to also be the least ordinal such that $L_{\beta_0}\models\mathsf{ZFC^-}$, or such that $L_{\beta_0}\cap\mathbb{R}\models\mathsf{Z}_2$. See Putnam, Marek/Srebrny, or Madore (entry 2.17).
Details
Here's a more precise definition of $\mathcal{L}'$. We take the closure of the $\mathcal{L}$-formulas under the addition of a whole family of new relation quantifiers $$\bigtriangledown^{\mathcal{L},p}_{\delta,\eta,\rho_1,…,\rho_n}.$$ Here the $\mathcal{L}$-superscript indicates the logic with respect to which we are quantifying over definable relations, $p\in\omega$ indicates the arity of the relations being quantified over, and $\delta,\eta,\rho_1,…,\rho_n$ are $\mathcal{L}$-formulas with respective arities $d, e, r_1,…,r_n$ such that $e=2d$ and each $r_i$ is divisible by $d$. The semantics of these new quantifiers is given as follows:
- In any structure $\mathfrak{A}$, if $\eta^\mathfrak{A}$ is an equivalence relation on $\delta^\mathfrak{A}$ and each $\rho_i^\mathfrak{A}$ is well-defined on $\delta^\mathfrak{A}/\eta^\mathfrak{A}$ in the obvious sense, then "$\bigtriangledown^{\mathcal{L},p}_{\delta,\eta,\rho_1,…,\rho_n}X[\mathit{stuff}]$" (with $X$ a $p$-ary relation variable) means
"For every $\eta^\mathfrak{A}$-invariant relation $X\subseteq(\delta^\mathfrak{A})^p$ such that $X/\eta^\mathfrak{A}$ is $\mathcal{L}$-definable in the related structure $(\delta^\mathfrak{A}/\eta^\mathfrak{A}; \rho_1,…,\rho_n)$, it is the case that $[\mathit{stuff}]$."
- On the other hand, if $\delta,\eta,\rho_1,…,\rho_n$ do not satisfy the above conditions in $\mathfrak{A}$, then we interpret $\bigtriangledown^{\mathcal{L},p}_{\delta,\eta,\rho_1,…,\rho_n}$ in some fixed trivial way (say, always outputting $\perp$).
Note that when we iterate $'$ we get multiple $\bigtriangledown$-quantifiers; so, for example, $\mathsf{FOL}^{(\omega)}$ has a separate quantifier (family) $\bigtriangledown^{\mathsf{FOL}^{(n)}}$ for each $n\in\omega$. (Incidentally, a stronger version of this construction was suggested in this MSE post, but I've ultimately decided that the more limited approach here is more natural.)
Best Answer
If I understand the question properly (I'm not sure whether I do), then it looks like your conjecture for question 2 is correct, i.e. $L_{\beta_0}\cap\mathcal{P}(\omega)$. Here is a hastily written sketch.
For in fact, letting $N_\alpha$ be the set of $\mathcal{L}^{(\alpha)}$ relations on $\omega$, then $N_\alpha=L_{\omega+\alpha}\cap\mathcal{P}(\omega)$ for all $\alpha\leq\beta_0$, and $\beta_0$ is a closure point.
The small issue here is to see that over $N_\alpha$, we can simulate $L_\alpha$ definably from parameters, assuming that $N_\alpha=L_\alpha\cap\mathcal{P}(\omega)$.
Suppose $\alpha=\beta+1$. Since $L_\beta$ projects to $\omega$, there is a real $x\in N_\alpha$ which codes $L_\beta$. We can refer to $x$, since this is given by some $\mathcal{L}^{(\alpha)}$ relation. Then in fact for all ordinals in $\gamma\in[\alpha,\kappa_\alpha)$, where $\kappa_\alpha$ is the least admissible $\kappa>\alpha$, we can define simulate $L_\gamma$ over $N_\gamma$ by looking at all models $M$ coded by reals which satisfy ``$V=L[x]$''; all of these are wellfounded, because otherwise the wellfounded part is a model of KP, but it easily enough follows then that $N\notin L_{\kappa_\alpha}$, so $N\notin N_\gamma$. So over $N_\gamma$ we can simulate $L_\gamma$, and hence define (from parameters) all reals in $L_{\gamma+1}$.
So we get that $N_{\kappa_\alpha}=L_{\kappa_\alpha}\cap\mathcal{P}(\omega)$.
Now suppose that $\alpha$ is a limit of admissibles, and we have $N_\alpha=L_\alpha\cap\mathcal{P}(\omega)$. Then over $N_\alpha$, we can simulate $L_\alpha$ by looking at all models $M$ coded by reals, which satisfy ``$V=L$'', and are wellfounded in $N_\alpha$, i.e. have no descending sequence through their ordinals which is in $N_\alpha$. (Any illfounded such model $M$ gets into some $L_\kappa$ for some admissible $\kappa<\alpha$, but then we get a descending sequence before $\alpha$.) So we can simulate $L_\alpha$ over $N_\alpha$ as desired.