On 7/4/23 14:45, Marshall Stoner wrote:
It seems like allowing bundled variables is what causes a lot of complexity in a few proofs. My philosophy would be to keep variables distinct except for special cases where it might be necessary or helpul
Specifying distinct variables most of the time is the way I would tend to write proofs. I'm not sure I can think of any case where you need to specify two different set variables without a distinctness constraint. Of course with a class variable and a set variable you need to omit the distinctness constraint where the class is in terms of that variable. Example: if A is "( x + 1 )" and a theorem has A and x in it, then there can't be a distinctness constraint between A and x . I guess a formula variable and a set variable are similar Example: if ph is "x > 5" then ph and x are not distinct.
-- 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/7c471de4-d112-3841-7642-41b1ae5a0f8f%40panix.com.
