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/c0f88d8f-723d-43aa-badb-225b154ae476n%40googlegroups.com.
