[mizar] Unique substitution

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

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?

>
>
> 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.

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.

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.

All the best,
Andrzej