# It is ok to ask the following question in MO?

Intuitively it doesn't look to me that much of a research level problem but, if it's not too trivial, I think it needs a bit of careful thought to answer my question. I don't know whether the requirement "bit of careful thought" is enough to render it as a research level problem and that's why I am asking it here. If this question doesn't suit for this site, please let me know the answer in comments.

In standard treatment of Peano Axioms, say for example in Terence Tao's book Analysis I, the definition of $1$ is given right after stating the first two axioms, namely the following axioms,

Axiom 1. $0$ is a natural number.

Then Tao elaborates the notion of successors (the successor of $n$ is taken there as $n{++}$) and then states the following axiom,

Axiom 2. If $n$ is a natural number, then $n{++}$ is also a natural number.

After stating these two axioms he then gives the following definition,

Definition We define $0{++}=1$.

My objection is regarding the place of occurrence of this definition. In my opinion the definition shouldn't occur in the text until we have proved that $0{++}=1$. What do I mean by saying to prove $0{++}=1$? Let me elaborate the question a bit.

My argument is that the statement $0{++}=1$ of course can be taken as a definition of $1$ but only when we have proved the following property of our intuitive natural number system, loosely speaking, $$\color{blue}{\text{There doesn't exist any natural number between 0 and 1.}}$$ The necessity for proving this statement is that without it we cannot say that the construction of our natural number from Peano Axioms is complete (note that Axiom of Induction only excludes the existence of any other "non-natural" elements but so far as I know, it doesn't trivially exclude the possibility of having natural number between $0$ and $0{++}$). For if there really exists any natural number between $0$ and $0{++}$, the resulting system doesn't (apparently) contradicts any one of the Peano Axioms but still clearly it isn't the natural number system that we have known since our childhood and which is our objective to treat formally. And since one of the most important objective of this axiomatic treatment of natural number is to formalize our notion of natural numbers, we mustn't include in our formalized system any property that contradicts out intuitive notion of natural numbers. Otherwise the whole point of construction becomes meaningless.

Up untill now I can't find any rigorous proof of the fact that I have stated above and which, using logical operators becomes (all the variables indicating natural numbers), $$\not\exists b:0<b<0{++}$$

Is there any proof of this result? Can anyone elaborate where am I wrong?

I have discussed this problem with some of my friends but none of them could give me a satisfactory answer. I thought that maybe we should take this as an axiom. That's why I have posted it here to ask for the expert opinions.

• You haven't even defined $<$. Once the Peano axioms are formalized, it is possible to define such a relation on the natural numbers, and quite trivial to show there are no natural numbers between $0$ and $1$. But all this is completely off-topic for MO. Please take it up at MSE. I am sure someone can explain it to you. – Todd Trimble Jan 9 '15 at 15:08
• The only thing that you need to prove before introducing a definition of a constant is that there exists a unique element satisfying the definition. Here, this holds trivially as the definition is just the value of a closed term. Whether the defined constant satisfies this or that other property is irrelevant. In any case, the property you want is stated right after the definition of < in Proposition 2.2.12, and you are asked to prove it yourself in Exercise 2.2.3, but you are obviously going to need the intervening material about addition. – Emil Jeřábek supports Monica Jan 9 '15 at 17:28
• Note that downvotes on meta can mean disagreement with the proposal, and not necessarily that this question "does not show research effort" or "is unclear or not useful." – Joel Reyes Noche Jan 10 '15 at 3:29
• It is now asked at MSE. – user 170039 Jan 10 '15 at 12:00
• I assume you mean this. – Joel Reyes Noche Sep 6 '15 at 14:19

• The construction of natural numbers from Peano Axioms is treated in the book at the very beginning and without any set theoretic ideas at all (except in some informal discussions) and so except the Axiom of Induction and order, there really isn't other assumption. The definition of $1$ appears just below the the stated axioms. – user 170039 Jan 9 '15 at 14:55