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: http://tinyurl.com/7qx72ou . 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