Thanks a lot for your reply! -stan
On Mon 2 Nov 2020 at 21:26, Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/a7fb1795-d584-4ee8-8c61-07d5d9557a76n%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/CACZd_0y%3D1PjxKThpjqZQAdzL%3Dtp1es0Tg4XGGbwS07vfUYzvnQ%40mail.gmail.com.
