An internal model of mathematical practice for interactive systems of theorem proof construction. Part 2. A mathematical dialect model

A formal model of the mathematical dialect is described. The mathematical dialect is the language used in the mathematical practice to prove mathematical statements. Its model is a formal language whose syntax, semantics and pragmatics as well as basic structures such as the definitions of mathematical terms and propositional, mathematical and metamathematical statements are defined.