Here we give a summary of a theory that covers the existence and uniqueness of factorizations in abelian cancellation monoids. The final theorems of this theory can easily be instantiated to give the fundamental theorem of arithmetic.
Basic Definitions The basic definitions for divisibility theory over an abelian monoid g are:
Here, | is the divides relation, is the associated
relation and p| is the `properly divides' relation. The
=
relation is Nuprl's typed equality
relation: it states that
and
are equal members of type
.
The divides relation is a preorder:
The type AbMonoid is the class of abelian monoids. An element g of this class is a tuple <|g|,xg,1g> where xg is an
commutative associative binary operator over the carrier |g|, and
1g is the unit. The i index in the {i} suffix is
implicitly quantified over the natural numbers: it indicates the size of
the universe of types that the carrier comes from.
The predicates and functions in factorization theory respect
associates and predicates concerning equality lift to predicates
concerning associates. For example, xg respects and
cancellation with respect to equality implies cancellation with
respect to
:
where:
Other definitions are for reducibility, atomicity and primeness. For convenience, both types and predicates were defined for atomicity and primeness:
From these definitions various facts were proven such as that every prime is an atom in a cancellation monoid:
Existence Theorem The theorem characterizing when factorizations into atoms exist is:
The theorem says that in a cancellation monoid with a well-founded
`properly divides' relation, every non-unit can be factorized into atoms.
The predicate Dec(reducible(g;c))) states that reducibility
is a decidable property in g. This assumption is necessary because
the theorem was proven constructively. The function g
takes
the product using xg of the elements of list
. If
is the
empty list, it returns 1g.
An abbreviated proof listing for the theorem is shown in
. The proof is presented in a style
very similar to that in which Nuprl proofs are normally presented: The
goal proven is shown at the top, and after each BY one or more
inference steps are explained which refine the goal immediately above
the BY into zero or more subgoals below the BY. For
compactness, the proof only shows those parts of the sequent that have
been changed by the refinement.
Normally, proofs show the names of tactics after each BY. Here, to improve readability, we have paraphrased the tactics in English and have elided a few intermediate steps of the proof. The full proof when printed out is less than two times longer.
Here is a version of the theorem and proof, closer to how it might appear in a text-book. See section ??? for how to generate this format.
For all Abelian Monoids ,
Proof: Let be an arbitrary Abelian Monoid with the given properties, and let
be an arbitrary non-unit of
. We must find the factorization
. Proceed by induction on the well-founded divisibility relation, written p|.
Uniqueness Theorem The theorem characterizing when factorizations are unique is:
The relation
upto
says that list
and
list
are a permutation of each other up to the equivalence relation
on the elements of the list. Here, with
being the relation
g, it captures the notion of factorizations being `essentially'
the same.
An abbreviated proof of the theorem is shown in
. The full proof printout is about 2.5
times longer. Additional notation is introduced in the proof
as follows:
