.Open 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
.As_is ------------------------------------
(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))
.As_is ------------------------------------
The following rules need special documentation
.As_is ------------------------------------
(eg):
.As_is W(e),(x=>e)|-for some x:T(W(x))
.As_is --(e is an expression of type T)
(ei):
.As_is for some x:T(W(x)), (x=>v)|-v:T, W(v)
.As_is --(v is free variable)
(ui):
.As_is for one x:T(W(x), (v=>x)|-W(v)
.As_is --(v is free variable)
(ui):
.As_is for all x:T(W(x)), (v=>x)|- W(e)
.As_is --(e is an expression of type T)
.As_is ------------------------------------
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.
.Open Valid Forms of Proof
. Natural Proof
.As_is ---------------------------------------------
.As_is |-(l): for x:T, if P then Q.
.As_is ...
.As_is . Proof of l
.As_is Let{(l1): x:T, (l2): P. ...|-Q. }.
.As_is -----------------------------------------
.As_is |-(l): P or Q.
.As_is ...
.As_is .Proof of l
.As_is Let{(l1): not P... |- Q. }.
.As_is -----------------------------------------
.As_is |- (l) for 0..1 x:T (W2(x)).
.As_is ...
.As_is . Proof of l
.As_is Let{ (l1): x1,x2:T,(l2):W(x1), (l3):W(x2).... |- x1=x2. }.
.As_is -----------------------------------------
.As_is |- (l) for one x:T (W2(x)).
.As_is ...
.As_is . Proof of l
.As_is |-(l1): for some x:T (W2(x)).
.As_is |-(l2): for 0..1 x:T (W2(x)).
.As_is ---------------------------------------------
. Example of a Natural Proof
|- if for some x, all y (x R y) then for all y, some x( x R y)
Let{
(np1): for some x, all y (x R y),
(np2): not for all y, some x( x R y).
(np1),(x=>a)|-(np3): for all y (a R y),
(np2), (qn)|-(np4): for some y, all x(not x R y),
(np4), (y=>b)|-(np5): for all x (not x R b),
(np3), (y=>b)|-(np6): a R b,
(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.
assertion::= axiom | conjecture | derived
derived::= conclusion (argument|) | (deduction | argument) conclusion,
label::="(" identifier "):",
axiom::= label wff,
conjecture::='??{' documentation "}??",
deduction::= O("("List( identifier | explanation ) ")" ) | algebraic_step | comment,
conclusion::="|-" O(label) derived_wff.
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:
|- if e1 R1 e2 R2 e3...R[n-1] e[n] then e1 ;R e[n].
.As_is -----------------------------
Consider{ e1
(y1). R1 e2
(y2). R2 e3
(y2). R3 e4
...
}|-(l) e1 ;R e[n].
.As_is -----------------------------
In the above the `y`s 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`.
.As_is -----------------------------
Consider{ e1
(y1). = e2
(y2). = e3
(y3). = e4
(y4). = e5
...
}|-(l) e1 = e[n].
.As_is -----------------------------
Consider{ e1
(y1). iff e2
(y2). iff e3
(y3). iff e4
(y4). iff e5
...
} |-(l) e1 iff e[n].
.As_is -----------------------------
David Gries has argued that this is the best kind of arguments for computer programming. He may be right.
.Source Gries ??
Other forms of reasoning have been developed by mathematicians, see
.See http://www/dick/maths/math_10_Intro.html#Algebra
. 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.
po::= "Po"|"Let"|"Case" | "Consider"|...,
Or::= "Or"|"Else"|"But"|....
ender::="End po."
argument::= (natural | analytical | reducto_ad_absurdum) &( po analysis #( or po analysis) ender).
analysis::= hypothesis derivation closure.
hypothesis::= #(axiom|comment|definition),
derivation::=#(derived|comment|definition).
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
analytical::= "Case" "{" analysis #(Or Analysis) "}".
.As_is -------------------------------------------------------------
(or): P or Q. Case{P. ... |-R. Else Q. ... |-R}. |- R
(if): if P then Q. Case{notP. ... |-R. Else Q. ... |-R}. |- R
(neg): not(P iff Q). Case{P,notQ. ... |-R. Else Q,not P. ... |-R}. |- R
.As_is -------------------------------------------------------------
|- analysis=reason"." "Case{" L(#(axiom | comment | definition) #(derived | comment | definition) derived, "Else" ) "}".
.Open Example Analytical Proof
. Example Classical Theorem
|-(constructive_dilemma): if ((P or Q) and (if P then R) and (if Q then R)) then R
. Proof of constructive_dilemma
Let{
(cd1): P or Q,
(cd2): if P then R,
(cd3): if Q then R,
(cd4): not R.
Case{
(cd5.1): P,
|- R
Else
(cd5.2): Q,
|- R
}
}
.Close Example
. Reducto ad Absurdum
reducto_ad_absurdum::= "Let" "{" hypothesis derivation closure "}".
.As_is -------------------------------------------------------------
(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))
.As_is -------------------------------------------------------------
. 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.
.See http://www/dick/maths/home.html
.Open Example of Useful Template
.See http://www/dick/maths/math_42_Numbers.html#INDUCTION
|-(triangle): for all n:Nat, +(1..n)=n*(n+1)/2.
. Proof of triangle
Let{
F::=fun[n:Nat](+1..n=n*(n+1)/2)).
P::={n:Nat || (F(n) }.
Consider{ (+(1..1)=1=1*(2)/2)
}|- F(1)
|-(1): 1 in P.
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).
}.
.Close Example of Useful Template
. Links to other useful Templates
.TBA (Your Page can be linked in here)
.Close Valid Forms of Proof
. 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.
.Close Proofs and Arguments