- digit::="0".."9",
- letter::=lower_case | uppercase,
- lower_case::="a".."z"
- upper_case::="A".."Z".
- eoln::= #whitespace (ASCII.CR | ASCII.LF) #whitespace.
- break::= eoln eoln #eoln, -- two or more eolns can break comments up into paragraph.
- indentation::= (ASCII.SP | ASCII.HT) #(ASCII.SP | ASCII.HT).
- quote::="\"", -- a backslash changes the meaning of the next char exactly as it does in ANSI C.
- backslash::="\\" -- as in C a backslash is an escape character and so two are needed to represent one.
Formal statements are distinguished by the presence of the double colon some where in the line or else by white space character at the start of a line:

::= is defined to be the same as

:: is declared to be a

Indented formula can be labeled:(label): display and name a formula, if indented at start of line

(label): Allows a label to be attached to an informal statemnt.

|-(label): State an assumption or axiom.

(reasons)|-(label): assert a provable theorem

In a logically complete document for each provable theorem labeled l has a proof in a section headed ".Proof of l". All the steps in the proof are either standard (and well known) or are listed as reasons. The reasons will all be labels of formula that have appeared previous to the statemnt of the theorem.|- yada::= Indicates a definition for `yada` has been introduced earlier.

The above is most useful when you want to include a package with many definitions in it and then draw the reader's attention to particular ones. This also creates a visible link in this document to the quoted definition.The ASCII characters "@#$ ^&|~" are used in place of written symbols used in discrete mathematics:

& intersection

| union/alternate syntaxes

~ complement

[ logic_30_Sets.html ]@ Subsets of/Subsets defined by

[ logic_31_Families_of_Sets.html ]# Numbered sequences of

[ logic_6_Numbers..Strings.html ] [ math_62_Strings.html ]$ Structured Set/Set defined by documentation

[ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ]^ Power, raise up, superscript

## Parentheses, Brackets and Braces

{} Sets, alternately use SET(...)

() Order of operations, lists, sequences, function application

[] Lower/subscript/map from, else use MAP[...]

\<...\> BNF Brockets (broken brackets -- term from Physics)

\[...\] Semantic brackets (shown like this [[...]] in some texts).

Additional non-ASCII symbols a described by using any of nroff or TEX code or by concatenating these symbols "~-*><:=." together. Here are some special arrows and crosses

+> Maplet

-> Mappings and functions

<>-> Partial Mappings and functions

>< Cartesian and Cross Products

=> Substitution

<= Less than or equal

>= greater than or equal

<> not equal (Pascal and BASIC)

==> subset

=>> proper subset

>== partitioning

[ logic_30_Sets.html ]|| "where" in intensional set descriptions {x:T || P}

. "where" in intensional set descriptions {x:T. P}

The slash("/") is used as a prefixed inversion/converse operator, rather than having "^{-1}" afterwards - it can be thought of as a generalised "root" symbol(sqrt=/(^2)), or possibly being short for "arc" (arcsin=/sin).

Lists, strings, and sequences can be treated as functions. Functions as relations. For example (a,b,c) = ( 1+>a | 2+>b | 3+>c). Further they can be inverted, so that for example: /(a,b,c) = ( a+>1 | b+>2 | c+>3 ).

All functions can used in prefix, postfix and infix form and are overloaded to also apply to sequences and sets of elements.

However some functions have a serial interpretation (for example +(1,2,3)=1+2+3), while others have a parallel interpretation (for example <(1,2,3)=(1<2<3)=(1<2 and 2<3)). This obviates the need for special signs for the same operations(with apologies to Lagrange who was the first to use Σ where MATHS uses "+").

Identifiers can be used for variables, constants, functions, operators etc. however there are two kinds of identifier. The mathemaatical is short and used locally in algebraic formula - for example "x", "λ", ... The others a longer and made up of words in the client's language. These have a wider scope and should indicate their meaning clearly, if at all possible. Here are some special identifiers with predefined meanings:

and Boolean conjunction

or Boolean inclusive disjunction

if Start of conditional

then Separates premise from conclusion in conditional

for Introduces a series of quantifiers

all, some, one, no, 1,2,3,4,... Quantifiers

not Boolean complement

the definite description of an object

## Formal Treatment

[ notn_10_Lexicon.html ]

. . . . . . . . . ( end of section Lexemes of MATH) <<Contents | End>>