Hi, I was wondering (and couldn’t convince myself entirely), is it valid and safe to add arbitrary distinct variable constraints to a proven theorem and consider it a new theorem?
Such arbitrary new statements can’t be easily constructed as DVs are generally bubbled up automatically and I don’t know of a good way to introduce arbitrary new ones? Yet it seems safe to consider a statement with extra constraints as true? (This is useful in an automated theorem proving setup where theorem statements are generated as it could allow more statements to be accepted as valid theorems even if they contain extra DVs) Thanks! -stan -- 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/CACZd_0wmNx5rqkuUe-EESC_mj9Cs%2B2x08MJuc8YGKCyZ2Azsow%40mail.gmail.com.
