Consider a set $A$ equipped with two binary relations $\le$ and $<$, related in the appropriate ways for the strict and non-strict version of an ordering. One might make different choices about exactly what axioms to impose, but some reasonable ones to choose from are:
- $\le$ is a preorder (or maybe a partial order).
- $<$ is irreflexive.
- $<$ is transitive.
- $x\le y$ and $y<x$ cannot both hold.
- If $x\le y$ and $y<z$, then $x<z$. Dually, if $x<y$ and $y\le z$, then $x<z$.
- If $x<y$, then $x\le y$.
- If $x<z$, then either $x<y$ or $y<z$.
In classical mathematics, strict and non-strict orders are usually interdefinable. (Edit: As Joel pointed out, this is only really true in the partial-order case.) Since this generally fails in constructive mathematics, the above abstract structure seems more likely to be interesting there. But even in classical mathematics there are interesting examples where $\le$ and $<$ don't determine each other in the naive way, such as the collection of transitive sets in ZFC with the relations $\subseteq$ and $\in$.
Has anyone defined an abstract structure like this? If so, what is it called?