Net

 	X::=Net{ a:A, b:B, W(a,b...)}.

 	Y::=Net{ parts of Y, S:=$ X,  more parts of Y}.

Then it is as if the definition of Y had been written:

 	Y::=Net{ parts of Y, S:={ a:A, b:B || W(a,b...) }, more parts of Y}.

However, if the definition of X changes, then so does the definition of Y. There is no need for the definition of X to be in the same physical document if there is a ".See" directive:

 	.See X_s_URL#X

remote_definition

 	X::=X_s_URL#X.

(End of Net)

 	X::=Net{ a:A, b:B, W(a,b...)}

 	Z::=Net{ parts of Y, X, more parts of Y}.

Then it is as if the definition of Z had been written:

 	Z::=Net{ parts of Y, a:A, b:B, W(a,b...), more parts of Y}.

However, if the definition of X changes, then so does the definition of Z. The "X" in Z acts like a kind of "hot-linked macro". As above a ".See" directive permits the use of terms defined in other documents. A copy of the definition of X can also be imported or inherited in two ways:

 	W1::=Net{ parts of Y, definition(X), more parts of Y}.

 	W2::=following

 	.Net

 		parts of Y

 		X::=X_s_URL#X

 		more parts of Y

 	.Close.Net

Then it is as if the definition of W had been written:

 	W::=Net{ parts of Y, X:=Net{a:A, b:B, W(a,b...)}, more parts of Y}.

(End of Net)

When name of a piece of documentation is used in another piece of documentation then some of the declarations and definitions of the referenced documentation become part of the document that makes the reference. Other definitions and declarations may be redefined or redeclared and so be hidden. This follows the Rule of the Most Visible Meaning - symbols in an expression always refer to the most visible definition or declaration of the symbols that fits their particular context in the expression.

When included documentation is inserted and includes a document that has already been included then this inclusion has no effect. Circular re-usage also has no effect.

The key logical problem is that re-used documentation is quoted "out of context". This is similar to questions of dynamic and static scoping in programming language semantics. The formal semantics implies that identifers that appear in a piece of document but not defined in it can gain a meaning from the document in which they are re-used. This is close to dynamic scoping -- each re-use of a document may create a different binding for identifiers that are free in the re-used document. Therefore it wise to design documents for re-use that have no free variables: all variable should be bound as parameters or to terms. So, for example, given

 		WORSE::=Net{ a+b=c }.

 		BETTER::=Net{ Set:Sets, a,b,c:Set, a+b=c}.

Sets

Further, a re-used piece of documentation looses its original context. If a piece of documentation makes use of an assumption that is stated in its definition's environment, then it can not be validly used in another document unless that document recreates the context in which the original was defined. It is wise then to design special pieces of documentation (Nets) that state their assumptions explicitly. On the other hand: to insist that every re-usable piece of documentation explicitly states its contextual assumptions seems to be a heavy burden for the producer of the documentation. For example: suppose
Let

(1): For all a:A,b:B, if W(a,b) then W2(a).
X::=Net{ a:A, b:B, W(a,b). |- W2(a) }
Z::=Net{ parts of Y, X, more parts of Y}.

The declared variables in piece of documentation are effectively parameters for that documentation. One interesting question is what happens when a piece of documentation is re-used in a context where a parameter (declared variable) is bound to a fixed meaning. For example: M below has three variables { "Nat0", "0", "+" }

M::=Net { Nat0:Sets, 0:Nat0, +:serial(Nat0), for all s:Nat0( s+0 = 0+s = s ) }.
We don't expect to see the symbols "0" and "+" used like this, perhaps. But, this is equivalent to the basic definition that results by taking the generic monoid
MONOID::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#MONOID
and substituting:
MONOID( Set=>Nat0, op=> +, unit=>0). [ [ Modified Re-Use ] below] Now, we know that the natural numbers with zero form a monoid under addition, so, in any context where the natural numbers are available (the standard one), we could re-use M:
|- (2): M. But to assert M like this means (apparently) that the declaration of M are added to our document and redefine 0, + and Nat0!
Thus we have the following rule:
When a piece of documentation D1 is re-used in document D2 and x is a variable declared in D1 like this
```
 	x::S
```
for some set S and also appears as a constant in D2, then the declaration is converted into an axiom x in S in D2.
So in any context where natural number exist, re-using or citing M above, effectively the following formulae:
Nat0 in Sets.
0 in Nat0.
+ in serial(Nat0).
for all s:Nat0( s+0 = 0+s = s ).
Finally note that since these are all true in a context that define Nat0 as the natural numbers with 0, we would like assert M as a theorem:
(above)|- (3): M. Meaning that the four formulae above are theorems.

