What does it really mean for a model to be pointwise definable?

Question

(Note: I'm only an amateur in logic, so I'm sorry for any weird terminology or notation, or excessive tedious details. Most of what I know is from Kunen's Foundations of Mathematics.)

I'm trying to learn a little about pointwise definable models. I'm looking at "Pointwise definable models of set theory" by Hamkins, Linetsky and Reitz, and I'm stuck on the really basic question of what
"pointwise definable" really means formally.

Let me give a toy example that I hope will illustrate my problem. Let's work in $\mathsf{ZFC}-\mathsf{Infinity}$, or $\newcommand{\ZFCI}{\mathsf{ZFC}-\mathsf{I}}\ZFCI$ for short, and let $HF$ be the class of hereditarily finite sets, which may not itself be a set. But there is certainly a first-order formula which says that $x$ is hereditarily finite, which will be abbreviated as usual by "$x \in HF$". Note that $HF$ is a model of $\ZFCI$, and given any first-order sentence $\varphi$, there is a first-order sentence $HF \vDash \varphi$ which relativizes $\varphi$ to $HF$, i.e. replacing all $\forall y$ with $\forall y \in HF$ and so on.

It's intuitively obvious that the model $HF$ is pointwise definable, because I "know" what all the hereditarily finite sets are, and for each one I can write down a first-order formula in the language of set theory that uniquely defines it. But if I want to try to prove this, I need to know where the statement "lives", and what axioms would be available. I can think of three different possibilities but they each have problems.

1. I could try to state and prove "$HF$ is pointwise definable" as a theorem schema in the metatheory. Now the best way I've found to understand the metatheory is as a system that reasons about "strings": its universe of discourse consists of first-order formulas, sentences, lists of sentences, proofs, etc. So I would have to say something like

   For every set $x \in HF$, there exists a first-order formula $\varphi(y)$ with $y$ free and a proof from the axioms $\ZFCI$ of the sentence $$HF \vDash \forall y (y=x \longleftrightarrow \varphi(y) )\tag{1}$$

   But I have two problems with that statement. Sets are not strings, and so the metatheory can't quantify over them. And the "sentence" (1) is not a sentence because $x$ is free, and I don't know what to put in its place. (This feels like the paradox illustrated by Hamkins' young son in a footnote in the paper: "Tell me any number, and I'll tell you a description of it.")

2. I could try to state and prove "$HF$ is pointwise definable" as a theorem of $\ZFCI$. Now I have the opposite problem with a statement like ``for every set $x \in HF$ there exists a first-order formula $\varphi$'', because first-order formulas are not sets and set theory cannot quantify over them, at least not as such. But I do know that I can encode first-order formulas $\varphi$ as sets $\ulcorner \varphi \urcorner$ using Gödel codes or the like. So I could try to write down a sentence in the language of set theory, of the form $$\forall x \in HF \: \exists\, \ulcorner \varphi \urcorner \: \dots $$ But now I am stuck again because the $\cdots$ needs to say $HF \vDash \forall y (y=x \longleftrightarrow \varphi(y))$, and Tarski's undefinability of truth tells me that there is no first-order formula in $\ulcorner \varphi \urcorner$ and $y$ that expresses that.

3. I could try to state and prove "$HF$ is pointwise definable" as a theorem of some stronger set theory, say $\mathsf{ZFC}$. This gives me a way out of the previous dilemma, because in $\mathsf{ZFC}$, $HF$ is actually a set. And Tarski's definability of truth tells me that there is indeed a first-order formula $\Phi(M, \ulcorner \varphi \urcorner, x)$ which says $M \vDash \varphi(x)$ for set models $M$. So finally I can write a sentence like $$\forall x \in HF \: \exists \ulcorner \varphi \urcorner \: \Phi(HF, \ulcorner \forall y ( y=x \longleftrightarrow \varphi(y) )\urcorner)).$$ But I've paid a price in consistency strength. More generally, if I want to do this for any other class model $M$ of $\ZFCI$, then by Gödel's second incompleteness theorem, I am going to have to work in an axiom system at least as strong as $(\ZFCI) + \mathrm{Con}(\ZFCI)$ so that $M$ has some hope of being a set.

So I'm wondering if 3 is really what's meant when we say that a model is pointwise definable, or if there's some way to salvage 1 or 2, or yet a fourth interpretation that I haven't thought of (some sort of meta-meta-theory, or a different logic or set theory altogether?).

Likewise in the HLR paper, I don't know whether the theorem "there exist pointwise definable models of $\mathsf{ZFC}$" is meant to be understood as a metatheorem, or a theorem of $\mathsf{ZFC}$, or of $\mathsf{ZFC}+\mathrm{Con}(\mathsf{ZFC})$ (in which the models in question are actually sets), or what. I can't figure out how to make sense of the first two, and if they meant the third, it seems surprising that they wouldn't say so explicitly.

I did notice a comment on HLR's page 3 that ``the property of being pointwise definable is not first-order expressible'', which I don't quite understand but is maybe a reference to my problem?

Answer 1

The first point is to distinguish between internal and external properties. This is exacerbated by the fact that we're looking specifically at $\mathsf{ZFC}$, which is "doing double duty" in the most confusing way possible.

The short answer to your question, though, is: "$3$."

---

First, the internal side of things. This is relevant to the end of your question only.

Almost always, when we say "Property X is not first-order expressible" what we mean is "There is no first-order sentence $\varphi$ such that for every appropriate structure $\mathcal{M}$, we have $\mathcal{M}\models\varphi$ iff $\mathcal{M}$ has property X." So, for example, being a torsion group is not first-order expressible.

In particular, "Pointwise definability is not first-order expressible" is a consequence of the following perhaps-simpler result:

Every (infinite) pointwise-definable structure is elementarily equivalent to a non-pointwise-definable structure.

The above statement is made and proved within $\mathsf{ZFC}$. The "nuke" is upwards Lowenheim-Skolem:

• $\mathsf{ZFC}$ proves "If $\mathcal{M}$ is a pointwise-definable structure, then $\mathcal{M}$ is countable."

  • Wait, what? See the very end of this answer.

• $\mathsf{ZFC}$ also proves "Every infinite structure $\mathcal{M}$ is elementarily equivalent to an infinite structure of strictly greater cardinality."

• Putting these together, we have the desired result.

As a corollary, we have the following (again proved in $\mathsf{ZFC}$):

For every first-order theory $T$, either $T$ has no pointwise-definable models at all or the class of pointwise-definable models of $T$ is not an elementary class.

(We need the first clause in case the relevant class is $\emptyset$. This can indeed happen, even if $T$ is consistent: consider the theory of a pure set with two elements.)

---

But the bulk of the issue in your OP is about the external side of things. Here it's your third option which holds, as follows:

• We state and prove each relevant fact $\mathsf{A}$ inside $\mathsf{ZFC}$.

• ... Except that sometimes as a matter of practice, we're sloppy - and either (the two options are equivalent) actually use a stronger system $\mathsf{ZFC+X}$ or prove $\mathsf{X}\rightarrow\mathsf{A}$ for some "unspoken but clear from context" (:P) additional principle $\mathsf{X}$. Standard candidates for $\mathsf{X}$ include the standard "generalized consistency" principles ("$\mathsf{ZFC}$ has a model/$\omega$-model/transitive model") and - far less benignly, but unfortunately with nonzero frequency - the whole slew of large cardinal axioms.

However, it seems to me that the HLR paper is actually pretty good on this point. For example, the first bulletpoint of Theorem $3$ is "If $\mathsf{ZFC}$ is consistent, then there are continuum many non-isomorphic pointwise definable models of $\mathsf{ZFC}$," which is indeed a $\mathsf{ZFC}$-theorem. (I could be missing an elision somewhere else, though.)

---

As a coda, note that above I mentioned that $\mathsf{ZFC}$ proves that every pointwise-definable structure is countable. It does this, moreover, by exactly the "math tea argument." So what gives?

Well, we have to unpack what "Every pointwise-definable structure is countable" means when we phrase it in $\mathsf{ZFC}$. When we say "$\mathcal{M}$ is pointwise-definable," what we mean is that there is an appropriate assignment of truth values to pairs consisting of formulas of the language and tuples of appropriate arity such that [stuff]. This blob of data exists "one level higher" than $\mathcal{M}$ itself, and in particular even the bit of this blob verifying that each element of $\mathcal{M}$ satisfies "$x=x$" is a collection of $\mathcal{M}$-many facts. As such:

Using the "all-at-once" definition of $\models$, which is totally fine for set-sized structures, we have $\mathsf{ZFC}\vdash$ "$V\not\models \forall x(x=x)$."

Hehehehe.

This is because the expression "$V\not\models\forall x(x=x)$," if we try to construe it directly as above, is shorthand for: "There is a function with domain $V\times Formulas(\{\in\})$ such that ...," and that's dead on arrival since there aren't any functions with domain anything like $V$ in the first place.

So actually $\mathsf{ZFC}$ does prove "$V$ is not pointwise definable" - as long as we formulate this blindly. But if we do that, then we have to admit that $\mathsf{ZFC}$ also proves e.g. "There is no sentence which $V$ satisfies." Which ... yeah.

Incidentally, the above should make you worry about a couple things:

• Relatively benignly, is the "all-at-once" definition of $\models$ actually appropriate for set-sized structures? As a matter of fact it is, but this is not entirely trivial. Specifically, the $\mathsf{ZFC}$ axioms are strong enough to perform the recursive construction of the theory of a structure, and so prove that for each (set-sized) structure $\mathcal{M}$ there is exactly one relation between formulas and tuples from $\mathcal{M}$ satisfying the desired properties. Weaker theories don't need to be this nice: while any non-totally-stupid theory can prove that at most one "theory-like thing" exists for a given structure, if we go weak enough we lose the ability to carry out Tarski's "algorithm." (Fortunately, we do in fact have to go quite weak; see my answer here.)

• More foundationally, why are we so blithe about how we formulate various mathematical claims in the language of set theory? Of course this isn't at all new, and in particular the above observation that in a precise sense $\mathsf{ZFC}$ proves "$V$ doesn't satisfy $\forall x(x=x)$" is just another example of a junk theorem. However, to my mind it's one of the more worrying ones: unlike e.g. "Is $\pi\in 42$?," it's not totally clear that "Does $V\models \forall x(x=x)$?" is something we'd never accidentally ask in day-to-day mathematics. Ultimately I'm still not worried, but I do think that this highlights the seriousness of the question "Is $X$ a faithful translation of $Y$?"

• Finally, on a purely technical level: what about set theories which do allow for functions on the universe, and with respect to which therefore the "internal naive $V\models ...$"-situation is nontrivial? Well, per Tarski/Godel(/etc.) we know that things have to still be nasty. See the end of this old answer of mine for a quick analysis of the specific case of $\mathsf{NF}$.