FOM: Re: "Relativistic" mathematics?

[Vladimir Sazonov]

Charles Silver wrote:
> V. Sazonov:
> > Any (mathematical) proof assumes (at least implicitly) a formal
> > system where it is written.
>
>         Already I disagree.  Maybe this is at the heart of our
> disagreement.  I think mathematics proceeds intuitively first, on the
> basis of agreed-upon structures.  For example, suppose I were to say to
> you: I'm thinking of a Tree that starts out with two elements.  To make
> this pseudo-Biblical, let these elements be Adam and Eve.  I'm supposing
> that each of them alone can beget "children".  And, in fact--continuing
> with this silly example--let us suppose each of them has two children the
> first generation, three the second, five the third, and so forth (i.e.,
> the children of each generation arrive in terms of the sequence of prime
> numbers). And, the children can have children too, in accordance with the
> same procedure of having 2,3,5,7,... in each generation.  I'd like to make
> this a little more complicated, but I'm not sure how.  Let's see.
> Supposing that some of them die according to the following pattern....
> I'm not going to continue with this.  It's probably rather a dumb example.
> My only point is that you and everyone else can follow this without
> benefit of some formal system.  I think when I started out saying that
> this whole thing begins with Adam and Eve, you pictured two entities.
> Then, when I said they each begat two children, I think you also pictured
> that.  And, I think you also pictured three children for the next
> generation, and so forth.  Of course, when it gets complicated, you may
> need to draw some lines or something.  My only very simple-minded point
> here is that there is no formalism involved.  Just you following along,
> picturing my silly made-up structure.
>
>         If you were to say that this *could* be formalized, I'd agree with
> you.  But, the thinking, the understanding, the theorem-proving, and so
> forth is *prior* to the formalization of it all.  Again, I'm not saying
> that it doesn't help to formalize things.  I agree that it does.  But, the
> fact that something ultimately is given a formal explanation does not, to
> my mind anyway, indicate that the essence of the mathematics involved is
> that it could later on be formalized.  I know many people disagree with
> this.  And, perhaps you do too.  Perhaps, our disagreement hinges on your
> thinking that all of mathematics makes sense only within a formal system.
> Do you?  I don't believe this at all.
>
>         I wanted to say some more things, but I think I'll stop and wait
> to hear what you have to say about this.

If you will tell this story on Adam and Eve to somebody from the 
street who really have NO mathematical experience and did not 
learn at school some examples of mathematical proofs (and actually 
of proof rules) he will be unable to understand even what are prime 
numbers and any informal proof you will present. Our teachers 
actually (usually implicitly, by examples) said us which are 
"correct" rules of inference. So, if somebody have any 
reasonable mathematical education and training, then he actually 
knows something like first-order logic. (But, most probably, he 
does not know that he knows this. But this does not matter.) 
Then he will implicitly, without even knowing this, formalize 
(some essential features of) your story.  Anyway, any proof 
which will present or understand that person will be formal in 
some essential respect. Mathematical proof is something which 
can be *checked* on correctness mostly relative to its form, 
rather than to its content.

Take axioms of Euclid. Where they not sufficiently formal (even in
the time when there was no predicate calculus around) to recognize
very reliably whether a proof is correct? Now we have a little bit
more rigorous mathematics. We realize more explicitly that proofs
may be formal. But at those old times mathematics was also rigorous
enough and there was some ideal of what is a correct proof. 

Let me also recall what M. Randall Holmes"
<M.R.Holmes at dpmms.cam.ac.uk> wrote on Fri, 2 Oct 1998 11:16:41:

> One cannot be more or less rigorous if there is no standard
> of perfect rigor to approximate.
>
> We may _not_ doubt that the conclusion of a valid argument follows
> from the premises.  We do have explicit standards, which we can spell
> out, as to what constitutes a valid argument.  This is the precise
> sense in which mathematics is indubitable.  No natural science is
> indubitable in this sense.
>
> This is not "19th century foundationalism"; it is a standard known
> to Euclid (though he did not perfectly exemplify it).

I think that having *explicit* standards means having known 
some rules of inference presented in any reasonable form. 
Say, children learn at school how to use in geometry the rule 
reductio ad absurdum. 

...

> The standards for what constitutes an
> acceptable approximation to a formal proof cannot be formally spelled
> out.  The actual process by which theorems are accepted is not a
> formalizable one (though one hopes that it is a careful
> approximation).

We use also some abbreviations which, 
strictly speaking, are assumed to be eliminated.  This is the 
place where there is possibility to reach even stronger ideal of 
rigorous proof because in practice the process of elimination 
may be infeasible. Thus, we should formulate our formalisms more 
carefully, by postulating explicitly which kind of abbreviations 
is allowed, and which isn't. By the way, this is the key point 
of my formalization of a feasible arithmetic. 

To sum, I mean by a formal system such a system of axioms and 
proof rules to which the term 'formal' may be applicable in any 
reasonable sense. Thus, even any semiformal proof is 
mathematically rigorous.  It is rigorous to that degree to 
which it is formal.

And finally, I think it is unnecessary to discuss very much that 
mathematics deals only with *meaningful* formalisms based on 
some *intuition* and that even formal proofs are mostly 
understood by us intuitively, may be with the help of some 
graphical and other images and that there is a very informal 
process of discovering proofs so that on the intermediate steps 
we have only some drafts of future formal proofs (and sometimes 
of axioms and proof rules, as well). Anyway, in each historical 
period (except the time of a scientific revolution) we usually 
*know* what is the ideal of mathematical rigour to which we 
try to approach in each concrete proof. 


Vladimir Sazonov