# The Axiom of Choice Isn’t Always Non-Constructive

The Axiom of Choice is usually introduced as a non-constructive axiom that mathematicians used to care about but don’t really pay much attention to anymore. It’s true that mainstream mathematicians often don’t pay much attention to it, but it turns out that AC isn’t inherently non-constructive: it depends on what the base system it’s being added to is.

Furthermore, adding it may or may not effect what arithmetic statements a system can prove (that is, what statements only involving quantifiers and relations over the natural numbers).

Here’s a list of what happens to various axiomatic systems when you add AC. I’m sure it’s very incomplete, it’s just what I happen to be aware of. Hopefully there aren’t significant errors; at some point I’ll actually go through and add links for these things.

• Martin-Lof type theory: Constructive, and constructive after AC is added. AC is actually already provable in the system.
• Heyting Algebra in all finite types: Constructive, and constructive after AC is added. AC is not already provable in the system, but it doesn’t change the provable arithmetic statements
• Local set theory (or the internal logic of the free typos): Constructive, but not constructive after AC is added
• IZF: Constructive, but not constructive after AC is added
• Peano Arithmetic in all finite types: Not constructive even without AC. Adding AC does allow proving more arithmetic statements.
• ZF: Not constructive even without AC. Adding AC does not allow proving more arithmetic statements.

## 3 thoughts on “The Axiom of Choice Isn’t Always Non-Constructive”

1. I actually cannot imagine the AoC being constructive. Any chance you expand on this, for readers who don’t have the time to learn Martin-Lof type theory (etc.)?

2. Some people would say the Martin Lof “theorem of choice” is not the axiom of choice. The homotopy type theory book states a different type — which is not provable within constructive MLTT and which I believe implies LEM — as the real thing within type theory that we should think of as the axiom of choice.