Help with Proofs and Demonstrations

Introduction

For Internet pointers to automated proof systems, see [ Automation ] below.

There has been a lot of research that makes use of formal logic of one sort an another. To generate a quick list of pointers to citations see LOGIC

For a discussion of some differences between the way people think and formal logic, see [ Three Kinds of Inference ] below.

For more on how formal methods and creativity complement each other see [ Further Reading ] below.

But Why Prove anything Anyway?

To convince unbelievers. Many proofs are needed to convince the readers of a paper or thesis that the writer knows what they are talking about. In other cases it is the writer that doesn't quite believe a result and constructs a proof to convince themselves.
To provide an explanation for why a result is true. Proofs are constructed using assumptions and rules. These form an explanation of the result. You can then think about and challenge the assumptions. For example, to make a planned system safer, construct proofs of its safety, and then challenge the assumptions you used.
To see where the result fits into the other facts. Proofs provide a structure to a collection of statements. The power of Euclid is the structure that he provided to geometry reasoning from postulates to theorems and constructions. The structure in turn provides a mnemonic framework to help you learn and recall the results.
Working out a proof helps you memorize the result. This is one reason for all those exercises in Math, Physics, and Computer Science classes.
Training and exercises. When proofs are assigned as class or home work they are preparing the student for a future presentations and publications.

Hints

Analyze before you prove

polya

understand the problem;
- What are you given?
- Are you trying to prove something or to find something?
- What is the goal?
- How to relate the givens to the goal?
Define a notation.
Make a plan;
Carry out the plan;
Review the result.
Write up result...

../samples/polya.html

Proving both_and

logic_25_Proofs.html#Valid Deductive Steps

Combine what you know already

Syllogisms

All men are mortal.
Socrates is a man.
:. Socrates is mortal

In formal logic:

For all x, if man(x) then mortal(x).
man(socrates)
(-2)|-mortal(socrates)

Man ==> Mortal, socrates isa Man,
(-2)|-socrates isa Mortal.

By medieval times we had a gigantic list of these [ ../samples/syllogisms.html ] and algebra added more:

x < y,
y < z,
:. x < z.

But what to combine...?

Proving universals

