[FOM] A proof that cannot be formalized in ZFC

[Timothy Y. Chow]

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 
omega-model"; then you should see that your "paradox" dissipates.

Tim