I agree with Norm. I think the current definitions (df-opab, df-ral...)
are simple and consistent, and the changes proposed by Mario, if needed for
the translation, should be done by the translation engine.
As for df-ral, yes, the current definition of "A. x e. A ph" will bind
occurrences of x in A, and I think this makes it syntactically simpler,
with nothing hidden. Most often, we do not want x to appear in A, but it
looks like with Mario's proposal
df-ral2 $a |- ( A. x e. A ph <-> A. y ( y e. A -> [ y / x ] ph ) ) $.
if one uses an A containing occurences of x, the "machine" says "oh, you
inadvertently used an A containing x, let me free the occurrences of x in A
for you". The machine means well, but this looks like a hidden mechanism,
and indeed it may cause much confusion. Additionally, df-ral2 is much
harder to understand than df-ral.
By the way, since we want to avoid as much as possible using df-ral with A
containing x, what do you think of:
$( ... Use ~ dfral whenever possible. (New usage is discouraged.) $)
df-ral $a |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) $.
${ $d x A $. dfral $p |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) $= ?
$. $}
A side question about Mario's proposal
df-opab3 $a |- { <. x , y >. | ph } = { z | E. x E. w ( z = <. x , w >.
/\ [ w / y ] ph ) } $.
It looks to me that this is incorrect: an instance of it is
|- { <. x , x >. | x = 2 } = { z | E. x E. w ( z = <. x , w >. /\ [ w / x
] x = 2 ) }
which yields, if I'm not mistaken,
|- { <. x , x >. | x = 2 } = { z | E. x z = <. x , 2 >. }
which is clearly false.
Benoit
--
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/8f3b6b89-152d-4f0d-9a96-385c4ab4e6ca%40googlegroups.com.
