[mizar] mathematical vernacular

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

It seems that the term 'mathematical vernacular' has different meanings in
Durham and Bialystok. I asked prof. de Bruijn
for His opinion. Here you are:

n.g.d.bruijn@tue.nl wrote:

> To: Andrzej Trybulec [trybulec@math.uwb.edu.pl]
> Sent: dinsdag 18 juni 2002 22:49
> From: n.g.d.bruijn@tue.nl
> Subject: Mathematical Vernacular
>
>     Eindhoven, June 19, 2001
>

...

>
>     You asked me what I think about the phrase 'mathematical vernacular'.
> I think it is a kind of household word, that might have been used long
> before it turned up in the proof checking community.
>     In the 1970's I was working on this project of an intermediate
> language between standard language and completely formalised
> language. I was looking for a good word for that standard language,
> and it was John Todd (Olga Taussky's husband) in Pasadena who
> suggested the word 'vernacular'. It had, of course, already been
> used quite often in the world of natural languages, in
> particular in the Catholic church to distinguish the language of the
> laymen from the official Latin.
>
>    I think that in the beginning I used titles like 'Formalizing
> the mathematical vernacular, suggesting that 'mathematical
> vernacular' was an existing notion, and that my system MV presented
> a stylized form of it.
>    In later years, several other people worked on such intermediate
> languages, and called them their 'mathematical vernacular'.
> I mention Rudnicki, Gilles Dowek, and Gilles Barthe.
> If you ask a search engine on internet for 'mathematical vernacular'
> you will get many references.
>    Let us just take the words 'mathematical vernacular' as the
> language that mathematicians use when writing papers. As such
> it is a vague notion, depending on area and on time.  I think that
> I should not have used the words in the title of some of my papers,
> with the suggestion that 'the' mathematical vernacular was just my
> system MV.