[FOM] The boundary of objective mathematics
paul at mtnmath.com
Sat Mar 14 11:49:37 EDT 2009
joeshipman at aol.com wrote:
> The practical attitude many mathematicians seem to take is that
> statements in the first-order language of arithmetic OR statements of
> higher type which have arithmetical consequences are meaningful. ...
As a practical matter I agree that arithmetical conclusions reached in
this way are probably correct and thus the statements are meaningful in
having useful consequences. However I do not think you can conclude a
statement is objective from its implications. It is possible to
construct different theories that have the same arithmetical
consequences. The objectivity of a statement depends on the assumptions
that lead to it and not the conclusions it leads to.
I think we need a different formulation for the foundations of
mathematics that explicitly and internally recognizes the unavoidable
limitations of any formal system. In the light of the Lowenheim Skolem
theorem, I think Cantor's proof that the reals are not countable should
be thought of as the first major incompleteness theorem. Reals are human
constructions and Cantor proved one can always construct more of them
and not that there exist more reals than integers.
> My own view is that any statement about sets of bounded rank is
> meaningful, and that statements like GCH which involve universal
> quantification for sets of arbitrary rank are vague. ...
I suspect all of ZFC and many of its proposed extensions have an
interpretation in terms of properties of recursive processes in a
potentially infinite universe. I think all of the implications of
systems that have such an interpretation are meaningful and they are
objective in that interpretation, but not objective as formulated in
ZFC. Figuring out this interpretation is extremely difficult beyond a
certain point. It almost certainly requires computer aided proofs and a
somewhat different approach to developing mathematics. However every
finite formal system is a computer program for enumerating theorems and
one can in theory come to a deep understanding of the combinatorial
implications of a relatively short computer program like the axioms of ZFC.
More information about the FOM