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



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

    2. Differential_Calculus::=
      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 ).


    3. Operational_Calculus::=
      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).


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


  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.