

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

Ozyavas, Adem wrote:

provides info on

1) the distinction between mizar functors and functions,


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.