*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Fri, 11 Nov 2011 10:29:47 +1300*In-reply-to*: <4EBC09D0.408@gmx.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com> <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@mail.gmail.com> <4EB5709A.3090203@gmx.com> <CAFP4q16dyEd=_SeC28GDN6kFkwTUyJvO-+_htuwXgNjsu8B43w@mail.gmail.com> <4EB654A4.6010500@netspeed.com.au> <4EB70322.3010507@gmail.com> <4EB800A2.2020200@gmx.com> <4EBB03B4.4000605@gmail.com> <4EBC09D0.408@gmx.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.23) Gecko/20110921 Thunderbird/3.1.15

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. Tim <><

**Attachment:
signature.asc**

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Josef Urban

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Jeremy Dawson

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

- Previous by Date: Re: [isabelle] No Code Equation for LIMSEQ
- Next by Date: [isabelle] Subset Types
- Previous by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list