116

Ten years ago, when I studied in university, I had no idea about definable numbers, but I came to this concept myself. My thoughts were as follows:

  • All numbers are divided into two classes: those which can be unambiguously defined by a limited set of their properties (definable) and those such that for any limited set of their properties there is at least one other number which also satisfies all these properties (undefinable).
  • It is evident that since the number of properties is countable, the set of definable numbers is countable. So the set of undefinable numbers forms a continuum.
  • It is impossible to give an example of an undefinable number and one researcher cannot communicate an undefinable number to the other. Whatever number of properties he communicates there is always another number which satisfies all these properties so the researchers cannot be confident whether they are speaking about the same number.
  • However there are probability based algorithms which give an undefinable number as a limit, for example, by throwing dice and writing consecutive numbers after the decimal point.

But the main question that bothered me was that the analysis course we received heavily relied on constructs such as "let $a$ be a number such that...", "for each $s$ in the interval..." etc. These seemed to heavily exploit the properties of definable numbers and as such one can expect the theorems of analysis to be correct only on the set of definable numbers. Even the definitions of arithmetic operations over reals assumed the numbers are definable. Unfortunately one cannot take an undefinable number to bring a counter-example just because there is no example of undefinable number. How can we know that all of those theorems of analysis are true for the whole continuum and not just for a countable subset?

Anixx
  • 9,302
  • Added [lo.logic] and [math-philosophy] since this seems to be a foundational issue on finitary versus infinitary logic. – Willie Wong Oct 29 '10 at 10:57
  • 2
    Well, no, for the simple reason that in university we often use the axiom of choice. – Qiaochu Yuan Oct 29 '10 at 11:48
  • 45
    I just wrote a long answer to this question, but it was closed just as I was about to click submit. Can we re-open please? I think that there are a number of very interesting issues here. – Joel David Hamkins Oct 29 '10 at 12:48
  • Joel, Anixx: I alos find this question interesting. Where do I click to support reopening? – Łukasz Grabowski Oct 29 '10 at 13:00
  • @Lukasz and Anixx: you need at least 3000 rep to vote on re-opening. – Thierry Zell Oct 29 '10 at 13:05
  • 5
    Meta thread: http://tea.mathoverflow.net/discussion/729/why-people-vote-to-close-questions-outside-of-their-field/ . I have also voted to reopen. – Qiaochu Yuan Oct 29 '10 at 13:07
  • And so, what the consequences for the analysis from the assumption that all objects are definable? Will that new analysis differ from the standard one or nothing changes? – Anixx Oct 29 '10 at 18:27
  • 47
    I disagree with the continuing votes to close. The topic of definability is mathematically rich and forms the basis of huge parts of model theory, particularly where it connects with algebra and algebraic geometry, such as in the deep work of o-minimality. In the set-theoretic context, various technical meta-mathematical issues become prominent. The question is well-motivated, sincere and has mathematically interesting answers. – Joel David Hamkins Oct 30 '10 at 22:43
  • 8
    In particular, I can imagine further technical answers arguing the line that in a model of $V=HOD$, the definable objects indeed form an elementary substructure of the universe, fulfilling the OPs observation that statements of analysis can be viewed as ultimately about definable objects. – Joel David Hamkins Oct 30 '10 at 22:43
  • 7
    Similar issues with definability lay at the heart of this MO question: http://mathoverflow.net/questions/34710/succinctly-naming-big-numbers-zfc-versus-busy-beaver/34730#34730 – Joel David Hamkins Oct 30 '10 at 23:27
  • @Joel David Hamkins what does your theory say about the limits of probability-based sequences (such as in the last point in the question)? Does it say that such sequences have no limit or that the limit is anyway definable or that throwing dice randomly is impossible? – Anixx Jan 07 '14 at 23:30
  • I don't think I have a "theory" here, but rather was only objecting to what I see as a naive and problematic treatment of definability. You probably don't really mean "definable" in your question, but rather something much more concrete, in which case the notion of definability for that class is not itself in that class. – Joel David Hamkins Jan 07 '14 at 23:46
  • @Joel David Hamkins I was wondering how your pointwise definable models handle the random sequences such as in the question. It seems to me that a random function (throwing the dice) would not be possible in such models, because it is undefinable, am I correct? – Anixx Jan 07 '14 at 23:59
  • 4
    Well, the pointwise definable models are still models of ZFC, which is a theory that can prove all the usual facts about random variables and so on. (And if one has some concept of randomness that cannot be formalized in ZFC, then I would want it become much clearer.) Nevertheless, every object in a pointwise definable model does has some expressible special feature that only it has, and I agree that this violates some of our naive prereflective intuitions that we might have about what it means to have a "random" object. – Joel David Hamkins Jan 08 '14 at 00:27
  • The link to tea.mathoverflow.net in a previous comment is broken, but a snapshot is saved on the Wayback Machine. – The Amplitwist Jan 31 '24 at 11:17
  • Reposting a link mentioned in a previous comment so that it appears in the "Linked" questions list: Joel David Hamkins's answer to "Succinctly naming big numbers: ZFC versus Busy-Beaver" – The Amplitwist Jan 31 '24 at 11:19

