I asked (and also answered) a more general version of this question a while ago. To summarize the answer, some results of Kanovei and Shelah have the following corollary:
Fact. In $\mathsf{ZFC}$ there is a uniform procedure for building 'set-saturated,' class-sized elementary extensions of arbitrary structures. That is to say there are formulas $S(M,L,x)$ and $F(M,L,f,x)$ in the language of set theory such that in any model $V \models \mathsf{ZFC}$ if $L \in V$ is a language and $M \in V$ is an $L$-structure, then the following hold (where $M^\ast = \{x \in V : V \models S(M,L,x)\}$):
- $M \subseteq M^\ast$,
- if $\varphi \in V$ is an $L$-formula with free variables $x_0,\dots,x_n$ and $\bar{a} \in M^\ast$ is an $n$-tuple, then $V \models F(M,L,\exists x_n\varphi,\bar{a})$ if and only if $V \models (\exists x \in M^\ast) F(M,L,\varphi,\bar{a}x)$ (where we are using some fixed coding of tuples in $\mathsf{ZFC}$),
- furthermore, if $\bar{c} \in M$ is an $(n+1)$-tuple, then $V \models F(M,L,\varphi,\bar{c})$ if and only if $V \models “M \models \varphi(\bar{c})”$ (in particular, if $\varphi$ is a sentence, then $V \models F(M,L,\varphi,\varnothing)$ if and only if $V \models “M \models \varphi”$),
- $F$ is compatible with Boolean combinations (i.e., $V\models F(M,L,\varphi\wedge \psi,\bar{a})$ if and only if $V\models F(M,L,\varphi,\bar{a})\wedge F(M,L,\psi,\bar{a})$, etc.), and
- if $A \subseteq M^\ast$ is a set and $p(x)$ is a finitely satisfiable set of $L_A$-formulas with free variable $x$, then there is $b \in M^\ast$ such that for any $\varphi(x,\bar{a}) \in p(x)$, $V \models F(M,L,\varphi,b\bar{a})$.
So to state it informally, $S(M,L,x)$ defines the universe of a class-sized elementary extension of $M$ and $F(M,L,f,x)$ is its truth predicate.
Applying this to the naturals tells us that there is a formula that defines a proper class monster model of $\mathrm{Th}(\mathbb{N})$ in any model of $\mathsf{ZFC}$.
One thing to note, though, is that without global choice (which makes my original question trivial), it's unclear whether there's always a definable isomorphism between different set-saturated class-sized models of a given theory. I believe this is related to an unanswered MathOverflow question of Hamkins. That said, if $M$ and $N$ are $L$-structures and $M \equiv N$, then there will be an isomorphism between $M^\ast$ and $N^\ast$ that is definable with certain parameters.
Another thing to note is that some constructions that model theorists commonly use with the monster model are unclear in the context of these class monster models. There isn't necessarily a good way to talk about arbitrary global types, for instance. You do, however, get a good homogeneity property: There is a subgroup $G$ of $\mathrm{Aut}(M^\ast)$ that can be represented as a class in a definable way which has the property that if $\bar{a}$ and $\bar{b}$ are set-sized tuples that realize the same type, then there is a $\sigma \in G$ such that $\sigma \bar{a} = \bar{b}$.
Best Answer
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
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.