[FOM] A proof that cannot be formalized in ZFC

[Arnon Avron]

On Mon, Oct 08, 2007 at 06:12:41PM +0200, Alex Blum wrote:
> 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?

No Alex. It follows from the completeness (in another sense
of "complete") of the predicate calculus.

 In fact, all the talks here on models (using Goedel's
completeness theorem for classical FOL) are unnecessary. 
They only provide here a roundabout way to get from the inconsistency 
of of S+{A} (where A is con(ZFC)) to the derivability of the 
negation of A from S (a trivial step, valid even in 
intuitionistic logic).

 As other have already noted, the real mistake in Larusson's 
argument is in thinking that from the assumption that ZFC 
proves that it can prove a contradiction it follows that there 
is indeed such a proof of contradiction in ZFC (that 
we "can translate into Hebrew"). To justify this inference step 
it is not enough to assume that ZFC is consistent (con(ZFC)), but that
it is \Sigma_1-consistent (thus the theory obtained from
ZFC by adding to it the negation of con(ZFC) proves its
own inconsistency, even though it is actually consistent).

Arnon Avron