Yes, it is valid and safe. Of course the extra dv's would either be redundant or weaken the theorem, but for some purposes that doesn't matter. There has been confusion about this before, which is why I added a comment about it at http://us.metamath.org/mpeuni/ax6v.html.
Of course, if a proof referencing the weakened theorem expects the stronger version, its verification will fail. Verifying all proofs will easily detect this, though. Norm On Monday, November 2, 2020 at 2:30:20 PM UTC-5 [email protected] wrote: > 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/a7fb1795-d584-4ee8-8c61-07d5d9557a76n%40googlegroups.com.
