Doing Algebra in Simple Type Theory

To fully utilize the power of higher-order logic in interactive theorem proving, it is desirable to be able to develop abstract areas of Mathematics such as algebra and topology in an automated setting. Theorems provers capable of higher order reasoning have generally had some form of type theory as theory object language. But mathematicians have tended to use the language of set theory to give definitions and prove theorems in algebra and topology. In this paper,we give an incremental description of how to express various basic algebraic concepts in terms of simple type theory. We present a method for representing algebras, subalgebras, quotient algebras, homorphisms and isomorphisms simple type theory, using group theory as an example in each case. Following this we discuss how to automatically apply such an abstract theory to concrete examples. Finally, we conclude with some observations about a potential inconvenience associated with this method of representation, and discuss a difficulty inherent in any attempt to remove this inconvenience.