*(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](https://math.stackexchange.com/a/4470134/28111) 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.



Are there quantifiers that require multiple "steps" to define?
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}$.


