Cfrgtkky

I know that the axiom of choice (AC)

For any set $X$ of nonempty sets, there exists a choice function defined on $X$.

is independent of ZF. Can one give an explicit example of such a set $X$ so that we have this independence?

Depending on what exactly you mean by "explicit example," we can do this.

The situation is simpler with respect to the well-ordering principle, which after all is equivalent to the axiom of choice: it is consistent with ZF that $mathbb{R}$ cannot be well-ordered.

To translate this into a concrete example of a possible failure of the axiom of choice, we can look at the proof that the axiom of choice implies the well-ordering principle: all we need to do in order to well-order $mathbb{R}$ is have a way to, given $Asubsetneqmathbb{R}$, pick some $ainmathbb{R}setminus A$, and so this means that the family $$(mathbb{R}setminus A)_{Asubsetneqmathbb{R}}$$ consistently has no choice function.

Of course, a snappier way to say this is that consistently the family of nonempty (as opposed to proper) subsets of $mathbb{R}$ does not have a choice function - we just switch from $A$ to $mathbb{R}setminus A$ - but the formulation above makes the connection with the well-orderability of $mathbb{R}$ clearer.

Now there are many subtleties around this. I'll mention just one (looking at the well-ordering principle instead of choice, just for simplicity):

Since $mathbb{R}$ is consistently non-well-orderable, there is no formula $varphi$ in the language of set theory which ZF proves is a well-ordering of $mathbb{R}$. However, this does notmean that there can be no definable well-ordering of $mathbb{R}$! There are many formulas which consistently define well-orderings of $mathbb{R}$, chiefly among them the following:

$rtriangleleft s$ iff $r$ precedes $s$ in the canonical well-ordering of $L$.

Here $L$ is Godel's constructible universe, which has a definable (class) well-ordering (if you prefer to avoid proper classes, you can just look at $L_{omega_1}$ since $mathbb{R}cap L=mathbb{R}cap L_{omega_1}$).

We can, however, do even snappier. It is disturbingly possible for everything to be definable: that is, there are models $Mmodels$ ZF such that every element of $M$ is definable in $M$ without parameters. In this case, the usual lexicographic well-ordering on the set of formulas in the language of set theory yields a well-ordering of the whole model, which restricts to a well-ordering of $mathbb{R}$ (or rather, what the model thinks is $mathbb{R}$). I mention this because it's a good example of just how subtle the situation can be, and starts to indicate why the "explicit example" above may not be as satisfying as it first appears.

The simplest example, I guess, is the power set of the real numbers (without the real numbers).

It is consistent that there is no choice function from that set, and of course assuming choice, there is a choice function.

But there is a subtle issue here or syntactic and semantic point. Since we can add a choice function for a fixed family by forcing, or similarly we can always extend a model of ZF so there is no choice function from the sets of real numbers, we need to be careful and ask what are the sets of reals. In different models the answer would be different.

In addition to that, starting from a model of ZFC, we can make choice fail badly but keeping some initial segment of the universe well ordered (and thus admitting a choice function). So this adds even more confusion to the fire, as Henno points out in the comments, which set is not well ordered is not something that ZF itself can decide. Not even ZF with the failure of AC.