A Formalization of Finite Group Theory

TL;DR

This paper introduces a new formalization of finite group theory using explicit operation tables, enabling inductive proofs of key theorems like Lagrange's and Cauchy's, which were difficult with previous approaches.

Contribution

It presents an alternative formalization based on operation tables and a macro for generating groups, facilitating inductive proofs of fundamental finite group theorems.

Findings

Proof of Lagrange's Theorem within the formalization

Inductive proof of Cauchy's Theorem for abelian groups

Implementation of a 'defgroup' macro for group generation

Abstract

Previous formulations of group theory in ACL2 and Nqthm, based on either "encapsulate" or "defn-sk", have been limited by their failure to provide a path to proof by induction on the order of a group, which is required for most interesting results in this domain beyond Lagrange's Theorem (asserting the divisibility of the order of a group by that of a subgroup). We describe an alternative approach to finite group theory that remedies this deficiency, based on an explicit representation of a group as an operation table. We define a "defgroup" macro for generating parametrized families of groups, which we apply to the additive and multiplicative groups of integers modulo n, the symmetric groups, arbitrary quotient groups, and cyclic subgroups. In addition to a proof of Lagrange's Theorem, we present an inductive proof of the abelian case of a theorem of Cauchy: If the order of a group G is divisible by a prime p, then G has an element of order p.