[FOM] The Natural Language Thesis and Formalization

Steven Gubkin steven.gubkin at case.edu
Wed Jan 23 12:35:45 EST 2008

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 :)