Finite Choice – Can It Be Disallowed?

co.combinatoricslo.logicset-theory

When people work with infinite sets, there are some who (with good reason) don't like to use the Axiom of Choice. This is defensible, since the axiom is independent of the other axioms of ZF set theory.

When people work with finite sets, there are still some people who don't like to use the "finite Axiom of Choice" — i.e., they don't like to pick out a distinguished element of a set, or a distinguished isomorphism between a set with $n$ elements and $\{0, 1, \ldots, n-1\}$ (without some algorithm to pick it, that is). This is still an aesthetically defensible position, since oftentimes proofs that proceed that way don't give as much insight as proofs that don't use finite choice. But ZF set theory allows us to do this for finite sets!

Is there a general framework in which we can disallow, if we so choose, the method of distinguished element? I have a hunch that the fact that, even for a finite-dimensional vector space $V$, $V$ and $V^\ast$ aren't naturally isomorphic is the first step towards the "right answer," but I don't really see where to go from there.

(To be clear, as Ilya points out, I'm referring primarily to set theory; I know that/how category theory tells us about the non-naturality of the dual vector space isomorphism, in particular. My question is, is there something that either subsumes this or parallels it for more combinatorial constructions?)

Best Answer

You might want topos theory. A topos is something like the category of sets, but the internal logic of a general topos is much weaker than ZF; it need not even be Boolean. An example of a topos is the category of sheaves of sets on a topological space. You can use topos theory to turn voodoo-sounding statements of constructive mathematics into ordinary mathematical statements which you can understand: for example "a nonempty set S might not have any elements" becomes "a sheaf S which is not the empty sheaf might not have any global sections" (or possibly "might not have local sections everywhere"), which is of course true. A canonical reference on this subject is Mac Lane & Moerdijk, Sheaves in Geometry and Logic.