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?