Special Characters

 @	prefix: Subsets of/Subsets defined by/SetOf

 @	prefix: Relations between...

 @	 - also  @={true,false}

 %	prefix: Numbered sequences of

 #	prefix: Strings of | any number of

 $	prefix: Set/tuple defined by documenting its structure and properties

 &	infix and prefix: intersection of sets

 |	infix and prefix: union of sets, alternative forms of syntax a la BNF

 ^	infix and prefix: Power, superscript

 !	infix and prefix: Concatenation  of sequences/strings/files/lists/...

 ?	Prefix/postfix items  to sequences/strings/...

 :>=-<	Used to build identifiers: arrows, operators, etc

 *	infix and prefix: Multiplication

 +	infix and prefix: Addition

 -	infix and prefix: subtraction and negate

 \	Nroff  or TEX symbols for strange characters: \Sigma

 {....}	Sets defined by extension(listing) or intension(property)

 ()	Algebraic precedence, function parameters, lists

 []	Lower/subscript/\lambda/Schema

 /	infix: division

 / 	prefix: inverts functions and relations.

 ,	separate parameters, elements in lists, sets, schema,...

 .	infix: apply.  Also separates sentences in schema.

 ::=     `is defined to be the same as`

 ::      `is declared to be of type`

 :       `has type`

 |-      `It is asserted that...`.  `It is assumed`,  or `It can be shown`

For more see [ notn_10_Lexicon.html ] , and [ math.syntax.html ] or below.

Lexemes

Here is a quick list of key words used in MATHS

key word	purpose
Close	Terminate the last Net, Set, Let, List, Open
For, for	Introduses quantifiers: all, some, 1, 0..1, ...
fun	Function
Let	Introduces a temporary assumption used to prove something else
List	Start an ordered sequential list
map	Indicates a map, function, λ
Net	Introduces a collection of variables and constraints
Open	Open a subsection of the document
rel	Relation
Row	An n-tpl of items separated by tabs in a Table
Set, set	Introduces an unordered set of items
Table	A table: an relation defined as a set of rows

TeX Symbols

Maths permits the TeX convention of putting "\" before a word to indicate a symbol. Some of these are handled correctly when mapped to HTML, see [ ../samples/tex2html.html ] for the mapping.

Syntax

A MATHS document has many pieces,
1. document::= #piece_of_documentation.

   Some pieces are sections (see Structure) and other are elementary:

2. piece_of_documentation::= section | elementary_documentation.
3. elementary_documentation::=#(formal | break | directive | gloss | (label| ) comment ).
4. formal::=formula | formal_definition | declaration | assertion.
5. definition::=formal_definition | gloss.
6. formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,

    		pi ::real= 3.14159.

    		paragraph_tag ::= "<p>".

7. gloss::= term "::"(context | )"=" (balanced ~ expression) ender.

    		pi ::real= ratio of circumference divided by radius.

8. balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
9. ender::= "." | ",".
10. declaration::= (for_clause (condition | ) | )term"::"context.
11. assertion::=axiom | theorem.
12. formula::= indentation ( label | ) well_formed_formula.
13. axiom::= (indentation | ) "|-"( label | ) well_formed_formula.
14. theorem::= (| indentation ) ( evidence ) "|-" ( label | ) well_formed_formula.
15. label::= "(" identifier "):".
16. context::=expression describing a type or set of possibilities.
17. break::= blank line.
18. indentation::=a tab at the start of the line followed by spaces and tabs.
19. paragraph_indentation::= a space indicates an item, element, or bullet point.
20. comment::=just about anything.

    For more see [ math.syntax.html ] and [ notn_13_Docn_Syntax.html ] and [ notn_14_Docn_Semantics.html ] and [ notn_15_Naming_Documentn.html ]

    Structure

21. section::=simple_section | open_close_section | local_section. simple_section::= header_line #(paragraph | blank_line | insertion).

22. header_line::="." white_space name #whitespace eoln,
23. header::syntax->syntax="." whitespace (_) eoln.
    
24. |-header_line= |[H:name](header(H)).

25. open_close_section::= |[H:name](open(H) #piece_of_documentation close(H))
26. open::syntax->syntax=".Open" SP (_) eoln,
27. close::syntax=".Close" O(SP (_)) eoln.

28. local_section::= |[T:"." type_of_section]( T eoln #piece ".Close" T eoln).
29. type_of_section::= {"Let", "Net", "Box", "List", "Set", "Table", ...}.

    Expressions

    
    (expressions): All functions can be used in prefix, postfix, and infix form. Functions are overloaded. In particular predefined operators are apply to sequences and sets. Some are serial (for example +(1,2,3)=1+2+3), while others act in a parallel (for example <(1,2,3)=1<2 and 2<3 and 3<4).

    For more see [ notn_11_Names.html ] and [ notn_12_Expressions.html ]

. . . . . . . . . ( end of section Introduction to Syntax of MATHS) <<Contents | End>>

Notes on MATHS Notation

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 = Net{radius:Positive Real, center:Point}.

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

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see