Finite products in commutative monoids: well-definition, recursion on finite subsets, and why the empty product is $1$

TL;DR

This paper justifies the convention that the empty product equals 1 in commutative monoids, using various structural and algebraic approaches, and discusses related concepts like empty sums and extensions to other algebraic structures.

Contribution

It provides a self-contained, formal proof of the empty product being 1 in commutative monoids, with multiple independent justifications and universal formulations.

Findings

Constructs finite set products and proves enumeration independence.

Shows the empty product is uniquely characterized by a recursion scheme.

Discusses extensions to trace monoids, heaps, and applications in various fields.

Abstract

The convention "empty product $=1$" is ubiquitous in mathematics, but often appears without an explicit structural justification. This note provides a self-contained reference to this fact in the context of commutative monoids. We construct the product of an indexed family by a finite set, prove its enumeration independence, and show that it is uniquely characterized by a recursion scheme in Fin$(I)$: value in the empty set and insertion rule of a new index. In particular, the value of the empty product is necessarily the neutral element $1$. We further record two complementary and independent justifications of this fact: one via the list-free monoid and another via distributive identities in semi-rings. Next, we formulate the same phenomenon in universal terms by means of the commutative multiset-free monoid of finite support. We also discuss partially commutative extensions, via trace monoids and heaps, and include brief applications in linear algebra, survival statistics, category theory, and analysis. The corresponding additive version recovers, by the same principle, the identity "empty sum $=0$".