I would like the assertion 'k in omega' to work without explicit reference
to the relevant definition. Is this possible?
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