Certain patterns turn up when using algebraic systems. For example the system declares a set and certain operators and axioms. The user wants to declare the set and have the standard operations and axioms added to their document.
It is useful to be able to useful to import from other documentation the properties of a variable by declaring it. For example suppose we have alread defined the system:
Then it would help reuse if we could automatically write declarations like the following to create specific examples:
The best system would be to always create a set of definitions for the normal way people use algebras. For example:
As a result we have: (x=>a, y=>b, ..., z=>c ) :: Xyz can declare variables a::X, b::Y,...,c::Z. (a, b, ..., c) :: Xyz can declare variables a::X, b::Y,...,c::Z.
For a single sorted algebra like a group, poset, etc we can formalize the relation as follows -
Notes on MATHS Notation
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.
Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block%20Structure in logic_2_Proofs ] for more on the structure and rules.
The notation also allows you to create a new network of variables and constraints, and give them a name. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents.