- Lexemes for MATHS
- : Informal Introduction
- : Parentheses, Brackets and Braces
- : Formal Treatment
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS

- digit::="0".."9",
- letter::=lower_case | uppercase,
- lower_case::="a".."z"
- upper_case::="A".."Z".
There is a one-to-one correspondence between the lower case letters and the upper case letters. This is not exploited in the MATHS notation but recorded here for completeness and so people can use it in their own documents:

- to_upper::#char>->#char, map lower case into upper case.
- to_lower::#char>->#char, map upper case into lower case.
- ignore_case::#char>->@#char.
- eoln::= #whitespace (ASCII.CR | ASCII.LF) #whitespace.
- break::= eoln eoln #eoln, -- two or more eolns can break comments up into paragraph.
- indentation::=
*ASCII*.HT #*white_space_char*, indicates a formula. - paragraph_indentation::=
*ASCII*.SP #*white_space_char*, indicates a break, item, bullet point, or element. - 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 has already been introduced.

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

\[...\] Semantic brackets

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 \Sigma 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", "\lambda", ... 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>>

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

For a complete listing of pages by topic see [ home.html ]