4 Answers4

234

The concept of definable real number, although seemingly easy to reason with at first, is actually laden with subtle metamathematical dangers to which both your question and the Wikipedia article to which you link fall prey. In particular, the Wikipedia article contains a number of fundamental errors and false claims about this concept.   (Update, April 2018: The Wikipedia article, Definable real numbers, is now basically repaired and includes a link to this answer.)

The naive treatment of definability goes something like this: In many cases we can uniquely specify a real number, such as $e$ or $\pi$, by providing an exact description of that number, by providing a property that is satisfied by that number and only that number. More generally, we can uniquely specify a real number $r$ or other set-theoretic object by providing a description $\varphi$, in the formal language of set theory, say, such that $r$ is the only object satisfying $\varphi(r)$.

The naive account continues by saying that since there are only countably many such descriptions $\varphi$, but uncountably many reals, there must be reals that we cannot describe or define.

But this line of reasoning is flawed in a number of ways and ultimately incorrect. The basic problem is that the naive definition of definable number does not actually succeed as a definition. One can see the kind of problem that arises by considering ordinals, instead of reals. That is, let us suppose we have defined the concept of definable ordinal; following the same line of argument, we would seem to be led to the conclusion that there are only countably many definable ordinals, and that therefore some ordinals are not definable and thus there should be a least ordinal $\alpha$ that is not definable. But if the concept of definable ordinal were a valid set-theoretic concept, then this would constitute a definition of $\alpha$, making a contradiction. In short, the collection of definable ordinals either must exhaust all the ordinals, or else not itself be definable.

The point is that the concept of definability is a second-order concept, that only makes sense from an outside-the-universe perspective. Tarski's theorem on the non-definability of truth shows that there is no first-order definition that allows us a uniform treatment of saying that a particular particular formula $\varphi$ is true at a point $r$ and only at $r$. Thus, just knowing that there are only countably many formulas does not actually provide us with the function that maps a definition $\varphi$ to the object that it defines. Lacking such an enumeration of the definable objects, we cannot perform the diagonalization necessary to produce the non-definable object.

This way of thinking can be made completely rigorous in the following observations:

  • If ZFC is consistent, then there is a model of ZFC in which every real number and indeed every set-theoretic object is definable. This is true in the minimal transitive model of set theory, by observing that the collection of definable objects in that model is closed under the definable Skolem functions of $L$, and hence by Condensation collapses back to the same model, showing that in fact every object there was definable.

  • More generally, if $M$ is any model of ZFC+V=HOD, then the set $N$ of parameter-free definable objects of $M$ is an elementary substructure of $M$, since it is closed under the definable Skolem functions provided by the axiom V=HOD, and thus every object in $N$ is definable.

These models of set theory are pointwise definable, meaning that every object in them is definable in them by a formula. In particular, it is consistent with the axioms of set theory that EVERY real number is definable, and indeed, every set of reals, every topological space, every set-theoretic object at all is definable in these models.

  • The pointwise definable models of set theory are exactly the prime models of the models of ZFC+V=HOD, and they all arise exactly in the manner I described above, as the collection of definable elements in a model of V=HOD.

In recent work (soon to be submitted for publication), Jonas Reitz, David Linetsky and I have proved the following theorem:

Theorem. Every countable model of ZFC and indeed of GBC has a forcing extension in which every set and class is definable without parameters.

In these pointwise definable models, every object is uniquely specified as the unique object satisfying a certain property. Although this is true, the models also believe that the reals are uncountable and so on, since they satisfy ZFC and this theory proves that. The models are simply not able to assemble the definability function that maps each definition to the object it defines.

