11
$\begingroup$

(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.

$\endgroup$
13
  • $\begingroup$ Do you have an example of a non-first-order quantifier that is definable from $\mathcal{L}_0$? $\endgroup$ Jun 13, 2022 at 4:57
  • $\begingroup$ What kind of thing is $U$ in the definition of $\Phi_\forall$ et al? @JamesHanson if we drop the finiteness restriction on $\Phi$, you can define $\exists^\infty$ in $\mathcal{L}_0(\exists)$. $\endgroup$ Jun 13, 2022 at 5:08
  • 2
    $\begingroup$ @GregNisbet $U$ is a unary relation symbol, and $a$ is a constant symbol. This was stated in more detail IIRC in my linked answer. $\endgroup$ Jun 13, 2022 at 5:08
  • 1
    $\begingroup$ @JamesHanson "Do you have an example of a non-first-order quantifier that is definable from $\mathcal{L}_0$?" No. However, we can define $\exists^\infty$ over $\mathsf{FOL}$ using a finite set of sentences (or single sentence of course). I've added the details since it makes $\exists^\infty$ a plausible candidate. $\endgroup$ Jun 13, 2022 at 5:18
  • 1
    $\begingroup$ @NoahSchweber Out of curiosity: is this notion of quantifier standard? What is the reason for requiring permutation invariance? $\endgroup$
    – Zhen Lin
    Jun 13, 2022 at 12:31

1 Answer 1

3
$\begingroup$

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}$.

$\endgroup$
4
  • 1
    $\begingroup$ I don't quite follow this. Can you elaborate? Why does truth in $\mathfrak{M}'$ imply truth in $\mathfrak{M}$? $\endgroup$ Nov 10, 2022 at 4:02
  • 1
    $\begingroup$ Of course, hopefully the new version is clearer. I explained in more details the main inferences and removed an assertion that was not necessary for the reasoning and might thus have been misleading. $\endgroup$
    – jmd
    Nov 10, 2022 at 8:56
  • $\begingroup$ I'm terribly sorry I only had a chance to read this carefully after the bounty had passed - this is a nice answer! $\endgroup$ Nov 18, 2022 at 2:19
  • $\begingroup$ Thanks and don't worry about it. The question is beautiful and I enjoyed puzzling it out. $\endgroup$
    – jmd
    Nov 21, 2022 at 8:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.