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.
On 6/22/21 1:13 PM, Patrick Brosnan 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 <http://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 <http://peano.mm/> I have
in the github repository here https://github.com/pbrosnan/ntg
<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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/42c295b7-2a0d-469f-9e16-cb615f1edf18n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/42c295b7-2a0d-469f-9e16-cb615f1edf18n%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/3d021845-256d-0e1e-7ca4-75b50def58b3%40panix.com.
