Is it true that "Axiom of Choice is true or Axiom of Choice is false"?

Question

Is it true that "Axiom of Choice is true or Axiom of Choice is false" in ZF with classical logic?

It looks like LEM would suffice to prove it.

Maybe I should write it as: Is it true "'Axiom of Choice' OR NOT('Axiom of Choice')"?

And for 'Axiom of Choice' I mean an expression that express the Axiom of Choice.

Edit: sorry people, I should have provide more hints about my concerns. I chose Axiom Of Choice because I know it is undecidable under ZF. I am not so interested in AC by itself but I would like to use it as an example of an undecidabe statement. AC has been a bad choice from my side, sorry. Anyway all links looks promising but I am not sure I want to go into that direction now.

To come back to my original question (that I didn't write until now, sorry), is it ok to be in a framework like ZF, being able to express "AC or ¬AC", proving that is true and at the same time knowing that AC is undecidable under ZF?

Edit: Not sure how to improve the question. The short answer to the question is "Yes.". It is just LEM when P is AC. So it is provable by LEM axiom and there is no problem.

Answer 1

Yes, we can prove (from $\mathsf{ZF}$, in classical logic) the sentence "$\mathrm{AC}\lor \lnot \mathrm{AC}$", where $\mathrm{AC}$ is the axiom of choice. This is just an instance of the tautology $P\lor \lnot P$, where $P$ is any sentence (the law of excluded middle).

There is no conflict with the fact that $\mathrm{AC}$ is independent of $\mathsf{ZF}$ (assuming $\mathsf{ZF}$ is consistent). Writing out the situation in words:

1. There are some models of $\mathsf{ZF}$ in which $\mathrm{AC}$ is false ($\mathsf{ZF}$ does not prove $\mathrm{AC}$) and some models of $\mathsf{ZF}$ in which $\mathrm{AC}$ is true ($\mathsf{ZF}$ does not prove $\lnot \mathrm{AC}$).
2. In every model of $\mathsf{ZF}$, $\mathrm{AC}$ is either true or false ($\mathsf{ZF}$ proves $\mathrm{AC}\lor\lnot \mathrm{AC}$).

An analogy with the theory of groups might help. The sentence $\varphi: \forall x\forall y\,(xy = yx)$ is true in a group $G$ if and only if $G$ is abelian. Now some groups are abelian and some are not. So $\varphi$ is independent from the theory of groups: we cannot prove $\varphi$ from the group axioms, and we cannot prove $\lnot \varphi$ from the group axioms. But we can prove $\varphi\lor \lnot \varphi$. This just means that for every group $G$, either $G$ is abelian, or $G$ is not abelian.