Timothy Y. Chow
tchow at alum.mit.edu
Sat Jan 28 10:24:04 EST 2006
Harvey Friedman wrote:
> One can attempt to formally justify the constant and pervasive use by
> taking some major Journals and textbooks, and counting up the number of
> uses, or counting up the number of implied uses, and comparing these
> numbers to the numbers for concepts that seem relatively specialized.
> Or at a meeting of mathematicians, or of people in a field of
> mathematics, what concepts can be named without any obligation on the
> part of the speaker to give their definition?
Surveying actual mathematical practice to get the right framework is
certainly a necessary step in trying to formalize "naturalness."
However, once this is done, it is not clear to me that measuring some
"stand-alone" property like length is going to do such a great job of
capturing naturalness. I would incline towards modeling the space of
mathematical statements as something like a graph, with vertices being
known theorems and conjectures, and edges representing "similarity" or
"relatedness" or some such. Then a statement would be natural if it has
high degree and is near the center of a giant connected component, or
something like that.
In other words, a statement is likely to be natural if it is similar to
many other statements that have been considered before, and/or if it is
conceptually linked with many other natural statements. In contrast, a
statement that is easily stated but has a strange form and is not related
to other known statements is probably unnatural.
The vaguest part of my picture is the notion of edges representing
"similarity" or "relatedness." What does this mean? I have some hope
that this question might answer itself, in the following way. As more and
more mathematics is strictly formalized and proved (a la Mizar, QED,
etc.), people will not only be interested in the "hierarchical" structure
that allows you to unravel the proof of a given statement, they will also
be interested in searching the database for (for example) information that
is relevant to their new conjecture. The mathematical community will then
be forced to figure out the correct definition of "relatedness" that will
cause the search engine to provide the right search results. These will
of course include "simple" matching of keywords and statement format, but
will also hopefully make use of elementary logical transformations, as
well as the graph-theoretic structure of the database itself.
It seems that this sort of web-like structure of mathematics captures the
way mathematicians think about their subject better than the hierarchical
structure that captures the structure of their proofs, but I'd better not
say more lest I join David Corfield as the target of flaming.
More information about the FOM