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

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

Hi:

It looks like Andrzej send this message only to me while it can be of general
interest. (If he meant it only for me it would not be in English.)

PR


----- Forwarded message from Andrzej Trybulec <trybulec@math.uwb.edu.pl> -----
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. In general the VERIFIER cannot generate such tautologies as
premises, the obviousness would become undecidable.

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).
Do we really need it ?

Andrzej

----- End forwarded message -----

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