[FOM] Notations in mathematical practice

[Arnold Neumaier]

On Sun, October 25, 2015 09:21, Arnon Avron wrote:
> In his posting on free logic, Harvey Friedman made
> the following side remark:
>
> "Mathematicians just want to make sure that there is no practical
ambiguity in what they write."
>
> Do they??

Yes, they do, since they want to communicate efficiently without losing
time and patience to spell out the obvious. This is also the reason why
most of them are unwilling to use proof assistants, since these are far
too dumb to pick up the cues that mathematicians learn during their study.


> Well, try the following experiment: ask an ordinary  mathematician
whether or not the following is an identity:
>
>      f'(x) = f(x)'
>
> My experience is that when I ask this question some professor of math
(with no much background in logic, and sometimes even with) he starred
at me, starred at the formula, and then, after some hesitation, tells me
:"well, it depends on what you mean."...

Of course. If you take a formula out of context, you lose much of the
information which ensures that there is no practical ambiguity. It is the
context that determines (in a well-written document) how to interpret a
given formula. Even to an extent that a typical mathematician can do error
correction! I still have to see the proof assistant that can replicate
this.


> So no mathematician that respects himself would talk about
> "the set x^2>0", only about "the set {x|x^2>0}".

But the latter is still far from formally correct, since it fails to
specify the ground set from which x is taken. Thus even you communicate in
your formulas only what you think is sufficient for successfully making
your point, and leave the remainder to the context. So you shouldn't
criticize mathematicians for carrying this even further!


> But the same mathematician
> would talk about "the function x^2", not about "the function \lambda
x.x^2".
>
>   Is there any chance of changing this?

There is no need to change this. It would make things only clumsy.

A typical mathematician reads and writes the customary informal
mathematical exposition far quicker than any of its full formalizations,
and probably obtains as a result much more insight.

In contrast, a proof assistant gives (at a much higher cost) only a
guarantee of correctness, but almost nothing beyond that. But it is the
insight that makes the mathematics, not the truth (which is just a
necessary requirement).


Arnold Neumaier
http://www.mat.univie.ac.at/~neum/FMathL.html#MathResS