- Introduction to Syntax of MATHS
- : Special Characters
- : Lexemes
- : TeX Symbols
- : Syntax
- : Structure
- : Expressions
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- document::= #piece_of_documentation.
Some pieces are sections (see Structure) and other are elementary:

- piece_of_documentation::= section | elementary_documentation.
- elementary_documentation::=#(formal | break | directive | gloss | (label| ) comment ).
- formal::=formula | formal_definition | declaration | assertion.
- definition::=formal_definition | gloss.
- formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,
pi ::real= 3.14159.

paragraph_tag ::= "<p>".

- gloss::= term "::"(context | )"=" (balanced ~ expression) ender.
pi ::real= ratio of circumference divided by radius.

- balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
- ender::= "." | ",".
- declaration::= (for_clause (condition | ) | )term"::"context.
- assertion::=axiom | theorem.
- formula::= indentation ( label | ) well_formed_formula.
- axiom::= (indentation | ) "|-"( label | ) well_formed_formula.
- theorem::= (| indentation ) ( evidence ) "|-" ( label | ) well_formed_formula.
- label::= "(" identifier "):".
- context::=expression describing a type or set of possibilities.
- break::= blank line.
- indentation::=a tab at the start of the line followed by spaces and tabs.
- paragraph_indentation::= a space indicates an item, element, or bullet point.
- 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

- section::=simple_section | open_close_section | local_section.
simple_section::= header_line #(paragraph | blank_line | insertion).
- header_line::="." white_space name #whitespace eoln,
- header::syntax->syntax="." whitespace (_) eoln.
- |-header_line= |[H:name](header(H)).
- open_close_section::= |[H:name](open(H) #piece_of_documentation close(H))
- open::syntax->syntax=".Open" SP (_) eoln,
- close::syntax=".Close" O(SP (_)) eoln.
- local_section::= |[T:"." type_of_section]( T eoln #piece ".Close" T eoln).
- 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 ]

- 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.

@ 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.

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 |

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

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 ]

For a more rigorous description of the standard notations see