Isn't the axiom of determinacy inconsistent with ZF? What am I overlooking?

Question

I'm sure there's something I'm missing here; probably a naive confusion of mathematics with metamathematics. Regardless, I've come up with what looks to me like a proof that (first-order) ZF+AD is inconsistent:

Assume otherwise. Then it cannot be shown that ZF+AD is consistent relative to ZF. However, ZFC is consistent relative to ZF, and as ZF+AD is consistent (by our assumption for contradiction,) a model of ZF+AD exists in ZFC by Gödel's completeness theorem. Hence ZF+AD is consistent relative to ZFC. This establishes that ZF+AD is consistent relative to ZF, a contradiction.

I'd appreciate anyone pointing out the problematic step(s).

EDIT: Upon further thought, under the (misguided) assumption that this argument holds, an adaption of this argument can be used to show that every first-order countable theory has a countable model in ZF: ZFC has a model in ZF (I think this was shown by Cohen via forcing?) and such a theory has a model in ZFC by the first incompleteness theorem. "Composing" these models gives us a model of the theory in ZF.

Answer 1

All of this is problematic. You claim that the theory is inconsistent. Okay. So by contradiction it is not inconsistent, therefore the working assumption is that the theory is consistent.

But a theory being consistent does not mean consistent relative to $\sf ZF$. it means consistent. Moreover the fact there is a model of $T$ in a universe of $T'$ is not a contradiction. It's a set model, it's a toy model. It's not saying what is true or false in the universe. Finally, you conclude that there is a model which is a contradiction, but the working assumption towards contradiction was that there is a model in the first place!

For the second part, forcing cannot increase the consistency strength. This means that it cannot generate models out of nowhere without additional assumptions. In particular forcing requires us to assume the consistency of $\sf ZFC$, rather than proving it. And since we already assume there are models of $\sf ZFC$ nothing wrong in using them.

I'd just like to add that the completeness theorem does require some choice to be proved, but for countable theories it can be avoided.

Answer 2

What Asaf Karagila says in the second paragraph of his answer is basically what you are overlooking in your argument. Namely, it is implied in your argument that the statement $''\text{Con}(ZF+AD)\implies ZFC\vdash\text{Con}(ZF+AD)''$ is true in the meta-theory. But this is not necessarily true. What is true in the meta-theory is that $''\varphi\implies ZFC\vdash\varphi''$ whenever $\varphi$ is a $\Sigma_1$ sentence. However, since $\text{Con}(ZF+AD)$ is a $\Pi_1$ sentence, then this fact doesn't apply. (By ''true'' I actually mean ''meta-theorem'' ).

So your conclusion that "a model of $ZF+AD$ exists in $ZFC$ by Gödel's completeness theorem" must actually be rephrased to "a model of $ZF+AD$ exists in $ZFC+\text{Con}(ZF+AD)$ by Gödel's completeness theorem". But this fact (along with the other facts you are using) isn't enough to establish the contradiction you are looking for.

Also, the method of forcing does not produce a set model for (all of) $ZFC$ from within $ZFC$. So we are not justified in inferring $''ZFC\vdash\text{Con}(ZFC)''$ by appealing solely to forcing results and Gödel's completeness theorem. ​

Answer 3

In the second line of your second paragraph, you assume the statement $Con(ZF+AD)$ and then get a set model of $ZF+AD$ by Gödel's completeness theorem (in $ZFC$ or $ZF$, as our meta theory). Then, you claim that $ZF+AD$ is consistent relative to $ZFC$. Why would the statement $Con(ZFC) \rightarrow Con(ZF+AD)$ follow? Your assumption to get the model of $ZF+AD$ was the statement $Con(ZF+AD)$ itself and it does not follow from $Con(ZFC)$ alone.