[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >>
[Contents] || [Notation] || [Copyright] || [Contact] [Search ]
Thu Jul 27 14:25:28 PDT 2006

Proof of Modus Ponens
  1. Let (1):P, (2):if P then Q, (3): not Q.
  2. (2)|-
    1. not P
    2. (1)|- P
    3. end case
    1. Q
    2. (3)|- not Q
    3. end case
Proof of Transitivity of Implication
|- If (if P then Q) and (if Q then R) then (if P then R).
  1. Let (1):if P then Q, (2):if Q then R, (3): not (if P then R).
  2. (3)|- (4): P, (5): not R.
  3. (1)|- following
    1. Case not P
    2. (4)|- RAA.
    3. end case
    1. Case (6): Q
    2. (2)|-
      1. Case not Q
      2. (6)|- RAA.
      3. end case
      1. case R
      2. (5)|- RAA.
      3. end case
    3. end case
Proof of a Dillema
  1. (1): P or Q
  2. (2): if P then R
  3. (3): if Q then R
  4. (1)|-
    1. Case (4): P
    2. (2)|-
      1. Case not P
      2. (4): RAA.
      3. end case
      1. Case R
      2. end case
    3. ()|-R
    4. end case
    1. Case (5) Q,
    2. (3)|-
      1. Case not Q
      2. (5): RAA.
      3. end case
      1. Case R
      2. end case
    3. ()|- R
    4. end case

Rules

  1. Case must cover all the possibilities (but can overlap).
  2. Some formulas Have only a single possibility made of a set of simpler formula
  3. Three ways to 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, 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 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

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

    Glossary

  5. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 2 or three statements.
  6. given::reason="I've been told that...", used to describe a problem.
  7. given::variable="I'll be given a value or object like this...", used to describe a problem.
  8. goal::theorem="The result I'm trying to prove right now".
  9. goal::variable="The value or object I'm trying to find or construct".
  10. let::reason="For the sake of argument let...", intoduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  11. hyp::reason="I assumed this in my last Let/Case/Po/...".
  12. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  13. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitte the goal you were given.
  14. RAA::conclusion="Reducto Ad Absurdum".

End