And therefore neither are you able to do this in general. The claims made in both in your question and the Wikipedia page on the existence of non-definable numbers and objects, are simply unwarranted. For all you know, our set-theoretic universe is pointwise definable, and every object is uniquely specified by a property.


Update. Since this question was recently bumped to the main page by an edit to the main question, I am taking this opportunity to add a link to my very recent paper "Pointwise Definable Models of Set Theory", J. D. Hamkins, D. Linetsky, J. Reitz, which explains some of these definability issues more fully. The paper contains a generally accessible introduction, before the more technical material begins.

  • 1
    So would you say "For all you know, there are only a countable number of sets"? – arsmath Oct 29 '10 at 13:59
  • Well, now I see what you said, Joel. As I understand you say it can be postulated in ZFC that undefinable numbers simply do not exist. And also such models use the term 'uncountable' in the constructivist meaning (uncountable=no practical way to enumerate).

    So, how an analysis built on top of such theories would differ from the conventional analysis based on a theory where the set of definable numbers has lower cardinality than that of continuum?

    – Anixx Oct 29 '10 at 14:25
  • 1
    And also how these theories deal with axion of choice. Take for example the sequence formed as described on the question: with throwing dice. In conventional analysis such sequence will necessary have limit and that limit will be undefinable. But what if the theory postulates that there are no undefinable numbers? What explanation then to choose for such experiment?
      1. There cannot be such sequence because undefinable (undeterministic) functions are not permitted
      1. Undeterministic functions permitted but the numbers do not form a sequence
      1. The sequence does not converge?
    – Anixx Oct 29 '10 at 14:40
  • 30
    @Anixx: No, this is not what Joel was saying. He did not say that it is consistent to "postulate in ZFC that undefinable numbers do not exist". What he was saying was that ZFC cannot even express the notion "is definable in ZFC". And no, this has absolutely nothing to do with constructivism (also please note that even in constructivism uncountable means "not countable", whereas you stated that it means "no practical enumeration" whatever that might mean). – Andrej Bauer Oct 29 '10 at 14:50
  • @ Andrej Bauer He clearly says there can be models of ZFC where undefinable numbers do not exist. So I suppose they are either modifications of ZFC or ZFC with an additional axiom. Regarding constructivism, in constructivism "not countable" has different meaning than in ZFC. So the constructivist continuum is not countable in constructivist sense but perfectly countable in ZFC sense. – Anixx Oct 29 '10 at 15:02
  • So I suppose, by analogy, that the definable continuum of such modified theories as put forward by Joel while is not countable by terminology of such theories, is still perfectly countable in terms of standard ZFC. – Anixx Oct 29 '10 at 15:07
  • 41
    Joel made a very fine answer, please study it carefully. Joel states that there are models of ZFC such that every element of the model is definable. This does not mean that inside the model the statement "every element is definable" is valid. The statement is valid externally, as a meta-statement about the model. Internally, inside the model, we cannot even express the statement. – Andrej Bauer Oct 29 '10 at 15:13
  • 10
    This is off-topic, but: it makes no sense to claim that "constructivist continuum is countable in ZFC sense". What might be the case is that there is a model of constructive mathematics in ZFC such that the continuum is interpreted by a countable set. Indeed, we can find such a model, but we can also find a model in which this is not the case. Moreover, any model of ZFC is a model of constructive set theory. You see, constructive mathematics is more general than classical mathematics, and so in particular anything that is constructively valid is also classically valid. – Andrej Bauer Oct 29 '10 at 15:15
  • @ Andrej Bauer regarding first comment, yes. This is also analogous to constructivism: you cannot express in a constructivcist set theory that something is not constructive. Not constructive means it does not exist in this theory. Regarding second comment, no, classical theory in in fact more general than constructivist theory. That's why not anything classically valid is constructively valid. – Anixx Oct 29 '10 at 15:22
  • A "definable-modified ZFC" theory should be somewhere in the middle, with classically(but not definably)-countable continuum. Since constructivism makes serious impact on analysis, it would interestiong to investigate what impact on analysis makes such "definable" theory. – Anixx Oct 29 '10 at 15:29
  • 9
    A minor technical comment on the first bullet point in Joel's answer: To use the minimal transitive model, one needs to assume that ZFC has well-founded models, not just that it's consistent. The main claim there, that there is a pointwise definable model of ZFC, is nevertheless correct on the basis of mere consistency, essentially by the second bullet point plus the consistency of V=HOD relative to ZFC. – Andreas Blass Oct 29 '10 at 16:44
  • 7
    Following the comment of Andreas got me thinking: as a topos theorist (which I am not) I would look at the syntactic model of ZFC (the "Lindenabaum algebra") in order to get to both the minimal model and the one in which every set is definable. But I suppose set theorists don't like that kind of model too much because they prefer transitive models that are "really made of sets". Is that so? Historically, where does this tendency come from? – Andrej Bauer Oct 29 '10 at 21:02
  • 7
    Andrej, one answer that I have heard from both Harvey Friedman and John Steel (in different contexts) is that we study set theory, not "models of set theory". As such we are interested in sets rather than "artificial" constructs like minimal models. (Of course, the study of models of set theory is in itself very interesting, and it is not always so easy to separate one from the other.) – Andrés E. Caicedo Oct 29 '10 at 23:38
  • 5
    @Andres: Interesting point, and I can see its validity. Nevertheless, should one prove something surprising using "artificial" constructs, it will become hard to ignore them on methodological grounds. A case in point might be non-standard models of arithmetic. I suspect many people wish they didn't exist, but they do. – Andrej Bauer Oct 30 '10 at 10:44
  • Oh, I agree. All the reasonable approaches to the still open question of the consistency of NF go through a syntactical route, which is less than ideal in a sense, but if it works, it is of course welcome. – Andrés E. Caicedo Oct 30 '10 at 17:10
  • 4
    Andrej, every pointwise definable model of ZFC must satisfy V=HOD, so not every model of ZFC will work in your plan. But if you take any model of ZFC+V=HOD, whether transitive or not, then there is a definable Skolem function, and this implies that the set of definable elements is an elementary substructure, which implies that this substructure is pointwise definable. Since this substructure is determined completely by the theory of the original model, I think that this amounts to the same as what you mean by the syntactic model of the Lindenbaum structure. (But you do need V=HOD.) – Joel David Hamkins Jul 25 '11 at 12:30
  • 3
    Thus, the pointwise definable models of ZFC are in one-to-one correspondence with the completions of ZFC+V=HOD. – Joel David Hamkins Jul 25 '11 at 12:31
  • "In these pointwise definable models, every object is uniquely specified as the unique object satisfying a certain property. The models are simply not able to assemble the definability function that maps each definition to the object it defines." But this means that the number of objects is at least smaller than the number of properties, even though there is no 1-to-1 function. As the number of properties is countable, does not it mean that the number of objects is contable? Or the number of properties itself is uncountable? – Anixx Jul 25 '11 at 12:41
  • 5
    The number of descriptions is countable, and there is a one-to-one function mapping definitions to the objects they define in a pointwise definable model (so all such models are countable), but this function is not one that exists inside the model. The situation is similar to that arising in Skolem's paradox (see http://en.wikipedia.org/wiki/Skolem_paradox), where a model is countable, but only from an outside-the-universe perspective. – Joel David Hamkins Jul 25 '11 at 12:48
  • 3
    Well viewing from exclusively from INSIDE the model, the number of definitions is countable, but the number of objects is uncountable? – Anixx Jul 25 '11 at 20:01
  • 5
    Yes, that's right. But this is not a contradiction, since the map from the definitions to the objects is not available inside the model. Thus, although the model actually has only countably many reals, as viewed from outside, inside the model it has no such bijection with $\mathbb{N}$ and thus thinks that its reals are uncountable. The main point is that the notion of a set being countable depends on the set-theoretic background, and not all models having a set in common necessarily agree on whether it is countable. – Joel David Hamkins Jul 25 '11 at 20:31
  • 3
    Hmmm, just read some of what was written in October about constructive set theory and describability. Actually, within constructive set theory, we can have that all sets are _sub_countable (see en.wikipedia.org/wiki/Subcountability), even from inside the theory. It makes sense to assume everything is finitely describable. Because, well, describe something that isn't! – Daniel Mehkeri Jul 26 '11 at 04:49
  • @Joel David Hamkins, Okay lets take standard analysis. It follows that the number of reals is uncountable (inside this model) while the number of definable numbers is countable. How can we be confident the the analysis theorems that employ definablility actually true for all reals? – Anixx Aug 02 '11 at 17:51
  • Would a hint to Skolem's paradox have been helpful in this context? – Hans-Peter Stricker Oct 14 '13 at 12:05
  • Joel I disagree with the conclusions of the linked article (Pointwise Definable Models of Set Theory) in regards to the math tea-party argument. In my opinion, the tea-party argument does withstand scrutiny, so long as we're using the "correct" definitions. Are you interested in discussing this possibility? – goblin GONE May 07 '14 at 12:22
  • @user18921 I'd suggest that you go ahead and make a blog post about it. It is also possible to make comments on my blog post about the paper at http://jdh.hamkins.org/pointwisedefinablemodelsofsettheory/. – Joel David Hamkins May 07 '14 at 14:05
  • @JoelDavidHamkins, thanks for your encouragement. I left a (longish) comment, so hopefully you find it interesting. (or better yet, convincing!) – goblin GONE May 08 '14 at 09:27
  • 2
    I think [t]he concept of definability...only makes sense from an outside-the-universe perspective [because of] Tarski's theorem on the non-definability of truth is not adequately argued for in this answer, since many people (such as myself) believe that, in fact, definitions in SOL can be perfectly adequate, it is only that SOL is not a proper logic as it lacks a semi-decidable proof theory. The claim that every definition must come equipped with a complete set of proof conditions is one that I dispute. Henkin showed that SOL, like PA, is a sound-but-incomplete multi-sorted FOL. – Charles Stewart Jan 10 '15 at 13:50
  • 2
    I view SOL itself as an outside-the-universe perspective, since these definitions quantify over second order objects, which are not present, and so we may be basically in agreement. If you don't mean "true" second order logic, but rather the second-order versions of set theory such as GBC, then the pointwise definable model phenomenon recurs, and that is the main theorem of our paper: every countable model of GBC has a class forcing extension that is pointwise definable, one in which every set and class is definable without parameters. – Joel David Hamkins Jan 10 '15 at 14:18
  • 1
    Wow! Thank you for this answer, it was very informative. I'm still a bit baffled that such an obvious thing can be wrong... Has this already been mentioned in the Common-misconceptions-list? – Johannes Hahn May 06 '15 at 13:17
  • 1
    The wikipedia article has at least taken notice that you found its mess up. – Christopher King May 17 '15 at 10:50
  • So just to clarify, as a metamathematical statement about an uncountable model of ZFC where the reals are uncountable, the "tea cup theorem" holds, right? – ziggurism Nov 24 '17 at 00:15
  • 3
    @ziggurism Yes, as a theorem of model theory, a model of set theory can have only countably many definable objects. – Joel David Hamkins Nov 24 '17 at 00:32
  • It sounds tautological when you say it like that – ziggurism Nov 24 '17 at 01:27
  • 3
    The point is that this statement is expressed in the meta-theory, about the model in the realm where one has the truth predicate, not inside the model. So one cannot argue in ZFC, say, that there are only countably many definable objects. But any model of ZFC has only countably many definable objects, enumerated in a countable sequence in the meta-theoretic context where one has the truth predicate. The difference between these two perspectives is what my post is about. – Joel David Hamkins Nov 24 '17 at 01:51
  • The argument re the ordinals doesn't seem correct? Having a α that isn't definable would only constitute a definition of α if α can be proved to be unique. But that doesn't seem to be demonstrated? – Michael Mar 31 '20 at 21:43
  • 2
    @Michael I suppose uniqueness is obtained by taking the least such ordinal, since we know that one such ordinal exists – user2103480 May 13 '20 at 11:31
  • The link to jdh.hamkins.org in a previous comment seems to be broken, but a snapshot is saved on the Wayback Machine. – The Amplitwist Jan 31 '24 at 11:15
