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
a^{2} = 2b^{2} (4.3.1) is soluble in integers a, b with gcd(a, b) = 1. Hence a^{2} is even, and therefore a is even. If a = 2c, then 4c^{2} = 2b^{2} , 2c^{2} = b^{2} , and b is also even, contrary to the hypothesis that gcd(a, b) = 1.
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): a^{2} = 2b^{2}and
gcd(a, b)=1;
thus
a^{2} is evenby
(4.3.1);
thus
a is evenby
;
consider
c∈ℤsuch that
a=2c;
thus
4c^{2}=2b^{2}by
,
(4.3.1);
thus
2c^{2}=b^{2}by
;
thus
b is evenby
;
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^{2} 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 theconsider
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.

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]". 
Proof by contradiction. "If p, then q" we want to "
assume
p and ¬q;
[Prove a contradiction]".

Suppose we wanted to prove a statement of the form "If p, then q" then we have our proof be of the form "
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 thelet
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 firstorder 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 Ghilbertstyle proofs would be useful to examine too.
No comments:
Post a Comment