[FOM] A proof that cannot be formalized in ZFC

[Richard Heck]

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