# Defining 'free monoid' without Nat?

Is there a definition of what is a 'free monoid' which does not pre-suppose that the natural numbers has already been defined? The definitions that I have been able to track down all use the natural numbers (since sequences/words need them).

In other words, I am trying to define the theory of free monoids (as a signature with sorts, operations and axioms), and I would like to know if I can do this without having the theory of the naturals already defined. For exhibiting/constructing a free monoid, I do expect to need Nat.

Note that my ambient logic is higher-order, so I am fine with a second-order axiomatization. If dependent-types are needed, that would also be acceptable.

-
Sure, by using the characterization of a free monoid by its universal property. Of course, supposing you are working in an extremely impoverished "set theory", in order to know that they exist, you need an axiom asserting the existence of Nat, since Nat is itself a free monoid. But I guess this isn't the answer you're looking for? – Reid Barton Mar 8 '10 at 16:34
I guess the question is does "theory [of free monoids]" mean something informal like "understanding", or did you have one of its technical definitions in mind? – Reid Barton Mar 8 '10 at 16:37
By "theory of free monoids" I meant an axiomatization, i.e. all the ingredients necessary to 'present' a free monoid. Existence is indeed a different matter, but at that point I am happy to assume Nat. I just would prefer to avoid Nat in my axiomatization, if it is possible. – Jacques Carette Mar 8 '10 at 17:47
Since freeness is not a first-order property, you will have a hard time defining the theory of free monoids. The theory of monoids with designated generators and induction as proposed by sigfpe is probably the closest you can get with a first-order theory. – François G. Dorais Mar 8 '10 at 23:35
@Jacques: If your underlying logic is powerful enough, then the universal property of free monoids is probably the way to go. This does not mention natural numbers at all. – François G. Dorais Mar 9 '10 at 5:16

As I pointed out in the comments, the theory of free monoids is somewhat ill defined. It is still unclear what your logic is and what you really want, but you have two basic options which were proposed by Pete Clark and sigfpe. Here are a few additional remarks that may help you sort things out.

Universal Property à la Pete Clark. The free monoid functor $F:Set\to Mon$ is left-adjoint to the forgetful functor $G:Mon \to Set$. This adjunction completely determines the isomorphism classes of free monoids. Moreover, many of the essential properties of free monoids follow directly from properties of sets and adjoint functors.

Alternately, the bijection between $Set(A,GB)$ and $Mon(FA,B)$ can be described as Pete Clark suggested, without any reference to adjoint functors. This latter option preferable if your logic can handle the categories $Set$ and $Mon$, but not functors between them.

The obvious advantage of this approach is that this is the true freeness property of free monoids (the fact that word monoids are free is nothing but an interesting accident from this point of view). Other than the fact that $F1$ is a natural number object, there is no mention of natural numbers here. However, I always thought that there was a lot of unnecessary tedium to show that free monoids can be viewed as word monoids in this context.

Induction Axiom à la sigfpe. The idea here is to attempt to capture freeness via induction. Here is a variant that fixes the minor problem I pointed out in a comment to sigfpe's answer -- free monoids are structures $(F,A,e,{\cdot})$ where $(F,e,{\cdot})$ is a monoid and $A \subseteq F$ (understood as a unary predicate) is a distinguished set of generators. The axioms to describe this setup are the usual monoid axioms together with the obvious modifications of sigfpe's two axioms

