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

Timothy Y. Chow tchow at alum.mit.edu
Sun Oct 7 14:12:37 EDT 2007

```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).

To put it another way, why should we "believe" a statement just because
there's a ZFC-proof of it?  It's clear that if ZFC is inconsistent, then
we *won't* "believe" ZFC-proofs.  What's slightly more subtle is that the
mere consistency of ZFC isn't quite enough to get us to believe
arithmetical theorems of ZFC; we must also believe that these arithmetical
theorems are asserting something about the standard naturals.  It is
"conceivable" that ZFC might be consistent but that the only models it has
are those in which the integers are nonstandard, in which case we might
not "believe" an arithmetical statement such as "ZFC is inconsistent" even
if there is a ZFC-proof of it.

So you need to replace your initial statement that "we assume throughout
that ZFC is consistent" to "we assume throughout that ZFC has an

Tim
```