Hi Patrick, You're right, pa_ax7 is a definition indeed, I oversaw it, so what you say applies: only add DV(x,z), DV(y,z). This is necessary for having a real definition, and if you added also DV(x,z), you could not recover that version (since you couldn't do anything with a wff of the form "x < x").
There are several axiomatizations of Peano arithmetic with different signatures (that is, different choices of "primitive" or "undefined" notions). The present one uses the signature (0, S, +, *), and "<" is a defined notion. As for recovering the axioms from their weakenings obtained by adding DV conditions, I'm not sure whether it is possible. If you use set.mm's version of FOL, then it is possible by Megill's metacompleteness theorem, but peano.mm's axiomatization of FOL (which I haven't looked) may not suffice. This is an interesting question indeed. Benoît On Tuesday, June 22, 2021 at 10:13:25 PM UTC+2 [email protected] wrote: > Hi Benoit, > > I think pa_ax7 should be viewed as a definition (because it defines "<" in > terms of previously defined things). And if you view it that way it > violates the soundness condition of having all (new) variables distinct. > This condition is in the "note on definitions" on the main metamath site > and I also saw it in the slides for a lecture Megill gave at IHP. (I think > it says "new" variables in the IHP lecture and maybe all variables in the > note on definitions.) It seems that the other axioms, pa_ax[1-6], are not > really definitions. Also it's pretty clear that they're true without the > DV condition. So I think my vote would be just for treating "<" as a > definition in peano.mm and adding the DV proviso to that. My guess is > it wouldn't matter anyway, because I think if you reformulated pa_ax[1-6] > with DV proviso's you could probably prove in the end that they hold > without the provisos. (That might be kind of fun of course. But, > somehow, also a little tedious at the same time.) > > Another possibility would be just to kick pa_ax7 out of the axioms > completely and rename it as a definition, "df-lt" or something like that. > I kind of like that idea because I wanted to work with "\leq" first > instead of "<". But having pa_ax7 as an axiom made it seem somehow > "primary." > > Patrick > > On Monday, June 21, 2021 at 11:00:54 AM UTC-4 Benoit wrote: > >> Good catch ! You're right, these two DV conditions are necessary to >> salvage the file (this is typical for a variable one quantifies over: it >> has to be "fresh"), and sufficient (well... provided PA is consistent and >> the rest of the axiomatization is correct). Actually, these axioms pa_ax1 >> to 7 are usually written in the object language (with v_0, v_1, etc.), so >> you could as well put DV conditions among all variables at once, i.e. >> ${ $d x y z$. >> pa_ax1 $a >> ... >> pa_ax_7 $a >> $} >> >> Benoît >> >> On Monday, June 21, 2021 at 4:37:19 PM UTC+2 [email protected] wrote: >> >>> Hi Metamath Community! >>> >>> I'm writing to let you know about a small problem with the metamath file >>> peano.mm (which allows you to prove that 0 = 1). It's in >>> pa_ax7 which reads >>> >>> pa_ax7 $a |- iff >>> < x y >>> exists z = y + x S z $. >>> >>> The problem is in the bundling of the variables x and y with z. I think >>> it could be easily fixed by adding distinct variable conditions >>> >>> $d z x $. >>> $d z y $. >>> >>> But if you allow z and y to be the same variable then you can derive a >>> contraction. I do >>> this in the development of peano.mm I have in the github repository >>> here https://github.com/pbrosnan/ntg. In the end I prove that 0 = 1 >>> and then >>> that any wff holds. (And I guess you can also get a contradiction if you >>> allow z and x to be the same variable.) >>> >>> Aside from pointing this out, I'd also like to say thanks to everyone on >>> this list for their work on metamath, which I think is an amazing and >>> beautiful creation. >>> >>> Patrick Brosnan >>> >>> >>> -- 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/738a7e66-6bee-48ee-88e5-f20550c06478n%40googlegroups.com.
