[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / math_44_Formal_Calculus
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 13 14:16:11 PST 2010

# Calculus

1. Calculus::=Net{Differential_Calculus, Operational_Calculus, Ordinary_differential_equations, Partial_differential_equations,...} .

2. Differential_Calculus::=
Net{
1. R::semi-ring=given.
2. F::@(R->R).
3. D::F<>->F=given.
4. DF::=pre(D), differentiable functions.
5. For x,y,z:R, f, g, h :DF. ...
6. For x:variable(R), e:expression(R), D[x](e) ::=D(map[x:R](e)).

Source: Thurston 94, Hugh Thurston, What is Wrong With the Definition of dy/dx, Am Math Monthly V101n9(Nov 94)pp855-857

7. For f,g, d f/d g::F = D(f)/D(g).

Convention: the variables x,y, and z are used to represent elements of F and in particular, x is often used as the Id function.

8. |-Id in DF and D Id = 1.
9. (above)|-D[x](x) = d x/d x=fun[x]1.
10. |-For a:R, D[x](a)=[x]0.
11. (above)|-D[x](a) = d a/d x=fun[x]0.
12. |-D(f + g)= D(f) + D(g),
13. |-D(f * g)= D(f) * g + f * D(g),
14. |-D(f o g)= D(g) * (D(f) o g).
15. (above)|-D(f ; g)=D(f) * (f ; D(g)).

16. (above)|-For a,b:R, D(a * f + c)=a * D(f).

17. (above)|-D[x](x^2)=fun[x]2*x,
18. (above)|-D[x](x^3)=fun[x]3*x^2, ... .
19. (above)|-For n , D(_^n)=n*(_^(n-1)).
20. (above)|-For non_zero_integer n , D[x](x^n)=fun[x]n*x^(n-1).

21. (above)|-D[x]f(g(x))=fun[x] ( D(g)(x) * (D(f))(g(x))).

22. (above)|-if R in Field then D/f = 1/( D(f) o /f ).

}=::Differential_Calculus.

3. Operational_Calculus::=
Net{
1. R::semi-ring=given.
2. F::@(R->R).
3. n::=dimension(R)=given. Assume n different and non-overlapping step operators.
4. D::F<>->F=given.
5. DF::=pre(D).
6. E::1..n->(F<>->F)= fun[i](fun[f](fun[r](f(r+δ[i])).
7. Δ::= E - 1.
8. Δ_upside_down::= 1 - /E.

9. |-semi_ring( generated=>Net{D, F, Δ, Δ_upside_down, ...}.

10. (above)|-if n=1, ... then E= e^(h D).

}=::Operational_Calculus.

. . . . . . . . . ( end of section Calculus) <<Contents | End>>

# Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

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 ]

# Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

2. 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).
3. given::reason="I've been told that...", used to describe a problem.
4. given::variable="I'll be given a value or object like this...", used to describe a problem.
5. goal::theorem="The result I'm trying to prove right now".
6. goal::variable="The value or object I'm trying to find or construct".
7. 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.
8. hyp::reason="I assumed this in my last Let/Case/Po/...".
9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.