A Refinement of de Bruijn’s Formal Language of Mathematics

Abstract. We provide a syntax and a derivation system for a formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples. WTT is a refinement of de Bruijn’s Mathematical Vernacular (MV) and hence: WTT is faithful to the mathematician’s language yet is formal and avoids ambiguities. WTT is close to the usual way in which mathematicians express themselves in writing. WTT has a syntax based on linguistic categories instead of set/type theoretic constructs. More so than MV however, WTT has a precise abstract syntax whose derivation rules resemble those of modern type theory enabling us to establish important desirable properties of W TT such as strong normalisation, decidability of type checking and subject reduction. The deriva-tion system allows one to establish that a book written in WTT is well-formed following the syntax of WTT, and has great resemblance with ordinary mathematics books. WTT (like MV) is weak as regards correctness: the rules of WTT only concern linguistic correctness, its types are purely linguistic so that the formal translation into W TT is satis-factory as a readable, well-organized text. In WTT, logico-mathematical aspects of truth are disregarded. This separates concerns and means that WTT can be easily understood by either a mathematician, a logician or a computer scientist. acts as an intermediary between the language of mathematicians and that of logicians