FOM: Re: constructive mathematics

[V. Sazonov]

This is reply to Jeffrey Ketland, Whim van Vessel, Matthew Frank,
Robert Black and Allen Haze.


Jeffrey Wetland wrote:

> Ayan wrote on 27 May (17:40 on my clock):
>
> >One thing may be worth pointing out, that constructive mathematics
> >(Bishop's style which I understand is the topic of current discussion) is
> >currently seen as working with
> >Intuitionistic logic. I guess this goes against any subjectivism in
> >constructive mathematics.
>
> Goes *against* subjectivism? I don't understand. The following is an extract
> of what Arend Heyting wrote in his 1956: Intuitionism: An Introduction
>
> (This is part of an excellent dialogue, between the characters called
> "Class" (classical mathematician), "Form" (a formalist, seems to refer to a
> mixture of Hilbert and Carnap), "Int" (an intuitionist, seems to refer to
> Brouwer), "Letter" (a sort of finitist formalist), "Prag" (a pragmatist,
> seems a bit like Quine) and a mysterious character called "Sign"):
>
> -------------------------
> Intuitionist mathematics consists ┘ in mental constructions; a
> mathematical theorem expresses a purely empirical fact, namely the
> success of a certain construction. ▒2 + 2 = 3 + 1▓ must be read as an
> abbreviation for the statement: ⌠I have effected the mental
> constructions indicated by ▒2 + 2▓ and ⌠3 + 1■ and I have found that
> they lead to the same result■. ┘
>

Faithfully speaking, I hardly understand all these (and below)
comments on subjectivism. Say, the above formal manipulations
seem to me quite objective and, moreover, having a very clear
relations to the objective world.


> The characteristic of mathematical thought is, that it does not convey
> truth about the external world,

Yes, in a sense, irrelevantly on classical or
intuitionistic mathematics.


> but is only concerned with mental
> constructions ┘

What are mental constructions if not formal ones?
May be formal ones of a specific (here - intuitionistic)
flavor.


> In fact, mathematics, from the intuitionistic point of view, is a study
> of certain functions of the human mind.
> (Heyting 1956) (quoted from Benacerraf & Putnam 1983, pp. 72-73).

I would say, from the classical point of view, too.
What is here so specific here about intuitionism?
Is classical mathematics anymore objective in comparison
with intuitionistic? Both reflect some specific kind of
mathematical thought and reasoning.


> ------------------------------------------------------
> Frege gave an example like the following in Foundations of Arithmetic (Die
> Grundlagen der Arithmetik: 1884). If someone were to say that astronomy
> (say) doesn't deal with bodies in the external world, but is "only concerned
> with mental constructions", one would rightly judge that they were an
> idealist or subjectivist of some sort. Frege was arguing that numbers are
> not (subjective) ideas.

I do not understand this mixture of the real world of
astronomy (planets, stars, etc.) with numbers (intuition
behind some formalisms).


> Surely the above quotation from Heyting makes it plain that intuitionism (or
> at least the form of intuitionism advocated by Brouwer and Heyting) is based
> on a mental (i.e., subjective) conception of mathematical entities.

In this sense all mathematics (classical or intuitionistic)
is mental - based on formalisms which reflect some mental
processes of mathematicians. But formalisms we use are quite
objective and have some sufficiently objective relation to
corresponding intuitions and sometimes directly to the real
world.


Vladimir Sazonov


>
> Regards - Jeff Ketland
>
> Dr Jeffrey Ketland
> Department of Philosophy C15 Trent Building
> University of Nottingham NG7 2RD
> Tel: 0115 951 5843
> E-mail: Jeffrey.Ketland at nottingham.ac.uk

Wim van Gessel wrote:

> My second remark about Jeffrey Ketland's contribution is that it would
> be wrong to simply identify Brouwer's and Heyting's views on
> intuitionistic mathematics. Brouwer had a strong aversion against
> formalism (in fact he had some unpleasant exchanges with Hilbert).
> Heyting had a more pragmatic attitude, and it is probably fair to say
> that Heyting was more interested in the formal, technical development
> of the subject than in its underlying philosophy.

Could not we consider Heyting as a carrier of a religion
which is of course against its formalization? Of course,
a religion may be "used" as a starting point for a
scientific (foundational) consideration. But afterwards
it seems more fruitful to use formalisms, etc. and to
reconsider the corresponding intuition from more contemporary
(realistic) point of view.

What is good about intuitionistic mathematics, it is that,
as I know, there exists even no attempt to make a unique
formalism for it. There are many diverging formalisms.
Is it true? I would consider this as a good sign in favor
of pluralism.


Matthew Frank wrote:

> Apropos of Stevenson and Ketland:
>
> I do think that Brouwer was subjectivist, but he may have been the last
> (real) subjectivist intuitionist.  (I agree that Heyting's Int was a
> subjectivist, but that was a fictional character.

I think that there are also other fictional characters
like stilted comedy heroes having nothing general with a
real life such as "ortodoxal" formalists (in the most
vicious form of neglecting *any* meaning behind formalisms;
I myself understand formalism quite differently; cf. below).


> Also, Sazonov asks:
>
> > By the way, if another philosophy(?) called formalism really
> > exists (which allegedly asserts that mathematics deals only with
> > formalisms without any meaning), who are full-fledged formalists,
> > personally? Or such a formalism is a philosophy without any real
> > ``philosophical formalists''?
>
> I am a formalist, in that I believe:  1) it is essential to modern
> mathematics that it can be formalized, and 2) for much of modern
> mathematics the only meaningful notion of truth (if it is a notion of
> truth at all) is provability in some formal system.
>
> I am also a methodological formalist in that I am skeptical of discussions
> of mathematical knowledge, mathematical objects, mathematical truth; I
> generally prefer those discussions (if and) when they can be recast in
> terms of formal systems.  I would not say that the formal systems are
> without any meaning, but I would rather frame the discussion in terms of
> the intuitions that we can associate to those formal systems.
>
> I presume one could identify various others as formalists on the basis of
> their publications, though I have not tried to do so.  So while I
> generally recommend against discussing "constructivists" (since I am not
> sure if there are any, and in any case they are very few), I do not have
> those reservations about the term "formalists".
>
> --Matt