For all whosis, if something then whatever introduce a new variable whosis and that something is true and try to show whatever as a result.
Let
1. whosis, something
2. <A miracle occurs>
3. whatever
(Close Let )
See [ logic_25_Proofs.html#Block Structure ] for a way to control the assumptions and results.

Proving equality and if_and_only_if
Often results of the form this = that or this if and only if that use [ logic_25_Proofs.html#Algebra and Calculations ] to figure from this to that.

Proving either_or
Sometimes when working with statements with special cases (P or Q) its easiest to use [ logic_25_Proofs.html#Proof by Cases ] to try out each possibility in turn.
Proving something exists
Sometimes you can find a suitable example. More often you need to construct an example out of existing objects using the construction rules are accepted in your discipline. For example, in Euclid, you used compasses and a straight edge. These days, we can use algebra -- or even a calculator. Indeed, in some disciplines, it is enough to show that an infnite series of approximations to a desired object get as close as we would like to what we want. So proving something exists boils down to [ Finding something ]
Sometimes we are forced to go a different route -- assume that an object does not exist and derive a contradiction. Notice that a whole branch of mathematics intuitionstic rejects this approach and demands that if you want to calim that something exists, then you must give a method for constructing an example.
Finding something
One way of finding something is to show how to construct it from other given things. The terminology goes back to Euclid.
In MATHS we might express a Euclidean construction like this
For all x:T1, where P1, find a y such that P2.
Let
1. x :T1=given,
2. (given)|-P1.
3. y :T2=goal,
4. (goal): P2.
5. z:=....,
6. z2:=....,
7. ...
8. y:=...
  ...|-(desired property): P2.
  Proof of desired property.
9. ...
(Close Let )

Example 1 Euclid Book I Proposition 1
. . . . . . . . . ( end of section Example 1) <<Contents | End>>
Algebra (using symbols for unknowns, and expressions to symbolize the construction of other things, ...) is a powerful tool for finding something that fits a property.
Algebra picks up Pappus's idea of stating with what you want -- expressed as an unkown -- and then expresing the constraints on the unkown... in the hope of transforming these into a known object.

Example 2
1. The sum of four consecutive numbers is one less than a square.
  I did a lot of exploration which, when pruned of errors and dead ends became:
  Net
  1. n(n+1)(n+2)(n+3) + 1
  2. The obvious approach is to multiply this out and then recognise that the formula is the square of some obvious expression. But when I tried this, the obvious escaped me.
    
    If it was multiplied out, it would be a polynomial in n with leading and last coefficients equal to one:
  3. n^4 + ... + 1.
  4. So, if this is a square, it must have form:
  5. (n^2 + a*n + 1)^2, for some a.
  6. When n=1:
  7. (1^1 + a*1 +1)^2 = 1*2*3*4 + 1,
  8. (a+1)^2 = 25,
  9. (a+1) = 5,
  10. a = 4.
    So we have found an a and so can now go to the rigorous proof of the simpler result
  11. n(n+1)(n+2)(n+3) + 1 = (n^2+5*n+1)^2.
  12. ...
  (End of Net)
  Notice that the algebra in the middle of the above is not a rigorous proof. It just discovers a formula that can then be proved using algebraic techniques -- ones where we can check every step by the rules.
  The proof goes like this... but you can fill in the blank:
  Let
  1. n:Int.
  2. n(n+1)(n+2)(n+3) + 1 = ... = ... = ...
  3. (n^2+5*n+1)^2 = ... = ... = ...
  4. (above)|-n(n+1)(n+2)(n+3) + 1 = (n^2+5*n+1)^2,
  5. (-1)|-for some m, n(n+1)(n+2)(n+3) + 1 = m^2.
  (Close Let )
. . . . . . . . . ( end of section Example 2) <<Contents | End>>
Example 3 Construction as a series of definitions
Proving something doesn't exist
About the only way to tackle this is to assume that the thing in question exists and show that if it did then impossible things happen. Sometimes the end point is a simple contradiction. This is called reducto ad absurdum -- in Latin. [ logic_25_Proofs.html#Reducto ad Absurdum ]
In other cases you show that if an A exists then some other object B can be constructed from A, and this object B we already know doesn't exist:
Let
1. Some A exists.
2. Construct B from A.
3. (-1)|-Some B exists.
4. (previous)|-B does not exist.
(Close Let )
(-1)|-A can not exist.
This kind of proof is popular in computer theory texts -- it is called reduction.

Stuck?
A weird but valid trick (when stuck?) is to start by denying the truth that you want to establish and show that the result is absurd: [ logic_25_Proofs.html#Reducto ad Absurdum ] is the Latin term for this...
If you are really stuck for ideas, then try relaxing and playing with various possibilities: what if, Suppose, perhaps,... [ logic_25_Proofs.html#Trying Ideas Out ] This is a traditional technique for mathematicians with a problem to solve. Often when you've worked on a problem long enough the key idea will come to you "out of the blue" while getting onto a bus or shopping.
Sometimes it helps to loosen up and do something silly. An example is DST [ The Dilbert Salary Theorem ] which was recently proved after years of diligent research.
Another strategy is to browse the ready made [ logic_25_Proofs.html#Proof Templates ] out there waiting to be used. Every field has it's own proof methods. It is, therefore, well worth studying these in preparation to publishing or presenting a proof.

Practice
It pays to practice the techniques on lots of unimportant problems just to train the brain. Hence the many exercises in good math classes.

Read
Finally: There are many excellent books that can improve your proving and problem solving skills: [ Further Reading ] below.

. . . . . . . . . ( end of section Hints) <<Contents | End>>

Even more intriguing: if a valid argument leads to a known truth then it say nothing about the truth of the assumptions. An argument never says anything positive about assumptions. It can show something positive about a conclusion however.

When a set of assumptions leads to a false conclusion then one of the assumptions (at least) is false. Thus arguments help us question our assumptions. Hence they lead us to revise them until we have a set the do not contradict reality. The revision process, by the way, is not a logical process, but a dialectical one -- the steps are error prone. Indeed we may need a way to record the counter-arguments or rebuttals that develop in a real argument.

Quick Example

All birds can fly,
All penguins are birds,
No penguin can fly.
(above)|-No penguins.

So when we meet a real penguin and it does not fly, we need to revise our assumptions. Perhaps penguins fly under water? Perhaps some birds are flightless? Perhaps we have mis-classified penguins as birds? Choosing the right one to change is not a logical process but you can probably do it intuitively... Or if we are scientific we spend more time studying birds: sparrows, ostriches, crows, kiwi, canaries, cassowary, and so on, We may end up with birds divided into normal_birds and flightless_birds.
Let

All birds are normal_birds or flightless_birds,
No normal_birds and flightless_birds,
All normal_birds can fly,
All penguins are birds,
No penguin can fly.
(above)|-Penguins are flightless_birds.

In every day reasoning we are used to arguments that can be defeated by other arguments. Many of these are like the above and can be resolved by refining our assumptions. There has been research into the structures of these defeasible, dialectic, or plausible arguments: see [ChesnevarMaguitmanLoui00] for a history. Handling contradictory assumptions is also a key part of requirements analysis in developing software and there have been attempts to develop logics that help in this task. See [HunterNuseibeh97] [Nuseibehetal94] [Finkelsteinetal94] etc. for example. You can get a quick bibliography of recent work consistency by using my search engine: [Cc]onsisten

In MATHS we can document rebuttals simply:
But

Penguins can't fly.

Rebuttals should be put after an argument that is not a full proof or a statement. Several rebuttals put after a statment and the all attack that proof/statment. To rebut a rebuttal, place it inside the first rebuttal.

Let

It is raining.
If it rains I get will get wet.
|-I will get wet.

I carry an umbrella.
But
1. The wind is blowing.
(Close But )

In a sense the penguin problem arises for the rarity of penguins and other flightless birds. If more birds did not fly we wouldn't have assumed that "all" fly. There have been attempts to develop reasoning based on statements like "All birds normally fly". In mathematics, some thing analogous happens. You will see statements like:

"In all but a finite number of cases,...."
"Everywhere, except on a set of measure zero, ..."
"For large enough values, ...."
"In the normal case,...."

Advanced%20Quantifiers in logic_11_Equality_etc

Probability and statistics are the branches of mathematics that are designed to handle these problems. Statements like 90% of all birds can fly. allow us to reason about uncertain situations. But they are essentially a more complicated than the propositions on this page. However, we can make a theory of probability using the simple logic discussed here. See [ math_81_Probabillity.html ]

. . . . . . . . . ( end of section Quick Example) <<Contents | End>>

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.

There has been a lot of work done in the 1990s on inconsistent requirements for software. When talking to people about what they want software to do it is common to find large numbers of small and large contradictions. It is wise to do something about these when they are discovered.

In any case a contradiction that occurs in MATHS is anything but a disaster! It is an opportunity to form a conclusion. It proves 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. The result is a new theorem!

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 demonstration 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.

Imre Lakatos studied the detailed behavior of mathematicians when faced with a proved theorem and a number of exceptions to it in the 19th century. From this he worked out an interesting heuristic (a guide for the in expert). A valid proof is(by definition) one that, given true 'givens' guarantees the truth of the conclusion. Now most proofs are some what incomplete but it is possible (by hard work) to construct such iron chains leading from assumptions to conclusions. In any case, Lakatos pointed out that this means that if the conclusion contradicts some other fact you should examine what you have taken as given, what you have assumed in the proof, to which of these are also contradicted. The assumptions that conflict with the new data can now either be improved, or they may have to be incorporated into the statement of the theorem. In summary, a proof plus a refutation improves the theory. See [ Further Reading ]

Absurdity happens! You will find that your cherished and documented assumptions leading to conclusions that do not fit with observation. Again this is an opportunity not 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". Astronomy is full of examples of absurd ideas being rejected that were accepted later. 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' philosophy, his followers later rejected Newton's law of gravitation. For more on the history of astronomy see: Koestler 59 , Arthur Koestler, "The Sleepwalkers" Acknowledgment:

I'd like to thank m.dolbear@lineone.net for advice on redrafting the above paragraph in September 2001.

An engineer is in trouble when reality shows up a misunderstanding - because the system often becomes unsafe or ceases to work. 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...".

. . . . . . . . . ( end of section Motivation and Theory) <<Contents | End>>

Automation

For example, formulas in the propositional calculus can be proved by several algorithms:
Table

Truth Tables (Mil Post)
Proof_by_cases+Indirect (Jensen)
Tree structured analysis [ logic_27_Tableaux.html ]
Boolean Algebra (Boole)

(Close Table)
Notice however that except in the simplest cases the problem is intractable. If we have n propositional variables the time to prove/disprove a statement increases as at least the exponential on n. The problem harder when we have predicates and equality to worry about. Indeed it has been shown to be unsolvable! For practical evidence of the difficulties of proving some theorems, consider that some (Fermat's Last Theorem for example) took 400 years to prove. Indeed sometimes a proof could only be discovered by somebody who is not searching for it. The proof lies within a separated field of study to where the theorem appeared!


Truth Tables (Mil Post)
Proof_by_cases+Indirect (Jensen)
Tree structured analysis [ logic_27_Tableaux.html ]
Boolean Algebra (Boole)

Tools and notations can clear the logical underbrush and allow the necessary creative steps to be made.

There are tools on the WWW. For example there is an automatic theorem prover for many non-classical propositional logics: [ LWBinfo.html ]

I have developed a very simple Prolog program to evaluate, test and disprove boolean expressions: [ bool.plg ] and in some courses students are asked to write a program to generate semantic tableaux: [ project2.html ]

Full blown theorem provers tend to need human intervention and guidance. The record for humans trying to prove a theorem is approximately 400 hundred years.

One popular tool for computer people is the Prototype Verification System:

PVS::= See http://pvs.csl.sri.com/, at SRI.
[click here Links to your tools can be put here. if you can fill this hole]

. . . . . . . . . ( end of section Automation) <<Contents | End>>

The Dilbert Salary Theorem

(physics, proverbs)|- (DST): Engineers and scientists can never earn as much as administrators and sales people.
The following proof was supplied to Tom and Ray [ http://cartalk.cars.com/ ] by From Kate Fowler, Denver, Colorado. As an informal proof [ 04.29.html ] in April of 2000.

Proof of DST

Net
1. (physics)|- (dst1): Power = Work / Time.
2. (proverbs)|- (dst2): Knowledge = Power.
3. (proverbs)|- (dst3): Time = Money.
4. (dst1, dst2, Power => Knowledge)|-
5. Knowledge = Work/ Time,
6. (dst3, Time => Money)|-
7. iff Knowledge = Work/ Money,
8. ( * Money, / Knowledge )|-
9. iff Money = Work/ Knowledge.
10. (-1)|-knowledge approaches zero, money approaches infinity, as long as some work is done.
11. (-1)|- (Conclusion): the less you know, the more you make.
(End of Net)
Exercise on the DST
So, why is the above argument invalid? And why is the conclusion still OK?

. . . . . . . . . ( end of section The Dilbert Salary Theorem) <<Contents | End>>

Glossary

above::reason="I'm too lazy to work out which of the above statements I need here".
given::reason="I've been told that...", used to describe the given part of a problem or a logical system.
goal::theorem="The result I'm trying to prove right now".
let::reason="For the sake of argument let...", many times a proof starts by assuming something called the hypothesis, [ logic_25_Proofs.html#Block Structure ]
hyp::reason="I assumed this in the last Let".
RAA::reason="Reducto Ad Absurdum".
reason::="Something that often appears as the evidence input to a step in an argument."

. . . . . . . . . ( end of section Glossary) <<Contents | End>>

Comments and Reviews

dick

Csci CSUSB edu

. . . . . . . . . ( end of section Comments and Reviews) <<Contents | End>>

Glossary

argument::=A sequence of steps that go from a set of assumptions(given) to a conclusion(goal).
valid::=Something that can not produce a false conclusion from true givens. There are valid arguments, valid proofs, and valid steps.

. . . . . . . . . ( end of section Help with Proofs and Demonstrations) <<Contents | End>>

Notes on MATHS Notation

intro_characters.html

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. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. 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. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

logic_0_Intro.html

For a more rigorous description of the standard notations see

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
Glossary
above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
given::reason="I've been told that...", used to describe a problem.
given::variable="I'll be given a value or object like this...", used to describe a problem.
goal::theorem="The result I'm trying to prove right now".
goal::variable="The value or object I'm trying to find or construct".
let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
hyp::reason="I assumed this in my last Let/Case/Po/...".
QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

Contents

Help with Proofs and Demonstrations

Introduction

Analyze before you prove

Proving something exists

Proof of desired property.

Example 1 Euclid Book I Proposition 1

Proof of p1

Proof of qe

Polya -- How to Solve it

Arguments

Exercise on the DST

Glossary

End