Question about (extra) DVs

[Stanislas Polu]

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  

[Norman Megill]

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

[Stanislas Polu]

Thanks a lot for your reply!

-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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a7fb1795-d584-4ee8-8c61-07d5d9557a76n%40googlegroups.com.

[Benoit]

Your answer made me read the comment of http://us.metamath.org/mpeuni/ax6v.html

It is written there that the DV condition was introduced "out of the blue, with no apparent justification".  I am not in Tarski's head, but here is a possible justification.  In a logic with terms, the analog axiom scheme would be

  \exists x x = t , DV(x,t)

where t is a term metavariable.  In this case, the DV condition is necessary (the axiom scheme would be false without it --- for instance, take t={x} in a well-founded set theory).  Therefore, returning to our logic without terms, the sufficiency of the axiom scheme

  \exists x x = y , DV(x,y)    (ax6v)

is noteworthy, even though the more general axiom scheme

  \exists x x = y    (ax6)

does hold.

(The analog axiom schemes for a logic with terms were given in Kalish--Montague).

Benoit