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 On 16/03/2020 00:07, Norman Megill wrote:
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. -- 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] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/11cdad8c-f77f-4d65-9f94-fbec7a20e7db%40googlegroups.com <https://groups.google.com/d/msgid/metamath/11cdad8c-f77f-4d65-9f94-fbec7a20e7db%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/d9b07910-3380-229e-f712-9d716a43e80b%40gmx.net.
<<attachment: Peano.zip>>
