Re: [mizar] non necessarily non empty types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Mon, 17 Nov 2003, Andrzej Trybulec wrote:

> > let A be set;
> > let B be infinite set;
> > surjective -> infinite Function of A,B;
> 
> OK You can of course to prove the coherence of such registration (see
> Attach). 

Oops, so that means that I am trying to break into an open door, with my 
shiny arguments for allowing conditional clusters to work with weak 
types :-). 
So I can have clusters like
measurable -> inaccessible Aleph;
and
circular -> triangular square;
working for me. 

The thing which did not work for me was a functional cluster, like (C):

let A,B be set;
let F be one-to-one Function of A,B;
let G be one-to-one Function of B,A;
cluster G * F -> one-to-one;

where an unregistered type is not allowed in the loci declaration.
So I wrongly supposed, that it will be the same for succedents of functor 
clusters, and also that it will be the same both for antecedent and 
succedent in conditional clusters. 

That actually means, that terms can get unregistered result types this 
way, and such unregistered types can be smuggled into quantification, 
by using diffuse statements, probably causing no harm, because such terms 
witness the nonemptiness of such unregistered types. 

So it would now seem to me quite natural, that if we allow unregistered 
types to be generated by functional clusters, and propagated and 
generated by conditional clusters, there is no reason why not to allow 
functional clusters to propagate them too.

I.e. the unregistered (and unregisterable - actually weak) type 
"one-to-one Function of A,B" can be generated by various clusters already 
now, e.g. by specific functor and conditional clusters for A,B empty, or 
A finite, B infinite, etc., and no matter how such F,G were generated, 
(C) is the cleanest thing how to deal with propagation of "one-to-one" 
into "G * F" generally. 

We need weak types also for such useful things :-).


> for a partial function it is obviously false.

If you define "onto" for "PartFunc of A,B" in the same way as for 
"Function of A,B", Mizar accepts your proof for PartFunc.

Josef