The term "mathematical vernacular" ("wiskundige omgangstaal" in the original Dutch) was introduced by de Bruijn in the 1980's, to describe the stylized language used by mathematicians to express proofs. Freek Wiedijk argues in a paper named The Mathematical Vernacular that the essence of this proof style is three ideas:
At least three popular proof systems implement some form of the mathematical vernacular: Mizar, Isar, and Hyperproof. Freek is also designing a prover of his own, Conproof, and plans to use MV as its basis.
Because MV proofs use "big steps", a verifier must include a first order prover. Thus, any translator from MV proofs into explicit proofs verifiable by metamath and friends must contain a first-order prover capable of outputting the low-level proof steps in such a language. While developers of first-order provers compete intensively on the basis of speed (for example, in the CASC competition), for such translation use an additional goal would be conciseness of translated proofs.
The "natural deduction" aspect of MV should be relatively straightforward to translate into a metamath-like langauge. For one, frl has proposed an axiomatization of natural deduction in metamath. Also, raph has been finding empirically that natural deduction style proofs can be expressed fairly easily in metamath's existing Hilbert-style axiomatization, especially with the help of assump.ghi, a library of propositional calculus statements designed to ease manipulation of large numbers of assumptions, represented as binary trees of conjunctions.
Perhaps surprisingly, the proof steps enumerated in Chapter 5 of Freek's paper already have close correspondences in metamath's set.mm:
let or forall-introduction: 19.21aiv assume (-> introduction): ex assume (-. introduction): mto (mtod is deduction-form variant) assume (reductio ad absurdum): mt3 (mt3d) thus or and-introduction: jca per cases or or-elimination: pm2.61i (pm2.61d) for boolean case consider or exists-elimination: 19.23aiv take or exists-introduction: vtocle
Note, when I used this phrase on the Ghilbert and HDM page, I wasn't thinking of any formal definition (perhaps de Bruijn also had a loose, informal understanding of the term?). What I meant was, whatever language people communicate mathematics in.
I'll be interested in reading what Freek has to say about it, but from the sketch above, I have my doubts.
As with mainstream languages, it may be appropriate to talk about mathematical vernaculars – for one thing, people embed mathematical languages in many different natural languages, and for another, different branches of mathematics may have very different standards for mathematical communication (e.g. different standards for proof).
Because of the widespread use of the term to mean the approach taken by Mizar (big steps, natural deduction, syntax roughly approximating natural language), I think you need to be very clear whether you mean Freek's sense, or a more informal sense. Geleijnse, in his thesis (see below), follows the terminology introduced by Kamareddine and Nederpelt's paper, "A refinement of de Bruijn's formal language of mathematics" (PDF) and uses the term "Common Mathematical Language", with the abbreviation CML (not to be confused with Concurrent ML or any of the other expansions of the acronym), to mean the informal natural language style used by mathematicians to present proofs.
I think de Bruijn's use was more formal than not, given what I've been able to glean from skimming his 1979 paper, Grammatica van WOT. Perhaps one of our Dutch-speaking friends can shed some more light.
When you say you have your doubts, what are you most doubtful of? To me, the biggest red flag with WTT is its complexity. I am also skeptical of the near-theological belief that types are the one true basis that should underly mathematics, as opposed to, say, sets. I am also skeptical of the assumption that the best language for developing a library of automatically checkable proofs must closely resemble informal mathematical language (this is the "reliability" criterion introduced by Kamareddine and Nederpelt). But that's just me.
Doubts - specifically, as to whether the Freek definition of "mathematical vernacular" really expresses the jcorneli definition. (It sounds more formal than the simple notion I have in mind.)
G. Geleijnse's masters thesis, Comparing two user-friendly formal languages for mathematics: Weak Type Theory and Mizar, has some interesting discussion comparing computer proof languages (in particular the ones in the title) and informal mathematical proofs. Weak Type Theory (WTT) is a refinement of De Bruijn's Mathematical Vernacular (MV). --norm 25 Aug 2006
Thanks for posting that. It's very interesting, not least for its detailed discussion of Mizar.
One immediate conclusion from this thesis is that there are many possible paths to "user-friendliness" in formal math. Personally, Mizar's use of pseudo-English reminds me of Cobol. It's nice to see that there are alternatives.
WTT, like Coq and NuPRL?, seems fundamentally based on type theory, although it seems to have a less constructive flavor than the latter. This raises a few questions for me:
--raph 26 Aug 2006, Zurich
When I try to think what I use when I try to write out a proof in English (well in French in fact but I adapt) I notice that I use what I would describe as meta-theorems. For instance supposing that I have a ( ph <→ ps) biimplication there are a lot of theorems in set.mm to replace ph by ps in a given formula. But when I write a vernacular proof I haven't these special cases in mind. In fact I informally use a more general theorem that I never write out in the eventual vernacular proof. This theorem could be described as following: in any propositional calculus formula I can replace ph by ps anywhere as soon as I know that ( ph <→ ps ) is a proved hypothesis. I would call this meta-theorem: the most general law of replacement. To tell the truth I wonder if there exists a system where this law can be proved. – 27-Mar-2007 fl