Edit: I didn't know about the Löwenheim–Skolem theorem when I wrote this question. I'm going to leave it, though, because I find some of the comments to be helpful.
Let $(X,\sigma,\prec)$ be a structure satisfying the following:
$1.\qquad \exists o.o\in X$
$2.\qquad \forall x\in X.\sigma(x)\in X$
$3. \qquad \forall x\in X. x\prec\sigma(x)$
$4. \qquad \forall x,y \in X. x\prec y\implies x\ne y$
$5. \qquad \forall x,y,z \in X. x\prec y \land y\prec z\implies x\prec z$
Prove
$A\qquad(X,\prec)\cong(\omega,\in)$
$B\qquad\nexists\beta\in\mathbf{Ord}.((X,\prec)\cong(\beta,\in))\land(\beta\ne\omega)$
As far as I am aware (I tried coding it in MetaMath, but it didn't work) it is not possible to prove either $A$ or $B$ from $1,\ldots,5$. In fact, the extent of $X$ should be ambiguous since there is no upper bound on the set "$X$ such that $X$ is inductive" - which, as far as I can tell, is exactly the structure being described (by way of $\sigma(x)=x\cup\{x\}$).
I believe that two additional conditions would be necessary in order to prove $A$, these being:
$6.\qquad\nexists x\in X.o=\sigma(x)$
and
$7.\qquad \forall y\in X\setminus\{o\}.\exists x\in X.y=\sigma(x)$
$B$ could be proven from $A$ iff $o=\emptyset$; otherwise $B$ is consistent with $1,\ldots,7$ for $o=\lambda$, for any limit ordinal $\lambda$.
Is this correct, and if not, what additional conditions must be met in order to prove $A$ and $B$?
Note: I have no idea what "constructive mathematics" actually is, I'm only using the term "constructively" in the title based on what I can infer about its meaning from how others have used it. If "constructive" isn't the appropriate term to describe what I am doing, please correct it.