There is a real number $\xi$ such that one can neither prove nor disprove that $\xi$ is positive.

Proof: There are uncountably many real numbers but only countably many proofs.

This is something I just thought of. I don't know anything about proof theory or anything like that. Is my reasoning correct?

Just to emphasize, I would like to know if the proof is correct. The statement itself is true, see for example Yves Daoust's answer.

  • 2
    $\begingroup$ Not much is known about this number- :-) $\endgroup$ – coffeemath Apr 21 '17 at 14:32
  • $\begingroup$ Interesting idea. Let's see what answers come up. One thought: there are only countably many real numbers that you can actually specify with an algorithm or description of some formal kind, since there are just countably many descriptions. $\endgroup$ – Ethan Bolker Apr 21 '17 at 14:32
  • $\begingroup$ @YvesDaoust How can a complete enumeration miss a single proof? $\endgroup$ – M. Winter Apr 21 '17 at 14:49
  • $\begingroup$ @M.Winter: you are right, it can't. $\endgroup$ – Yves Daoust Apr 21 '17 at 17:02

Your question is ill-defined, simply because proofs are strings of symbols, and how will you describe every real number by a string of symbols, so that it can even be part of a proof? Based on that alone you cannot talk about proving or disproving some sentence about an arbitrary real number. If that answers your inquiry, then that is all there is to it. $ \def\rr{\mathbb{R}} $

That said, there is an interesting separate question that can be made out of it:

Is there a real number $x$ that is definable over ZFC such that ZFC cannot prove or disprove that $x > 0$?

The above statement can easily be made precise as follows:

Let $\rr$ be the set of real numbers as defined in ZFC, and $0_\rr$ be the zero element in $\rr$. Is there a $1$-parameter sentence $P$ over ZFC such that ZFC proves "$\exists! x ( P(x) \land x \in \rr )$" but ZFC proves neither "$\forall x ( P(x) \to x > 0_\rr )$" nor "$\forall x ( P(x) \to x \le 0_\rr )$".

Notice that this question cannot be easily answered by resorting to cardinality considerations. But the answer to this question is, curiously, "yes". Let $1_\rr$ be the unit element in $\rr$. (Actually all that matters is that ZFC proves "$1_\rr > 0_\rr$".) Let $Q$ be some independent sentence over ZFC, such as $\neg \text{Con}(\text{ZFC})$, and let $P(x) \overset{def}\equiv Q \land x=1_\rr \lor \neg Q \land x=0_\rr$. Then ZFC proves "$P(0) \lor P(1)$" and "$\forall x,y ( P(x) \land P(y) \to x=y )$", and hence also proves "$\exists! x ( P(x) \land x\in\rr )$". However, ZFC cannot prove "$\forall x ( P(x) \to x > 0_\rr )$" otherwise it would also prove "$\neg P(0_\rr)$" and hence "$Q$". Similarly ZFC cannot prove "$\forall x ( P(x) \to x \le 0_\rr )$" otherwise it would also prove "$\neg P(1_\rr)$" and hence "$\neg Q$".

So you can see from this that the syntactic incompleteness of ZFC has an effect on the decidability of even basic questions about definable reals.


Proof: There are uncountably many real numbers but only countably many proofs.

The fact that there are more numbers than there are proofs doesn't mean anything, because a single proof can be about any number of numbers. One proof can be a proof about a single number, a few numbers, countably infinitely many numbers, or an uncountable amount of numbers.


Claim: If $x+2 > 2$ then $x>0$.

Proof: Given $x+2>2$, subtract $2$ from both sides. Then we get $x>0$. $\Box$

This is a (very simple) proof about an uncountable amount of numbers. There are uncountably many numbers that are larger than $2$ (and larger than $0$).

A less trivial example of a proof that characterizes uncountably many numbers is the proof that there are uncountably many real numbers.


Take any unprovable theorem $T$ from your theory and define

$$\xi:=\begin{cases}T\text{ is true}\to +1,\\T\text{ is false}\to -1.\end{cases}$$

Can you prove $\xi>0$ ?

  • $\begingroup$ Ah, well, you got me. But my question wasn't really about the claim itself, but about my proposed proof. Is it valid? Perhaps I should have picked a different title. $\endgroup$ – Vincent Apr 21 '17 at 15:01
  • $\begingroup$ This is not a real number for which we cannot prove the sign, but a desciption of a real number that does not allow us to deduce the sign. I would differentialte here. $\endgroup$ – M. Winter Apr 21 '17 at 15:11
  • $\begingroup$ @M.Winter : this is a valid definition, because the formula $\exists ! \xi\in \mathbb{R}, (T\implies \xi = 1\land \neg T\implies \xi = -1)$ is provable from ZFC (where $\exists ! x, P(x)$ is an abbreviation for $\exists x, (P(x)\land\forall y, P(y) \implies y=x)$), and so it does define a real number. You can use the same trick to answer the question "does there exist a sequence that you cannot prove converges or diverges ?" $\endgroup$ – Max Apr 21 '17 at 15:41
  • 1
    $\begingroup$ @Max I think all this proves is "There is a definition/description of a real number that does not allow us to deduce the sign". This is not the same as what was asked in the original question. The trick here is that we have no way to deduce the actual value of $\xi$. Once we know the value, we can prove the sign. I'm no expert in this, but im quite sure that there is a big difference between the value of a real number and its description/definition. The value is either 1 or -1 and in both cases, we know the sign. 1 and -1 are the actual real numbers here. Do you know what I mean? $\endgroup$ – M. Winter Apr 21 '17 at 15:50
  • $\begingroup$ Well the thing is, the real numbers aren't absolute, they depend on the model of ZFC under consideration. So if the question is about provability, then it's one step away from models (it's looking at models and first order logic). Thus it either makes no sense, or is asking for a formula which is a definition, and such that you cannot prove whether the real number that's defined by said formula is $>0$ or not $\endgroup$ – Max Apr 21 '17 at 15:55

The problem here seems to arise from the missing differentiation between real numbers on the one hand, and descriptions of real numbers on the other. When you want to talk about a specific real numbe, your only chance to communicate which number you are talking about, is by giving a finite description in a language with at most countably many symbols. A description should be a predicate $P(x)$ which can provably be satisfied by only a single real number, i.e. we can prove $$P(x)\wedge P(y)\rightarrow x=y.$$

Some languages directly enable you to decide if the number is bigger than $0$, e.g. the usual decimal expansion. Other languages may not even allow you to compute a single digit, let alone a sign. So the property of being not abled to prove the sign of your number is not a property of the number itself, but a property of the description you use.

One can ask if there is a real number $\xi$ for which no decription exists from which we can prove the sign. Here, you can use your cardinality argument again. There are more real numbers than descriptions. So Yes there is such a number. But this does not mean that we cannot prove the sign of the number at all, as it might be possible to proof the sign from a statement that does not uniquely specify this number but describes this number as part of a whole set of real numbers. For example, it might be possible, to compute the first three digits, which might suffice.

So No, I do not think your proof is correct. As others have stated, a proof must not address a single number, so cardinalities cannot be compared here.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.