Abstract:
MathLang: A language for Mathematics.
Fairouz Kamareddine
Frege was frustrated by the use of natural language to describe
mathematics. In the preface to his Begriffsschrift he says:
"I found the inadequacy of language to be an obstacle; no matter how
unwieldy the expressions I was ready to accept, I was less and less
able, as the relations became more and more complex, to attain the
precision that my purpose required."
Frege therefore presented in his Begriffsschrift, the first extensive
formalisation of logic giving logical concepts via symbols rather than
natural language. Frege developed things further in his Grundlagen and
Grundgesetze der Arithmetik which could handle elementary arithmetic,
set theory, logic, and quantification. In his Grundlagen der
Arithmetik, Frege argued that mathematics can be seen as a branch of
logic. In his Grundgesetze der Arithmetik, he described the elementary
parts of arithmetic within an extension of the logical framework of
Begriffsschrift. Frege's tradition was followed by many others:
(Russell, Whitehead, Ackermann, Hilbert, etc.). Russell discovered a
paradox in Frege's work and proposed type theory as a remedy.
Advances were also made in set theory, category theory, etc., each
being advocated as a better foundation for mathematics. But, none of
the logics proposed satisfies all the needs of mathematicians. In
particular, they do not have linguistic categories and are not a
satisfactory communication medium. Moreover:
-
Logics make choices (types/sets/categories,
predicative/impredicative, etc.). But different parts of mathematics
need different choices. There is no agreed best formalism.
-
A logician's formalization of a mathematical text loses the original structure
and is thus of little use to ordinary mathematicians.
-
Mathematicians can do their work without formal mathematical logic.
In the second half of the twentieth century, programming languages
were being developed and this led to the creation of softwares,
systems and tools to computerize and check mathematics on the
computer, and to give some help and assistance to teachers, students,
and users of mathematics. But, a mathematical text is structured
differently from a machine-checked text proving the same facts.
Making the latter involves extensive knowledge and many choices:
-
The Choice of the underlying logic.
-
The Choice of how to implement concepts (equational reasoning,
induction, etc.).
-
The Choice of the formal system: a type theory (which?), a set theory
(which?), etc.
-
*The Choice of the proof checker: Coq, Isabelle, PVS, Mizar, etc.
Furthermore, checking mathematics on the computer has other problems:
-
*An informal mathematical proof will cause headaches as it is hard to
turn in one big step into a (series of) syntactic proof expressions.
-
*During the checking of mathematics, the informal proof is replaced by
a complete proof where every detail is spelled out. Very long
expressions replace the clear mathematical text and this is useless to
ordinary mathematicians.
-
so, despite the enourmous work on logics for mathematics as in Frege's
tradition, and computer tools and systems for implementing and
checking mathematics as in the second half of the twentieth century,
mathematicians remain sceptical about using logic and using computers.
In this talk, I argue that both the logic for mathematics and the
computation of mathematics have forgotten the mathematician and the
language of mathematics during their development. I start from de
Bruijn's mathematical vernacular which he refined almost twenty years
after the begin of his Automath project (Automating Mathematics). I
compare this vernacular to modern approaches for putting mathematics
on the computer (e.g., OMDOC, MathML, versions of XML, etc.) and
discuss how we can find a language of mathematics that is open to
future developments through logic and computation.