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

On 11/6/2011 3:58 PM, Tim (McKenzie) Makarios wrote:
This discussion reminds me of this thesis:
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: .  In the interests of
full disclosure, the author of Topoi is Rob Goldblatt, who is my current

Thanks for the link.

The range/codomain part of function definition shows that much of math is just logic games.

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. So someone, somewhere back in history, conveniently decided to loosen up the definition of function to allow that. Otherwise, a tighter definition of function becomes a big show stopper.

Begin reasonably pragmatic, I'd say all these logic games are useless other than the fact that it recently occurred to me that using the Axiom of Choice is not just a useless logic game. If you can know two sets aren't equal, and the Axiom of Choice can give you that, then that's useful.

As to how this applies to me, it's not my fault. I'm a product of a centuries old university system that has programmed me to have certain expectations, and want certain things.


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