Help request: Fraenkel term definition

[Greg Frascadore]

 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];

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

 Thanks
 - Greg Frascadore

[Josef Urban]

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

[Adam Naumowicz]

Hi,

On Fri, 12 Dec 2008, Greg Frascadore wrote:

>
> 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];
>
> Yet, I don't see it in hidden.miz. How does one know what definitions
> are available but hidden?

Currently set comprehension using Fraenkel terms is a built-in feature of
Mizar, so it has no definition in the library. Its meaning is therefore a
part of the semantics of Mizar, just like in the case of other Mizar
constructs (definitions of functors, predicates, etc.).

Some time ago, however, Freek Wiedijk proposed a more general approach,
i.e. to allow defining binders (see his note at
http://www.cs.ru.nl/~freek/mizar/binder.pdf). If we had such a mechanism
in Mizar, then it would be possible to define Fraenkel terms on the user
level.

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================