[FOM] Formalization Thesis: A second attempt

[Paul Budnik]

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:
>>
>> 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.

Paul Budnik
www.mtnmath.com