Towards a Formal Mathematical Vernacular

Abstract

Contemporary proof verificators often use a command language to construct proofs. These commands are often called tactics. This new generation of theorem provers is a substantial improvement over earlier ones such as AUTOMATH. Based on experience with these new provers we feel the need to study these languages further, especially, because we think that these may be improved in their adequateness to express proofs closer to the established mathematical vernacular. We also feel that a systematic treatment of these vernaculars may lead to an improvement towards the automatic inference of trivial proof steps. In any case a systematic treatment will lead to a better understanding of the command languages. This exercise is carried out in the setting of Pure Type Systems (PTSs) in which a whole range of logics can be embedded. We first identify a subclass of PTSs, called the PTSs for logic. For this class we define a formal mathematical vernacular and we prove elementary sound and completeness. Via an elaborate example we try to assess how easy proofs in mathematics can be written down in our vernacular along the lines of the original proofs.