- Notes on Circularity
- : Note
- : Warning -- circular definitions of formal languages
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- A><B::=Set of Pairs, first element in A and second in B, is an informal definition of the Cartesian product of A and B. The following is a formal definition as a type of object that has a documented structure with two components labelled 1st and 2nd:
- A><B::= $ Net{1st:A, 2nd:B}. Now 1st and 2nd in the above act like be mappings or functions from A><B into A and B respectively:
- 1st:A><B ->A,
- 2nd: A><B -> B. Further maps can be described as special relations:
- A->B::={R:Relations(A,B)| for all a:B, one b:B(a R b)} Now relations are described as special sets of pairs
- For Types T1,T2, A:@T1, B:@T2, Relations(A,B)::=@(T1><T2).
- ...which is where we came in.
What is important at the start is to learn how all the different notations fit together, not which notation is actually defined in terms of which other notation. The best way to do this is a meta-mathematical problem.

## Warning -- circular definitions of formal languages

Worse it is impossible to formally define the formal semantics a formal language of any interest using that language.[ Tarski%27s_undefinability_theorem ]

So the syntax is trustworthy here.... but not what it all means.

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

. . . . . . . . . ( end of section Notes on Circularity) <<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 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 ]

For a more rigorous description of the standard notations see