Probability without Choice, computer scientists' worldview

[gusl]

I'd like to see probability and measure theory reformulated in a theory where the Axiom of Choice isn't used. Non-measurable sets would never come up.

http://en.wikipedia.org/wiki/Non-measurable_set

<< In 1965, Solovay constructed Solovay's model, which shows that it is consistent with standard set theory, excluding uncountable choice, that all subsets of the reals are measurable. >>

Now every subset of the reals is measurable, and has the Baire property. Thus: a lot fewer concepts to worry about! And no more Banach-Tarski paradox.

Do we lose anything, really?

The idea that the only objects that exist are the constructible ones is, I think, a central idea in the worldview of computer scientists, who are, afterall, the current bearers of the intuitionistic flame; besides being central figures in ideas like cognition is computation, and so is the universe. To me, it's a direct consequence of thinking of the world (including ourselves) as machines; and the alternative borders on mysticism (a.k.a. metaphysics).

Coming back to mathematics, why don't I see any computer scientists working on Choice-free mathematics? And why don't I see mathematical librarians cataloging which bits of mathematics are still kosher, according to constructivists? I'd love to see a choice-free graduate mathematics curriculum, but I'd be happy to just see a book on Probability.

Comments

[gustavolacerda.livejournal.com]

I sure hope that choice-elimination (when possible) is less expensive than cut-elimination.

Hang on... aren't you working on proof-mining??

[htowsner.livejournal.com]

The specific issues between eliminating choice and cut-elimination are rather different. Most importantly, I'm not aware of any "choice-elimination" theorems. More typically, someone decides to analyze a particular proof, and finds that the choice functions involved are actually unnecessary, or can be replaced by something explicit.

Conversely, unlike with cut-elimination, one isn't often guaranteed that a choice-free proof exists. Instead, it's a matter of doing some additional real mathematics to verify that there is such a proof. (And yes, I'm working on proof-mining, which is why I spend a lot of time thinking about these concerns; and yes, there's some overlap with ideas from descriptive set theory, which is part of why I'm in Los Angeles, the world capital of descriptive set theory.)