[mizar] Global choice

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

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

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.

I think it is a long way before we can allow the users to set their own defaults.

Andrzej


Josef Urban wrote:

>
> But then the undecidability can prevent you from setting a suitable
> (actually any) default for some type (because until we (dis)prove the "is"
> statement, we risk contradiction with your rule). For instance, we will
> never be able to say what the default is for all types, that are
> undecidable for containing the empty set (e.g. all structures now :-) )
> (actually, if we really _know_ that it is undecidable, we can choose any
> consistent variant and thus strengthen the axiomatics, but we may fail to
> know even that).
> The restriction to the widening case (I suppose you meant 'theta_2 of
> args_2' widens to 'theta_1 of args_1') does not help this.