Strict and non-strict orderings

Question

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:

1. $\le$ is a preorder (or maybe a partial order).
2. $<$ is irreflexive.
3. $<$ is transitive.
4. $x\le y$ and $y<x$ cannot both hold.
5. If $x\le y$ and $y<z$, then $x<z$. Dually, if $x<y$ and $y\le z$, then $x<z$.
6. If $x<y$, then $x\le y$.
7. 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?

Answer 1

This doesn't really answer your question, but I don't agree with your statement that $\leq$ and the associated $<$ are usually interdefinable in classical mathematics. To my way of thinking, the question isn't one of classical logic vs. constructive logic, but simply whether you have a partial order or a pre-order.

Although $\leq$ and the associated strict order $<$ are indeed interdefinable for partial orders $\leq$, this is never true for pre-orders that are not partial orders. Indeed, for every pre-order $\leq$ that is not a partial order (that is, not anti-symmetric) there is another partial order $\leq'$ with the same strict order $<$. In $\leq'$, just let the $\leq$-equivalence classes become little antichains, instead of clusters of equivalent nodes.

For example, consider the difference between the relations: $a\leq b$ iff $b$ is at least as tall as $a$, versus $a\leq' b$ iff $b$ is strictly taller than or equal to $a$.

I often teach logic to philosophy students, and I always have a section on relational logic, where we also study the various order concepts. One main point I make is that philosophically natural orders, such as preference relations or reduction concepts, tend generally to be pre-orders rather than orders. It follows that most philosophical principles or axioms concerning such orders should be stated in terms of the pre-order rather than in terms of the strict order, since the strict order is definable from the pre-order but not conversely. The pre-order is the fundamental relation and not the strict order.

Some of my papers on the subject of infinite utilitarianism, for example, which are based on the preference relations on infinite worlds, mount criticisms of axioms that had been stated in terms of the strict order, when in my view they should have been given in terms of the pre-order relation, a more fundamental relation. We use this descrepancy to give counterexamples to the proposed principles, and explain that if the axioms had been stated in terms of the pre-order, things would have worked out better.

• pre-order = reflexive + transitive

• partial order = reflexive + transitive + anti-symmetric ($x\leq y\leq x\to x=y$)

Answer 2

Here is an example, which I think is similar to what you are asking for.

A graded digraph is a structure $\langle A,\rightharpoonup,\leq\rangle$, where $\langle A,\rightharpoonup\rangle$ is a digraph and $\leq$ is a linear pre-order on $A$, such that $a\rightharpoonup b$ implies $a<b$, using the strict version $<$ of the linear pre-order $\leq$.

The digraph relation might be a (strict) partial order relation. The grading order $\leq$ effectively lays out the elements of $A$ on levels, such that all edges in the digraph climb from a lower level to a higher level.

Thus, the digraph part of a graded digraph must be acyclic, and indeed, every acyclic digraph can be graded in ZFC, since if $\rightharpoonup$ is an acyclic digraph relation on $A$, then the reachability relation, the reflexive transitive closure of $\rightharpoonup$, is a partial order, which extends to a linear order, which provides the desired grading.

Grading is important in the class of acyclic digraphs, because of the fact that the collection of acyclic digraphs does not have the amalgamation property and so lacks a Fraïssé limit. The collection of graded digraphs addresses this because when one adds the gradings, it does have the amalgamation property. The Fraïssé limit of all finite $\mathbb{Q}$-graded digraphs is the countable random $\mathbb{Q}$-graded digraph, which I introduced in my paper J. D. Hamkins, Every countable model of set theory embeds into its own constructible universe, J. Math. Log., vol. 13, iss. 2, p. 1350006, 27, 2013. This graph enjoys similar saturation, homogeneity and universality properties as the countable random graph, but with respect to acyclic graded digraphs.

You can construct a copy of the countable random $\mathbb{Q}$-graded digraph by giving yourself a level of countably many nodes for each rational number, and then for any pair of nodes on different levels, flip a coin to see if there is an edge from the lower node to the upper node. The resulting graded digraph exhibits the finite-pattern property and therefore is almost surely isomorphic to the countable random $\mathbb{Q}$-graded digraph.

In that paper, the main proof used an analogue of the countable random $\mathbb{Q}$-graded digraph to the case of proper class digraphs, using the surreal numbers in place of $\mathbb{Q}$. The result is what I called the hypnagogic digraph, which is a proper class surreals-graded digraph with the set-pattern property, which ensures the desired saturation and universality properties.

Answer 3

An answer in the opposite direction (helpfully meant, for completing the picture):

In 'old-fashioned' constructive mathematics, the set $A$ already has an apartness $\#$.

Then we have: $x<y\leftrightarrow (x\leq y\wedge x\# y)$ and $x\leq y\leftrightarrow \forall z\, [\,z<x\rightarrow z<y\,]$.

So there is always a sensible way to express $\leq$ in terms of $<$, and the necessary information to express $<$ in terms of $\leq$ is precisely the apartness $\#$.

[Addition for completeness: if we have $<$, and it is a 'total' relation in the sense that $(\neg(x<y)\wedge\neg(y<x))\rightarrow x=y$, then we can define $x\# y\leftrightarrow(x<y\vee y<x)$, and the above also still holds.]

---

[Update to incorporate some exchange in the comments below:]

In constructive mathematics usually the symbol $<$ is used for a relation where $x<y$ indicates constructive existence of numerical/finitary evidence that $x$ and $y$ are apart in some sense, and order-comparable. The symbol $\leq$ usually is derived from $<$, for total orders most often I believe by defining $x\leq y\leftrightarrow \neg(y<x)$. This usually amounts, quantifier-wise, to for all.

The alternative $x\leq y\leftrightarrow \forall z\, [\,z<x\rightarrow z<y\,]$ mentioned above also uses for all, not surprisingly.

In intuitionistic mathematics, for expressing $<$ in terms of $\leq$ without using an existing apartness, perhaps we could turn to the strong intuitionistic interpretation of the logical connective $\vee$. Then, without using an existing apartness, we can define:

$$(*)\ \ \ \ x<y\leftrightarrow \,\forall z\,[\,(z\leq y\wedge \neg(y\leq z))\vee (x\leq z\wedge \neg(z\leq x))\,]$$

I'm moderately optimistic that this definition will satisfy the specified axioms in many situations, like the real numbers for example.

One might think the quantifier $\forall$ in contrast to what is stated earlier, but it helps to read $(*)$ as $ x<y\leftrightarrow \,\forall z\,\exists i\in\{0,1\}[\,(i=0\wedge z\leq y\wedge \neg(y\leq z))\vee (i=1\wedge x\leq z\wedge \neg(z\leq x))\,]$

Answer 4

Floris van Doorn pointed out to me that such a definition of an "order pair" was used in version 2 of the Lean library of formalized mathematics. (In version 3 it was replaced by a definition -- using classical logic -- which defines one in terms of the other.) The definition is here; it says that $\le$ is a partial order (axiom (1)) and the axioms (2), (5), and (6) from the question hold.