Order theory as a foundation of mathematics?

I know the followings kinds of formalization of mathematics:

• based on set theory (e.g. ZFC)
• based on type theory (e.g. the formalism of Coq proof assistant, as an advanced example)
• based on category theory (topoi theory)

Now (as I am developing the formalism in a book I am writing) I feel that math can be somehow formalized in order theory, because the set of subsets of an "universal" set is formalized as complete atomic boolean algebra.

Is it a right idea that all mathematics can be expressed in the language of order theory (probably with propositional calculus or with second order predicates)? Has any such work been done?

• ZFC can be considered as theory of sets ordered by inclusion. Axiomatically, this is done by considering a triple $(V, \leq, s)$ where $x \leq y$ for $x, y \in V$ is to be interpreted as inclusion between sets, and $s: V \to V$ as a "singleton" operator, interpreted as taking a set $x$ to a singleton set $\{x\}$. Then $x \in y$ is defined to mean $s(x) \leq y$. So ZFC can be presented in terms of axioms involving a relation $\leq$ and an unary operator $s$. This is done for example in Algebraic Set Theory. – Todd Trimble Apr 26 '15 at 21:10
• Coming at the topic from a different angle, one of the musings that came out of the investigations into higher category theory was some musings on negative category theory, and that suggested that in the place where we use the notion of "set", that the notion of "poset" (or better, "preordered set") may well be a better fit. Sets (or better, "setoids") are the special case where the ordering is invertible. (i.e. that $a \leq b$ implies $b \leq a$) – user13113 Apr 26 '15 at 21:24
• By the way, you'll almost surely not get a suitable formalization as a Boolean algebra. For one thing, there is no top element (the universal set is not itself a set, i.e., an element of itself, for all the usual reasons), and similarly there is no good way of taking complements, etc. You might try reading up on Algebraic Set Theory to see what sort of universal poset you do get. – Todd Trimble Apr 26 '15 at 21:49
• @Hurkyl: Google personalizes results. It's quite unfortunate since people think that "literally the first result on Google" is a universal thing, but it's quite far from the truth. – Asaf Karagila Apr 26 '15 at 21:52
• Something that is not exactly what you are talking about but nevertheless emphasizes order is Oliver Deiser's approach of not considering sets as the fundamental object but rather list, i.e., families with a well ordered index set. This works rather smoothly. Here is the reference: [O. Deiser, An axiomatic theory of well-orderings, Rev. Symb. Logic 4, No. 2, 186-204 (2011)] – Stefan Geschke Apr 27 '15 at 8:18

A partial order can be regarded as a specific example of a category with an arrow from $a \rightarrow b$ if $b \leq a$. Thus your formalism would be a subcase of the category theoretic approach.

• When a subcase is sufficient to describe the full theory, this proves a stronger result than for the supercase. So the question asks the other way round. – Tobias Schlemmer Mar 31 at 7:50