e. in the context of fol or sol + Peano

[Norman Megill]

fl requested that I post this.

Norm

-------- Forwarded Message --------
Subject: e. un the contexr of fol or sol + Peano
Resent-From: nm
Date: Sun, 15 Mar 2020 16:27:03 +0100 (CET)
From: fl
To: Megill, Norman

Hi Norm,

I'm explorating the Peano axioms
in the context of first or second order logic.

Peano uses a "e." symbol
to express phrases like "x e. NN",
"x is a number". There was no set theory
intent in his m'indiquer. So I'd like to reuse the
material in set.mm related to
e., class variables, class builder. They
are in the set theory part,
but it seems to me they don't use
any set theory axiom.
Could you post this message for me.
Due to quarantine, I no
longer have access to my usual
computers and my Google account
is no longer available. And maybe you
can also answer if you want.

[Thierry Arnoux]

Hi Norm and Frédéric,

There is a Peano Arithmetic in Metamath authored by Robert Solovay here: http://us.metamath.org/metamath/peano.mm.
I don't see any theorem proved in that version. Also, it is using reverse polish notation.

So out of curiosity, I have stripped "set-pred.mm" out of set.mm, to get only the predicate logic, and actually truncated it to remove even quantifiers.
Based on that, I have built a small peano.mm file which I attach. It includes the axioms, plus some basic proofs (commutativity, associativity of addition, and room for more)

In that version, I don't use quantifiers at all, and define the induction axiom as an axiom scheme just like the induction theorems in set.mm, using substitution hypothesis.
I'm using the "N e. NN" notation for "is a natural number", however there is no concept of set or class at all; instead, I've defined a "term" as a building block in a wff.

This is rather a sketch and there might be better axiom choices.

BR,

_
Thierry

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/11cdad8c-f77f-4d65-9f94-fbec7a20e7db%40googlegroups.com.

[Norman Megill]

I'm explorating the Peano axioms

in the context of first or second order logic.

Peano uses a "e." symbol
to express phrases like "x e. NN",
"x is a number". There was no set theory
intent in his m'indiquer. So I'd like to reuse the
material in set.mm related to
e., class variables, class builder. They
are in the set theory part,
but it seems to me they don't use
any set theory axiom.

I was unsuccessful finding reliable historical information about Peano's epsilon.

For example, Wikipedia https://en.wikipedia.org/wiki/Epsilon says 'The symbol \in, first used in set theory and logic by Giuseppe Peano and now used in mathematics in general for set membership ("belongs to") did, however, evolve from the letter epsilon, since the symbol was originally used as an abbreviation for the Latin word "est" ["is"].'

First, I didn't know Peano was actually doing "set theory".  Was he?  Also, if it 'was originally used as an abbreviation for the Latin word "est"' then who was the original user?  Presumably it wasn't Peano, since he was doing "set theory" per Wikipedia.

If we assume, contrary to Wikipedia, that it was Peano who introduced epsilon as its first user, and that he was using epsilon to abbreviate "est", then perhaps he just meant "a property" and not "an element of".  For example, "the apple epsilon green" might have just meant "the apple is green" as in ordinary conversation, not necessarily conceptualizing it as the apple being a member of the set of all green objects.  And "A epsilon NN" might have simply meant "A has the property of being a natural number" rather than "A is a set contained in the larger set NN".

All of that is my guess, though.  If someone has better access to historical sources, please feel free to correct me.

Norm

[Sine Flexione]

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