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...".
------------------------------------
When P and Q have the same set of free variables we have:
------------------------------------
The following rules need special documentation
------------------------------------
W(e),(x=>e)|-for some x:T(W(x))
--(e is an expression of type T)
for some x:T(W(x)), (x=>v)|-v:T, W(v)
--(v is free variable)
for one x:T(W(x), (v=>x)|-W(v)
--(v is free variable)
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:
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:
So it is valid to derive
are often proved by documentation that
---------------------------------------------
|-(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)).
---------------------------------------------
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.
-----------------------------
-----------------------------
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.
-----------------------------
-----------------------------
-----------------------------
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 ]
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.
-------------------------------------------------------------
-------------------------------------------------------------
. . . . . . . . . ( end of section Example) <<Contents | Index>>
-------------------------------------------------------------
-------------------------------------------------------------
. . . . . . . . . ( end of section Example of Useful Template) <<Contents | Index>>
. . . . . . . . . ( end of section Valid Forms of Proof) <<Contents | Index>>
. . . . . . . . . ( end of section Proofs and Arguments) <<Contents | Index>>