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?

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$)

  • 2
    I suppose this is fair. As a category theorist, I generally treat preorders as categories, up to equivalence, so that they are equivalent to their preorder reflection. But I suppose if you're treating them differently then the difference matters. However, I do think this should have been a comment or chat discussion rather than an Answer. – Mike Shulman Nov 22 '17 at 13:52
  • Wouldn't the issue I raise apply no matter how you consider pre-orders? The point is that you cannot generally recover the pre-order from a strict order, when it arises from a pre-order that is not a partial order, since it also always arises from a partial order (where the equivalence classes are made into antichains). This would happen also with a category-theoretic treatment, as I understand it. Meanwhile, you can always recover a partial order from its strict order and vice versa. – Joel David Hamkins Nov 22 '17 at 13:57
  • I'm sorry to have posted the answer if you find it inappropriate. I can delete it. I think my other answer is likely closer to what you are asking about. – Joel David Hamkins Nov 22 '17 at 13:57
  • 2
    I mean that when I have a preorder I consider equivalent objects to be indistinguishable, and I don't forget their indistinguishability when I consider the associated strict order. So it doesn't make sense to make the equivalence classes into antichains. – Mike Shulman Nov 22 '17 at 14:00
  • 2
    Would you also say that I don't really have a concept of category, but only of skeletal category? – Mike Shulman Nov 22 '17 at 14:09

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.

  • 1
    Hmm... so is the point that in classical mathematics, even though there are examples where $<$ and $\le$ aren't defined from each other, we can still regard them as both strict or both non-strict and thus consider the structure as a relationship between two preorder relations? – Mike Shulman Nov 22 '17 at 13:55
  • 1
    No, rather, every pre-order relation $\leq$ determines its strict order $<$, so we can refer to the strict relation whenever we have a pre-order $\leq$. We cannot do so conversely, because $<$ does not determine $\leq$. – Joel David Hamkins Nov 22 '17 at 14:04
  • 1
    I guess that your $\rightharpoonup$ is my $<$? Then of my axioms (now numbered above) it seems that 1, 2, 4, and 6 hold, plus linearity of $\le$, and any of my structures satisfying these properties is a graded digraph? That's progress, although the axiom that's most characteristic of my examples is #5, which doesn't seem to hold for a graded digraph. – Mike Shulman Nov 22 '17 at 14:05
  • 1
    Note that I split one of the axioms in two at the same time that I assigned numbers to them. So the axiom that was the fourth bullet point is now #5. – Mike Shulman Nov 22 '17 at 14:40
  • 1
    Ah, I had made my (now deleted) comment before you numbered your axioms. I agree that axiom 5 is not generally true for graded digraphs. – Joel David Hamkins Nov 22 '17 at 15:03

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))\,]$

  • Thanks! Note, though, that your expression for $\le$ in terms of $<$ fails in the case of transitive ZF-sets with $\subseteq$ and $\in$ that I mentioned in the question. In that case you need the opposite version. For surreal numbers, I think neither version works; maybe the conjunction of both would, although in that case I think you still need to define $\le$ mutually with $<$ even if it can afterwards be expressed in terms of it. And neither of these examples has an apartness. – Mike Shulman Mar 31 at 18:09
  • Yes, I was really only talking about the traditional constructive setting, knowing that your question is meant more broadly. Still, for your example of transitive sets, I don't understand your remark since surely $x\subseteq y\leftrightarrow \forall z\, [\,z\in x\rightarrow z\in y\,]$ ? – Frank Waaldijk Mar 31 at 19:36
  • Oh, somehow I misread your definition as saying $\forall z [ y < z \to x < z]$, I'm not sure how I did that. But anyway, the point is that neither choice is always going to be the right one. I'm not sure what you mean by "the traditional constructive setting" -- certainly your definitions of $<$ and $\le$ in terms of each other are true for some sets $A$, but I don't see how a choice of "setting" could ensure that they would be true for all such sets. – Mike Shulman Mar 31 at 21:40
  • I will turn it around: please give me an example of $<$ and $\leq$ where my characterization fails... because I cannot easily think of one. Such an example must involve the existence of two elements which have precisely the same order properties w.r.t. all other elements, and yet are distinct. It would surprise me if this is possible for interesting intuitionistic spaces, but never say never I guess... – Frank Waaldijk Apr 1 at 5:37
  • An easy example is to take any set $A$ with a strict order $<$ (like $\mathbb{R}$) and define $x\le y$ to be true always. This satisfies all the axioms listed in the question except #4 (with #1 being a preorder rather than a partial order), but $<$ and $\le$ are not definable in terms of each other. – Mike Shulman Apr 1 at 7:37

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.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.