Proof of 3
By inspection.

A documentation system would help the users to disclose and hide the content quickly and easily. Either an 'out liner' or a hypertext model is an appropriate implementation. The system needs to also record the use of a given piece of documentation, and ensure that when the used documentation is changed then the all references to it are automatically kept in step - or (at least) protected from losing the linkage. When feasible a documentation system will make visible to a viewer the dependencies between documents buy placing two directives near the start of the document:
.Uses list of names
.Used_by list of names
This ideal is difficult to reconcile with the freewheeling nature of the World-Wide Web. What happens if you refer to a document that someone else has written, and owns. How can they know? Can they be forced to maintain their end of the link? What happens if they need to revise their document -- formal documents evolve by a dialectical process of proposal, refutation, and improvement? I don't think there is any real solution to this problem. Clearly it means that it is best to link to documents that appear stable: well argued, reasonable, and based on stable assumptions. Clearly it means that it is necessary to regularly review links. Finally it is very wise to tell the author that you need the link and for authors to maintain a subscriber list who can be notified when changes are about to happen.
Perhaps some form of deprecation process should be introduced. In standard deprecated features are likely not to be supported in a future version.

Modified Re-Use
A name can be followed by operations that describe modifications to the documentation to which it refers. These work as if they generated an edited copy that is inserted in place of the modified name.
For example suppose
```
 	X::=Net{ a:A, b:B, W(a,b...)},
```
```
 	V::=Net{ parts of Y, X(a=>x, b=>c), more parts of Y},
```
then it is as if the definition of V had been written:
```
 	Net{ parts of Y, x:A, x:B, W(x,y...), more parts of Y}.
```
If
```
 	V1::=Net{ parts of Y, X with P, more parts of Y},
```
then it as if V1 was written
```
 	 Net{ parts of Y, a:A, b:B, W(a,b...). P.  more parts of Y}.
```
Extension
Experience of object-oriented technology and methods provides convincing evidence of the need to take previous work and quickly extend it by adding new features and/or constraints. MATHS has two predefined notations to do this.
First to add a constraint w to a document named N right 'N and w'. This is a simple reuse notation described earlier.
To add a set of features (including both declarations and wffs) use: "with". This is again a simple abbreviation.
(with):
```
 	N with v:S
```
```
 	N with{ D }
```
```
 	N with following
```
```
 	.Net
```
```
 		D
```
```
 	.Close.Net
```
If a set S is defined as $ N then
S and w::= $ Net{ N. w . }. S with {D}::=$ Net{ N. D. }.
A common example:
ALGEBRA::=Net{ Set:Sets }.
SEMIGROUP::= ALGEBRA with op:associative(Set).
MONOID::= SEMIGROUP with u:neuter(op).

Inheritance
Notice that a new formal system can easily be created that inherits features from many different formal systems -- merely by asserting them:
RING::=following,
Net
1. |- (r1): GROUP(Set, +, 0, -).
2. |- (r2): MONOID(Set, *, 1).
3. |- (r3): (*) distributes_over (+).
4. ...
(End of Net)
The result is a system (a logic, an algebra, a model, ...) that satisfies the properties of both its parent systems. MATHS includes multiple inheritance... just like its less formal parent "mathematics" did.
.Dangerous_Bend
However there is a danger in combining a pair of systems like this. You may end up describing a class that can not exists - a triangle with four sides. Therefore it is important that whenever you reuse a mathematical system you always create an example that satisfies all the rules you have gathered together. For example the Natural numbers {0,1,2,3,...} satisfy the three axioms r1, r2, r3 above.
This may also help your readers understand what you are getting at.

Summary
1. Similarly it is possible to hide all variables and terms except a specified subset, by using a projection.
```
	documentation.(list_of_variables_to_be_kept)
```
2. Parts can be added to a defined network as well:
```
 	documentation with element
```
3. Two or more pieces of documentation can also be combined using the Boolean operations.
  If a document is basic (it has no definitions or theorems) then it is possible to remove axioms from it
```
	basic_documentation without (list_of_axioms)
```
  However this is deprecated because it indicates that there is a simpler network of assumptions that could have been studied first.
  These (possibly modified) pieces of documentation can be combined as if they were propositions - MATHS defines the resulting documentation, it does not entail any logical calculus of documentation yet (unlike Z). The result of editing and combining can be used as a macro in any other piece of documentation. These structures can be used any where the name of a local piece of documentation can be used.
  The usage of terms needs be documented (automatically) in both the reference and also in the referred to documentation.
  
  Example -- Piping two specifications
  Suppose that N1 is the name of some documentation describing a variable called output and N2 is the name of documentation that describes a variable input then
