Set of representable real numbers

[Office_Shredder]

From what I understand, the class of all real numbers that we can represent as a sentence in logic is countable. But I'm not sure if it's a set under the standard ZF axioms... it seems intuitive that it should be, since the axioms are really designed to prevent problems involving sets that are too large, and countable sets are fairly innocent, but was wondering if anyone knew one way or the other.

 

[Preno]

Well, every subclass of a set is a set, according to the axiom of separation, but the question is whether the set of definable/representable real numbers is a class, i.e. can be defined by a formula of set theory.

Here's my attempt at a proof: the class of all formulas of set theory is clearly a set (it can easily be defined inductively). Now if there is a class function f: formula phi -> the subset of R defined by phi, then (because the image of a set is a set) the class of all definable subsets of R is a set. Being a singleton set is a definable condition, so we take the intersection of this class and the class of singletons. We take the union of this set to get the set of definable real numbers. So we need to construct the function f, but this can be done inductively (unless I'm mistaken). Therefore, the definable reals form a set.

 

[Office_Shredder]

Well, every subclass of a set is a set, according to the axiom of separation

Only if they can be described as satisfying a first order logic statement right? According to wikipedia, no such statement exists for the definable reals.

 

[Preno]

Yes, which is what I said and then went on to attempt a proof without using the presupposition that the definable numbers form a class.

ETA: every class is definable by a first-order formula of set theory, so your "only if they can be described as satisfying a first order logic statement" is merely a restatement of the assumption that it's a class.

ETA 2: to try to make the construction of f explicit: [itex]f(x \in a) = a, f(\neg\varphi)=\neg f(\varphi),f(\varphi \wedge \psi) = f(\varphi) \cap f(\psi), f(\exists y \varphi(x,y))=\cup_{y \in V} f(\varphi(x,y))[/itex]

The quantifier step doesn't work as it is, I can't figure out how to fix it right now, but intuitively speaking it should be possible, as first-order logic can be immersed into set theory.

 

[Office_Shredder]

I think the problem is we're defining class differently. I think I see what you're saying there

 

[AKG]

You're looking at:

{x in R : there exists phi s.t. "phi is a formula" and "there exists unique y in R s.t. V models phi[y]" and "V models phi[x]"}

The condition for x to be in this set doesn't look like a formula of ZFC, but you can probably arithmetize the language such that it becomes equivalent to a formula of ZFC, e.g. (there exists phi s.t. "phi is a formula") is equivalent to (there exists n s.t. n is in the set of Godel numbers of ZFC formulas) where the set of Godel numbers of ZFC formulas is somehow definable.