Are there quantifiers that require multiple "steps" to define?

Question

(Below I conflate quantifiers and quantifier symbols in a couple places for readability; I can change that if that actually makes things less readable.)

For the purposes of this question, an $n$-ary quantifier is a (class) function $\mathscr{Q}$ assigning to each (nonempty) set $X$ a family $\mathscr{Q}X$ of subsets of $X^n$ which is stable under permutations of $X$. Given a logic $\mathcal{J}$ and a quantifier $\mathscr{Q}$, let $\mathcal{J}^\mathscr{Q}$ be the extension of $\mathcal{J}$ gotten by "adding $\mathscr{Q}$;" the full definition is a bit tedious, but (for a structure $\mathfrak{M}$ with underlying set $M$) the key clause is $$\mathfrak{M}\models\mathscr{Q}x.\varphi(x)\quad\iff\quad\{a\in\mathfrak{M}:\mathfrak{M}\models\varphi(a)\}\in\mathscr{Q}(M).$$

We can then say that a quantifier $\mathscr{Q}$ is $\mathcal{J}$-definable iff there is a finite set $\Phi$ of $\mathcal{J}$-sentences augmented with a new quantifier symbol $\mathsf{Q}$ such that $\mathscr{Q}$ is the unique quantifier, when used to interpret $\mathsf{Q}$, which makes each sentence in $\Phi$ a tautology. For example, letting $\mathcal{L}_0$ be the quantifier-free fragment of first-order logic, each of the standard unary quantifiers $\forall$, $\exists$, and $\exists!$ is $\mathcal{L}_0$-definable:

• $\Phi_\forall=\{\mathsf{Q}x.\top, (\mathsf{Q}x.U(x))\rightarrow U(a)\}$

• $\Phi_\exists=\{\neg\mathsf{Q}x.\perp, U(a)\rightarrow(\mathsf{Q}x.U(x))\}$

• $\Phi_{\exists!}=\{\mathsf{Q}x.U(x)\wedge U(a)\wedge U(b)\rightarrow a=b,\neg\mathsf{Q}x.\perp, \mathsf{Q}x.x=a\}$

(See here for more discussion of this.) More interestingly (pathologically?), the "infinitely-many" quantifier $\exists^\infty$ is definable over full first-order logic; since it provides a possible solution to this question, I'll put the proof of this at the end of this answer.

I'm curious whether there is a quantifier which is not definable over $\mathcal{L}_0$ but is definable over $\mathcal{L}_0^{\mathscr{Q}_1,...,\mathscr{Q}_n}$ for some definable-over-$\mathcal{L}_0$ quantifiers $\mathscr{Q}_1,...,\mathscr{Q}_n$. More snappily:

Main question: Over $\mathcal{L}_0$, if a quantifier is definable relative to definable quantifiers, is it definable?

A natural follow-up question is to understand what properties of a general logic $\mathcal{J}$ lead to an answer one way or the other, but $\mathcal{L}_0$ seems like an already-interesting starting point. Note that although this question isn't directly about quantification over sets, there is a fundamentally higher-order aspect to this idea of quantifier definability, hence the "higher-order-logics" tag.

EDIT: perhaps the following sub-question may be more easily attacked:

Secondary question: Can $\exists^\infty$ be defined over $\mathcal{L}_0$ using a set of formulas each of which contains exactly one instance of "$\mathsf{Q}$"?

My hope is that this secondary question has a relatively easy negative answer, which would constitute helpful progress towards the expected answer ("yes, and $\exists^\infty$ does the job") to the main question.

---

A natural candidate

I didn't notice this at first, but there is a natural candidate for a positive answer: the quantifier $\exists^\infty$. This is definable over $\mathsf{FOL}$ (and so is "two-step-definable" over $\mathcal{L}_0$) as follows.

The sentences $$\mathsf{Q}x.U(x)\rightarrow\mathsf{Q}x.[U(x)\vee V(x)],$$ $$\neg\mathsf{Q}x.\perp,$$ and $$[\neg\mathsf{Q}x.U(x)]\rightarrow\neg\mathsf{Q}x.(U(x)\vee x=a)$$ are "tautologized" by exactly those $\mathscr{Q}$ which are "sub-quantifiers" of $\exists^\infty$; the first sentence corresponds to monotonicity, while the second and third rule out the sufficiency of a finite sets of satisfying instances.

Now let $\nu$ be a first-order sentence which only has infinite models not using the unary relation symbol $U$; the sentence $$\nu^U\rightarrow\mathsf{Q} x. U(x)$$ (where $\nu^U$ is the relativization of $\nu$ to $U$ as usual) gets us the rest of the way there.

This results in a finite defining set for $\exists^\infty$ ... over $\mathsf{FOL}$. However, there is no obvious way to bring this down to $\mathcal{L}_0$, specifically because of the last step.

Answer 1

The quantifier $\exists^\infty$ is not definable over $\mathcal{L}_0$.

To prove it, we show that a sentence $S$ tautologised by $\exists^\infty$ is also a tautology for the "always false" quantifier $\mathsf{F}$.

Let $\mathfrak{M}$ be a model for $S$. From $\mathfrak{M}$, we build a finite model $\mathfrak{M}'$ which gives the same values to the subformulas of $S$ containing no $\mathsf{Q}$ and no bound variable. The model $\mathfrak{M}'$ is constructed by restricting to a finite subset of relevant elements and changing the values of functions on elements that do not appear in the evaluation of the atomic subformulas of $S$. Since $S$ evaluates to true over $\mathfrak{M}'$ for $\exists^\infty$, it also evaluates to true for $\mathsf{F}$ because the two quantifiers are equal on finite models.

The sentence $S$ is a boolean combination of atomic subformulas and quantified subformulas. For $\mathsf{Q}=\mathsf{F}$ over $\mathfrak{M}$ and $\mathfrak{M}'$, the quantified subformulas evaluate to false and the atomic subformulas do not change their values (by contruction of $\mathfrak{M}'$). This implies that $S$ is true for $\mathsf{F}$ over $\mathfrak{M}$ also. Since $\mathfrak{M}$ is arbitrary, $S$ is tautologised by $\mathsf{F}$.