Can we define the uniqueness quantifier, in a sense made precise below, without additional quantifiers?
You can extend a first-order structure with user-defined quantifiers of arity $n$ by adding the following rule to the semantics of $\models$.
$$ M, \vec{v} \models Q \vec{x} \mathop. \varphi(\vec{x}, \vec{v}) \;\; \textit{if and only if} \;\; \{\vec{x} : \varphi(\vec{x}, \vec{v})\} \;\; \text{is in $[\![Q]\!]_M$ } $$
$[\![Q]\!]_M$ is a subset of $2^{M^n}$, the $n$-place quantifier that is always true.
The universal quantifier can be defined by the following formulas if we didn't already have it.
- every formula in $(Qx \mathop. \alpha(x)) \to \alpha(y)$
- $Q x \mathop. \top$
This is a definition of $\forall$. The only quantifiers that satisfy the formulas in 1 are $\forall$ and the trivial 1-place quantifier that is always false. $\forall$ is the only possible value for $Q$.
For concreteness, if I say the quantifier $Q$ is definable using $W$ where $W$ is a valuation associating quantifier symbols to their interpretation, it means the following.
There exists a set of well-formed formulas $\Phi$ whose quantifier symbols are $Q$ and the keys of $W$ such that, for every structure $M$ that interprets the symbols of $\Phi$ but does not interpret $Q$, there exists a unique extension $M'$ that defines $Q$ such that $M' \models \Phi$ and $[\![Q]\!]_M$ has the intended interpretation.
We can cook up some genuinely weird quantifiers, like membership in a specific non-principal ultrafilter $U$ on $M$ when $M$ is infinite or something that probably aren't definable.
I'm curious whether the uniqueness quantifier is definable or not if we have no other quantifiers.
If we have $\exists$, which can be defined, then $\exists!$ is the solution to:
- $(\exists w \mathop. \alpha(w) \land \lnot (\exists v \mathop. v \neq w \land \alpha(v))) \leftrightarrow (Q x \mathop. \alpha(x))$
Without having $\exists$ or $\forall$ already, or a spare quantifier symbol that we could endow with their meanings via additional formulas, it seems like we're stuck.
Is this actually true? Can $\exists!$ not be defined without additional quantifiers?
Best Answer
As often happens in logic (and was suggested by the comment thread), this question is easier to answer than it is to state. I'll first give an answer, and then explain how I'm interpreting the question precisely.
Answer
Yes, $\exists!$ is so definable. Here's a set of defining formulas for $\exists!$ which don't use any other quantifiers:
$(a)$: $(\mathscr{Q}x.U(x))\rightarrow [[U(a)\wedge U(b)]\rightarrow [V(a)\vee\neg V(b)]]$.
$(b)$: $\neg\mathscr{Q}x.\perp$.
$(c)$: $\mathscr{Q}x. x=a$.
Intuitively, $(a)$ says that $\mathscr{Q}$ doesn't contain any sets with more than one element, $(b)$ says that $\mathscr{Q}$ doesn't contain the empty set, and $(c)$ says that $\mathscr{Q}$ does contain every set with one element.
(We could have replaced "$V(a)\vee\neg V(b)$" in $(a)$ with "$a=b$," but I think it's cute that we don't need equality there, even if equality is needed in $(c)$.)
Question
OK, now how do we phrase the question precisely?
Alex Kruckman raised the key issue - that once we fix a single structure $\mathcal{M}$, we run into trouble when we try to think about the non-definable subsets of $\mathcal{M}$. However, there is a saving grace here: all the quantifiers you consider are "set-based," that is, their behavior over a structure $\mathcal{M}$ is entirely determined by the underlying set $M$ of $\mathcal{M}$. To be precise, a set-based $n$-ary quantifier is a (class) function assigning to each set $X$ a family of subsets of $X^n$, which is stable under permutations of $X$.
This lets us shift from trying to describe a quantifier over a single structure to describing its behavior over all structures at once. For example, we can describe the definability of $\forall$ as follows:
The proof is exactly the intuitive argument. Suppose $\mathscr{Q}$ is a set-based quantifier satisfying $1$ and $2$ above, $\mathcal{M}$ is any structure with underlying set $M$, and $\varphi$ is a formula in the language of $\mathcal{M}$. If $\mathcal{M}\models\neg \mathscr{Q}x.\varphi(x)$ then we must not have $\varphi$ hold on all of $\mathcal{M}$, by $1$; on the other hand, if $X\subseteq M$ is "$\mathscr{Q}$-big" then considering the expansion of $\mathcal{M}$ by a predicate naming $X$ we get $X=M$ by $2$. So $\mathscr{Q}=\forall$ as hoped.
More generally, given any set-based quantifier $\mathscr{Q}$ let $\mathsf{QFL}[\mathscr{Q}]$ be quantifier-free logic augmented by $\mathscr{Q}$. Basically, we take $\mathsf{FOL}$, remove the quantifiers, and add $\mathscr{Q}$. Your question can (I claim!) be precisely asked as follows:
If you buy this phrasing, then it's easy to check that the answer I gave above does in fact work: if $\mathscr{Q}$ is a set-based quantifier such that $(i),(ii),(iii)$ are each $\mathsf{QFL}[\mathscr{Q}]$-validities, then $\mathscr{Q}$ is in fact $\exists!$.
Coda
First of all, note that "set-based" is not a standard term. I don't think there is one. Sorry about that. Second, and relatedly, not all quantifiers are set-based, with one example being the quantifier $\mathfrak{S}x.\varphi(x)\equiv$ "$\{x:\varphi(x)\}$ meets every substructure of the universe."
Third, and most substantively, we can keep this story going! The above amounts to showing that $\exists,\forall$, and $\exists!$ are each "definable" over $\mathsf{QFL}$ in a particular sense. It turns out that the quantifier $\exists^\infty$ is "definable" over $\mathsf{FOL}$ in the same sense but is not "definable" over $\mathsf{QFL}$, so there is a meaningful hierarchy of quantifiers in terms of steps needed to define them. Not much is known to me about this - for example, is there any quantifier that takes three steps to define? - but see this MO post (and note that the $\mathcal{L}_0$ used there is this post's $\mathsf{QFL}$).