Re: [isabelle] Trying to fit HOL to traditional math verbiage

On 11/11/11 06:28, James Frank wrote:
> SHORT ANSWER: Let f(x)=sin(x).

This could define several different functions.  For example, it could
define a function from the complex numbers to the complex numbers; it
could define a function from the real numbers to the real numbers; or,
it could define a function from the real numbers to [-1,1].  The point
is that according to the standard definition of functions, the last two
are identical.

> YOU ASK: What? Why?
> Because the definition requires it.
> Let f be a subset of AxB. Then f is a function if
> 1) for every x in A, their exists some y in B such that (x,y) is in f, and
> 2) if (x,y1) is in f, and (x,y2) is in f, then y1=y2.
> We call A the domain of f, and we call B the codomain of f.

But "the codomain" isn't well defined.  I think the example from Topoi
illustrates my point quite well.  What is the identity function on the
natural numbers?  According to the traditional definition, the answer is
{(0,0), (1,1), (2,2), ...}.
What is the injection function from the natural numbers to the integers?
{(0,0), (1,1), (2,2), ...}.
The traditional definition requires that an identity function on a set A
is exactly the same function as every injection function from A to any
superset of A.  I don't believe that this is how mathematicians actually
treat identity and injection functions.

And the crucial thing is this:  If I ask "What is the codomain of
{(0,0), (1,1), (2,2), ...}?",
the answer has to be that the codomain isn't uniquely defined, but must
be some superset of the natural numbers.


Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.