[FOM] The Natural Language Thesis and Formalization
messing
messi001 at umn.edu
Fri Jan 25 06:37:16 EST 2008
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
More information about the FOM
mailing list