[FOM] Formalization Thesis: A second attempt
paul at mtnmath.com
Tue May 25 11:57:14 EDT 2010
On 05/21/2010 02:11 PM, Timothy Y. Chow wrote:
> Vladimir Sazonov<vladimir.sazonov at yahoo.com> wrote:
>> But my main disagreement is with the status of your Thesis as "thesis",
>> i.e. as a kind of a neutral observation. I would prefer to replace this
>> Thesis by something relevant and stronger what explains the nature of
>> Mathematics ***is*** formalising of our thought and intuition.
That seems too general. I see mathematics as formalizing what
conclusions (theorems) are logically determined by assumptions
(axioms). From Gödel we know that 'logically determined' can never be
completely formalized. In particular, the consistency of a formal
system is logically determined by its axioms, but, if it is consistent
and can embed the primitive recursive functions, its consistency is not
deducible from those axioms.
> I want to be able to say that *any* proof of the consistency of
> mathematics that someone might come up with can be imitated in *one*
> particular system, to which Goedel's second theorem applies. Only then
> can I reach the desired conclusion that Goedel's second theorem rules out
> the possibility of a mathematical proof of the consistency of mathematics.
On page 135 of volume 1 of Gödel's Collected Works, Kleene discusses how
general Gödel's two Incompleteness Theorems are. Paraphrasing Gödel
Kleene observed that the proof depends only on two aspects of the formal
system. One must be able to model the system with primitive recursive
relationships in which symbols in the system are translated to numeric
values. One must be able to express every primitive recursive
relationship in the system. The only loopholes seem to be mathematics
too weak to embed the primitive recursive functions, a definition of
formal system that does not require proofs to be effectively computable
or a violation of Church's thesis.
The bottom line seems to me that once you have a system that includes
the primitive recursive functions, you are in the domain of
incompleteness from which there is no exit. Stronger systems can prove
the consistency of weaker ones but there is no limit to the hierarchy of
more powerful systems.
More information about the FOM