If mathematics comprises algebra and analysis, it's curious that Spivak's <i>Calculus</i> begins with an axiomatization of algebra.<p>It's not complete - addition and multiplication are not defined, nor even "number". Instead, it's properties of commutativity, associativity, distributivity, identities and inverses, and it's astonishing how far that takes us.<p>I really enjoyed this approach, but it has omissions: details like <i>equality transitivity</i> (things equal to something are equal to each other), and there's deliberate gaps (like using 0.a=0 twice in a proof before being proven, while claiming a comsequence).<p>I'd like full rigour, a treatment I could code, without need of mathematical maturity to paper-over abbreviations.<p>This is a big ask: I also want this detail without tedium; to retain the <i>joie de vivre</i> of Spivak, without gaps. The fun of building, like a construction set or building blocks.<p>Any recommendations? (perhaps I'll have to write it myself)
Everything you are looking for is provided in the Epilogue of Spivak. For instance, in chapter 28, you will be able to show that 0a = 0 in any field. In chapter 29, you will rigorously define the reals as well as the operations on them. You will also show that they form a complete ordered field, which allows you to use the results from chapter 28. In chapter 30 you will show that all complete ordered fields are "essentialy the same" as the real numbers---i.e., the real numbers are "unique."<p>At the moment I'd advise not worrying much about the construction of the reals. Ideas such as limits, continuity, differentiation, integration, and even fields are much more important for later mathematics and applications (abstract algebra, topology, geometry, physics) than the construction of the reals. Constructing the reals is pretty much something you do a couple of times (traditionally once with Dedkind cuts, as in Spivak, and once more with Cauchy sequences) and then never think about again.<p>Edit: I'm not sure what you mean by "something I could code." If you want something that you could type in a proof assistant you might have some luck looking at the mathlib library of Lean <a href="https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Basic.html#:~:text=lean%20.&text=The%20type%20%E2%84%9D%20of%20real,Cauchy%20sequences%20of%20rational%20numbers.&text=Lean.ParserDescr-,The%20type%20%E2%84%9D%20of%20real%20numbers%20constructed%20as%20equivalence,Cauchy%20sequences%20of%20rational%20numbers.&text=The%20real%20numbers%20are%20isomorphic,Cauchy%20sequences%20on%20the%20rationals" rel="nofollow">https://leanprover-community.github.io/mathlib4_docs/Mathlib...</a>.