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?

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 youdoget. – Todd Trimble♦ Apr 26 '15 at 21:49