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



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
Description: OpenPGP digital signature



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