[FOM] The Natural Language Thesis and Formalization

[Timothy Y. Chow]

Steven Gubkin <steven.gubkin at case.edu> wrote:
> 3= {{{0}}}= {{{0},{0}}}= {{{0},{0,0}}}={<0,0>} 
> which is the function whose domain and codomain are both {0}. Is it 
> reasonable to conclude that there are natural numbers which are also 
> functions? Clearly this "result" is an artifact of the way we 
> translate concepts into (and out of) ZFC.

This is a nice observation.  I don't find it particularly perplexing 
though.  For starters, it's not so clear to me that the statement is 
false.  It's a little odd, to be sure, but is it false?  If you're 
convinced that it's false, can you prove that it's false?  I'm not sure 
how I would go about proving that no natural number is a function.

The second thing is that translating *out of* ZFC is different from 
translating *into* ZFC.  The formalization thesis as I stated it initially 
says only that for every theorem of interest we can find a formal theorem 
that expresses it, in the sense that we agree to accept the theorem as 
proved iff the formal theorem is formally proved.  It does not necessarily 
imply that every formal theorem expresses some "natural" theorem.

Having said that, I agree that in sufficiently complicated situations, we 
might find a formal proof of a formal theorem that relies in an essential 
way upon "artifacts" of the sort you mention, and then realize, a 
posteriori, that the formal theorem does not in fact correctly express our 
intent.  It is an empirical question how much of a practical concern this 
will turn out to be, as databases of formal theorems continue to grow.

Tim