*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*: Mon, 07 Nov 2011 10:58:58 +1300*In-reply-to*: <4EB654A4.6010500@netspeed.com.au>*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>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.23) Gecko/20110921 Thunderbird/3.1.15

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 <>< On 06/11/11 22:34, Jeremy Dawson wrote: > On 11/06/2011 05:38 AM, Josef Urban wrote: >> Hi, >> I think it would not >> hurt the formal systems to go where the mathematicians are. >> >> Josef >> > > Unfortunately "where the mathematicians are" is to use language in a way > which is typical of natural languages, which contain exactly the sort of > inconsistencies and ambiguities which lead people to use formal systems > instead. > > For example, mathematicians say things like "the derivative of f(x)", > when they are referring to the derivative of f, and they say f(n) = > O(g(n)) (but that O(g(n)) is a set of functions), when they mean f is > _in the set_ O(g) - etc. > > Jeremy > >

**Attachment:
signature.asc**

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

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

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: [isabelle] Research Assistant position on EPSRC project "Formal Representation and Proof for Cooperative Games"
- 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