Suppose ZFC proves its own inconsistency
Suppose we find a proof, in ZFC, that ZFC is inconsistent. Does it follow that ZFC is inconsistent?
On the one hand, if we could infer from ZFC ~Con(ZFC) that ZFC is inconsistent, we could contrapositively infer the consistency of ZFC & Con(ZFC) from Con(ZFC); and since ZFC & Con(ZFC) obviously entails Con(ZFC), ZFC & Con(ZFC) would thereby entail its own consistency. Which it only can if it is inconsistent (Gödel's second incompleteness theorem). So it seems that we can only infer that ZFC is inconsistent from the observation that ZFC entails its own inconsistency if we presupposes that ZFC & Con(ZFC) is inconsistent.
(~Con(ZFC) says that some number encodes a ZFC-proof of 1=0. So assume ZFC is consistent but entails ~Con(ZFC). By the consistency assumption, there is no proof of 1=0 from ZFC, and no number that encodes such a proof. The number 17, for example, does not encode such a proof. Moreover, ZFC entails that the number 17 does not encode a proof of 1=0, for "encodes a (ZFC-)proof of" is representable (definable) in ZFC. Similarly for all other numbers. So for all numbers n, ZFC entails that n is not a proof of 1=0, and yet by assumption ZFC entails that some number is a proof of 1=0. So if ZFC & Con(ZFC) is inconsistent, ZFC itself is omega-inconsistent. Hence if we find a ZFC-proof for ~Con(ZFC), we can at least conclude that ZFC is omega-inconsistent (and false, of course).)
However, if we know that ZFC ~Con(ZFC), we also know that ZFC & Con(ZFC) is inconsistent. And surely we can presuppose what we know! So doesn't the above argument break down and we can after all conclude that ZFC is inconsistent?
Um, how do you get from "ZFC + Con(ZFC) is inconsistent" to "ZFC is inconsistent"?