Mathematics Asked on January 5, 2022
(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.
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.")
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.
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?
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}modelsvarphi$ 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."
$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}rightarrowmathsf{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$ "$Vnotmodels forall x(x=x)$."
Hehehehe.
This is because the expression "$Vnotmodelsforall x(x=x)$," if we try to construe it directly as above, is shorthand for: "There is a function with domain $Vtimes 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 $piin 42$?," it's not totally clear that "Does $Vmodels 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 $Vmodels ...$"-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}$.
Answered by Noah Schweber on January 5, 2022
2 Asked on November 2, 2021
1 Asked on November 2, 2021 by titanium
elliptic equations heat equation multivariable calculus partial differential equations
0 Asked on November 2, 2021
1 Asked on November 2, 2021 by minyoung-kim
7 Asked on November 2, 2021
1 Asked on November 2, 2021 by saulspatz
6 Asked on November 2, 2021 by perturbative
abstract algebra algebras ring isomorphism ring theory vector spaces
2 Asked on November 2, 2021 by meowdog
2 Asked on November 2, 2021 by lereau
3 Asked on November 2, 2021 by mr_e_man
complex numbers convergence divergence dynamical systems inequality sequences and series
1 Asked on November 2, 2021 by vincent-granville
additive combinatorics modular arithmetic number theory sumset
6 Asked on November 2, 2021
2 Asked on November 2, 2021 by drift-speed
calculus ceiling and floor functions limits sequences and series
6 Asked on November 2, 2021
integration multiple integral multivariable calculus physics
4 Asked on November 2, 2021
2 Asked on November 2, 2021 by user808945
2 Asked on November 1, 2021 by gregory-j-puleo
5 Asked on November 1, 2021 by user766881
4 Asked on November 1, 2021
algebra precalculus inverse function solution verification trigonometry
2 Asked on November 1, 2021 by user525966
algebra precalculus geometry mathematical astronomy trigonometry
Get help from others!
Recent Questions
Recent Answers
© 2023 AnswerBun.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP