0 = 1 (in peano.mm)

[Patrick Brosnan]

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

[Benoit]

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

[Patrick Brosnan]

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

[Jim Kingdon]

I have taken the liberty of making https://github.com/metamath/set.mm/pull/2054 to add the distinct variable constraints as suggested in the first email.

I'm not sure I have an opinion about whether to rename it or any other changes, so I'm not trying to say whether anything else is worth changing in addition.

--
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/42c295b7-2a0d-469f-9e16-cb615f1edf18n%40googlegroups.com.

[Benoit]

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