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})$?
$\begingroup$
$\endgroup$
4
-
2$\begingroup$ You have to draw the distinction between a theory $T$ proving $T\vdash p$ and $T$ proving $p$, i.e. $T\vdash p$ being true. A theory that proves something that's false need only be $\omega$-inconsistent, and need not be inconsistent. $\endgroup$– J.G.Sep 20 at 21:12
-
$\begingroup$ I think a better formulation of "if $\mathsf{ZFC}$ is not consistent, then $\mathsf{ZFC}$ proves everything" might be "$\mathsf{ZFC} \vdash \text{''}\lnot \mathsf{Con}(\mathsf{ZFC}) \implies \forall p, \mathsf{ZFC} \vdash p\text{''}$". Everything inside the $\text{''}$ quotes is an actual sentence in the language of $\mathsf{ZFC}$, which talks about strings of symbols and syntactic entailment and so on. It's confusing because of the seeming self-reference! If you actually sit down to try and prove what you've written in detail, you will hopefully struggle. $\endgroup$– Izaak van DongenSep 20 at 21:15
-
1$\begingroup$ It's true (but subtle) that for any formula $p$ in the meta-theory, we have $\mathsf{ZFC} + \lnot \mathsf{Con}(\mathsf{ZFC}) \vdash \text{''} \mathsf{ZFC} \vdash p \text{''}$. However it doesn't follow from this that $\mathsf{ZFC} + \lnot \mathsf{Con}(\mathsf{ZFC}) \vdash \text{''} p \text{''}$. The problem is the nonstandard proofs that spaceisdarkgreen talks about! $\endgroup$– Izaak van DongenSep 20 at 21:23
-
$\begingroup$ Thanks to both of you for the comments! $\endgroup$– Jianing SongSep 20 at 22:53
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
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.
answered Sep 20 at 21:15
-
$\begingroup$ Thanks! I think my problem is the misunderstanding of what it means by a proof. You meant that, since the proof of $p$ from $\mathsf{ZFC}$ relies on $\neg\mathsf{Con}(\mathsf{ZFC})$, we cannot construct a proof of $p$ from $\mathsf{ZFC}+\neg\mathsf{Con}(\mathsf{ZFC})$ without the assuption $\neg\mathsf{Con}(\mathsf{ZFC})$. Have I got it correctly? $\endgroup$ Sep 20 at 22:52
-
$\begingroup$ @JianingSong We need to distinguish carefully between levels. There are actual proofs from a theory $T$ in the real world, and there are statements about proofs that we have coded into the same formal language $T$ is written in. We are considering "if $\sf ZFC$ is inconsistent, then it proves everything" in this latter sense. This can be proved, in the real world and in $\sf ZFC$ (or weaker systems). So the system $\sf ZFC + \lnot Con(ZFC)$ proves "$\sf ZFC$ proves everything". But that doesn't mean $\sf ZFC$ actually proves everything... $\sf ZFC + \lnot Con(ZFC)$ is just wrong. $\endgroup$ Sep 20 at 23:30
-
$\begingroup$ @JianingSong The theory $\sf ZFC + \lnot Con(ZFC)$ proves the incorrect statement "$\sf ZFC$ proves everything" because we baked into it the incorrect assumption that $\sf ZFC$ is inconsistent. But proving incorrect statements is not the same as proving an inconsistency. And the incompleteness theorem tells us that this theory will not actually prove any inconsistencies (if it is indeed true in the real world, as we've been assuming, that $\sf ZFC$ is consistent.) $\endgroup$ Sep 20 at 23:39
-
$\begingroup$ That makes things clear. Thanks for your detailed explanation! $\endgroup$ Sep 22 at 14:27