[FOM] The Natural Language Thesis and Formalization

[messing]

Steven Gubkin wrote:

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


Concerning Steven Gubkin's "perplexity" about can whether the statement
Ex(Natx) & Func(x)), I think a simple resolution is to adopt the point 
of view that a function f is, by definition, an ordered triple <A,B,G> 
where G is the graph of f, that is Gubkin's set of ordered pairs 
definition and A is the source and B is the target of f.  This 
eliminates the possibility that either 0 or 3 is a function.    For 
example 0 is not a function.  The ordered triple <0,0,0> is by 
definition <<0.0>,0>.  As <0,0> is {{0}, {0,0}} = 2, <0.0,0> = <2,0> =
{{2},{2,0}} = {3,{2,0}} which is visibly not a natural number under 
Gubkin's definition. I do not maintain that translations from formal ZFC 
statements to English language statements and conversely will never lead 
to perplexity, but I tend to doubt it.

William Messing