[FOM] Notations in mathematical practice

[A. Mani]

On Mon, Oct 26, 2015 at 1:48 PM, Arnold Neumaier
<arnold.neumaier at univie.ac.at> wrote:
>> 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).


Your post seems to assume that the language of proof assistants are
not configurable as per user needs.

I don't see too much of a problem in permitting users to configure the
object level language of proof assistants and that should be a
direction for future work. Proof assistants can be more intelligent.


Here is how a specifications can be:

1. Proof Assistant has its own standard language.

2. Mathematician-1 modifies a user-specific config file as per their needs.
(this assumes that the mathematician has a minimal understanding of
the language used by proof assistant).

3. Proof assistant  confirms it can translate back and forth (optional step).

4. Mathematician-1 performs a computation with PA. PA outputs results
in both mathematician's and its native language.

5. Ambiguities resulting by way of omission of the learning step (3)
can be handled by if-then trees.

I don't think we even need a exceptional learning engine in the proof
assistant for all this because mathematicians are far more rigorous
than non mathematicians - deep learning techniques, for example,
address the latter class.



Best

A. Mani



Prof(Miss) A. Mani
CU, ASL, AMS, ISRS, CLC, CMS
HomePage: http://www.logicamani.in
Blog: http://logicamani.blogspot.in/
http://about.me/logicamani
sip:girlprofessor at ekiga.net