[FOM] A proof that cannot be formalized in ZFC

[Alex Blum]

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  
>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. 
>
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?

Alex Blum