Embedding a linearly ordered free monoid into a linearly ordered group A linearly ordered (shortly, l.o.) monoid is a triple $\mathbb M = (M, \cdot, \le)$ for which $(M, \cdot)$ is a (multiplicatively written) monoid and $\le$ is a total order on $M$ such that $xy < xz$ and $yx < zx$ for all $x,y,z \in M$ with $y < z$. In particular, $\mathbb M$ is called an l.o. group if $(M, \cdot)$ is, well, a group, and an l.o. free monoid if $(M, \cdot)$ is the free monoid on an alphabet $X$.
What is known about the following question?


(Q) Let $\mathbb M = (M, \cdot, \le)$ be a linearly ordered free monoid. Does there always exist an embedding of $\mathbb M$ into a linearly ordered group? In more plain words: do there always exist a linearly ordered group $\mathbb G = (G, \cdot, \le)$ and a (monoid) monomorphism $f: (M, \cdot) \to (G, \cdot)$ such that $f(x) < f(y)$ for all $x,y \in M$ with $x < y$?


The answer is affirmative in the case when $\le$ is the lexicographic order induced on $M$ by any well-ordering of the underlying alphabet (this can be proved, e.g., by the "Magnus trick"). 
But what about the rest? Any reference?
 A: I suspect this is false, although I don't have a proof. The Thompson group $F$ is generated by $A, B$, which are piecewise-linear homeomorphisms of the interval which change slope at dyadic points, and piecewise have slopes in $2^\mathbb{Z}$. As described in Theorem 4.6 of Cannon-Floyd-Parry, the submonoid generated by $A,B$ is free. The group is linearly ordered (called bi-ordered in the literature), and the spaces of bi-orderings has been classified. I suspect that some of these bi-orderings, when restricted to the submonoid generated by $A, B$, do not extend to the free group generated by $A, B$. I would try one of the 8 isolated bi-orderings of the Thompson group, and see if it can be extended to the free group generated by $A,B$. If it can't, then one can detect this in a ball of finite-radius in the free group. 
A: It suffices to show this for l.o. free monoids on finite alphabets, as follows from the Compactness Theorem in logic - which can be found in any text on First Order Logic. [This principle can be applied to a range of similar problems.]
Indeed, let $\mathbb M = (M, \cdot, \le)$ be a linearly ordered free monoid on the alphabet $X$, and consider the first-order language $\mathcal{L} = (\circ, \preceq, \{x_m|m \in M\})$ consisting of a binary function symbol $\circ$ to represent multiplication, a binary relation symbol $\preceq$ representing ordering, plus an individual constant symbol $x_m$ for each element $m$ of the set $M$.
Then let $T$ be the $\mathcal{L}$-theory having the following axioms:


*

*the usual axioms for linearly ordered groups, expressed using
$\circ$ and $\preceq$

*$x_m \ne x_n$ for all $m, n\in M$ with $m\ne n$ [these axioms ensure
that $M$ naturally injects as a subset of any model of $T$ via the
interpretation of the $x_m$ constants]

*$x_m \preceq x_n$ for all $m, n\in M$ with $m\le n$ [these make this
injection an embedding of l.o. sets]

*$x_m \circ x_n = x_{m\cdot n}$ for all $m, n\in M$ [which make the
embedding a monoid homomorphism].


So any model $\mathbb G = (G, \cdot, \le, \{g_m|m \in M\})$ of $T$ will provide a desired l.o. group, with $m\mapsto g_m$ (being the interpretation of the constant $x_m$ in $\mathbb G$) giving the desired embedding $\mathbb M\to \mathbb G$. And conversely.
By the Compactness Theorem, the theory $T$ admits a model iff every finite subset $\Delta$ of the axioms of $T$ does. Now only finitely many symbols $x_m$ can occur in sentences belonging to such a $\Delta$, and the finitely many elements $m\in M$ so involved can be expressed as words in a finite subalphabet $Y\subseteq X$. This $Y$ generates a l.o. free submonoid $\mathbb S$ of $\mathbb M$ that contains all the $m\in M$ for which $x_m$ figures in statements occurring in $\Delta$. And so any l.o. group that "extends" $\mathbb S$ (in the sense of the OP) will be a model of $\Delta$.
Hence it is enough to consider free l.o. monoids on finite alphabets.
[Incidentally, by the same token, if all finitely generated free groups are linearly orderable, so are all free groups.]