• $A(a) \land A(a') \land x\cdot a = x' \cdot a' \to x = x' \land a = a'$,
• $\forall P\,(P(e) \land \forall x,a\,(P(x) \land A(a) \to P(x\cdot a)) \to \forall x\,P(x))$,

where $P$ varies over all unary predicates $P \subseteq F$. In first-order logic, quantification over such $P$ is not possible and the induction axiom must be replaced by the corresponding induction scheme where $P$ varies over all formulas of the language instead. (In higher-order logics without predicate types, you can usually replace $P(x)$ by $f(x) = g(x)$ for appropriate $f$ and $g$.)

In the standard semantics for second-order logic, these axioms completely describe free monoids. However you must be careful since not all formulations of higher-logic are equal. Much like first-order logic, some of these formulations will implicitly allow for models of the above theory which are not free in the categorical sense. In truth, this is unlikely to be a problem for you but I am compelled to warn you of this possibility.

-
Excellent! This is definitely what I was looking for. FYI, the logic I use is Chiron, designed by William M. Farmer, for the purposes of doing 'mechanized mathematics'. See imps.mcmaster.ca/doc/chiron-tr.pdf. – Jacques Carette Mar 9 '10 at 14:37

Well, yes. You define it in terms of its universal mapping property: the free monoid on a set $S$ is a monoid $FM(S)$ and a set map $\iota: S \rightarrow FM(S)$ such that for any monoid N and set map $f: S \rightarrow N$, there exists a monoid map $F: FM(S) \rightarrow N$ such that $f = F \circ \iota$.

This definition doesn't mention natural numbers at all. A construction of $FM(S)$ might involve sequences, but this could probably be avoided, e.g. by applying some general nonsense to show that the forgetful functor from monoids to sets has a left adjoint.

Or is this not what you had in mind?

-
This is definitely closer to what I had in mind. I am indeed expecting that the construction of most(?) free monoids will require sequences, but I was hoping that the theory of free monoids would not. – Jacques Carette Mar 8 '10 at 17:45
You might enjoy George Bergman's book "An Introduction to General Algebra and Universal Constructions" which talks about these things quite thoroughly. – Pace Nielsen Mar 8 '10 at 18:44
@Pace: thanks, I'll look it up. – Jacques Carette Mar 9 '10 at 3:09

Could we mimic the definition of a list in a programming language?

So if you want $M$ to be the free monoid on $A$ you can say $M$ is a structure equipped with a function $m:A\times M\rightarrow M$ and an identity element $e\in M$.

You'd have some axioms like $m(x,y)=m(x',y')$ iff $x=x'$ and $y=y'$.

You'd also need some kind of inductive axiom. So for any property $P$, if we have ($P(e)$ and $P(x)\Rightarrow\forall a P(m(a,x))$ ) then $\forall x P(x)$.

This inductive axiom now implies that the elements of $M$ are finite strings of elements of $A$, and we can define the usual monoid multiplication the way we'd append two lists in a programming language. The inductive axiom should guarantee that appending is well-defined.

-
I don't think this quite works. For one, your axiom will not work since m(x,e) = m(e,x) for all x; you would have to replace that axiom by a guarded axiom. The property idea is nice. Although isn't this a rephrasing of 'no junk, no confusion', which I asked about some days ago? [The axiom mimics 'no confusion', and the property is a sort of 'no junk']. My problem is how to make this generic (free X structure) -- Pete Clark's universal property seems to be generic once I have X-morphisms defined. – Jacques Carette Mar 8 '10 at 19:38
Note that m is not the monoid multiplication. In general, there is no m(e,x). m takes an element of the generating set on the left and an element of the monoid on the right. You define the usual monoid multiplication in terms of m. So I think your objection doesn't stand. Where else do you think my approach might fail? – Dan Piponi Mar 8 '10 at 19:47
I think this is the closest to an axiomatization of free monoids. The only problem is that I don't think that monoid multiplication ${\cdot}:M \times M \to M$ is definable, so it probably needs to be introduced as a formal operation to ensure that $M$ really is a monoid. – François G. Dorais Mar 9 '10 at 0:16
@sigfpe: I misunderstood, thanks for the clarification. Defining the monoid multiplication (recursively) as a generalized 'append' will require a finiteness assumption for termination. Isn't that Nat sneaking back in? – Jacques Carette Mar 9 '10 at 3:26
Elements of free monoids are lists from a set. The proof assistant Coq gives a way to reason about lists. So I have just tried to copy the axioms Coq gives you if you define a list type. These axioms don't involve the naturals in any direct way. So I'd be surprised if it wasn't possible to make something along these lines work. As for Nat sneaking back in. Well it must, mustn't it? The free monoid on a single generator is the naturals. So surely you expect to be able to find the naturals in there. – Dan Piponi Mar 9 '10 at 17:40

I am not this is what you want, but there is an old theorem of Levi that a monoid is free iff

1. It is cancellative.
2. It has only trivial group of units.
3. It is equidivisible (you can google the definition; the key thing is that it is first order).
4. There are only finitely many principal right ideals containing any given principal right ideal.

1-3 are first order. Probably 4 is a problem for what you want.

-
4. definitely quantifies over sets-of-sets, so not first order. But it is nevertheless interesting, thanks. – Jacques Carette Jun 28 '11 at 23:10

Can you give a good example of this in another instance?

The Wikipedia definition seems to imply that if you do not have natural numbers defined yet, they follow as the lengths of the finite strings.

In particular, given any Free Monoid, the unique word length function maps elements of that monoid into the natural numbers.

-
The definition of 'word' uses finite strings, which are functions from Nat to the alphabet. – Jacques Carette Mar 8 '10 at 17:39