[FOM] The boundary of objective mathematics

[Paul Budnik]

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.

Paul Budnik
www.mtnmath.com