The "Mathematical Vernacular"

I'd like to write some remarks about Wiedijk's Mathematical Vernacular article. Wiedijk credits de Bruijn's "The mathematical vernacular, a language for mathematics with typed sets" (in P. Dybjer et al.'s Proceedings of the Workshop on Programming Languages, Marstrand, Sweden 1987) as the origin of a formal language — a "mathematical vernacular" — underlying mathematical proofs.

Wiedijk departs from de Bruijn by inspecting declarative proof assistants (e.g. Mizar or Isar) and using this as the foundation for the mathematical vernacular.

There are four "syntactic categories" in Wiedijk's mathematical vernacular: label, variable, term and formula.

Let us recall from mathematical logic that terms are expressions which can be obtained from constants, variables, and functions (or, if you'd prefer, formulas). I will be a little bit sloppy here, since "we all know" what a variable and a formula are.

A label is a generalisation of the notion of equation numbering. It is used to indicate references to specific locations in the proof, typically to justify some reasoning in a proof.

Introducing the Formal Grammar

The mathematical vernacular can be pictured as a programming language for proofs. So it has a formal grammar. Lets quickly run through it.

statement = proposition justification ;
proposition = [ label : ] formula
justification =
  empty
| by reference {, reference}
| proof {step} [ cases ] end
reference =
  label
| -
step =
  statement
| thus statement
| let variable {, variable} ;
| assume proposition ;
| consider variable {, variable} such that proposition justification ;
| take term {, term} ;
cases = per cases justification ; {suppose proposition ; {step}}
empty =

Note that the keywords are typed in a different font. Also note that when justifying the current step by the previous line, we indicate this as "by - ;".

Most of these are straightforward in their design, but lets consider an example of how to translate a given proof into the vernacular.

Theorem 43 (Pythagoras' Theorem). √2 is irrational.

The traditional proof ascribed to Pythagoras runs as follows. If √2 is rational, then the equation

a2 = 2b2	(4.3.1)

is soluble in integers a, b with gcd(a, b) = 1. Hence a² is even, and therefore a is even. If a = 2c, then 4c² = 2b² , 2c² = b² , and b is also even, contrary to the hypothesis that gcd(a, b) = 1.

G.H. Hardy and E.M. Wright An Introduction to the Theory of Numbers,
4th edition, Clarendon Press, Oxford, 1960. Pages 39–40

Lets try to consider this in the mathematical vernacular. We are assuming for contradiction that 2^1/2 is rational, then we obtain a contradiction.

Theorem 43: sqrt(2)∉ℚ
proof
    assume sqrt(2)∈ℚ;
    consider a, b∈ℤ such that
(4.3.1): a2 = 2b2 and
    gcd(a, b)=1;
    thus a2 is even by (4.3.1);
    thus a is even by -;
    consider c∈ℤ such that a=2c;
    thus 4c2=2b2 by -, (4.3.1);
    thus 2c2=b2 by -;
    thus b is even by -;
    thus ⊥ ;
end;

Note we use the notation ⊥ for "falsum," or contradiction.

Of course, here we are a little bit sloppy since the assertion that a² being even implies a being even is not proven. But it is elementary arithmetic that may be verified quickly.

Also we are a little bit sloppy since the label "Theorem 43" should really be "Theorem_43", but still little is affected by that. We are humans!

It's actually kind of fun to start verifying proofs in the mathematical vernacular, because it makes any mistakes in a proof manifestly evident. You also get the same feeling of rigor you get if you tried putting the proofs in a purely symbolic way (cf. Russell and Whitehead's Principia Mathematica).

Explaining the Formal Grammar

Wiedijk does a wonderful job explaining the logical structure of each of these statements, but I'll give a "user's manual" explanation of what these steps mean in practice.

let step

This has always confused me, at least distinguishing it from the consider…such that…; step. When you consider it as introducing a variable taking values in a given collection, it becomes clear how to use it. This is where we declare a variable (in the computer science sense), and the consider step initializes it to a value.

If we want to prove, e.g., a set X satisfies some property P(x) for all x∊X, it's done in two steps: let x∊X; [and then prove that P(x) is true].

assume step

This can be used in several different ways.

1. Suppose we wanted to prove a statement of the form "If p, then q" then we have our proof be of the form "assume p; [prove q logically follows]".
2. Proof by contradiction. "If p, then q" we want to "assume p and ¬q; [Prove a contradiction]".

thus statement

This is really the meat and potatoes of a proof, it's the transition to do deductions.

per cases statement

Often in practice, we end up reducing our proof to several simple cases. This is precisely what we do in this step.

consider step

This step initializes a variable to a certain value, or introduces a constant.

take step

This introduces a "term", with an existential quantifier. That is to say, if we want to prove "∃x P(x)", we first "take a;" for our "x". Then we will prove (constructively!) that P(a) is true.

Alternatively, if we use the approach of proof by contradiction to consider proving "⊤ and ¬(∃x P(x))" which is logically equivalent to "⊤ and ∀x ¬P(x)", then we could use the let step. More precisely it would be "let x; assume ¬P(x); [prove a contradiction]". We should note that ⊤ is always assumed at each step, so we don't need to explicitly state "assume ⊤ and ¬P(x);".

Although to be truthful, I don't believe I've used the take step. This may be due to my lack of work applying the vernacular to proofs.

Automatic Proof Checker?

If anyone was crazy enough to want to write an automatic proof checker using the mathematical vernacular as the language, one would first have to consider writing a first-order theorem prover.

I will not do this, but give a few references for the curious among us, namely David Amos's A Theorem Prover for Intuitionistic Propositional Logic. LC Paulson's eprint "Designing a Theorem Prover" would be a useful reference as well.

Perhaps Marnix Klooster's A Haskell module for sound Ghilbert-style proofs would be useful to examine too.