We know two things (two smart people told me these) :

1.) Gödel's famous Incompleteness Theorem can be established (proved) using the ZFC axiom system. In particular, there exists an undecidable statement in ZFC.

2.) you $cannot$ prove within ZFC that there exists an undecidable statement in ZFC. If you could prove that, then you could conclude that ZFC is consistent (since if it were inconsistent, it would prove everything, since anything follows from a contradiction, so your undecidable statement should have a prove). But we cannot prove from ZFC that ZFC is consistent.

Don't you think that 1. and 2. contradicts?! Something is very very fishy here. Which one is not true, 1. or 2.?

• There is a problem here of using "ZFC" to mean two different things. I can't tell if such a confusion is harmless, or if you are mistake in the same vein as Skolem's paradox. – Hurkyl Jan 26 '18 at 17:48
• "I don't understand this" vs. "There is something fishy here". Always assume that anything fishy is on you, and not on the theorem. – Asaf Karagila Jan 26 '18 at 18:45
• Have our answers cleared things up? If not, what is the remaining confusion? – Noah Schweber Mar 5 '18 at 21:54

No, there is no contradiction here. (I'm rephrasing Stella Biderman's answer above, but I think this might be slightly simpler.)

EDIT: based on your recent post, I think there is a bit of a confusion regarding what Godel actually proved; the following addresses this.

• Godel proved (among other things, but let's focus on these for now) two important statements:

• $(*)$ "If $T$ is a reasonable consistent theory, then $T$ is incomplete."

• $(**)_{PA}$ "PA is incomplete." (OK fine, he actually talked about a different system, but ignore that for now.) I'm writing this with the subscript "PA" since we can also consider $(**)_{ZFC}$ = "ZFC is incomplete," etc.

• It is often said that "Godel's incompleteness theorem is provable in PA." This is true only of $(*)$ - the proof of $(**)_{PA}$, unsurprisingly, takes place in a stronger theory, namely one which can prove the consistency of PA.

• Similarly, ZFC proves $(*)$ - and so ZFC proves in particular "If ZFC is consistent, then ZFC is incomplete" - but (assuming ZFC is consistent!) ZFC doesn't prove $(**)_{ZFC}$ since ZFC doesn't prove "ZFC is consistent."

• Indeed, Godel's second incompleteness theorem is exactly the observation that no consistent reasonable theory $T$ can prove $(**)_T$, since otherwise we'd have a contradiction.

I think this is ultimately stemming from a misphrasing of a special case of Godel's incompleteness theorem (the case when the theory is ZFC in particular). So let's go back to the precise statement of the incompleteness theorem. It states:

If $T$ is a computably axiomatizable, sufficiently strong theory which is consistent, then $T$ does not prove its own consistency.

That bolded part is going to be the key here; essentially, it means that we can't get something for free, and it prevents the contradiction you anticipate from arising.

Now ZFC does indeed prove Godel's theorem, but we need to be careful to say this precisely correctly. What ZFC proves - taking $T$=ZFC - is the following:

If ZFC is consistent, then ZFC does not prove its own consistency.

(ZFC easily proves that ZFC is computably axiomatizable and sufficiently strong, so these hypotheses aren't relevant here.)

Now ZFC further proves:

If ZFC does not prove its own consistency, then ZFC is consistent

simply because ZFC proves that if ZFC were inconsistent then ZFC would prove everything. So putting these together, ZFC proves the statement

If ZFC is consistent, then ZFC is consistent.

... Which isn't very surprising. The point is that that consistency hypothesis in the incompleteness theorem can't be avoided, so no contradiction actually appears (since the only theories which can use Godel to deduce an incompleteness in ZFC are those which already prove that ZFC is consistent).

This is a very interesting point, but can be untangled with a little more technical analysis. Godel’s incompleteness theorem (provable in ZFC) says the following:

Here is a statement $\phi$. Either $\phi$ is true but unprovable, or $ZFC$ is inconsistent. Therefore $ZFC$ is either complete or consistent, but cannot be both.

Under the further assumption (that virtually all mathematicians make) that ZFC (really a big enough subset for the Incompleteness Theorem to go through) is not inconsistent, we have an undecidable statement. However, if ZFC is inconsistent, every statement is decidable. Since we believe that ZFC is consistent (or, enough of it is), it follows that we believe that we cannot prove $\phi$. But that’s different from saying ZFC proves that we can’t prove $\phi$.

In short, you have an excellent objection, brought on by your friend’s loose speaking.

NB: I say “a big enough subset for the Incompleteness Theorem to go through” because ZFC is far more powerful than what is necessary for the theorem to be proven. In particular, the Axiom of Choice (by far the most contentious axiom) is entirely extraneous. It’s a little difficult to be precise about what the axiomatic system needs, but any system that can “do arithmetic,” that is, that can prove the usual properties of $+,\cdot,$ and exponentiation for the integers is almost certainly enough. There are definitively ZFC skeptics, but there are very few skeptics of the minimal axiomatic requirements to prove the Incompleteness Theorem.