Xrfgtjtk

I am working through Apostol's Calculus I and just read about the order axioms. He presents a new undefined concept called positiveness, gives the axioms and then defines symbols $<, >, leq, geq$ in terms of this new concept of positiveness. Apostol then states

Thus we have x > 0 if and only if x is positive.

I attempted a proof of this before reading other proofs and quickly ran into something I know is incorrect (I read other proofs later) but haven't developed an intuition for, hoping someone can set me straight.

I'll provide the definitions and axioms from Apostol for reference, then show my attempt.

From Apostol

We shall assume that there exists a certain subset $mathbb{R}^{+} subset mathbb{R}$ called the set of positive numbers, which satisfies the following three order axioms:

Axiom 7: $text{If } x text{ and } y text{ are in } mathbb{R}^{+}, text{ so are } x + y text{ and } xy$

Axiom 8: $text{For every real } x neq 0 text{, either } x in mathbb{R}^{+} text{ or } -x in mathbb{R}^{+}, text{ but not both }$

Axiom 9: $0 notin mathbb{R}^{+}$

...classifies the symbols...

(1) $x < y$ means that $y-x$ is positive;

(2) $y > x$ means that $x < y$;

(3) $x leq y$ means that either $x < y$ or $x = y$;

(4) $y geq x$ means that $x leq y$

Thus we have x > 0 if and only if x is positive.

My attempt
$$begin{align}
x > 0 &iff x in mathbb{R}^{+}\
x > 0 &= x-0 in mathbb{R}^{+} &text{(2) and (1)}\
x - 0 &= x + (-0) &text{theorem 1.3: b - a = b + (-a)} \
x + (-0) &= x + (0) &text{exercise in the previous section}\
x + 0 &notin mathbb{R}^{+} &text{ this is where I'm hung up }
end{align}$$

I arrive at the last line because we know $0 notin mathbb{R}^{+}$ from axiom 9. Then, from axiom 7, $(x + 0) notin mathbb{R}^{+}$.

Perhaps I can't conclude that because axiom 7 is in form $P implies Q$ which allows for $x + y in mathbb{R}^{+}$ to be true even when the statement $(x in mathbb{R}^{+} wedge y in mathbb{R}^{+})$ is false. Am I correct in my assessment of where I made the mistake?

Axiom $7$ Says that if $x, y in mathbb R^+$ then $x + y$ is too.

It does not say if $xin mathbb R^+$ but $ynot in mathbb R^+$ then $x + ynot in mathbb R^+$.

And you know that statement can not true because $5 in mathbb R^+$ and $-3 not in mathbb R^+$ and $5 +(-3) = 2 in mathbb R^+$. Even if you can't figure out how to prove that, you know, the Apostle is not just making sh!t up. You know he is trying to formally define the math you've been doing all your life. ... And you KNOW if $x$ is positive and $y$ is not positive then you can't tell if $x + y$ is positive or not. You know that. You know it depends on the relative sizes of the absolute values.

So..... you have $x+0 in mathbb R^+$. And you know by definition of $0$ that $x + 0 = x$. So..... $x= x+0 in mathbb R^+$.

That's it.

The proof is.

If $x > 0$. then

$x - 0 in mathbb R^+$. (1)

$x- 0 = x$ (...various reasons)

So $x = x-0 in mathbb R^+$.

So that's the $implies $ direction.

If $x in mathbb R^+$

then $x = x-0$

And $x-0in mathbb R^+$ so $x > 0$.

And that's the $Leftarrow$ direction.

.....

And yes. The statement $P implies Q$ does !!!!!!!NOT!!!!!!!* mean $lnot P implies lnot Q$.

Consider $P = x$ is even. And $Q = x$ is an integer.

$P implies Q$ means "If $x$ is even then $x$ is an integer". That's obviously true.

So if $x$ is not even does that mean $x$ is not an integer?

Of course not!

======

For what it's worth. $P implies Q$ does not mean $lnot P implies lnot Q$.

But it does mean $lnot Q implies lnot P$. (That's called the contrapositive.

This means if $x + y not in mathbb R^+$ then it is not true that both $x$ and $y$ are positive (otherwise $x + y$ WOULD be $in mathbb R^+$). At least one of them must be non-positive.

I fail to see what is the complication for you, but you are basically saying the right things. If $x>0$, this means that $x-0inmathbb R^+$, and $x=x-0$, so $xin mathbb R^+$. And conversely, if $xinmathbb R+$, then $x-0=xinmathbb R^+$, so $x>0$.

That said, the reasonable way (especially for beginners) to prove and "if and only if" is to prove each implication separately.