Say that a Positive Group is a poset $(G,\geq)$ with an operator $\cdot$ s.t.
(Closure) For all $a, b \in G$ we have $a \cdot b \in G$
(Associativity) For all $a, b, c \in G$ we have $a \cdot (b \cdot c) = (a \cdot b) \cdot c$
(Identity element) $\exists e \in G$ s.t. $\forall a \in G$ we have $a \cdot e = e \cdot a = a$
(Divisibility) For all $a, b \in G$ s.t. $b \geq a$, $\exists c$ s.t. $a \cdot c = b$
First question: I made up the name "Positive group". Is there a more standard name for this?
Second question: We can add the following axiom to get something we might term Strictly Positive Group:
(Non-invertability) For any $a\neq e \in G$, $\nexists b$ s.t. $a \cdot b = e$
Is there a standard name for what I am calling a "Strictly positive group".
The basic idea here is that we want to modify the definition of a group so that combining two elements always leads to a larger elements.
$(\mathbb{Z}, +)$ is a group. $(\mathbb{N},+)$ is a strictly positive group.
$(\mathbb{R_+}, *)$ is a group. $( \{ x\in\mathbb{R}|x\geq1 \},* )$ is a strictly positive group.
Third question: Suppose we have a set $G$ with an operator $\cdot$. Let $X$ be some subset of $G$. Let $-X$ denote the set of all inverses of the elements of $X$.
Conjecture: If $X \cup -X$ is a group, then $X$ is a positive group and $X \setminus -X$ is a strictly positive group.
Is this a known result?