Re: Question about environments

Hi,


 I would like the assertion 'k in omega' to work without explicit reference
>> to the relevant definition. Is this possible?
>>
>
> Essentially the answer is 'no'.
>
>
>  Previously when I've come across what appear to be insurmountable problems
>> I've copied the offending lines to the end of existing MML articles and
>> then
>> wittled down the environments, but when I copy and paste this assertion
>> into
>> PYTHTRIP, for example, and try to verify it, I get the same *4 error. This
>> makes me suspect that the assertion can never be accepted without explicit
>> reference to the definition. Is this true?
>>
>
> The registration mechanism only that works on adjectives cannot be used to
> infer the 'in' predicate. It would, of course, be possible to build it into
> the requirements directive, but the gain is relatively small as references
> to ORDINAL1:def 13 are not so frequent.
>

I think we have recently discussed, how this could work in general for
adjectives (like "natural") whose extension is a set (not a proper class),
i.e. they are "small". This would be similar to what is being done
automatically for the type "Element of" now.

What has to be done for this to work is to add a property for adjectives
("smallhood", "set-like", etc), and somehow make Mizar aware of the fact
that NAT is the set which is the extension of the adjective "natural".
Either have some default naming ("the naturals", etc) or treat specially the
corresponding Fraenkel term ({x: x is natural}), etc., and then either use
synonyms or  "identify" for NAT and "the naturals".

Josef