On Wed, 22 Nov 2006, Jesse Alama wrote:
Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:I think the problem is that the type "0-chain of p" does not syntactically widen to "Element of ..." . I checked just now, and it seems that non-emptiness is no longer a problem. So yes, this really has to be done syntactically in the (re)definition of "0-chain of" like mode 0-chain of p -> Element of foo means .... If it is e.g. just a proved theorem, Mizar will take no notice.I see now, thanks. If I choose to not redefine 0-chain of p, what form should the theorem take?
just to repeat for sure: if you choose not to have the type widened through (re) definitions into Element of ..., the fraenkel term will not work (with the current implementation)
My first guess is: for x being 0-chain of p holds x is Element of <something> Does that look right?
yes, it is exactly the "coherence" condition which would need to be generated by the system and verified for the typing above - if you click on "coherence" e.g. at http://mmlquery.mizar.org/mml/current/relset_1.html#M2 , you'll see the system-generated condition for a similar definition
By the way, why does the use of the fraenkel operator require that my term c of type 0-chain of p also have type `Element of X' for some term X of type `non empty'?
as I said, it seems that the non-emptiness is no longer required by the system
Does the mizar logic become inconsistent if we drop this general requirement on the use of the fraenkel operator?
there has to be something to avoid Russel's paradox ( { x where x is set: not x in x } ), ZF does it by restricting Replacement/Comprehension (which is behind Fraenkel terms) only to domains of existing sets. So if we know that type of all free variables in the Fraenkel widen to "Element of Foo_i", then the domain of Replacement is limited by product of Foo_i (i ranging over the free variables). There are other methods how this can be done, we discussed some general "sethood" ("smallness") mode/attribute property some time ago - http://mizar.uwb.edu.pl/cgi-bin/wilma/wilma_hiliter/mizar-forum/0607/msg00000.html
Josef