What are the interesting models of this theory other than those of ZFC + (V=L)?

Question

Language: first order logic with equality, plus primitive binary relations: $=,\in, <$

Axioms:

1. Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$

2. Well ordering: $<$ is a well ordering on the universe

3. Membership: $x \in y \to x < y$

4. Replacement: if $\phi(x,y)$ is a formula in which $x,y$ are free that doesn't have the symbol $B$ free, then all closures of: $$ \forall A [\forall x < A \exists! y( \phi(x,y)) \to \\\exists B \forall y (y \in B \leftrightarrow \exists x < A: \phi(x,y))]$$; are axioms.

5. Infinity: $\exists x: \exists y (y < x) \land \forall y < x \exists z (y < z < x)$

6. Successor cardinals: $\forall x \exists y: |y| > |x|$

Where, well ordering is the schema:

$x < y \to y \not < x \\ x < y < z \to x < z \\ x \neq y \leftrightarrow [x < y \lor y < x] \\ \exists x \phi(x) \to \exists x \phi(x) \land \forall y (\phi(y) \to x \leq y)$

\theory definition finished.

Now my guess is that all models of $ZFC + (V=L)$ are models of this theory!

What are the examples of interesting models other than those of $ZFC+(V=L)$ can be models of this theory?

I've first posted this theory to Mathoverflow when I came to know that fine structural models can be an example of such models, but I transferred this topic here, because I think it is not research level question. Are there other known interesting models of this theory?

Answer 1

First, note that it's not quite right to say that all models of ZFC+V=L - or more generally, ZFC + "$V=HOD[x]$ for some $x$" - is a model of your theory; rather, any such model has a natural expansion to a model of your theory (the point is that we have to talk about expansions since the languages are different).

But "natural" expansions aren't the only kinds of expansions. Working in some $M\models$ ZFC, use the proper class forcing of partial well-orderings of set-sized fragments of the universe. The expansion $(M,\triangleleft)$ will satisfy your theory.

So your theory is conservative over ZFC in the strong sense that any model of ZFC can be expanded to a model of your theory. $V=HOD[x]$ comes in when we try to get a "natural expansion" - that is, where we want $\triangleleft$ to in fact be a class in the sense of $M$ - but isn't truly necessary.

---

Interestingly, replacement plays a crucial role here.