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

Re:Ask HN: Axiomatic algebra, like ch 1 Spivak's Calculus? by octed on Saturday September 21, 2024 @07:22PM (#41613384)

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

[ Parent | on HN ]

Re:Ask HN: Axiomatic algebra, like ch 1 Spivak's Calculus? by hyperthesis on Sunday September 22, 2024 @05:38PM (#41620305)

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

[ Parent | on HN ]

Re:Ask HN: Axiomatic algebra, like ch 1 Spivak's Calculus? by hyperthesis on Monday September 23, 2024 @06:16PM (#41631173)

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.

[ Parent | on HN ]