[Date Prev][Date Next][Thread Prev][Thread Next]
[Date Index]
[Thread Index]
[Author Index]
Some thoughts on formalization
- From: Tim Gwinn <***>
- Date: Sun, 21 Aug 2005 13:02:30 -0400
Some of my
thoughts on the discussions earlier this month about Rosen's mentions of
formalization, Gödel, etc. I hope I have done
my research adequately. Apologies for the length. See references at the end of
the post.
--------------------------
I think it is
useful to keep in mind two things. One is the central role of the
modelling relation. The other is the perspective that the language of
mathematics is part of natural language: "I have argued above that mathematics,
in the [broadest] sense, is the study of formalisms and that formalisms, in
their turn, are parts of natural language whose inferential or entailment
structures are defined in purely syntactic terms."[LI p. 49-50] It also has
to be remembered that classical mathematics [to use Kleene's term] did not arise
historically by first creating a fixed axiomatic foundation, from which all
of classical mathematics was generated over time. Instead, a concern
for foundations came after the fact, much of it only in the 19th-20th
century.
One of Rosen's
interests is in exploring the Cartesian machine metaphor and the limits it
places on science if the machine metaphor is assumed as valid with respect to
organisms specifically, as well as the laws of physics generally; specifically,
the limits such an assumption places on the class of mathematical models of
a natural system. To define the machine metaphor more rigorously, Rosen in LI
uses the notions of simulability, algorithm, and mathematical machine to clearly
define the class of 'mechanisms' - and the sub-class of 'machines'
- by specifying conditions on the kinds of formal models each of those
classes possesses (see LI). These models, among other things, must all be
computable, in the Turing sense - they are "effectively calculable". The
question remains: are these classes of formal models comprehensive enough
for describing natural systems, such as organisms, or do they place inordinate
a priori limitions on formal descriptions of those natural
systems?
One way to
investigate that question about formal models is to examine an analogous
situation contained entirely in the formal world: mathematics. As it turns out,
Hilbert's formalist program exemplified this situation in question. In Rosennean
terms, the idea was to create a commuting modelling relation between classical
mathematics (or some significant portion of it) and a fully-syntactic,
computable model of that system. As Rosen says:
"The first thing
to bear in mind is that both Number Theory and any formalization of it are
both systems of entailment. It is the relation between them, or more
specifically, the extent of to which these schemes of entailment can be
brought into congruence, that is of primary interest. The establishment of
such congruences, through the positing of referents in one of them for
elements of the other, is the essence of the modeling relation, which
I have discussed at great length elsewhere." [LI p. 8, ital.
orig.]
The model was to
contain only meaningless (i.e., semantic-free) symbols manipulated by mechanical
rules. This is the formalization to which Rosen refers, and adheres
precisely to the description of formalization Rosen cited from Kleene1952 [sec.
15] in LI p.6-7 and EL p.91-92. Simpson describes the formalist program
similarly to Kleene (keep in mind while reading this, the Cartesian machine
metaphor which was the subject of Rosen's inquiry as well as the chapter
on the Newtonian formalism in LI):
"According to formalism, mathematics is only a formal game,
concerned solely with algorithmic manipulation of symbols. Under this view,
the symbols of the predicate calculus do not denote predicates or anything
else. They are merely marks on paper, or bits and bytes in the memory of a
computer. Therefore, mathematics cannot claim to be any sort of knowledge of
mathematical objects. Indeed, mathematical objects do not exist at all, and
the profound questions debated by Plato and Aristotle become moot. Mathematics
is nothing but a kind of blind calculation. " [Simpson1999]
The stipulating of
symbol manipulation by mechanical finitary methods means that these
processes are effectively calculable. By Church's Thesis, processes which
are effectively calculable are l-definable, or
equivalently, Turing-computable. Thus, we have a situation where we
can investigate the ability of such a model to be in a commuting modelling
relation with some portion of classical mathematics, and learn if such a
formalization imposes any serious restrictions which would
have counterpart restrictions in utilizing only computable models in
science.
The value in
such a program for mathematics would be that if it could be accomplished, then
it would no longer be necessary to retain classical mathematics - it could be
replaced with the formalization itself and the clarity and certitude which
its syntactic, mechanical, finitary methods would provide.
As we know
historically, this modelling relation did not successfully commute with much of
mathematics. See, for example, Simpson's concise description of the
Hilbert program [Simpson1986]:
Hintikka notes
the inevitable fate of the program in this way:
"Again, Hilbert
could not have conceived of his famous project of proving semantical
(model-theoretical) consistency of mathematical theories by establishing their
proof-theoretic [i.e., formalized - TG] consistency, if he had realized that
the true logic he needed in those theories would not have a complete
proof-theoretical axiomatization." [Hintikka1996, p.
90]
In order for such
a formalization to not run afoul of Gödel's Incompleteness theorems, it is therefore
required that the formalization must forsake much of its power and thereby
be a formalization of only a much smaller and weaker fragment of classical
mathematics. This is the sense in which Rosen states:
"Basically, he
[Gödel] showed that, no matter how one tries
to formalize a particular part of mathematics (Number Theory, perhaps the
innermost heart of mathematics itself), syntactic truth in the formalization
does not coincide with (is narrower than) the set of truths about numbers."
[LI p.7]
To be very clear,
in saying "(is narrower than) the set of truths about numbers", Rosen is
not asserting that "truths about numbers" refers to some kind of absolute
or Platonic sense of truth. Instead, it is a reference to "truth about numbers"
in the original system attempting to be formalized, namely, classical
mathematics. As he stresses, "...one cannot forget that Number Theory is
about numbers. The fact that Number Theory is about numbers is essential,
because there are percepts or qualities (theorems) pertaining to number that
cannot be expressed in terms of a given, preassigned set of purely syntactic
entailments." [LI p. 8, ital. orig.]
As stated in
Simpson1986, "Tait argues convincingly that Hilbert's finitism is captured by
the formal system PRA of primitive recursive arithmetic". Primitive
recursive functions constitute a sub-class of the class of partial
recursive functions - those functions which are Turing computable. How generic
are these functions? As Kleene states it:
"It should have been apparent that
there must be uncomputable number-theoretic functions, as soon as we met the
Church-Turing thesis in [sec. 41], by which the set of different possible
machines is countably infinite because each machine is describable by a finite
table in a fixed symbolism (cf.[sec. 32]). The set of machines is countable,
while the set of all the number-theoretic functions is uncountable."
[Kleene1967, p. 246]
(More
specifically, there are aleph-zero partial recursive (computable) functions,
whereas there are 2^aleph-zero functions which are not recursive; the former is
a countable infinity, the latter an uncountable finity. See Rogers1967, p.22)
Thus, formalizations of this nature are inherently limited to encompassing an
infinitesimal portion of the whole of number-theoretic functions. I think (and
this is a bit of speculation on my part) this is the sense in which Rosen
is not merely being dramatic, but is being factual when he makes statements
like:
"The status of
these formalizations is informative. They turn out to be infinitely feeble
compared with the original mathematical systems they attempted to objectivize.
Indeed, these attempts to secure mathematics from paradox by invoking
constructibility, or formalizability, ends up losing most of it." [EL
p.92]
At the very least,
however, it is also clear, from Rosen's arguments about model of complex systems
in LI, that from the modelling relation perspective, it would take an infinite
number of simple models (i.e., formalizations) to capture the entire complex
system (i.e., classical mathematics, or even only Number Theory). In this sense,
too, it is entirely factual to say that each individual formalization (or
any finite collection of them, for that matter) captures only an infinitesimal
portion of the original system.
Now, on to PA
and ZFC. It is an uncontroversial remark to say that neither PA or ZFC are
completely formalizable in the sense used above. Although they are sometimes
described as "formalizations" of mathematics, this is not at all the same
sense of the word. Rosen always refer specifically to the Hilbert (formalist)
sense of the word 'formalization'. In Rosennean terms, to model classical
mathematics with axiomatic systems such as PA or ZFC is to model one complex
system with another complex system. This has intrinsic interest, to be sure,
however it does not bear at all on the question Rosen was interested in,
because it no longer meets the criteria of being an analogue of the Cartesian
machine metaphor as made rigorous by Rosen. Therefore, what they (i.e., PA, ZFC,
or the like) can capture of classical mathematics is entirely besides the point.
To summarize,
I do not think that Rosen has made any comments with respect to this topic
which are either misleading or not factual. Nor do his comments seem to me to be
at all controversial.
Regards,
Tim
[Hintikka1996]
The Principles of
Mathematics Revisited. Jaako Hintikka. 1996, Cambridge.
[Kleene1952]
Introduction to
Metamathematics. S.C. Kleene. 1952, North-Holland.
[Kleene1967]
Mathematical
Logic. S.C. Kleene. 1967, Dover.
[Rogers1967]
Theory of
Recursive Functions and Effective Computability. Hartley Rogers. 1967,
McGraw-Hill.
[Simpson1986]
Partial
Realizations of Hilbert's Program. Stephen Simpson. Published in 1988,
Journal of Symbolic Logic.
[Simpson1999]
Logic and
Mathematics
See
also:
--------------------------------------