I don't really have an opinion about whether set.mm and iset.mm should use the same definition as each other or not, but as for the options in iset.mm, we have http://us2.metamath.org/ileuni/nf3.html http://us2.metamath.org/ileuni/nf2.html and http://us2.metamath.org/ileuni/df-nf.html . Since we've shown these are equivalent in iset.mm, there isn't a practical difference between them (given the current axioms, anyway).
The nf4 one only holds in one direction: http://us2.metamath.org/ileuni/nf4r.html To the extent that this is all about what the axioms are and which axioms are needed for what, I think iset.mm has been much less explored than set.mm that way. I wouldn't be surprised if we still have redundant predicate logic axioms (even after having eliminated a few), for example. On May 28, 2019 4:04:55 PM PDT, Benoit <[email protected]> wrote: >I was considering the same thing... Intuitionistically, one has > >( A. x ph \/ A. x -. ph ) => ( E. x ph -> A. x ph ) => ( -. A. x ph -> >A. x >-. ph ) > >To me, this was an argument that ( A. x ph \/ A. x -. ph ) is too >strong >though, and that the correct characterization of "non-free" should be ( >E. >x ph -> A. x ph ). I still have to think about it, though... Do >people >who have some iset.mm practice see a practical advantage to either ? > >-- >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/666138b8-b9d3-40d9-b444-7b2eb456189d%40googlegroups.com. -- 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/D16FA593-5608-4C1F-B449-C27655C589B8%40panix.com.