19

You can also talk about arithmetically definable real numbers: those for which the Dedekind cut of rationals is of the form: $$\{m/n: \forall x_1 \exists x_2 \ldots \forall x_{k-1} \exists x_k\, p(m,n,x_1,\ldots,x_k)=0\},$$ where the $x$'s range over integers, and $p$ is a polynomial with integer coefficients.

Then on this definition of definability: $e$ and $\pi$ and all the familiar reals are definable. Only countably many numbers are definable. There must be other real numbers which are undefinable. And it all makes sense, and is even provably consistent, in ordinary set theory.

A standard reference for this way of thinking is the system $ACA_0$ in Simpson's Subsystems of Second-Order Arithmetic.

The cost of this metamathematical simplicity is a small change to the mathematics: any definable bounded sequence of reals has a definable least upper bound, but an uncountable definable set of reals may not. Feferman's notes on Predicative Foundations of Analysis show how to develop standard analysis on this basis. If we changed mathematics as taught in universities to be based on predicative analysis, few undergraduates or people outside the math department would notice much difference.

  • Interesting. What are polynomials for $e$ and $\pi$? – Gerald Edgar Sep 01 '17 at 12:25
  • 2
    @GeraldEdgar, start from $e$ as $${m/n: \exists x\exists y\exists z\ y=(1+x)^x\ &\ z=x^x\ &\ m/n<y/z}.$$ The rest is standard coding, of which the only difficult part is using Godel's $\beta$ lemma to encode lists verifying $y=(1+x)^x$ and $z=x^x$. The easy references are from the use of these techniques in Hilbert's 10th problem, e.g. section 1 here: https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/MartinDavis.pdf –  Sep 01 '17 at 13:45
  • In more detail, using 13 positive-integer variables: $$\newcommand{\e}{\exists} e = {m/n: \e a \e b \e c \e d, \e q \e r \e s \e t \e u, \forall v \e w \e x \e y\ (mc-nb + d)^2+\ (q - (1+r)s - c)^2+ (q - (1+ra)t - b)^2+ (r - u - b)^2+\ (v + 1 - w - a)^2 ((q - wa - (1+(v+1)r)x)^2+(q - w(1+a) - (1+vr)y)^2)=0 }$$ –  Sep 04 '17 at 09:17
  • @MattF I wish I could understand the last part – Mark C Oct 25 '17 at 17:59
  • It's not really important, but it's a little weird to say $x^x$ and $(1+x)^x$ are polynomials. – Zach Teitler Apr 30 '18 at 20:05
  • 2
    @ZachTeitler, you can replace $x^y=z$ with its Diophantine definition (again, as in the references on Hilbert’s 10th problem), and that will convert these definitions from exponential polynomials to ordinary polynomials. –  Apr 30 '18 at 20:29
  • 3
    @ZachTeitler It's not saying $x^x$ or $(1 + x)^x$ are polynomials, rather that for the expressions $y = (1 + x)^x$ and $z = x^x$ there exist polynomial expressions (using extra variables) that are satisfiable if and only if the original ones are (equisatisfiable). – orlp Jul 08 '20 at 18:16
