We introduce the MMT language, which provides a simple and scalable Module system for the development of Mathematical Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation format that can represent the meta-theoretic foundations of mathematical and logical systems together with the represented knowledge itself and interlink the foundations at the meta-logical level. This ``logics-as-theories'' approach makes system behaviors as well as their represented knowledge interoperable and thus comparable.

Logic is the study of formal languages for propositions and truth. Logics are used both as a foundation of mathematics and as specification languages in mathematics and computer science. Since logic is intricately intertwined with the nature of mathematics, the question how to represent logics in our minds is a constant challenge to our understanding. And only when it is understood can we begin to answer the corresponding question about logic translations. At the same time logics are used to a large extent in computer science to reason about both mathematics and software systems.

We propose extensions and corrections of the syntax and semantics of OMDoc that are necessary to define a formal semantics of OMDoc theory graphs. Since OMDoc theories are also OpenMath content dictionaries, this provides a module system and rudimentary syntax checking for OpenMath.

Our proposal includes a new constructor for OpenMath objects that is needed in the context of this module system. Together with related, so far unpublished work, this contribution provides a formal semantics and full type checking for OMDoc theory graphs.

Although outsiders may get the impressions that mathematical practitioners form a homogeneous, unified community and share the same practice all over the world, they actually form various sub-communities that differ in their preferred notations, basic assumptions, and motivating examples. This heterogeneity can even be observed when looking at the foundation of mathematics. Here very large and relatively stable communities have formed in the late 19th and 20th century that differ in their basic assumptions about the nature of mathematics.