Re: [trybulec@math.uwb.edu.pl: Re: [mizar] Why *4?]

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

On Fri, Jan 09, 2004 at 08:25:18PM +0100, Andrzej Trybulec wrote:
>
>
> Piotr Rudnicki wrote:
>
> >
> >  consider f being Function of NAT, NAT;
> >
> >  dom f = NAT by FUNCT_2:def 1;
> > ::>           *4
> >
> >  NAT = {} implies NAT = {}; then
> >  dom f = NAT by FUNCT_2:def 1;
> >
> >
+------------------------------------------------------------------------------
> >
> > we get *4.  Why?  Why adding an obvious premise here solves the problem?
> >
>
> If you write it in a bit different way:
>
>     NAT <> {} or  NAT = {};
>  then  dom f = NAT by FUNCT_2:def 1;
>
>
>  you probably see what is the problem. You just press VERIFIER to consider two
> cases. It is not exactly news. You
> might remember a conference in Plock ("Technology of Science", around 1978)
+when
> this phenomenon was observed by Dimiter Skordev.
  
I have never met Dimiter Skordev although I heard of his "device" from you but
I cannot say that I ever understood its signifcance.
  
> In general the VERIFIER cannot generate such tautologies as
> premises, the obviousness would become undecidable.
  
I do not see how this can immediately lead to undecidability when only one
universal sentence is in the reasoning.
  
> However, and I believe you took part in the discussion, if a heuristic is used
+to
> find which tautologies of this form could be added (what in Mizar jargon we
+call
> "Skordev device", if you recall), then it might be feasible. It enables to
> use two or more universal premises as main premises (i.e. to substantiate
+them).

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

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.

Best,

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