[FOM] A proof that cannot be formalized in ZFC
blumal at mail.biu.ac.il
Mon Oct 8 12:12:41 EDT 2007
Finnur Larusson wrote:
>Let con(ZFC) be a sentence in ZFC asserting that ZFC has a model.
>Let S be the theory ZFC+con(ZFC). Let con(S) be a sentence in S (or
>ZFC) asserting that S has a model. We assume throughout that ZFC is
>Claim 1. S is consistent.
>Proof. Assume S is inconsistent, that is, has no model. This means
>that there is no model of ZFC in which con(ZFC) is true, so the
>negation of con(ZFC) has a proof in ZFC.
Why does it follow that if there is no model of ZFC in which con(ZFC) is
true that the negation of con(ZFC) has a proof in ZFC?
Doesn't this assume that ZFC is complete?
More information about the FOM