Can you explain your remark about properties? What I mean is, if you have two noncomputable reals, there is no property that distinguishes them. And Lightstone's paper giving a notation for infinitesimals clearly shows that we can write down distinct infinitesimals. I'm no expert, just seeking clarification.

@user4894 "if you have two noncomputable reals, there is no property that distinguishes them" That's false. If $r<s$ are reals - computable or not - there is a rational $q$ between them, and the formula "$x<q$" is expressible in the language of arithmetic, is true of $r$, and is false of $s$. By contrast, infinitesimals in a hyperreal field are in general automorphic: there is an automorphism of the structure which swaps them. So in particular, they satisfy all the same formulas.

@user4894 As to Lightstone's notation, that's really just dodging the issue. A Lightstone representation of a hyperreal is an infinitely long sequence of decimals, which are indexed by hypernaturals. This is a huge problem, and is why Lightstone's notation doesn't actually provide a way of "naming" the hyperreals in a nice way. Specifically, suppose $r<s$ are two different hyperreals. Then their Lightstone expansions differ at some decimal place, say the $H$th place. But if $H$ is an infinite hypernatural, then there is no way of describing $H$ in the language of arithmetic! (cont'd)

I see your point. This contradicts something I've always heard. If there are only countably many properties (finite strings over a countably infinite alphabet) and uncountably many noncomputable reals, then most noncomputable reals can't be characterized by a property. But you just separated each pair of noncomputable reals via a property. Can you help unconfuse me on this point?

So all Lightstone's notation does is give us a way to express arbitrary hyperreals in terms of the hypernaturals. But the hypernaturals, just like the hyperreals, have lots of nontrivial automorphisms, so this doesn't give us a way to definably distinguish arbitrary distinct hyperreals. (Note that of course there are hypernaturals which are distinguishable from each other - e.g. an "even" hyperreal versus an "odd" hyperreal - but there are also lots of pairs of hyperreals which are automorphic, and hence indistinguishable.)

@user4894 Re: your most recent comment, here's what's going on. To characterize a real $r$ by a property, I need a formula $\varphi(x)$ which is true only of $r$. When I say that $r$ and $s$ are distinguishable, I mean that there is a formula $\psi(x)$ which is true of $r$ but not $s$. This is vastly weaker! In particular, take a concrete example: $0$ versus $1$. One formula distinguishing them is "${1\over 2}>x$" - in the language of arithmetic, this is expressible as "$\exists y(\forall z((y+y)z=z)\wedge x<y)$". But this formula doesn't distinguish between $0$ and ${1\over 3}$! (contd)

This is exactly what's going on with the fact that the rationals, while countable, are dense in the reals, which are uncountable: any two reals are separated by a rational, but there is no way to characterize a real by a single rational: to separate reals which are "closer and closer" to $r$ from $r$, I need to use rationals which are "closer and closer" to $r$. There's no sense in which some specific rational "always works for $r$". (Another example: countably many finite binary strings, but uncountably many infinite ones; and infinite ones can be distinguished by finite ones.)

@user4894 Also, there are in fact definable non-computable numbers - "definability" is a much weaker property than "computability." E.g. an example of a definable non-computable number is Chaitin's constant, and there are many others, see e.g. these two questions. (cont'd)

And actually, the word "definable" is a bit vague - you need to specify a context (e.g. "definable in the first-order language of ordered fields"). A real which is undefinable in one sense may be definable in another; this is analogous to the situation in Goedel's Incompleteness Theorem, where we prove that a certain sentence is unprovable in this theory, but then prove that sentence in this other theory.

Thank you for your clarifying remarks. Very helpful.

It's not clear to me what you mean by hyperreals "existing" exactly. Would you mind clarifying?

@NoahSchweber: So "there exists a hyperreal exists" just means "it is possible to define a field whose properties don't contradict those of the reals, and which behaves as one might hope infinitesimals to behave"? The reason I ask is that (as a non-mathematician) I find it hardly surprising that it's possible to define something noncontradictory with other things. Just avoid adding too many axioms to prevent making your theory contradictory. Like, I could define that every real number has an associated dog and cat. It "exists" since it doesn't contradict anything I know. Is that surprising?

@Mehrdad No, a hyperreal field is much more complicated than that. It is an ordered field with a bunch of properties. Showing that such a thing exists is not trivial! Existence theorems are hard: for example, try proving that a nonprincipal ultrafilter on $\mathbb{N}$ exists, that a winning strategy for an arbitrary Borel game exists, or that a sentence undecidable in PA exists.

You suggest as a strategy "just avoid adding too many axioms to prevent making your theory contradictory". Well, the problem is that those "axioms" are part of the definition of a hyperreal field. You can't exactly say "A hyperreal field exists, if you drop some of the axioms of 'hyperreal field'"; you need to prove that those specific axioms don't give a contradiction, and that's hard! For example, you need the axiom of choice to prove the hyperreals exist! So it's provably not easy at all.

@Mehrdad The key weird property that a hyperreal field has to satisfy is the transfer principle, which looks innocuous at first . . . but actually hides a ton of mathematical complexity.

@NoahSchweber [reply to your first 2 replies]: I guess the issue I have with your examples is that it's not clear to me a priori what properties the hyperreal field should have, and it's not clear to me that those properties were even clear before the field was proposed. If all you require is that the "hyperreals" form a field, then that's too loose and uninformative; of course such a thing exists, since the real numbers already form a field. So we need more properties beyond that. So I'm just saying, avoid adding any properties that are contradictory, and you're done. [cont'd]

@NoahSchweber: [cont'd] so the only way this fails is if mathematicians already had a preconceived notion of what properties these things called "hyperreals" might have. And I guess you answered that in your last comment re: the transfer principle.

@NoahSchweber: You react way too fast. I literally wrote [cont'd] to let you know I wasn't finished (since you kept adding more every time I was about to press Enter) and when you were done and I replied, you didn't wait 60 seconds before bashing my comment in bold... relax, let people finish typing out their thoughts!

@Mehrdad Sorry, my bad, I didn't see "[cont'd]". But yes, the hyperreals have a precise definition - a hyperreal field is a non-Archimedean ordered field with the transfer property (which itself has a lengthy formal definition). Incidentally, I wrote in bold because I'd already said that in a previous comment: "No, a hyperreal field is much more complicated than that. It is an ordered field with a bunch of properties." So I just wanted to bring that part to the fore, and make it more visible than the rest of my comment.

@NoahSchweber: What wasn't clear to me was whether such properties are merely incidental (i.e. proven after the hyperreals were shown to exist) or whether they are required (i.e. necessary before the field is acknowledged as hyperreal in the first place). It looked to me like the former but you seem to be saying the latter, and I think that's the key answer to my question.

@Mehrdad Ah, yes, I wasn't clear - those properties are exactly the definition of a hyperreal field. And so the existence of such is a nontrivial theorem.