Statements independent of ZF that quantify over the real numbers (This question is a bit vague, because I probably haven't aquired all the logical tools needed to express it in a more concise way)
I've seen a few examples of statements in set theory that can neither be proved or disproved from the ZF axiomatic system.
The basic statement is of the form: $\exists x \in A:\varphi(x)$, where $A$ is a fixed set and $\varphi(x)$ is a proposition with $x$ as a free variable.
Most of the times this happens, it appears that the set $A$ we're quantifying over is very large.
Here are some examples for clarification:


*

*(A specific case of) The well-ordering theorem: There exists a well-order on $\mathbb{R}$.


This statement quantifies over the set $P(\mathbb{R}\times\mathbb{R} )$ of all binary relations on $\mathbb{R}$. 


*

*There exists a non-principal ultrafilter on $\mathbb{N}$.


This statement quantifies over $P(P(\mathbb{N})))$, as every filter on $\mathbb{N}$ is a collection of subsets from the set.


*

*The negation of The Continuum Hypothesis: There exists a set $A\subseteq\mathbb{R}$ s.t. $|\mathbb{N}| < |A|< |\mathbb{R}|$. 


This statement quantifies over $P(\mathbb{R})$.
All statements written above are independent from ZF, but all sets they quantify over are strictly larger than the set of real numbers.
Here's a non-example:


*

*The well-ordering theorem on $\mathbb{N}$. This is clearly true in ZF, as the regular order on $\mathbb{N}$ is a well-order. 


The question is: Is there a 'natural' statement of the form $\exists x \in \mathbb{R}:\varphi(x)$, that is independent of ZF?
By 'natural', I want to exclude some subtle constructions such as the existence of $0^{\#}$; I don't know a lot about the subject, but I do know that it encodes a statement about formulae in set theory. I'm looking for more simple statements (perhaps my goal could be expressed formally using a hierarchy on propositions).
My intuition says that such an example doesn't exist. Statements independent of ZF are highly non-constructive; They say that you can (or can't) find some set, but the options to select it from are so vast that the existing axioms are just not sufficient. 
However, the set of real numbers appears 'small enough' for us to have a complete grasp of it and its set-theoretic properties.
But who knows? Maybe you could prove me wrong. Maybe there's even a statement like that which quantifies over the natural numbers?
 A: It is the same thing to quantify over the real numbers and to quantify over sets of natural numbers. So second-order arithmetic and quantifying over the real numbers is the same.
Shoenfield's absoluteness theorem tells us that very simple statements about the real numbers (namely $\Sigma^1_2$ statements over the natural numbers, or "there exists a real number $x$ such that for every real number $y$ something arithmetic happens") are absolute between the universe of $\sf ZF$ and $L$ of that universe.
So in particular, such statements cannot be independent of $\sf ZF$. Not in a "reasonable way" anyway.
There are natural statements in a set-theoretic sense, like "There exists a Cohen real over $L$" which might not be very natural otherwise. But these are not natural in the sense of the real numbers. Because they are not simple enough, and they usually involve models of $\sf ZF$ in some sense or another.
But this is a deep-seated point. For one thing, you don't specify what is a simple enough statement. But most of the set theoretic independence results involve things like $0^\#$ or "a unique solution to a $\Pi^1_2$ predicate" (e.g., a Jensen real) and so on. Which might not be very "natural" as far as the real numbers go. And since the real numbers in set theory play an entirely different role than the real numbers in analysis, it's not clear what is a simple enough statement.
(For example the statement that there exists a real which encodes the constructible reals, i.e. $\omega_1^L$ is countable, is a statement about the real numbers, but is it simple enough for you?)
