Re: Help request: Fraenkel term definition

Hi Greg,

> Hello. I am having trouble finding Mizar's definition of the
> Fraenkel term, and more generally, what definitions are hidden.
>
> After reading the scheme axiom at TARSKI:sch 1 and looking around the
> rest of the MML, I don't understand how the constructor-like notation:
>        { x : P[x] }
> is defined. It's as if there is an invisible Mizar declaration resembling:
>
>        func { x : P[x] } means y in it iff ex x st y = x & P[x];

yes, a minor correction is that (corresponding to TARSKI:sch 1 -
Replacement) a functor can be applied to the "comprehended" set, i.e.:

func { F(x_1,...,x_n) : P[x_1,...,x_n] } means y in it iff ex x_1,...,x_n st y = F(x_1,...,x_n) & P[x_1,...,x_n];

and that the the predicate P can be arbitrary in Mizar, which means that
additionally x_i have to belong to "small types" - types that are known to
be sets. This is currently implemented by requiring that these types are
known to be subtypes of "Element of Foo_i" for all i

> Yet, I don't see it in hidden.miz.  How does one know what definitions
> are available but hidden?

This is not an explicit definition in Mizar, the language is not strong
enough for it (though there were propositions for adding binders to Mizar
before). It probably could be noted somewhere in hidden or tarski in
comments.

Generally, every logic has some implemented core. People normally learn
this by reading good documentation, and, if needed, by looking at
well-commented open sources of implementations. Mizar lacks the latter, so
your chance is to search e.g. Freek's tutorial for such explanations. Or
search this forum and ask if needed :-).

Best,
Josef