Classes of mathematical structures abound in modern math. Examples include:
- The class of all groups.
- The class of all partially-ordered sets.
- The class of vector spaces.
- The class of ordered fields isomorphic to $\mathbb{R}$.
- The class of all metric spaces.
- The class of all topological spaces.
- The class of all measurable spaces.
- The class of all probability spaces.
These classes can be described via a sequence of increasingly expressive specification languages.
- Equationally definable.
- Definable as a set of first-order sentences.
- Definable as a set of first-order sentences in multiple sorts.
- Definable as a set of first and second order sentences.
- Definable as a set of first and second order sentences in multiple sorts.
- [Don't know].
- [Don't know].
- [Don't know].
Is there a specification language that covers all of the above structures? I also want partial functions to be available e.g. for reciprocation in fields. Basically, something that covers all structures encountered in a typical undergraduate curriculum.
Note that vector spaces over fixed field can be defined as first order structures. Topological spaces can be made first order in multiple sorts (see (Why) is topology nonfirstorderizable?). The same approach should work for measurable spaces and probability spaces (however for probability spaces there is a problem with fixed concrete object $\mathbb{R}$ like for metric spaces so this may get you to second order). Can you write or give link to the multisorted second order axiomatization of metric spaces?
For partial functions in a signature, you can probably add their domains as new sorts and define the structure as first order multisorted. However structures allowing partial functions can be formalizes directly. There are „partial algebras“. Note that a category is just kind of partial monoid.