# [FOM] A proof that cannot be formalized in ZFC

Richard Heck rgheck at brown.edu
Wed Oct 10 14:12:46 EDT 2007

```Timothy Y. Chow wrote:
> Finnur Larusson <finnur.larusson at adelaide.edu.au> 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
>> consistent.
>>
>> 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.  By translating this proof
>> from the formal language of ZFC into English (that is, by applying
>> the standard interpretation), we get a proof -- a mathematical proof
>> in the everyday sense -- that ZFC has no model, contrary to the
>> assumption that ZFC is consistent.
>>
> In order to deduce "ZFC is inconsistent" from "ZFC |- ~con(ZFC)" one needs
> something more than the consistency of ZFC, e.g., that ZFC has an
> omega-model (i.e., a model in which the integers are the standard
> integers).
>
Or, more directly, what you need is reflection for ZFC: Bew_{ZFC}(A) -->
A. And that of course is not available in ZFC, by L"ob's theorem.

Richard

```