[FOM] A proof that cannot be formalized in ZFC

[Finnur Larusson]

Dear FOM members,

I am a mathematician with a layman's interest in logic and  
foundations.  I would be grateful if someone who knows more than I do  
would tell me whether the following remarks make sense -- or have I  
perhaps rediscovered a well-known fallacy?

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.

Claim 2.  There is no proof in ZFC that con(ZFC) implies con(S).

Proof.  By Claim 1 and Godel's Second Incompleteness Theorem applied  
to S, con(S) is unprovable in S.

Thus we seem to have a down-to-earth mathematical statement ("If ZFC  
is consistent, so is S") with a proof that, provably, cannot be  
formalized in ZFC.  This appears to contradict the common belief that  
all mathematics can be formalized in ZFC.  Is my argument correct?   
If so, it must be well known -- are there other such examples?  If  
not, where is the mistake?

Thanks and best regards,
Finnur Larusson