Re: [mizar] A general question on writing recursive functions in mizar

[trybulec <trybulec@math.uwb.edu.pl>]

Ozyavas, Adem wrote:

> provides info on 
>
> 1) the distinction between mizar functors and functions, 
>
>  
Hi:

the distinction is not specific for Mizar.
We use two different names for formula constructor (predicate) and the 
similar set theoretic object (relation). Unfortunately there is no such 
commonly accepted distinction in the case of functions. Usually we use 
'function' for a set theoretic object and 'lingual function' for the 
term constructor. The name 'functor' for the term constructor was 
borrowed from Rasiowa&Sikorski "Mathematics of Metamathematics". A 
little bit better that 'function'. Still, it should be not confused with 
'functor' in category theory, that is a (specific) function.

The distinction is important, beacuse mixing two concepts may lead to 
the inconsistency. E.g. we may define ther
union of two sets (a functor):
         A \/ B
but there is no corresponding function (the domain cannot be the 
Cartesian square of the set of all sets, because there is no such thing).

In concrete mathematics the distinction is not so important, but there 
are stll technical issues described by Adam.

Regards,
Andrzej