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

William M. Farmer and Dennis Y. Zvigelsky

2025

Abstract

Alonzo is a practice-oriented classical higher-order version of
predicate 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 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.  Instead of using
the standard approach to formal mathematics in which mathematics is
done with the help of a proof assistant and all details are formally
proved and mechanically checked, we employ an alternative approach in
which everything is done within a formal logic but proofs are not
required to be fully formal.  The standard approach focuses on
certification, while this alternative approach focuses on
communication and accessibility.