On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:
>
> qed::foo |- ( T. -> RH )
>
I don't understand: it looks like you are using foo with the substitutions
ph <- T. and THM <- RH, but in order to make the latter substitution, you
need to prove that RH has type |- , which means you need to prove it ?
>This is not sufficient; you actually want the axiom to be
> df-iota $a |- ( E! x ph -> ( iota x ph ) = U. { x | ph } ) $.
Indeed, my bad.
> ... ( x = y -> P(x) = P(y) )
Is this really needed unconditionally ? For instance, for division by zero,
do we really need |- ( x = y -> 1/x = 1/y ) ? Isn't it enough to have, for
instance, |- ( ( x e. CC \ {0} /\ x = y ) -> 1/x = 1/y ) ?
> So ( 1 / 0 ) = ( 1 / 0 ) should not be rejected.
It would not be rejected with proposals 2 and higher, since every class is
equal to itself.
> I have had a similar conversation about this in Lean
If it was online, do you have a link ?
> but contrary to metamath [Lean] chooses to define x / 0 = 0 (and exploits
this equality without any hedging).
So it considers the "meadow" (a new term for an older concept) associated
with the field CC. Side remark: I prefer the version 1/0 = \infty that I
used in ~df-bj-invc.
> The key insight is that because this does not affect consistency (it's a
definition)
I don't understand: definitions like this may lead to inconsistencies (for
instance, here, you'd better avoid the axiom x x^{-1} = 1). The theory of
meadows is of course consistent, but in general, one has to be careful. Or
you were referring to something more specific ?
> I contend that we already follow proposal 3 except in specific whitelist
situations.
I do not see any discouragement tag for df-iota nor even for iotanul. Or is
this part of the whitelist ? Could we document this whitelist somewhere ?
Benoît
>
--
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/e0650713-9c2d-4311-92fb-06f296cd22ea%40googlegroups.com.
