[FOM] The Natural Language Thesis and Formalization

[Steven Gubkin]

Note: I use E for the existential quantifier.

As an example of a case where the standard "translation" of a true 
theorem of ZFC is actually false, consider the following. Let's 
formulate the natural numbers this way 0={ }, 1= {0}, 2= {1}, ... , 
n+1=
{n}. Let Nat(x) be the formula of ZFC expressing the fact that x 
is a natural number. Let's also agree to take the standard formulation 
of functions, i.e. a function is a set of ordered pairs where no two 
distinct ordered pairs have the same abscissa. The ordered pair <x,y>=
{{x},{x,y}}. Let Func(x) be the formula of ZFC expressing the fact 
that x is a function. Then the formula Ex [Nat(x) & Func(x)] 
is provable in ZFC. In fact 0 and 3 both satisfy this formula. 0 is 
the 
empty set, and so is also the empty set of ordered pairs, and thus 
a function. 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. Thus proving Ex A(x) is true 
in ZFC for some formula A does not guarantee that there really is 
something satisfying the "translation of A into English". 
This sort of difficulty might be due to the particulars of ZFC (in 
particular a 
global, as opposed to local, membership relation), but I am guessing 
that the problem will extend to first order foundational systems in 
general. Sorting out exactly which theorems "translate faithfully" 
seems like a huge problem. Does anyone have any insight on this?

Perplexedly,
Steven Gubkin :)