## 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