Freek, Mark, Bill,
Thanks very much for the stimulating and I think helpful responses,
including Mark's historical sketch. I'm glad to learn that inclusion of an
axiom of choice is considered unsurprising, perhaps leading to less weird
consequences than if it is left out. Freek's example of the union of
countably many countable sets is certainly interesting and surprising.
At a philosophical level I'm surprised that Freek's intervals of Platonism
are during the week, with formalism on weekends. Formalism seems like such
a practical attitude for the working week. ;-)
On choice operators, as a constructive software engineer / computer
scientist I certainly prefer my sets tidy and countable with least elements
I can pick out in a clear way. Wandering in the wilds of larger infinities
less well-ordered sets can get disorienting.
Regards,
-Cris
On Mon, Aug 6, 2012 at 6:31 AM, Freek Wiedijk <fr...@cs.ru.nl> wrote:
> Hi Cris,
>
> To chime in on this:
>
> I don't have any problems with a system that doesn't allow
> you to disable the axiom of choice. In other words:
> hardwire choice all you like as far as I'm concerned.
> Without AC you get weirdnesses as that a union of countably
> many countable sets doesn't need to be provably countable.
> Who would like to reason in such a weak system :-)
>
> I know, keeping track of where you used AC in a proof
> is a fun game, and textbooks sometimes do this too.
> But _mathematically_ it doesn't seem _too_ interesting to me.
>
> However, I _do_ have problems with HOL's choice operator!
> Mainly this is for philosophical -- i.e., for not very good
> -- reasons. See, I'm a Platonist (that is to say: during
> the week; in the weekend I'm a formalist :-)) So when I
> think about mathematics, I imagine a "space" of ZF sets,
> where the ZF sets "live". And when writing mathematics I
> would like to consider that as "pointing" at those sets
> and talking about them. ("Look, that set there, that's
> the natural numbers!")
>
> Now, _without_ Hilbert's choice operator epsilon, every HOL
> term clearly denotes at a welldetermined set. (That is, if
> you fix some straight-forward set theoretic encoding of the
> HOL universe.) However, once you add the epsilon, that's
> no longer true. It then depends on _what_ choice operator
> you choose, what the set is that you are talking about.
> And it's not clear how to (Platonically!) distinguish one
> choice operator from the other. Therefore once you write
> HOL terms that contain an epsilon somewhere, _I_ don't know
> (Platonically!) anymore what they mean.
>
> So the choice operator in HOL always makes me a bit uneasy.
>
> Not that it really matters of course. And a choice operator
> _is_ a really useful thing to have :-)
>
> Freek
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