17

While you cannot define undefinable numbers, you can quantify over all real numbers, whether or not they are definable. "Let $a$ be a number" does not assume that $a$ is definable, but is merely a shorthand for quantification over $a$. The theorems in analysis are safe.

Definability is a subtle issue that was only partially dealt with in Joel David Hamkins excellent answer. $(V,∈)$-definability (as a predicate on sets) is $(V,∈)$-definable if and only if every ordinal is already $(V,∈)$-definable (in which case, $(V,∈)$-definability coincides with ordinal definability; a set is $(V,∈)$-definable iff it is first order parameter-free definable in $(V,∈)$). Intuitively, not every ordinal is $(V,∈)$-definable, and this can be formalized and proved by adding a $(V,∈)$ satisfaction relation Tr and replacement axiom schema for formulas involving Tr (this is not conservative over ZFC and does not hold in the minimal transitive model of ZFC). However, every consistent theory T extending ZF has a model (called definable ordinal model or Paris model) in which every ordinal is definable; for a complete T with a well-founded model, all Paris models are well-founded. This applies even if T proves that the set of ordinal definable real numbers is countable. It also applies to theories with Tr by using $(V,∈,\mathrm{Tr})$ definability, and analogously with other extensions.

In any case, we can speak of existence of $(V,∈)$-definable examples without ambiguity since there is a $(V,∈)$-definable set satisfying $P$ iff there is an ordinal definable set satisfying $P$ (and analogously if $P$ has parameters and we allow definability with those parameters). A set is ordinal definable iff it is definable in some $V_κ$. Now, V=HOD is $Π^V_2$ conservative over ZFC (and over ZFC + $φ$ for a $Σ^V_2$ $φ$), so even if the proofs assumed definability (which they do not), the theorems (which for analysis and 'ordinary mathematics' are all $Π^V_2$) would still be correct.

