The $\mmath$-language

To reach the objectives, the idea came up to develop a formal language providing ways to both formulate models in an intuitive way and to work rigorously with the fomal rules of logical arguing.

This language is not defined in terms of its surface syntax, which remains variable. Instead, its syntax is defined in terms of an abstract definition of the language constructs, their combinations and interactions. The concrete surface syntax may be altered for different purposes.

Compared to many other formal systems the $\mmath$-language is not based on any type theory (like intuitionistic type theory or the calculus of construction), since this would not reflect students' everyday experience with mathematics making the language inappropriate for use in beginner courses. In order to represent the structure of a common lecture, a text written in the $\mmath$-language is basically made up of a sequence of definitions of objects and proofs about their properties.

Proofs and definitions in $\mmath$ are summed up under the term action, since they have a strongly imperative character. This resembles the usage of these concepts throughout lectures, where things are defined or proven to use them later on. An action can use all previously defined names and proven statements, the so called context in which it is embedded. The semantic correctness of an action is determined by the initial context it is embedded into. If an action is correct, it modifies the current context in terms of adding new names or new valid statements. As a result of this context dependence also the order of actions play an important role for the validity of a $\mmath$-text.

The semantics of the $\mmath$-language describes under which requirements on its initial context an action is supposed to be correct and in which way it then modifies this context. There are several actions which reflect the different kinds of proofs students are taught (like direct proof, proof by contradiction,...).

In order to reflect the importance of modeling on the object level, the $\mmath$- language uses the model as its fundamental construct. A model is made up of a list of names for abstract objects (the model parameters) and a list of assumptions which describe properties of and relations between those objects. In addition, a conclusion section may collect statements which follow from the assumptions. An object $x$ is said to fulfill the assumptions (and then also the conclusions) of a model $A$ (in a given context) if $x$ is a list with as many entries as $A$ has parameters and if, after replacing them by the entries of $x$, all assumptions of $A$ are valid statements (in this given context).

Apart from the list of assumed and concluded properties of the model parameters (the model intension), a model $M$ also possesses an extension which, in the simplest case, consists of the collection of all objects satisfying the assumptions. In general, the extension is generated by inserting the admissible objects into an additional expression of the model parameters and collecting the results. Obviously, this return value adds a function-like behavior to models: By applying $M$ to an admissible object $x$, one can get the return value $M(x)$ of $M$ for the specific value $x$. The simple case is recovered for identity-type return values $M(x)=x$.

The fundamental statement that an object $x$ belongs to the extension of a model $M$ is denoted $x:M$. In case of identity-models this is the case if $x$ fulfills the assumptions of $M$. In particular, such models have a set-like meaning with the "$:$"-relation resembling the "$\in$"-relation. If a statement of the form $x:M$ is proven or assumed, then automatically all $M$-intensions instantiated with $x$ become valid too.

Since models itself can be objects, there is the danger of inconsistencies like Russell's paradox. To avoid them, not all models may be labeled as objects. For this purpose the semantics of the $\mmath$-language also includes rules when a model may be considered to be an object.

Another important mathematical concept implemented in the $\mmath$-language are implicit conditions. These occur, for example, when assumptions contain evaluation terms $F(x)$ which are valid only if $x$ fulfills the conditions of $F$. With the convention that all terms appearing in assumptions are valid, the admissibility of $x$ as argument of $F$ is implicitly assumed. But for futher arguing ths implicit assumption has to be available. Hence the semantics of the $\mmath$-language contains rules for handling those implicit assumptions.

For a deeper insight into the details of the $\mmath$-language see the upcoming documentation section.