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/cfd037ae-04f5-4216-85d2-b339c45b3f5bn%40googlegroups.com.
