Just denying the axiom of choice doesn’t buy you much. If you’re going to throw away AC, you should add some powerful incompatible axiom in its place. The Axiom of Determinacy (AD) has been studied in this light.
Here’s one formulation. Let S be ℕℕ, i.e., the set of all infinite strings of natural numbers. Let G⊆S. Alice and Bob play a game where at step 2n, Alice chooses a number s2n, and at step 2n+1, Bob chooses a number s2n+1. If s0s1s2…∈G, Alice wins, otherwise Bob wins. We say elements of G are assigned to Alice, and elements not in G are assigned to Bob. We’ll call the infinite strings results (of the game). Rather than think of G as a set of results, think of it as a function G:S→{Alice,Bob}.
A strategy for Alice tells her how to play each move. Formally, it’s a function from the set of all number strings of finite even length to ℕ. Likewise, a strategy for Bob maps number strings of finite odd length to numbers. A game is determined if Alice or Bob has a winning strategy, i.e., if the player follows the strategy then that player will win. The Axiom of Determinacy says that each game is determined.
Interesting thing about the proof that AC → ¬AD: it’s much easier using the well-ordering theorem instead of Zorn’s lemma.
First note that there are c=ℵ0ℵ0 strategies (lumping together both Alice and Bob strategies), likewise c results. Assuming AC, well-order the strategies {Sα:α<ωc}. Here ωc is the least ordinal with cardinality c, so the set {α:α<κ} has cardinality less than c for each κ<ωc.
We construct a game G by inducting transfinitely through all the strategies, at step κ considering Sκ. Our goal is to assign some result to Alice or Bob that prevents Sκ from being a winning strategy. Say Sκ is an Alice strategy. Since we assign only one result at each step, fewer than c results have been assigned before step κ. However, there are c possible results if Alice follows Sκ, since Bob can play his numbers however he wants. So there exists a result where Alice follows Sκ but this result has not yet been assigned to either player. Assign it to Bob; this thwarts Sκ. If Sκ is a Bob strategy, just switch everything around. QED
The cardinality argument at the heart of this proof is harder to pull off with Zorn’s lemma (though possible, of course). (The exact same argument works with bit strings instead of strings of natural numbers, but for some reason AD is generally stated using ℕℕ instead of 𝒫(ℕ).)
Diagonal Argument 