Redefining iota

[sctfn]

So, it's possible to redefine ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) ). This has two big virtues: a) it's somewhat clearer what's going on (at least to me) b) it doesn't require dummy variables, so iotajust becomes unneeded

What does everyone think? I can do the footwork.

[digama0]

I think that would be a good theorem to prove as an alternative definition.

Re: (b), iotajust is already unneeded. set.mm is very inconsistent about whether definitions with bound variables require justification; in fact only ~iotajust and ~vjust are explicitly justified, while many many other definitions involving bound variables lack an actual justification theorem. It follows from a general metatheorem that these definitions with bound variables have a justification theorem, but the metatheorem also proves vjust and iotajust so these theorems can really just be thought of as demonstrations of a general technique.

[icecream17]

It seems like this new definition would at least remove ax-10 ax-11 ax-12 from iotauni iotanul, and ax-11 from iotaex fvex

[tirix]

I think that would be a good theorem to prove as an alternative definition.

Scott's already proved it as ~dfiota4

[benjub]

I think that would be a good theorem to prove as an alternative definition.

Scott's already proved it as ~dfiota4

This confirms my theory that @sctfn and @scott-fenton are actually two different persons !

And more seriously, I'm adding the analogous definition for the alternate description binder at #4177