In ordinary universal algebra, we consider only equational axioms like $$x + y = y + x, \qquad x + -x = 0.$$
There's a generalization of universal algebra in which quasi-equations are permitted, which are basically implications between finite conjunctions of equations. For example, the notion of a cancellative monoid can be axiomatized by quasi-equations; the left-cancellation law is $$ax = ay \rightarrow x = y$$
It seems reasonable to consider a variant on this in which inequalities are also fair game. For example, to axiomatize integral domains, we might use an appropriate cancellation law: $$a \neq 0 \wedge ax = ay \rightarrow x = y.$$
Alternatively, we could use a version of the null-factor law: $$ab = 0 \wedge a \neq 0 \rightarrow b = 0.$$
I envisage that the morphisms between models would be taken as injective homomorphisms. Such categories won't usually have products or a terminal object, though they'll often have an initial object and/or coproducts.
Here's an example of how such categories might be useful.
Definition. A non-degenerate Peano structure consists of a triple $(X,S,0)$ where $X$ is a set, $S :X \rightarrow X$ is an injective function, $0 \in X$ is an element, and $\forall x \in X(S(x) \neq 0)$ is assumed to hold.
The informal statement that every non-degenerate Peano structure contains a natural copy of $\mathbb{N}$ can be formally stated as "$\mathbb{N}$ is the initial non-degenerate Peano structure."
Question. Can any interesting results be proved for category of models of "quasi-equations with negation", where the morphisms are taken to be injective homomorphisms?