Context-relative syntactic categories and the formalization of mathematical text

Abstract

The format of grammar presented by Montague (1974) is widely applied in the study of the logical structure of informal language. Thus it is natural to try how it works in the analysis of language in which logical content is uncontroversially a prominent part of meaning, the language of mathematics. In Ranta 1995, we presented a system of syntactic categories obtained from categories of Montague style by adding domain parameters; semantically, this corresponds to the transition from simple type theory to a type theory with multiple domains of individuals and dependent function types. In this paper, we shall generalize the system of categories further, by adding context parameters. In this way, it becomes possible to express arbitrarily complex quantificational structures in English. We go on by defining a category of proof texts, which are interpreted as type-theoretical proof objects. A system of introduction and elimination rules will be presented for the logical constants, as well as some mathematical proof rules. The rules presented in this paper are a fragment of a grammar implemented in the proof editor ALF. A similar grammar has been implemented for French, too. The implementation can be used as an interactive proof text editor, so that the user chooses proof steps, wordings, and grammatical structures, and the system checks that the text is both mathematically and grammatically correct.