*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Thu, 10 Nov 2011 11:28:48 -0600*In-reply-to*: <4EBB03B4.4000605@gmail.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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

Tim,

Now to your questions. SHORT ANSWER: Let f(x)=sin(x).

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 ARGUE:

Otherwise, a tighter definition of function becomes a big show stopper.Why? Can you give an example?

Regards, --James On 11/9/2011 4:50 PM, Tim (McKenzie) Makarios wrote:

On 08/11/11 05:00, James Frank wrote:To prove that f is a function, you have to show that for every element in the domain, there exists an element in the codomain that it's mapped to. But the best you might can do is show that it maps to an element in some interval.What? Why?So someone, somewhere back in history, conveniently decided to loosen up the definition of function to allow that.To allow what? I'm not convinced that anyone deliberately decided that the definition of functions shouldn't correspond with how mathematicians actually think about them. I think it's just a long-standing imprecision.Otherwise, a tighter definition of function becomes a big show stopper.Why? Can you give an example?--JamesTim <><

On 11/9/2011 4:50 PM, Tim (McKenzie) Makarios wrote:

On 08/11/11 05:00, James Frank wrote:To prove that f is a function, you have to show that for every element in the domain, there exists an element in the codomain that it's mapped to. But the best you might can do is show that it maps to an element in some interval.What? Why?So someone, somewhere back in history, conveniently decided to loosen up the definition of function to allow that.To allow what? I'm not convinced that anyone deliberately decided that the definition of functions shouldn't correspond with how mathematicians actually think about them. I think it's just a long-standing imprecision.Otherwise, a tighter definition of function becomes a big show stopper.Why? Can you give an example?--JamesTim <><

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

**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

- Previous by Date: [isabelle] New AFP entry: Efficient Mergesort
- Next by Date: Re: [isabelle] No Code Equation for LIMSEQ
- 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