The mistake you are making is assuming that “ZFC is consistent” = Consistent(ZFC) where the ladder is the Godel encoding for “ZFC is consistent” specified within the language of ZFC.
If your logic were valid, it would just as well break the entirety of the second incompleteness theorem. That is, you would say “well of course ZFC can prove Consistent(ZFC) if it is consistent, for either ZFC is consistent, and we’re done, or ZFC is not consistent, but that is a contradiction since ‘ZFC is consistent’ ⇒ Consistent(ZFC)”.
The fact is that ZFC itself cannot recognize that Consistent(ZFC) is equivalent to “ZFC is consistent”.
@Morpheus you too seem confused by this, so tagging you as well.
Completeness theorem states that consistent countable FO theory has a model. Compactness theorem states that FO theory has a model iff every finite subset of FO theory has a model. Both theorems are provable in ZFC.
Therefore:
Consistent(ZFC) <-> all finite subsets of ZFC have a model ->
not Consistent(ZFC) <-> some finite subsets of ZFC don’t have a model ->
some finite subsets of ZFC + not Consistent(ZFC) don’t have a model <->
The mistake you are making is assuming that “ZFC is consistent” =
Consistent(ZFC)where the ladder is the Godel encoding for “ZFC is consistent” specified within the language of ZFC.If your logic were valid, it would just as well break the entirety of the second incompleteness theorem. That is, you would say “well of course ZFC can prove Consistent(ZFC) if it is consistent, for either ZFC is consistent, and we’re done, or ZFC is not consistent, but that is a contradiction since ‘ZFC is consistent’ ⇒
Consistent(ZFC)”.The fact is that ZFC itself cannot recognize that
Consistent(ZFC)is equivalent to “ZFC is consistent”.@Morpheus you too seem confused by this, so tagging you as well.
Completeness theorem states that consistent countable FO theory has a model. Compactness theorem states that FO theory has a model iff every finite subset of FO theory has a model. Both theorems are provable in ZFC.
Therefore:
Consistent(ZFC) <-> all finite subsets of ZFC have a model ->
not Consistent(ZFC) <-> some finite subsets of ZFC don’t have a model ->
some finite subsets of ZFC + not Consistent(ZFC) don’t have a model <->
not Consistent(ZFC + not Consistent(ZFC)),
proven in ZFC + not Consistent(ZFC)