Monoid Theory in Alonzo: 
A Little Theories Formalization in Simple Type Theory

William M. Farmer and Dennis Y. Zvigelsky

2023

Abstract

Alonzo is a practice-oriented classical higher-order logic that
extends first-order logic and that admits undefined expressions.
Named in honor of Alonzo Church, Alonzo is based on Church's type
theory, Church's formulation of simple type theory.  The little
theories method is a method for formalizing mathematical knowledge as
a network of theories called a theory graph consisting of theories as
nodes and theory morphisms as directed edges.  The development of a
mathematical topic is done in the "little theory" in the theory graph
that has the most convenient level of abstraction and the most
convenient vocabulary, and then the definitions and theorems produced
in the development are transported, as needed, to other theories via
the theory morphisms in the theory graph.  The purpose of this paper
is to illustrate how a body of mathematical knowledge can be
formalized in Alonzo using the little theories method.  This is done
by formalizing monoid theory -- the body of mathematical knowledge
about monoids -- in Alonzo.