4. (N1 and N2 and output=input)(for some input, output), specifies a process that connects N1 to N2 and hides the connection.
  
  Beyond Re-use
  In MATHS combining documentation is merely a notational convenience. A full calculus could be developed in the future. The basis will be an equivalence relation or congruence on pieces of documentation. Two pieces of documentation are semantically equivalent if they have the same signature (variables and types) and for all values of the variables the constraints are equal. Thus D1 and D2 are equivalent if they are of the same type and define the same set of tuples:
5. For Documentation D1,D2, if signature(D1)=signature(D2) then D1 equivalent D2::= ($ D1 = $ D2) else D1 equivalent D2::=false.
  In the example above, Z is equivalent to Y and X.
. . . . . . . . . ( end of section Summary) <<Contents | End>>
Formal description of Reuse
. . . . . . . . . ( end of section Formal description of Reuse) <<Contents | End>>

Combining named documentation
1. N with P::= N and Net{P}.
  
  Negation
  The formal definition of the result of negating a name describes a structure:
2. For X : name of pieces of documentation, declarations(not X ) = declarations(X) and definitions( not X ) = definitions(X) and assertions(not X) = not constraint(X)
  Example of negation
  If
```
 	ABC2::=following.
```
```
 	.Net
```
```
 	        a::A,
```
```
 	        b::B(a),
```
```
 	        c::=C(a,b),
```
```
 	        P(a,b,c)
```
```
 	.Close.Net
```
  then
```
 Formula		Expansion
```
```
 not ABC2	a::A,
```
```
 		b::B(a),
```
```
 		c::=C(a,b),
```
```
 		not P(a,b,c)
```
  Boolean combinations
  
  When two pieces of documentation are combined, common variables and terms must have compatible declarations or definitions. The formal definition of the result of a boolean operation between two named is:
3. For X : name of piece of documentation, Y an elementary piece or another name, *:{and,or,iff,if__then__},
4. declarations(X * Y) = declarations(X) | declarations(Y) and definitions(X * Y) = definitions(X) | definitions(Y) and assertions(X * Y) ={ constraint(X) * constraint(Y)}.
  The result will not be valid if X and Y give two different definitions to a term in a single context, or two different declarations to a variable. Sometimes one piece of documentation declares a variable that is defined as a term in the other piece. This is OK, as long as the type of the definition is that of the declaration.
  
  Example of Boolean Operations
```
 AB::=Net{ a:A, b:B},  XY::=Net{ x:A, y:B}.
```
```
 Formula		        Expansion
```
```
 AX and XY	        a,x:A, b,y:B
```
```
 AB and Net{x:X}       a:A, x:X, b:B(a), c:=C(a,b),  P(a,b,c)
```
```
 ABC2 or a=b	        a:A, b:B(a), c:=C(a,b), P(a,b,c) or a=b
```
```
 if ABC2 then a=c	        a:A, b:B(a), c:=C(a,b), if P(a,b,c) then a=c
```
. . . . . . . . . ( end of section Modifying named documentation) <<Contents | End>>
Noting and defining
Section headings give a name to part of a document and also includes it as part of the document. A definition attaches a name to be bound to a piece of documentation but without the content being inserted in the document. To name a piece of documentation for future use,
```
 	Name "::=" cross_reference.
```
Later the name can be used or modified and inserted.
Example
Another variation is to import a copy of the definition of a named piece of documentation into another piece of documentation:
```
 .As_is 	Use N
```
or
```
 	With N
```
inserts the original
```
 	N::=Net{... x:X. ...}.
```
Thus the effect is like 'with' in Ada: Terms defined in N's documentation can only be referred to by qualifying by the name N by their name:
```
 	N.x.
```
Example of Use/With
Parametric or Generic Documentation
In MATHS we create documentation with declared terms so that it can be used for similar purposes by substituting and/or hiding the them.
Example of Generic Documentation
Formulae defined as documentation
MATHS lets the writer define an expression whose meaning is a piece of documentation, once certain substitutions are carried out:
```
 	"For" declare_arguments "," model_expression "::=" "Net{" documentation "}"
```
An example,
For A,B:variable, Either A or B::=Net{ A,B:@. A iff not B.},
For A,B,C:variable, Either A, B, or C::=Net{ A,B,C:@. if A then not B and not C else Either B or C.}.

