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

Proofs and Arguments

Introduction

Absurdity and Contradictions

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

Natural Deduction

if P and R then Q

P, R|-Q

P|-Q

Q|-P

W(P) iff W(Q)

f(P) = f(Q)

Valid Deductive Steps

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

(and1): if P and Q then P
(and2): if P and Q then Q
(demorgan1): not(P and Q) iff not P or not Q
(and3): if P and Q then P and Q
(or1): if (P or Q) and not P then Q
(or2): if (P or Q and not Q then P
(or3): if not(P or Q) then not P
(or4): if not(P or Q) then not Q
(mp): if (P and(if P then Q) then Q
(mtp): if (not Q) and (if P then Q) then not P
(nif1): if not(if P then Q) then P
(nif1): if not(if P then Q) then not Q
(iff1): if (P iff Q)then if P then Q
(iff2): if (P iff Q)then if Q then P
When P and Q have the same set of free variables we have:
(iff3): if (P iff Q)then (W(P) iff W(Q))
(iff4): if (P iff Q)then (f(P) = f(Q))
(qn1): not for some x:T(W(x)) iff for all x:T(not W(x))
(qn2): not for all x:T(W(x)) iff for some x:T(not W(x))
```
  ------------------------------------
```
The following rules need special documentation
```
  ------------------------------------
```

(eg):

 	W(e),(x=>e)|-for some x:T(W(x))

			--(e is an expression of type T)

(ei):

 	for some x:T(W(x)), (x=>v)|-v:T, W(v)

			--(v is free variable)

(ui):

 	for one x:T(W(x), (v=>x)|-W(v)

			--(v is free variable)

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

(mp): |- if P and if P then Q then Q.
(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:
(Sqrt): For all Real x, y, if x=sqrt(y) then y=x*x,
So it is valid to derive
(s2): 9 = 3*3 from (s1): 3=sqrt(9) by
(Sqrt, x=>3, y=>9) |- if 3=sqrt(9) then 9=3*3,
(1, mp) |- 9=3*3. Normally details are omitted:
(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
for x:S, if P then Q
are often proved by documentation that
(declare): introduces a temporary declaration (x:S),
(assume): makes an assumption (P) and
(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
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
  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

reducto_ad_absurdum::= "Let" "{" hypothesis derivation closure "}".
```
  -------------------------------------------------------------
```
(rabs1): Let { P, not Q... } |- if P then Q.
(rabs2): Let{ not P, not Q....} |- P or Q.
(rabs3): Let{ not P... }|- not P
(rabs4): Let{x:T, not W(x)... } |- for all x:T(W(x)).
(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
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.
  }
|- (2): for all k:P(k+1 in P)
(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

1 (Axiom)
2 (Axiom)
algebraic_step (Definition)
analysis (Definition)
analytical (Definition)
and1 (Formula)
and2 (Formula)
and3 (Formula)
argument (Definition)
assertion (Definition)
assume (Formula)
axiom (Definition)
cd1 (Formula)
cd2 (Formula)
cd3 (Formula)
cd4 (Formula)
cd5.1 (Formula)
cd5.2 (Formula)
closure (Definition)
conclusion (Definition)
conjecture (Definition)
constructive_dilemma (Axiom)
declare (Formula)
deduction (Definition)
demorgan1 (Formula)
derivation (Definition)
derived (Definition)
derive (Formula)
eg (Formula)
ei (Formula)
e is an expression of type T (Label)
e is an expression of type T (Label)
ender (Definition)
F (Definition)
hypothesis (Definition)
iff1 (Formula)
iff2 (Formula)
iff3 (Formula)
iff4 (Formula)
l1 (Axiom)
l2 (Axiom)
label (Definition)
l (Axiom)
l (Axiom)
mp (Formula)
mtp (Formula)
nif1 (Formula)
nif1 (Formula)
np1 (Formula)
np2 (Formula)
np3 (Theorem)
np4 (Theorem)
np5 (Theorem)
np6 (Theorem)
np7 (Theorem)
or1 (Formula)
or2 (Formula)
or3 (Formula)
or4 (Formula)
Or (Definition)
po (Definition)
P (Definition)
qn1 (Formula)
qn2 (Formula)
reducto_ad_absurdum (Definition)
s1 (Label)
s2 (Formula)
Sqrt (Formula)
triangle (Axiom)
ui (Formula)
ui (Formula)
v is free variable (Label)
v is free variable (Label)

Contents

Proofs and Arguments

Introduction

Absurdity and Contradictions

Two Systems of Proof

Natural Deduction

Valid Deductive Steps

Omitting reasons

Theorems Linked to Proofs

Block Structure

Generic Semantics of a Proof

Valid Forms of Proof

Natural Proof

Example of a Natural Proof

Algebra and Calculations

Trying Ideas Out

Analytical Proof

Example Analytical Proof

Example Classical Theorem

Proof of constructive_dilemma

Reducto ad Absurdum

Proof Templates

Example of Useful Template

Proof of triangle

Links to other useful Templates

Note

Tools

Plans

Formulae and Definitions in Alphabetical Order