Confusion about the consistency of $\mathsf{ZFC}+\neg\mathsf{Con}(\mathsf{ZFC})$

Question

I know that this question may look foolish because $\mathsf{Con}(\mathsf{ZFC})$ is independent of $\mathsf{ZFC}$, but still I have some problems understanding this. "If $\mathsf{ZFC}$ is not consistent, then $\mathsf{ZFC}$ proves everything." I was very tempted to formulate this sentence as: for any given formula $p$, we have $\neg\mathsf{Con}(\mathsf{ZFC})+\mathsf{ZFC}\vdash p$ (there must be some problems here, but otherwise I don't know how to formulate it), but this would imply that $\mathsf{ZFC}+\neg\mathsf{Con}(\mathsf{ZFC})$ is inconsistent (since it proves everything). So how should I convince myself that we cannot prove the inconsistency of $\mathsf{ZFC}+\neg\mathsf{Con}(\mathsf{ZFC})$?

Answer 1

Yeah, you're mixing up the levels.

We formalize it as $$ \sf \lnot Con_{ZFC}\to \forall p\in Sentences_{LST}\; Prov_{ZFC}(p),$$ where $\sf Prov_{ZFC}$ is the same provability predicate that goes into $\sf Con_{ZFC}$, i.e. $\sf Con_{ZFC} := \lnot Prov_{ZFC}(\ulcorner 0=1\urcorner),$ or what-have-you.

Just because we are given $\sf\lnot Con_{ZFC}$ (against a $\sf ZFC$ background) does not mean we can prove everything, since this is not an actual inconsistency... it's merely a formal statement that $\sf ZFC$ can prove one. In models of $\sf ZFC+\lnot Con_{ZFC},$ the witnesses to the provability of inconsistency (and any other statement $\sf ZFC$ can't actually prove) will be nonstandard natural numbers / nonstandard hereditarily finite sets, so such a model does not contain a real proof either, and thus doesn't conflict with $\sf ZFC$ being consistent.

Also, note there's nothing particular to $\sf ZFC$ here. Everything here holds equally well for $\sf PA$ or any other first-order system in which we might formalize provability and to which the incompleteness theorem applies.