[FOM] A proof that cannot be formalized in ZFC

[Marcin Mostowski]

Firstly, by the 2nd Goedel Theorem (2GT) you cannot infer existence of a 
model for ZF inside ZF assuming consistency of ZF. AC adds nothing, so I 
consider ZF instead of ZFC. Therefore your claim 1 should be formulated as a 
theorem of ZFC as follows: 

If con(ZF) then con(ZF+con(ZF)). 

Assuming consistency of ZF this claim cannot be justified so easily because 
the theory ZF+con(ZF) is essentially stronger than ZF by 2GT. Take T being 
ZF+(not con(ZF)) instead of ZF in your reasoning. con(T) holds provided 
con(ZF) holds (everything inside ZF), but con(T+con(T)) is false. 

 From the assumption that not con(ZFC+con(ZFC)) you can infer only (again in 
ZFC) the following: 

D: there is a proof d such that d is ZF-proof for not Con(ZF) 

Or equivalently (by the completeness theorem inside ZF) 

D.: for each ZF-model M, Con(ZF) is false in M (this sentence should be 
understood as ZF-statement). 

The sentence D does not contradict to con(ZF). The proof d would be a 
nonstandard finite object . in this case it would not be translated into 
real proof. 

Your last philosophical remark that the common belief that all mathematics 
can be formalized in ZFC is false is trivially true. In this sense that some 
interesting mathematical sentences cannot be decided inside ZFC. The 
simplest example is con(ZFC). Moreover this is true about any reasonable 
axiomatic theory. This common belief is popular between some mathematicians 
who are not interested in such foundational questions. However even 
neglecting logic .all. in the belief declaration cannot be understood 
literally. 

 


Finnur Larusson napisał(a): 

> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
 


_____________________ 

Marcin Mostowski
Department of Logic
Institute of Philosophy
Warsaw University