That does not mean that the theorems have definable examples. In second order arithmetic (where the examples are real numbers), existence of definable examples holds assuming projective determinacy (and for $Σ^1_2$ predicates in just ZFC), but existence of ordinal definable nonmeasurable sets (and likely other 'non-well-behaved' sets of reals) is independent of ZFC and ordinary large cardinal axioms.

2

It might be of some small interest to note the following result of Kenneth McAloon (from his paper, "Consistency Results About Ordinal Definability", Annals of Mathematical Logic, Vol. 2,No. 4 (1971) 449-467--note that he denotes as '$K$ = $V$' the statement "Every set is ordinal-definable" so his result also holds for $HOD$ as well):

Theorem. If $ZF$ is consistent, then so are

(i) $ZF$ + $GCH$ + $V$ = $OD$ + $V$ $\neq$ $L$;

(ii) $ZF$ + $V$ = $OD$ + $2^{\aleph_0}$ $\neq$ $\aleph_1$. [Since Andres is correct in pointing out that McAloon abbreviates "Every set is ordinal-definable" ($V$ = $OD$) as '$V$ = $K$' and also notes that "...if $V$ = $OD$ then $V$ = $HOD$", I wil replace McAloon's $V$ = $K$ with $V$ = $OD$ in order to strike an uneasy balance between directly quoting from a Source and paraphrasing the Source]

Since one can replace $V$ = $OD$ with $V$ = $HOD$, the models of these theories might be interesting universes for analysts to study in case mathematical practice should ever find use for definable non-constructible sets.

  • 2
    You misquoted the result. Again, the confusion is identifying a model with a theory. – Andrés E. Caicedo Aug 31 '17 at 13:06
  • 2
    (Using $K $ is unfortunate here, since the letter now has a different, technical meaning.) – Andrés E. Caicedo Aug 31 '17 at 13:08
  • @AndrésE.Caicedo: Exactly how did I misquote the result? I have a copy of the paper right in front of me. What I wrote is exactly what appears in McAloon's paper, exactly as written. Also, I did not confuse models with theories. (i) and (ii) are theories. I write, "...the models of these theories might be interesting universes...". Models are universes in the multiverse view. However, I am always happy to correct errors in my thinking and writing. If there is a better (or more acceptable) paraphrase of McAloon's theorem, please let me know. – Thomas Benjamin Sep 01 '17 at 03:43
  • 1
    (cont.) I can always re-edit. Thanks in advance for your help in this matter, it is always appreciated. – Thomas Benjamin Sep 01 '17 at 03:44
  • 1
    $V=K$ makes no sense if $K$ is a statement. – Andrés E. Caicedo Sep 01 '17 at 03:44
  • 1
    I also have the paper, in fact. What is written there is that "The proposition `Every set is ordinal-definable' is abbreviated ${\rm V} = {\rm K}$'' (p. 449). This is different in an essential way from what you wrote. – Andrés E. Caicedo Sep 01 '17 at 03:51
  • @AndrésE.Caicedo: On pg. 449 of his paper McAloon writes, "The proposition 'Every set is ordinal-definable' is abbreviated $V$ = $K$." I have re-edited to take that into account. Thanks. – Thomas Benjamin Sep 01 '17 at 03:52
  • 1
    You introduced another mistake now, since we cannot replace a statement (what you call `$K=V$') with a model ($\mathsf{HOD}$). – Andrés E. Caicedo Sep 01 '17 at 03:56
  • Either you define $K$ (rather than the statement '$K=V$'), and then replace $K$ with $\mathsf{HOD}$ in the statement of the theorem, or you keep things as they are (with '$K=V$' defined, but not $K$ itself), and then replace the statement $K=V$ with the statement $V=\mathsf{HOD}$. – Andrés E. Caicedo Sep 01 '17 at 03:58
  • By the way, if you want to think of $K$ as a structure, it is the class of ordinal-definable sets, and the currently standard notation for it is $\mathsf{OD}$. It is obvious that if $V=\mathsf{OD}$ then $V=\mathsf{HOD}$, so pointing this out is more distracting than useful. – Andrés E. Caicedo Sep 01 '17 at 04:01
  • (Anyway, I suggest you use $\mathsf{OD}$ rather than following McAloon's notation, since $K$ is used differently nowadays, and its mention is distracting.) – Andrés E. Caicedo Sep 01 '17 at 04:03
  • 1
    @AndrésE.Caicedo: Your comments are helpful. I will re-edit. – Thomas Benjamin Sep 01 '17 at 04:33