Re: [mizar] Global choice

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

On Thu, 7 Nov 2002, Andrzej Trybulec wrote:

> I guess you use 'undecidable' in an old fashioned manner ('independent'), undecidability is
> not an issue.

Yes, I probably have some gaps here. I understand the differecne between 
complete and decidable theory, but sentence "undecidable" in a theory and 
"independent" of a theory seem to be synonyms for me. Could you enlighten 
me further? Anyway, I meant several things - the "is" statement can really 
be "independent", or its status can be unknown, or it is decidable (would 
you use "dependent" here?), but the proof can be very difficult in Mizar 
(the terminology colonizers should create some notions e.g. "Mizar-hard", 
or "formalization-hard" :-). 

> For pure Mizar (without requirements) I believe the convenient semantics is :
> Let U be the universe and let U be well ordered. Let
>     the fixed theta = the first element of U that is in | theta |
> ( | theta | - the denotation of the type theta).
> 
> As defaults goes, I intend to be a very careful about it. For the beginning I would be
> quite satisfied with
> 
>     the fixed set = 0
>     the fixed non empty set = 1
>     the fixed non trivial set = 2
> 
> i.e. I just want 0,1, and 2  to be the first three in U (wrt the ordering). Even better,
> let's assume that natural numbers constitute an initial segment in U.

OK, I just looked at the abstracts, to get some measure of what we talk 
about. It seems that {} (or empty set or 0) is used pretty often as a 
default.
Interesting examples are CLOSURE2:def 4 and FUNCTOR0:def 4:
ManySortedSet of I defaults to [0]I there. Will we have 
enough rules for the Global Choice function to show this? Should we e.g. 
make the global well-ordering respect rank? - But it contradicts having 
omega as initial segment (and can be insufficient for this case anyway). 
Similarly, I doubt pretty much that you will sacrifice the obvious 
"product" default for structures.
My bet is that we will end up adjusting (or precising) the rules (and if 
not the rules, then the well-ordering) each time such example appears (and 
the magic ENOD word will come in handy :-). But why not, it is a middle 
way between the two approaches.

Josef