Shouldn't there be more basic properies of real numbers in Spivak's Calculus book?

Question

In his Calculus book, Spivak wants to establish all basic properties of real numbers so that he can prove calculus upon it. But I thought of some properties which Spivak should have also listed. And my question will be "Are this properties (which I will list below) ones which should/have to/must be there (in the list of basic properties of real numbers) and can't be proved from the other basic properties Spivak listed ? By " should/have to/must be there" I mean that these are the properties which can be proved from any construction of real numbers or are one of the axioms of this construction and cannot be proved from basic properties Spivak listed. Properties I was talking about:
1)For any real number $a$ and $b$ there exists real number $c$ such that $$a+b=c$$ (Spivak actually says kind of this before listing the basic properties but not includes it as a property).
2)For any real number $a$ and $b$ there exists real number $c$ such that $$a•b=c$$.
3)Reflexive, symmetric and transitive property of equality.
4)If $$x=y$$ then for any function $f$ $$f(x)=f(y)$$.
Or alternatively for any predicate $P$ $P(x)$ is logicaly equivalent to $P(y)$. (I am not sure what of this two will be enough). Thanks in advance and ready to listen critics of this question (if there is some).

Answer 1

Some of this is built into the usual logical semantics. Spivak is sweeping this under the rug: otherwise he'd also have to explicitly describe the behavior of quantifiers, "and," "or," "not," etc., as well as providing a formal language and proof system. It's possible he also sweeps other points of logic under the rug; Spivak's interest here is in the "mathematical," rather than "foundational," logical structure of the reals.

Amongst these semantic assumptions are the symmetry/transitivity/reflexivity of "$=$" (your point (3)) the substitution property for "$=$" (your point (4)), and the equivalence of $\forall xP(x)$ and $\forall yP(y)$ (assuming neither $x$ nor $y$ appears bound in $P$) (your point (5)). It's a good catch that you noticed these basic principles also need justification; these issues are treated in more detail in a text on mathematical logic (e.g. Enderton). However, as I said above I think it's reasonable for Spivak to ignore them (although I personally would have included a paragraph or two explaining that they're being ignored, and mentioning where one can find a more thorough treatment).

EDIT: I misread your points (1) and (2). They assert the closure of the universe under "$+$" and "$\cdot$" - and this again is a consequence of the usual logical semantics, which requires that function symbols correspond to total (= everywhere defined) operations on the structure.

Note that lots of texts do explicitly include closure as an axiom (e.g. when something like "$g_1*g_2$ is in the group for all $g_1, g_2$ in the group" is included as a gropu axiom); this is done (when it is done) either for pedagogical value, or because the context does allow for structures with partial functions (e.g. if we're distinguishing between a group and a groupoid).