*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*: Mon, 07 Nov 2011 10:00:34 -0600*In-reply-to*: <4EB70322.3010507@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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

On 11/6/2011 3:58 PM, Tim (McKenzie) Makarios wrote:

This discussion reminds me of this thesis: http://people.pwf.cam.ac.uk/mg262/GanesalingamMdis.pdf I've only read fragments of it, but particularly relevant to what started this whole discussion is the observation on page 189 that the standard set theory definition of functions doesn't reflect how mathematicians actually think of functions. In particular, according to that definition, functions don't have unique codomains. (The footnote about this observation being novel indicates that the author was unaware of page 19 of Topoi: http://tinyurl.com/7qx72ou . In the interests of full disclosure, the author of Topoi is Rob Goldblatt, who is my current supervisor.) Tim <><

Thanks for the link.

--James

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

- Previous by Date: Re: [isabelle] problem with locales
- Next by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- 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