Löwenheim number of the logic $\mathrm{FOL}[L]$ ($(Lx)[\varphi,\psi]$ holds iff $|\{x:\varphi\}| \ge 2^{|\{x:\psi\}|}$) What is the Löwenheim number of the logic $\mathrm{FOL}[L]$?
Let $L$ be the quantifier with the intended reading a lot more, and the semantics shown at the end of this section. $D_1$ and $D_2$ are sorts. The variable introduced by $L$ can have different sorts in the left and right branches. $2^\square$ is the ordinal map $ \omega \mapsto 2^\omega$.
For the purposes of this question, I will treat the cardinals as a subclass of the ordinals.
$$ (L x : (D_1, D_2))[\varphi(x), \psi(x)] \;\text{holds} \;\;\textit{if and only if}\;\; |\{x : \varphi(x)\}| \ge 2^{|\{x : \psi(x)\}|} $$

A Löwenheim number is defined as:

the smallest cardinal $\kappa$ such that if an arbitrary sentence of [the logic] has any model, the sentence has a model of cardinality no greater than $\kappa$.

I'm interested in this quantifier because it can be used to define $\exists$ and thus $\forall$.
$$ (\exists x)[\varphi(x)] \;\; \text{can be defined as} \;\; (Lx)[\varphi(x), x \neq x] $$
I'm curious what the Löwenheim number of $\mathrm{FOL}[L]$ is.
Let $\varphi^0$ be a first-order axiom of infinity. $\varphi^0$ is also a $\mathrm{FOL}[L]$ sentence, therefore the Löwenheim number is at least $\beth_0$.
However, we can define $\varphi^1$ by introducing a new predicate symbol $R^1$. This shows that the Löwenheim number is at least $\beth_1$.
$$ \varphi^1 \;\;\text{is defined as}\;\; (Lx)[R^1(x), \varphi^0(x)] $$
And we can define $\varphi^{(n+1)}$ as follows.
$$ \varphi^{(n+1)} \;\;\text{is defined as}\;\; (Lx)[R^{(n+1)}(x), \varphi^{n}(x)] $$
I think this proves that the Löwenheim number of this logic is at least $\beth_\omega$, but I'm not sure. I'm also not sure how much higher the true Löwenheim number of $\mathrm{FOL}[L]$ is (assuming my argument is correct).
 A: You are correct that the Lowenheim number of this logic, which I'll call "$\lambda$," is at least $\beth_\omega$. However, $\lambda$ is in fact much larger than $\beth_\omega$, due to the power which parameters bring into the new quantifier $\mathsf{L}$.
Roughly speaking, suppose I have a pair of binary relation symbols $R, S$. Then in $\mathsf{FOL[L]}$ I can write a sentence $\theta$ saying the following:

*

*$R$ is a linear order;


*whenever $R(x,y)$ we have $\mathsf{L} z(S(y,z),S(x,z))$.
Basically, this says that $R$ and $S$ together describe a sequence of sets which increase rapidly in size. Building off of this we can for example write a satisfiable sentence $\beta$ whose smallest model has cardinality $\min\{\alpha:\beth_\alpha=\alpha\}$, the least "$\beth$ fixed point," which is much bigger than $\beth_\omega$ (it's the limit of the sequence $\beth_\omega,\beth_{\beth_\omega},\beth_{\beth_{\beth_\omega}}$, ...): basically, say add to the above sentence a clause saying that the domain of $R$ is the whole universe. Note that if we drop the exponential aspect of $2^-$, we'll still get a rather large lower bound on the Lowenheim number, namely the least $\aleph$ fixed point.
(As a cute aside, note that there is no infinite sequence of sets $(A_i)_{i\in\omega}$ such that $2^{\vert A_{i+1}\vert}<\vert A_i\vert$. This means that the $\theta$-trick above also lets us restrict attention to well-orderings in a way quite beyond the capacity of first-order logic alone. Note that the nonexistence fact two sentences prior does not rely on the axiom of choice as long as we use the exponential version of $\mathsf{L}$; this is a good exercise, and falls e.g. out of the proof of the existence of Hartogs numbers.)
