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

Tue May 25 17:43:54 EDT 2010

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

they will be in a sense just informal consequences of this formulation.