[FOM] Mathematics ***is*** formalising of our thought and intuition

[Vladimir Sazonov]

I changed the subject to not mix things with Timothy Y. Chow's Formalization Thesis. 

See the discussion below.

-- VS


----- Original Message ----
> From: Paul Budnik <paul at mtnmath.com>
> To: tchow at alum.mit.edu; Foundations of Mathematics <fom at cs.nyu.edu>
> Sent: Tue, May 25, 2010 4:57:14 PM

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

I understand that you consider my assertion on mathematics as too general 
because I do not restrict formalisations to the form of formal first 
order logic plus some non-logical axioms (FOL + Ax). I do not see the 
need to restrict mathematical formal systems (and mathematics) in advance 
in this way. Of course, I agree that the format FOL + Ax is sufficiently 
general and corresponds well to the contemporary mathematics. 


Anyway, do you agree with such a restricted formulation? 
I could also temporary agree to restrict. 

But continuing my objections to any such restrictions for mathematics 
in general, I would ask: 
should we consider FOL as classical or intuitionistic logic? 
For any case, I would like to have even much more freedom. 
For example, we could restrict applicability of the cut rule. 
If we naturally agree that 


      any formal proof must be of a feasible length 


then such a version of FOL is much weaker than the ordinary version 
with cut. (Cut elimination theorem does not work in such a situation 
since cut elimination costs too much - is non-feasible.) So restricted 
version FOL' of FOL leads to new, unusual kind of formalisms FOL' + Ax 
which in the ordinary terms of FOL + Ax would be inconsistent. 
(In fact, I would prefer to formulate this restriction to FOL in 
somewhat different and more intuitively natural form that in terms 
of the cut rule, but not now.)
Why to exclude such formalisms? In general, how can we know in advance 
which other kinds  of formal systems we will need to consider for 
formalisation purposes? Even the First Order Language in the 
contemporary form is not compulsory. 
Thus, I suggest a general and very simple formulation: 

 

Mathematics ***is*** formalising of our thought and intuition 
because formalisation is a tool to make our thought and intuition stronger. 


(See also my first e-mail from May 19.) 

 
There could also be some additional clarifying comments. But it seems 
they will be in a sense just informal consequences of this formulation. 
Even if such comments will be **essential** additions, the above formulation 
seems to me the most crucial one for understanding the nature of mathematics.  

 Vladimir Sazonov