Thus, our positions on formalisms seems to coincide.
Cf. also some additions in my posting to FOM from
Sat Dec 04 15:24:46 1999 and
Tue Dec 28 11:36:39 1999.
Some additions seems necessary to explain why and how
formalism in principle does not assumes lack of meaning
of formal systems. The problem only consists in that
formalism is usually understood in the above "stilted"
form. The meaning of this word should be slightly changed.
Say, as I understand, Jan Mycielsky does not agree
to be called formalist only because of the traditional
meaning of this term. (Cf. corresponding discussion in
FOM and the first posting above.)

Nevertheless, my question you replied remains non answered,
because I asked about formalism philosophy and formalists
which reject meaning. Or all of this is a fiction?


Robert Black wrote:

> Matthew Frank:
>
> >I am a formalist, in that I believe:  1) it is essential to modern
> >mathematics that it can be formalized, and 2) for much of modern
> >mathematics the only meaningful notion of truth (if it is a notion of
> >truth at all) is provability in some formal system.
>
> I don't think anyone on this list is likely to quarrel with (1), but if one
> starts pressing (2) (and disregards the let-out 'much of') I think it
> starts to fall apart. Bourbaki says something closely related (_Theorie des
> Ensembles_ I,22) when he says that the claim that some sentence is not a
> theorem of a formal system 'can have no sense *in mathematics*' (Bourbaki's
> emphasis).
>
> When we prove a sentence S in a formal system, if all we take ourselves to
> be really doing is announcing that it is so provable, then we are always
> announcing a sigma_1 result, whatever the logical complexity of S, and our
> proof of that result is of course constructive; we have exhibited the
> (Goedel numer of the) array of dried ink which is a proof of S. So this is
> really the view that all mathematical knowledge consists of constructively
> proved sigma_1 results.
>
> Consider now a pi_1 claim like 'PA is consistent'. What is the 'formalist'
> going to say about this claim? He can of course announce that it's
> provable, in, say, ZF (a sigma_1 fact), or that it's disprovable in, say,
> PA+not-Con(PA) (another sigma_1 fact), but what about the claim itself's
> being true or false?
>
> There seem to be two options:
>
> Either: You say it's not the sort of thing that could be true. I find this
> pretty zany, particularly because it could (for all we know) be false! Do
> you really want to go down this road? Is the claim meaningless though its
> negation is meaningful? Or do it and its negation suddenly become
> meaningful only if the negation turns out to be true? Or is it meaningful
> but couldn't be true though it could be false???
>
> Or: You say that it probably is true, but the claim that it's true is not
> *mathematical*. (Is this Bourbaki's let-out?) But then what on earth is the
> name of the branch of human intellectual endeavour to which that claim
> *does* belong? Perhaps universities should open up some departments for
> this new subject!
>

It belongs to mathematics because mathematics can
find (suggest) an appropriate meaning of this question
(may be not the unique possible one) via some
formalization as it is shortly discussed below.


According to the rules (of the "game") of classical
first order logic it is either true or false
(the excluded middle low. From the point of view of
a meaning which me, as a mathematician, would assign
to this formal statement, we should start with the
meaning of Peano Arithmetic. What is it about?
On some abstract natural numbers? What kind of
abstraction? First we think, say, about pebbles.
One, two, three pebbles, etc. What does it mean "etc."?
There is no last number? (Why?) But let it be. Can we
repeat successor operation many times, as many as is a
given natural number? (Addition operation.) Are we sure
that this is always possible? But let it be. Let us also
iterate addition and allow multiplication as total
function. Then, exponentiation, etc. But what does *this*
"etc." mean? Let us postulate induction schema which
seems very plausible and formally (according to the
FOL rules) equivalent to the least number principle
which seems even more plausible. But, as faithful
mathematicians we should, note that there are some
problems with these principle because the induction
formula may involve unbounded quantification over
natural numbers which we are trying to understand
and ***simultaneously*** to formalize. (Let us also
recall the well-known paradox of the least natural
number which cannot be denoted by a phrase, etc.)
How far from the initial intuition related with
pebbles we are now! Is Peano Arithmetic really
about natural numbers or it is about something
rather unclear (but formalized) which we still call
as "natural numbers"?

Then we are asking whether this formal system is
consistent. What do we mean by this? Something
on the level of pebbles, i.e. is there any *real*
formal proof of 0=1 which could be written by a
human or by a computer? If so, which relation
to this (quite meaningful) question has the formal
statement Con(PA)? It has some, but which exactly?

Or we mean by the question on consistency possibility
of considering of some imaginary proofs. But are they
proofs, if they are imaginary? Sorry, I am not completely
sure on the meaning of the formula Con(PA). Of course,
we could consider model theory in the framework
of ZFC and consider so called "standard model" of PA.
In this framework Con(PA) is, of course true in
corresponding ***technical*** sense. But this is only
a ***relativised*** (to ZFC) meaning of Con(PA). But
Robert Black asked some absolute question. I do not
know what the ***absolute*** meaning of Con(PA).


Allen Hazen wrote:

>     A lot of very different points of view have gone under the name
> "formalism."  Some of the cruder and more extreme 19th century ones were
> criticized by Frege in his "Foundations of Mathematics."  For a reasonably
> short, very readable, account of the history of these ideas, my favorite
> book is Michael Resnik's "Frege and the Philosophy of Mathematics" (Cornell
> U.P. 1980; I think out of print, alas).

Thanks for the reference! But
Could you name, please, those old or contemporary formalists
who rejected meaning of formal systems considered in
mathematics and may be outline in several words the main
ideas of these formalists?


Vladimir Sazonov