Re: [mizar] Unique substitution

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Sun, Jan 11, 2004 at 05:03:27PM +0100, Andrzej Trybulec wrote:

> Piotr Rudnicki wrote:
> 
> >
> > I have always hoped this would be implemented along the lines of the Davis's
> > criterion for obviousness, ie. when unique substitutions are forced which is our
> > case.  If we take after Josef Urban (for want of any other source) that
> > referring to FUNCT_2:def 1 means referring to
> >
> > for X,Y being set  for R being Relation of X,Y holds
> >  ((Y = {} implies X = {}) implies ( X = dom R iff R is quasi_total))
> >  &
> >  (not (Y = {} implies X = {}) implies ( R = {} iff R is quasi_total))
> >
> > then it seems quite a natural expectation that for f being a Function of NAT,
> > +NAT
> > we should get that
> >
> >         dom F = NAT
> 
> What about if you take an arbitrary set A instead of NAT. Is it still obvious?

If the only relation in the inference is of type Relation of A, A then
I would say yes.

> > without any ado as all instantiations for universally bound variables are
> > uniquely forced and we are left with propositions only. So mayby after
> > all substitutions are done the checker could check whether it got a tautology?
> >
> > > Do we really need it ?
> >
> > I do not think that checker should generate any tautology while I am sure
> > that coping with unique substitutions in a special way would be beneficial.
> 
> As a rule, we have several terms that may be substituted. I do not like to implement
> special rules that may be used once in a thousand inferences.

True, but I am only suggesting that once all substitutions are made one can
do propositional reduction once more and without experiments it is impossible
to say how frequent this can be.

> BTW It is not the point, but:
> 
> 1. In the inference in the question the substitution is not unique, NAT is "Subset
> of REAL" so REAL occurs in the inference and it may be substituted as well.

But there is only one substitution for R which forces substitutution for X and Y.

> 2. Davis' criterion is not that a unique substitution is forced but that there is a
> substitution that results in the contradiction, and the obvious problem is how to
> find it.

Right, it was my simplification of Davis's criterion that I called
"unique substitution" in the 87 paper in JAR.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr