B.3 General Strategies
Direct Proof Given some knowledge K,
the usual situation is that we want to find out whether a formula G is
true or not, i.e., we don't know the truth of G in advance.
Therefore we have two possibilities of a direct proof:
- We try
. If we are successful,
then G holds.
- We try
. If we are
successful, then ~G holds.
If the first proof does not work out, it may give sufficient insight in order
to establish the second proof. If we can show ~G, we may have
gained additional insight that enables us to transform G into some
G' whose validity we can actually prove.
Indirect Proof
If we are not successful with direct attempts, we may try an indirect
proof where the goal is to derive a contradiction.
Proposition 140 (Proof by Contradiction)
For proving with knowledge K the goal G, it suffices to
prove F(alse) with additional knowledge ~G.
~~>
In natural language, a proof of G by contradiction is usually indicated
as
We assume ~G and show a contradiction.
A contradiction is usually derived by establishing a proof situation
because we then immediately have
~~>
K union {F(alse)} |
F(alse) |
~~>
.
Examples of such proofs are given in the proof of the Peano
laws from the set-theoretic construction of the natural
numbers or the proof that the square root of
2 is not a rational number.
Again, since we don't know the truth of G for sure, we generally
we have two possibilities:
- We try
. If we are successful, then G
holds.
- We try
.
If we are successful, then ~G holds.
If all attempts have failed, we have hopefully gained more insight to start a
new round of attempts with refined ideas.
Proof Directions
When pursuing a proof, we may proceed in two ways:
- Top-Down by decomposing the goal into simpler formulas
with corresponding subproofs.
~~>
...
- Bottom-Up by deriving new knowledge from the given knowledge
such that the goal ultimately becomes part of the knowledge.
~~>
In the course of a proof we mix top-down steps with bottom-up steps;
usually we begin with the top-down strategy.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999