Can we disallow finite choice?

Question

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?)

Answer 1

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.

Answer 2

This is possible in constructive mathematics, because it distinguishes between finite sets and sets with a counted number of elements. (I'm not quite sure what the standard terminology is, though.)

A set $S$ is finite if there is a natural number $n$, such that there is a surjective map from $[0, \ldots, n-1]$ to $S$. A set $T$ is counted, if there is an $m$ such that there is an isomorphism between it and the numbers $[0, \ldots, m-1]$.

Now, note that finiteness bounds the number of elements in $S$ -- there can be no more than $n$. However, we do not necessarily know exactly how many elements there are, since equality may not be decidable on $S$. (That is, we might not know how to show for every $s$ and $s'$ that $s = s'$ or $s \not= s'$.) Of course, countedness implies finiteness (just take one half of the iso). It also implies decidable equality on the elements (since we can convert two $T$s to natural numbers, and compare those). Likewise, finiteness and decidable equality imply countedness (iterate over the elements of $S$, and use equality to identify the duplicates). But finiteness alone is not sufficient to imply countedness.

This seems to me to capture the intuition that we might not always have the distinguished isomorphism available. A combinatoric argument gives a method for (constructive) counted sets. One that doesn't use choice gives a method which will also work (constructive) finite sets.

Answer 3

Actaully, you can avoid such arcane horrors as categories and topoi. When moving from infinite to finite, much of the difficulty (imo) is in figuring out 1) how the original statement was really algorithmic in nature and 2) what the implicit resource bounds were. Once you figure these statements out, it becomes much clearer what the AC-oracle is actually doing for the algorithm, and then come up with analogous resource bounds.

My sense is that approaching your problem(s) this way will be both more useful and satisfying that assuming that some battery of huge guns is going to work one day.

For specific references, you might look at the work of Blass, Gurevich and Shelah on "Choiceless Polynomial Time" -- this is essentially computing using the hereditarily finite sets over a finite set of atoms. The finite-model theory literature is full of work on the power of various models of computation with and without a linear order. There is also a (largely incomprehensible, but what can you do) paper of Shelah's on classifying second-order quantifiers over finite universes.

Answer 4

Since we're all generating ideas, here's a way to tell the difference between a set with n elements and a set with a chosen enumeration, i.e. a chosen bijection with {1,...,n}. Namely, consider the endofunctor on the groupoid of finite sets (so only isomorphisms are allowed) that assigns to each finite set its set of permutations, and on the other hand consider the endofunctor that assigns to each set S of size n the set of bijections between S and {1,...,n}. Then each functor assigns a set of size n! to each set of size n, but the functors are not isomorphic — they behave differently on morphisms. However, they are isomorphic on the groupoid of sets with chosen enumerations, because this groupoid has no nontrivial automorphisms.

So what's the point? Most combinatorial constructions can be worded as endofunctors on the groupoid of finite sets. And wording them this way requires at the very least that you be very attentive to whether you have picked some elements. If you can word your proof as an isomorphism of endofunctors, then probably it's good without "axiom of finite choice".

Answer 5

Note that, in a nitpicky sense, ZFC does not allow you to make finite choice; at best it simply tells you whether there are choices available to be made. Instead, it's the logic you use to reason with ZFC that permits you to make choices.

You might instead change your point of view on what such an argument means: arguments that involve making an arbitrary choice are instead defining functions, or involve generalized elements, or reasoning using dependent type theory.

For example, consider the following proof that every vector space $V$ has a basis:

Choose a well-ordering of $V$. Let $B$ to be the set of all elements of $V$ that cannot be written as a linear combination of smaller elements. .... Therefore $B$ is a basis.

This argument can instead be construed as defining a function from the set of well-orderings of $V$ to the set of basis for $V$.

Sometimes, this point of view is so natural that it changes how you even think about the subject; e.g. when doing finite dimensional linear algebra, when I see the words "basis of a vector space $V$", I usually read that as "isomorphism $\mathbb{R}^n \to V$". (admittedly, I made this shift in POV before I learned any thing else I described above)

Answer 6

Yes, this framework is called category theory.

Let's indeed start with the example of vector spaces. What you do is you say that some operations are natural. These operations should make sense not only for the space itself, but also for any map between two vector spaces.

Here's an example: the "top power" $\bigwedge^{\mathrm{top}}$ of finite-dimensional vector space $V$ is the one-dimensional space $$V\wedge V\wedge \dots \wedge V$$ (where the wedge operation is taken with $\dim V$ copies of $V$.) This is a natural operation, because if you take a map $V\to W$ then there's a natural map $\bigwedge^{\mathrm{top}}V\to \bigwedge^{\mathrm{top}}W$ (given by determinant).

This disallows the arbitrary choice in the following way: if the operation is natural, you're not allowed to pick a distinguished element to construct it, because if you do, you will break the property for a map of a space into itself that changes distinguished element.

The $V$ and $V^* $ example also fits here, though with a slight twist: for any map $V\to W$ there is a dual map that goes from $W^ * \to V^ * $ (this will be a contravariant operation in contrast to a covariant operation above).

Starting from this observation, category theory proceeds to learn a lot about the general properties that categories (of which vector spaces is the first example) and natural operations (explained above) might have. It's a big and vibrant area of math represented here under the tag category-theory.

There are many good introductions, the standard one is

Categories for the Working Mathematician by Mac Lane (Springer Amazon)

Answer 7

There is quasi-set theory in which the elements are indistinguishable. See

http://en.wikipedia.org/wiki/Quasi-set_theory

Answer 8

Look at the paper Choiceless Computation and Symmetry of Benjamin Rossman. It looks like that your intuition towards the "right answer" was correct. The main result of the paper is about dual vector spaces.

From the abstract:

... we show that there is an isomorphism-invariant polynomial-time computable function problem on finite vector spaces (“given a finite vector space V , output the set of hyperplanes in V”) that is not computable by any CPT+C program.