# [FOM] The Natural Language Thesis and Formalization

Timothy Y. Chow tchow at alum.mit.edu
Sat Jan 26 12:32:52 EST 2008

```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
```