[mr_gibbins]

I like Bill Wadge's stuff and this is a great explanation of the axiom of choice. I spent a fair bit of time on ZF set theory + AC working in databases, and AC is essential for data-driven set-theory to function.

Bit confused about the unit sphere explanation but then again I'm unfamiliar with the underlying paper.

[zomglings]

I'm confused why you would need the Axiom of Choice when working with computable programs.

Unless you were proving theorems about possible contents of a database? But even that seems like you wouldn't need the Axiom of Choice.

Could you elaborate on what you were doing with ZFC with databases?

[mr_gibbins]

Not to cop out but a HN reply isn't the best place to provide a full explanation. Suffice to say I use the ZF axioms as a basis to teach how sets both differ from and are similar to tables, particularly using the more accessible parts of Stoll's textbook on axiomatic set theory. To give a single example, the axiom schema of replacement is a good analogy for how the output of a SELECT command over a set will also result in a set.

In terms of AC, the comment below about how this is actually the AFC is correct, since the sets I am talking about are finite. Of course, set projections or selections are arguably choice functions themselves, which makes them relevant, and ZFC includes AC in order to infer well-orderedness, which tables (after all, collections of sets) can indeed be.

[algon33]

By database do you mean a finite 2d array with column headings? Or something that can be represented by such an object? And its entries are elements of some countable sets? If so, what are you doing using ZFC there?

[mr_gibbins]

Thanks - see comment above.

[lupire]

That's the Axiom of Finite Choice, not the full Axiom of Choice.

https://en.m.wikipedia.org/wiki/Axiom_of_finite_choice

[mr_gibbins]

Yes - you are correct :)