Il giorno lunedì 16 marzo 2020 23:33:38 UTC+1, Norman Megill ha scritto: > > If someone has better access to historical sources, please feel free to > correct me. > > Norm >
Hi, Norm! This is my first message in the group, so first of all I would like to thank you for Metamath; one of my dreams was to build an automated theorem prover, but after discovering Metamath (and mmj2), I saw that there was everything that I wanted to do and better than I would have done. Well, access to historical sources... I suppose the answer is "Arithmetices principia, nova methodo exposita" https://en.wikipedia.org/wiki/Arithmetices_principia,_nova_methodo_exposita https://archive.org/details/arithmeticespri00peangoog/page/n7/mode/2up (original book in latin) https://github.com/mdnahas/Peano_Book/blob/master/Peano.pdf (english translation, not complete) In brief: 1. In the "Arithmetices principia" there is the first presentation of Peano Axioms and the first appearance of the symbol epsilon 2. Peano explicitly recognizes the influence of Grassmann and Dedekind (on page V, so it is quite fair to say Dedekind-Peano axioms) 3. Peano was actually doing naive set theory (proposition 57 on page XII) 4. Peano chose the symbol epsilon because it is the first letter of the word ἐστί (es-tee'), third person singular present active indicative of the verb "to be" in ancient Greek If you want to read it, enjoy reading! It's pretty much Metamath 0.1 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/06013d9f-07fb-40f7-86ba-5ea04ba35e6e%40googlegroups.com.
