Ask HN: Axiomatic algebra, like ch 1 Spivak's Calculus? | Hacker News Reader

Ask HN: Axiomatic algebra, like ch 1 Spivak's Calculus?

3 pointshyperthesis3 comments

If mathematics comprises algebra and analysis, it's curious that Spivak's Calculus begins with an axiomatization of algebra.

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.

I really enjoyed this approach, but it has omissions: details like equality transitivity (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).

I'd like full rigour, a treatment I could code, without need of mathematical maturity to paper-over abbreviations.

This is a big ask: I also want this detail without tedium; to retain the joie de vivre of Spivak, without gaps. The fun of building, like a construction set or building blocks.

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."

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.

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 https://leanprover-community.github.io/mathlib4_docs/Mathlib....

Thanks, I'll take a look at those late chapters.

The algebra is my main interest, that happens to be in a calculus text.

0a = 0 is proven later in ch 1, it's just the ordering.

By "something I could code", I mean implementimg these properties (more like writing a proof assistant).

Being more precise: I like Spivak not defining addition, multiplication or number. I just want the other steps explicit, like equality transitivity, enough to implement it (for a computer without "mathematical maturity".)

I feel I already know what's needed - but I didn't catch the 0.a=0 omission at first, and there's surely others I'm still missing... Part of the problem is I have too much implicit knowledge.

Reply on news.ycombinator.com