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.
