FOM: What is mathematics?

[Gordon Fisher]

Vladimir Sazonov wrote:

[deletion]

>
> This is absolutely unnecessary. We have a very good standard
> of mathematical rigor without complete formalization. Only
> potential formalizability (whatever it means) plays the role
> in contemporary mathematics. Also partial formalization usually
> suffices.
>

I think you have introduced here a crucial idea in connection
with our conversation, namely that of "potential formalizability,"
together with the modifier "whatever it means".  What does it
mean?  Has anyone ever tried to deal with idea in a precise
way.  Of course, observation and experience show that many
mathematicians who don't use much formal logic in their work
have a feeling, or a faith, that what they present as proofs in
fairly ordinary language could be put into some formal
language based, for example, on a traditional predicate calculus
of some sort.  But is this actually possible?  That is, can all
that is communicated by way of ordinary language in the way
of rigorous proofs actually be so translated?  This is related
to the idea of making proofs with computer programs, which
I take it has so far had only limited success.

As you probably know, Michael Polanyi, the chemist and
philosopher of science described in his book _Personal
Knowledge_ the situation in which not everything a scientist
(or anyone else) knows about his work, after some years
of experience and theorizing, can be communicated in ordinary
language, or so I interpret him.  I suggest, though, that ordinary
language is better suited to _suggest_ or, as I like to say,
to _trigger_ certain kinds of responses to mathematical proofs,
which vary in kind and degree according to the knowledge,
experience and previous theorizing of a recipient to the
proof (listener, reader).

In short, I am suggesting that something may be lost in
translating from _rigorous_ presentations of mathematical
proofs in ordinary languages to formal languages of the sort
found in symbolic logics.  If one _defines_ rigor by saying that
the only kind of _rigorous_ proof is one formulated in some
formal logic system, then presumably one will be able to
say that whatever may be lost in translating from ordinary
language will not be concerned with rigor.  But is this the
case?  Quite aside from the fact that, as you have said, only
short proofs of an elementary sort have ever been translated in
this way, there is a question of whether or not one gets
the rigor out of such a proof only in making use of a background
of knowledge which has to some extent already been formulated
in one or more ordinary languages, and also to some extent
by virtue of knowledge which cannot be, or hasn't ever been,
formulated in an ordinary language.  This is related to ideas
concerning relations between the neurological constitutions
of humans (and at least some other organisms), and what
they "know," where knowledge is taken to be something
more than can be said or written.

As I have indicated above, I like to think of proofs, be they
formal or informal, more or less rigorous, etc., as communications
between people, or with oneself, which _trigger_ certain
responses. in passing from sender to receiver, or more
generally in the course of discussions between senders and
receivers.

Gordon Fisher     gfisher at shentel.net

[deletion]

>
> In conclusion, I would say that Prof. Fisher and me seemingly have
> no essential disagreements, at least in this conversation. I used
> the term "formalist view on mathematics" somewhat in non-traditional
> sense. This could bring some problem in understanding what I mean.
> I think, all misunderstandings are easily resolvable.

I agree that we agree, generally speaking, on numerous
points which have come up in this dialogue.  Have either
of us proved anything yet? :-)

Gordon

>
>
> > Gordon Fisher
> > Prof Emeritus, Mathematics and Computer Science
> > one-time Senior Lecturer in Mathematics, and History &
> >              Philosophy of Science, Univ of Otago & Unive
> >              of Waikato, New Zealand
> > James Madison Univ
> > Harrisonburg VA 22801 USA
> > gfisher at shentel.net
>
> --
> Vladimir Sazonov                        V.Sazonov at csc.liv.ac.uk
> Department of Computer Science          tel: (+44) 0151 794-6792
> University of Liverpool                 fax: (+44) 0151 794 3715
> Liverpool L69 7ZF, U.K.       http://www.csc.liv.ac.uk/~sazonov