Quantified Documentation.
If N is the name of documentation s, n::= |declarations(s)| and d is a list of all declarations(s) in some order and Q a list of n quantifiers, and v is the list of variables in d (in the same order) and X is declared to be of type @N then
@{N ||for (Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n])}::= {X:@$ N|| for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)) }.
Notice that X:@$ N, so X satisfies the constraints of N.
(for Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n](N)) ::= for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)).
Notice that this is meaningless whenever there are no constraints defined in N.
For X:@$ D then (for Q1 v1, Q2 v2, ...(X)) ::= Q1 d1, Q2 d2,...($(N) in X).
A useful abbreviation is to use the name of the documentation rather than listing all the remaining variables.
(for Q1 v1, Q2 v2,...Q[p] v[p], Q[q] N) ::= for Q1 d1, Q2 d2, ..., Q[p] d[p], Q[q] d[p+1],..., Q[q] d[n](N).

Dynamics
A dynamic proposition is any proposition with a primed variable in it. The primed variables are said to be dynamic variables, and the remainder static. Such predicates a not completely specified until the types of the variables are specified. A piece of documentation that declares the variables and includes a dynamic predicate describes a change of state. The space of states is defined by the declarations. Additional static propositions state any invariants that are maintained. A prime is used only in wffs, and not used in declarations because a primed variable is implicitly declared as being the same type as the unprimed version.
There follows a summary, for more details see: [ math_14_Dynamics,html ]
A dynamic proposition in a piece of documentation means that the '$' operator forms a set of pairs or binary relation rather than a set of single states. For example, if
```
 	X::=Net{ a:A, W1(a) },
```
```
 	Y::=Net{ a:A, W2(a, a')}
```
then
```
	$ X={a:A || W1(a) }
```
and has type @A but
```
	$ Y=rel[a,a':A](W2(a,a') )
```
and has type @(A,A).
If 'D2' is a piece of documentation with one or more dynamic variables in it then
$ D2=rel[ declarations(D2), primed(declarations(D2)] (constraint(D2) and static variable do not change)
The declarations(D2) are list of the declarations of D2.The primed(declarations(D2) are declarations of D2 with a prime added to each variable. So (unlike Z) the primed variables are implicitly in the same state space as the unprimed variables.
Consider a piece of documentation D1 with no dynamic propositions in it and documentation
```
	D2 ::=Net{D1, W(x1',x2',x3',...,x1,x2,x3,...)}
```
```
		where x1,... in variables(D1).
```
Thus
```
	assertions(D2)=assertions(D1)|{`W(x1',...,x1, ...)`}
```
Let z=(z1,z2,...)=variables(D)~{x1,x2,x3,...} then in D2
```
 (1) A duplicate set of `x`s are implicitly added to D1's variables.
```
```
 	variables(D2) =variables(D) | {x1,...} | {x1',...}  | {z1',...}
```
```
 (2) The relation is constrained by the requirement that static variables do not change.
```
```
 	constraint(D2) = constraint(D1) and z1'=z1 and z2'=z2 and ...
```
The Z idiom of defining the state space separately is also used in MATHS. Here is an example from recreational mathematics:
HAILSTONE::=following.
Net
1. State::=Net{ n: Nat },
2. Op1::=Net{ State, 2*n'=3*n+1},
3. Op2::=Net{ State, 2*n'=n},
4. End::=Net{ State, n=1}.
5. Delta::= Op1 or Op2.
6. (above)|-pre($ Delta) = pre ($ Op1) | pre ($ Op2) =State.
7. (above)|-no pre($ Op1) & pre ($ Op2).
8. (above)|-State >== {pre($ Op1) , pre($ Op2)},
9. (above)|-$ End.$ Op1.$ Op2=$ End.
10. ??{ Nat. do($ Delta) = $ End. }??
11. Loop::=Net{State, n'=n}.
12. ??{ For all n0, if $ Net{State, n=n0}==>$ Net{State, n=n0}. do($ Op1 | $ Op2) then n0 in {1,2}. }??
(End of Net)
Theory
There is a suitable theory of the MATHS re_use in [Wirsing90].

. . . . . . . . . ( end of section Re-use & Inheritance) <<Contents | End>>

Notes on MATHS Notation

intro_characters.html

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 Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. 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. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

logic_0_Intro.html

For a more rigorous description of the standard notations see

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
Glossary
above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
given::reason="I've been told that...", used to describe a problem.
given::variable="I'll be given a value or object like this...", used to describe a problem.
goal::theorem="The result I'm trying to prove right now".
goal::variable="The value or object I'm trying to find or construct".
let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
hyp::reason="I assumed this in my last Let/Case/Po/...".
QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.