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.