Select this to skip to main content [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> l2
 [Index] || [Contents] || [Source] || [Definitions] || [Search] || [Notation] || [Copyright] || [Comment] Fri Jan 16 12:32:03 PST 2004

Contents


    Proofs and Arguments

      Introduction

      MATHS is designed to make the validation and proof of software a more practical process. It therefore includes a checkable way to derive conclusions from previously established results. It uses a block-structured form of logic called natural deduction augmented by abbreviations and algebraic steps. The goal is a natural but verifiable way to discover and present arguments.

      Absurdity and Contradictions

      A logiistic system can only be trusted if it does not lead to contradictory or absurd propositions. If the proof rules of MATHS are followed this should not occur. Natural deduction systems work by deviding up the current situation into special cases and showing that the majority of these (even all of them) are contradictory. If all are contradictory then the assumptions can be rejected. If some are open then the assumptions are taken to imply these conclusions.

      By Murphy's Law, it will happen that MATHS users will construct documentation that is inconsistent. The symptom of this is when a proposition and its negation are derived within a piece of documentation. This is not a disaster - it is an opportunity to prove something. The correct thing to do is to close off the conclusion and the assumptions and declarations leading to the contradiction into a "set of documentation" that proves a result. Thus by simple editing the whole is protected from inconsistency and a new theorem is proved.

      A historical example of a project that failed through not doing this are the Pythagoreans who failed as mathematicians when they killed the man who proved that the assumption that sqrt(2) was a ratio lead to a contradiction. They could have proceeded by making this into an argument that there must exist numbers that are not ratios. Instead they preferred to support a mystical theory which they knew to be unsound. There are no Pythagoreans left today.

      Absurdity happens - MATHS users will find that their cherished and documented assumptions lead to conclusions that do not fit with observation. Again this is an opportunity rather than a problem! Science takes a leap forward whenever reality destroys a theory. First the data has to be checked and then the theory may have to be modified.

      For example the first evidence for a hole in the ozone layer was rejected by NASA because the values couldn't happen - it had to be "experimental error". There is an early map of the stars that someone drew which shows that one star had been erased and put near by - because a later observation showed it in a new position. The star was one of the unknown outer planets. Kepler wrote and crossed out "These points might as well fit an ellipse", and delayed his discovery of "Kepler's Laws" by several years. Because "action at a distance" was repugnant to Descartes' philosphy, his followers later rejected Newton's law of gravitation [In Koestler59, "The Sleepwalkers, Arthur Koestler]

      An engineer is in trouble when reality shows up a misunderstanding - because the system ceases to work as required. The wise engineer takes time to scientifically examine and model the situation prior to searching out the problems and solving them. No work is started until a mathematical analysis proves that the system is safe (within a generous "safety factor"). The wise engineer also finishes up by making experimental prototype versions first. As an example, in the UK there were once two rival groups designing an airship. One was designed on an elegant mathematical model and known to be safe. The other was "hacked" together - despite evidence that it would fall to pieces. The properly engineered system flew, the other one was the R101 and crashed in flames - breaking up as predicted[Nevile Shute, "Sliderule"].

      However never totally discard a theory - document the context in which it did/does work and file it under - "It seemed like a good idea at the time...".

      Two Systems of Proof

      MATHS combines two systems for proving things:a "Natural deduction" and Algebra. In Natural deduction systems there is, at any point a stack of things which are currently taken to be true, plus rules permitting various changes to this stack. First any valid algebraic step can be used to add a new proposition. Second, MATHS has three "Natural" ways of deriving new consequences from assumed or proven truths. We look at the "natural" steps first.

      Natural Deduction

      First, propositions can be deduced directly from what is currently held to be true. In the following table the rules are written as wffs: if P and R then Q means that P, R|-Q is a valid step in an argument. The labels are not needed. Similarly, a rule written like this "P iff Q" validates deductions like P|-Q, Q|-P, or the substitution of P for Q in any other formula: W(P) iff W(Q) or expression f(P) = f(Q).

      Valid Deductive Steps

        ------------------------------------
    1. (and1): if P and Q then P
    2. (and2): if P and Q then Q
    3. (demorgan1): not(P and Q) iff not P or not Q
    4. (and3): if P and Q then P and Q

    5. (or1): if (P or Q) and not P then Q
    6. (or2): if (P or Q and not Q then P
    7. (or3): if not(P or Q) then not P
    8. (or4): if not(P or Q) then not Q

    9. (mp): if (P and(if P then Q) then Q
    10. (mtp): if (not Q) and (if P then Q) then not P
    11. (nif1): if not(if P then Q) then P
    12. (nif1): if not(if P then Q) then not Q

    13. (iff1): if (P iff Q)then if P then Q
    14. (iff2): if (P iff Q)then if Q then P

      When P and Q have the same set of free variables we have:

    15. (iff3): if (P iff Q)then (W(P) iff W(Q))
    16. (iff4): if (P iff Q)then (f(P) = f(Q))

    17. (qn1): not for some x:T(W(x)) iff for all x:T(not W(x))
    18. (qn2): not for all x:T(W(x)) iff for some x:T(not W(x))
        ------------------------------------

      The following rules need special documentation

        ------------------------------------
    19. (eg):
       	W(e),(x=>e)|-for some x:T(W(x))
      			--(e is an expression of type T)
    20. (ei):
       	for some x:T(W(x)), (x=>v)|-v:T, W(v)
      			--(v is free variable)
    21. (ui):
       	for one x:T(W(x), (v=>x)|-W(v)
      			--(v is free variable)
    22. (ui):
       	for all x:T(W(x)), (v=>x)|- W(e)
      			--(e is an expression of type T)
        ------------------------------------

      Notice that rules like Modus Ponens (mp) let us use theorems as deduction rules:

    23. (mp): |- if P and if P then Q then Q.
    24. (x=>e):|- if for all x:T(W(x)) and e:T then W(e).

      So we can and will express new rules for particular systems as well formed formula. For example, in the theory of real numbers we have:

    25. (Sqrt): For all Real x, y, if x=sqrt(y) then y=x*x,

      So it is valid to derive

    26. (s2): 9 = 3*3 from (s1): 3=sqrt(9) by
    27. (Sqrt, x=>3, y=>9) |- if 3=sqrt(9) then 9=3*3,
    28. (1, mp) |- 9=3*3. Normally details are omitted:
    29. (Sqrt, x=>3, y=>9, 1) |- 9=3*3.

      Omitting reasons

      I theory you shouldn't have to document which of the above rules you use. In practice it depends on the sophistication of the audience. It is at least wise to indicate which formal system contains the rules in use.

      Theorems Linked to Proofs

      In a complete piece of documentation every theorem will have a label l and a possible separate section headed Proof of l. A Hypertext system should make links between the labels and the proofs. Similarly between identifiers of other theorems and axioms used as evidence to the statement of the evidence.

      Block Structure

      In addition to deductive steps we can use nested pieces of documentation can explore the consequences of extra assumptions. Propositions of the form

    30. for x:S, if P then Q

      are often proved by documentation that

    31. (declare): introduces a temporary declaration (x:S),
    32. (assume): makes an assumption (P) and
    33. (derive): derives a consequence Q. The syntax using the symbols "Let{" and "}" like this: Let {(1)x:S, (2)P. |-..., |-Q}.

      Generic Semantics of a Proof

      After the end of the proof the declarations and assumptions are discarded and the whole proposition is derived in their place. The declarations and assumptions work exactly like the declarations in a block structured language (say C) - each argument adds a collection of declarations, assumptions and consequences on to a stack - all of which are deleted at the end of the argument, producing the desired conclusion in their place.

      Valid Forms of Proof

        Natural Proof

         ---------------------------------------------
         	 |-(l): for x:T, if P then Q.
        	...
         	. Proof of l
         	Let{(l1): x:T, (l2): P.	...|-Q. }.
          -----------------------------------------
         	|-(l): P or Q.
        	...
         	.Proof of l
         	Let{(l1): not P...	|- Q. }.
          -----------------------------------------
         	|- (l) for 0..1  x:T (W2(x)).
        	...
         	. Proof of l
         	Let{ (l1): x1,x2:T,(l2):W(x1), (l3):W(x2)....	|- x1=x2. }.
          -----------------------------------------
         	|- (l) for one  x:T (W2(x)).
        	...
         	. Proof of l
         	|-(l1): for some  x:T (W2(x)).
         	|-(l2): for 0..1  x:T (W2(x)).
         ---------------------------------------------

        Example of a Natural Proof


      1. |-if for some x, all y (x R y) then for all y, some x( x R y)
      2. Let{
        1. (np1): for some x, all y (x R y),
        2. (np2): not for all y, some x( x R y).
        3. (np1),(x=>a)|- (np3): for all y (a R y),
        4. (np2), (qn)|- (np4): for some y, all x(not x R y),
        5. (np4), (y=>b)|- (np5): for all x (not x R b),
        6. (np3), (y=>b)|- (np6): a R b,
        7. (np5), (x=>a)|- (np7): not a R b,
          }

        The third way to prove a proposition is by assuming the contrary and analysing it. The aim is to find contradictions in all possible alternatives. This has been called "Reducto ad Absurdum" for the last 2000 years or so. More recently it has been formalised as the method of Semantic tableau and used in Artificial Intelligence.

        Proofs do not always work out the way we want - for example sometimes to prove P, we assume not P but find one or more alternatives being left open, for instance Q. In this case, we can still 'harvest' a weaker proposition than P - P or Q.

        Thus in MATHS - at any time in a document - we can open up a hypothetical context, examine the consequences and then draw conclusions as we discard the context. An important guideline, which you may find goes very much against the grain - do not assume your goal, assume the opposite. In short proof consists of playing the devil's advocate, unsuccessfully.

      3. assertion::= axiom | conjecture | derived
      4. derived::= conclusion (argument|) | (deduction | argument) conclusion,
      5. label::="(" identifier "): ",
      6. axiom::= label wff,
      7. conjecture::='??{' documentation "}??",
      8. deduction::= O("("List( identifier | explanation ) ")" ) | algebraic_step | comment,
      9. conclusion::="|-" O(label) derived_wff.
      10. algebraic_step::=expression relation expression #( EOLN label relation expression),

        Algebra and Calculations

        MATHS combines natural deduction with algebra. An algebraic step uses an inference like the following:
      11. |-if e1 R1 e2 R2 e3...R[n-1] e[n] then e1 ;R e[n].

         -----------------------------

      12. Consider{ e1
      13. (y1). R1 e2
      14. (y2). R2 e3
      15. (y2). R3 e4
      16. ...
        }|-(l) e1 ;R e[n].

         -----------------------------

        In the above the ys are explanations of why the step is valid - typically a list of labels of theorems and axioms.

        Two forms are particularly useful. First when all the relations are equalities, and secondly when they are all iff.

         -----------------------------

      17. Consider{ e1
      18. (y1). = e2
      19. (y2). = e3
      20. (y3). = e4
      21. (y4). = e5
      22. ...
        }|-(l) e1 = e[n].

         -----------------------------

      23. Consider{ e1
      24. (y1). iff e2
      25. (y2). iff e3
      26. (y3). iff e4
      27. (y4). iff e5
      28. ...
        } |-(l) e1 iff e[n].

         -----------------------------

        David Gries has argued that this is the best kind of arguments for computer programming. He may be right. Gries ??

        Other forms of reasoning have been developed by mathematicians, see [ Algebra in math_10_Intro ]

        Trying Ideas Out

        For many years mathematicians have tended to use the words 'Let' and 'Consider' to introduce ideas for examination. MATHS also encourages creative (or lateral) thinking. At any time an idea can can be documented and experimented with - as long as it is in an enclosed context. Edward de Bono's work suggests there is need for a new word that frees the mind to examine the ideas without pre-judging them. He suggested "Po". "Po" invites the reader (or listener) to suspend judgment of an idea for a time. It means that the idea is thought about without evaluating it as true or false. Signiificantly the string "po" is found in "hypothesis", "suppose", "posit", "proposition" which indicates something of the way it is intended to work. It is also part of "poetry" - indicating that an idea can be thought about for aesthetic as well as pragmatic reasons. In MATHS the word 'Po' is followed by a set of (braced) documentation which includes the assumptions and derives the consequences. After the end of the argument a conclusion can be drawn from the complete process. Edward de Bono had no intent for "Po" to be part of a formal language, but by the lateral move of trying it out this author concludes that it works better than other words.

      29. po::= "Po"|"Let"|"Case" | "Consider"|...,
      30. Or::= "Or"|"Else"|"But"|....
      31. ender::="End po."
      32. argument::= (natural | analytical | reducto_ad_absurdum) &( po analysis #( or po analysis) ender).
      33. analysis::= hypothesis derivation closure.
      34. hypothesis::= #(axiom|comment|definition),
      35. derivation::=#(derived|comment|definition).
      36. closure::=derived.

        A case or proof must be closed when any proposition is derived which is the negation of a proposition previously derived in the current case, or any case that contains the current case.

        Analytical Proof

      37. analytical::= "Case" "{" analysis #(Or Analysis) "}".
          -------------------------------------------------------------

      38. (or): P or Q. Case{P. ... |-R. Else Q. ... |-R}. |- R
      39. (if): if P then Q. Case{notP. ... |-R. Else Q. ... |-R}. |- R
      40. (neg): not(P iff Q). Case{P,notQ. ... |-R. Else Q,not P. ... |-R}. |- R
          -------------------------------------------------------------

      41. |-analysis=reason"." "Case{" L(#(axiom | comment | definition) #(derived | comment | definition) derived, "Else" ) "}".

        Example Analytical Proof

          Example Classical Theorem


        1. |- (constructive_dilemma): if ((P or Q) and (if P then R) and (if Q then R)) then R

          Proof of constructive_dilemma

        2. Let{
        3. (cd1): P or Q,
        4. (cd2): if P then R,
        5. (cd3): if Q then R,
        6. (cd4): not R.

        7. Case{
        8. (cd5.1): P,
        9. |-R
        10. Else
        11. (cd5.2): Q,
        12. |-R
          }

        }

    . . . . . . . . . ( end of section Example) <<Contents | Index>>

    Reducto ad Absurdum

  1. reducto_ad_absurdum::= "Let" "{" hypothesis derivation closure "}".
      -------------------------------------------------------------

  2. (rabs1): Let { P, not Q... } |- if P then Q.
  3. (rabs2): Let{ not P, not Q....} |- P or Q.
  4. (rabs3): Let{ not P... }|- not P


  5. (rabs4): Let{x:T, not W(x)... } |- for all x:T(W(x)).
  6. (rabs5): Let{for all x:T(not W(x)),...} |- for some x:T(W(x))
      -------------------------------------------------------------

    Proof Templates

    An argument is a just special piece of documentation. MATHS naming/cross-reference rules apply, so a pattern of proof can by given a name and then be used in many places. Indeed modern mathematics forms a "rattlebag" of interesting and more or less useful templates. [ home.html ]

    Example of Useful Template

      [ INDUCTION in math_42_Numbers ]


    1. |- (triangle): for all n:Nat, +(1..n)=n*(n+1)/2.

      Proof of triangle

    2. Let{
    3. F::=fun[n:Nat](+1..n=n*(n+1)/2)).
    4. P::={n:Nat || (F(n) }.
    5. Consider{ (+(1..1)=1=1*(2)/2)
      }|- F(1)
    6. |- (1): 1 in P.

    7. Consider{ +(1..(k+1))= +(1..k) +(k+1)=k*(k+1)/2+k+1=(k+1)*(k+2)/2=(k+1)*((k+1)+1)/2.
      }

  7. |- (2): for all k:P(k+1 in P)
  8. (1),(2),(math_42_Numbers.html#INDUCTION) |- for all n:Nat, P(n).
    }.

. . . . . . . . . ( end of section Example of Useful Template) <<Contents | Index>>

Links to other useful Templates

.TBA (Your Page can be linked in here)

. . . . . . . . . ( end of section Valid Forms of Proof) <<Contents | Index>>

Note

MATHS proofs tend to be almost mechanical except for (1) choosing an expression to substitute for universally quantified variables (2) selecting the special cases to analyse. This can be quite difficult. Much theoretical work has been done in the field of Artificial Intelligence to make this as automatic as possible. It has been shown that in any interesting logic there can not exist an algorithm that will prove all true statements.

Tools

MATHS is a formal system designed for preparing documentation that includes valid reasoning. I have hopes that people will develop tools that do the routine derivations automatically, and automatically check the validity of the creative steps. Ideally the tools would point out the holes in incomplete arguments rather than just give an error message. .TBA Links to your tools can be put here... send me mail!

Plans

All the valid proof forms and documentation that I have experimented with have ended up with the same underlying structure. They are hierarchical labelled directed acyclic graphs. I therefore plan to re-examine the theory of lablled graphs in order to derive a more unified notation.

. . . . . . . . . ( end of section Proofs and Arguments) <<Contents | Index>>


Formulae and Definitions in Alphabetical Order