I think you are right - the appropriate intuitionistic version is F/2, which is equivalent to F/1 so is least disruptive. But in set.mm, we're being classical anyway so if the "naive" reading is simpler (always true or always false) then that seems best. The intuitionistic version is a little lopsided - if it's sometimes true then it's always true - not as easy to grasp. The best intuitive version is A. x A. y ph(x) <-> ph(y) but that requires more axioms than we are assuming at this point.
On Tue, May 28, 2019 at 7:04 PM 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 > <https://groups.google.com/d/msgid/metamath/666138b8-b9d3-40d9-b444-7b2eb456189d%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSt6Bcbv7YAjUPu_aJ_41%2B3Zj1Bieq9Oz2LhK4HVUxSLLA%40mail.gmail.com.
