Re: Help request: Fraenkel term definition

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. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================