Go backward to B.3 General StrategiesGo up to B Proving PropositionsGo forward to B.5 Deriving New Knowledge |

K |

G |

~~>

Kforallx:G(

KG[x<-a]anot inKunion {G})

In the proof of a universal formula we thus replace the variable by a constant about which no assumptions have been made yet. This may be indicated in a natural language proof in a very verbose form as

We have to prove (forallx:G). We take an arbitrary (but fixed) constantaand showG[x<-a].

Usually, we choose instead of `a` some name that indicates the name of
the corresponding variable, e.g., __ x__. Even more
frequently, we simply chose

We have to prove (or even shorterforallx:G). We take arbitraryxand showG.

We have to prove (However, we have to understand thatforallx:G). Take arbitraryx. Then ...(proof ofG).

Frequently also the *indirect method* is applied in such a situation.
Instead of proving (**forall** `x`: `G`) we assume
(~**forall** `x`: `G`), i.e.,
(**exists** `x`: ~`G`) and proceed to derive a contradiction
with the help of a constant `a` such that `G` holds (see
Proposition *Existential Knowledge*):

~~>

Kforallx:G~~>

Kunion {existsx: ~G}F(alse)

Kunion {~G[x<-a]}F(alse)

This is typically indicated as

We have to prove (In this formulation,forallx:G). Assume ~Gfor somex. Then ... (derivation of a contradiction with additional knowledge ~G).

~~>

Kexistsx:G

KG[x<-T]

An existential proof requires creativity. We have to find a
*witness (Zeugen)*, i.e., a value for `x` that makes `G`
true. This value can be only constructed from those function and object
constants about which we have some knowledge in `K` such that we can
proceed to prove `G`.

In natural language, such a proof is usually indicated as

We have to prove (existsx:G). We proveG[x<-T].

or, if `x` occurs multiple times in `G`, shorter as

We have to prove (existsx:G). Takea:=T. We proveG[x<-a].

where `a` is an object constant that does not appear in `K` and for
which we assume the additional knowledge `a` = `T`. Even shorter,
we may write

We have to prove (existsx:G). Takex:=T. We then have ...(proof ofGwith additional knowledgex=T).

This is possible if `x` *does not occur freely in* `K`.

For examples, see the proof of Proposition *Density of
Rationals* or the
proof of the existence of a factorization into prime
numbers.

The *indirect method* may be applied by assuming
(~**exists** `x`: `G`), i.e.,
(**forall** `x`: ~`G`) and deriving a contradiction,
see Proposition *Universal Knowledge*:

~~>

Kexistsx:G.

Kunion {forallx: ~G}F(alse)

This is usually indicated as follows:

We have to prove (existsx:G). Assume (forallx: ~G). Then ... (derivation of a contradiction with additional knowledge (forallx: ~G)).

~~>

KG_{0}<=>G_{1}

KG_{0}=>G_{1}

KG_{1}=>G_{0}

An equivalence is shown by proving the implication "from left to right" and "from right to left", sometimes denoted as

We have to proveG_{0}<=>G_{1}:

- => : ...(proof of
G_{0}=>G_{1}).- <= : ...(proof of
G_{1}=>G_{0}).

If we have to show `G`_{0} <=> `G`_{1} <=> `G`_{2}, i.e.,
(`G`_{0} <=> `G`_{1}) /\ (`G`_{1} <=> `G`_{0}), it
suffices to "traverse the circle", i.e., to show (`G`_{0} => `G`_{1}) /\ (`G`_{1} => `G`_{2}) /\ (`G`_{2} => `G`_{0}) (and analogously for an arbitrary number of
equivalences).

Examples are shown in the proofs of Proposition *Equality and
Subset* and of
Proposition *Relation Laws*.

~~>

KG_{0}=>G_{1}

Kunion {G_{0}}G_{1}

Almost every proof contains applications of above rule indicated as

We have to showG_{0}=>G_{1}. AssumeG_{0}. Then ...(proof ofG_{1}with additional knowledgeG_{0}).

Because of (`G`_{0} => `G`_{1}) iff
(~`G`_{1}
=> ~`G`_{0}), an alternative is to apply the rule

indicated as~~>

KG_{0}=>G_{1}

Kunion {~G_{1}}~ G_{0}

We have to showG_{0}=>G_{1}. Assume ~G_{1}. Then ...(proof of ~G_{0}with additional knowledge ~G_{1}).

Because of ~(`G`_{0} => `G`_{1}) iff
(`G`_{0} /\ ~`G`_{1}), the indirect method yields

which is typically indicated as~~>

KG_{0}=>G_{1}

Kunion {G_{0}/\ ~G_{1}}F(alse)

We have to showG_{0}=>G_{1}. AssumeG_{0}/\ ~G_{1}. Then we have ... (derivation of a contradiction).

Examples are given in the proofs of
Proposition *Equality* and of the Second Peano
Law.

~~>

KG_{0}/\G_{1}

KG_{0}

KG_{1}

A conjunction is shown by showing both conjuncts in turn:

We have to showG_{0}/\G_{1}.

- ...(proof of
G_{0}).- ...(proof of
G_{1}).

Because of ~(`G`_{0} /\ `G`_{1}) iff
~`G`_{0} \/ ~`G`_{1}, the *indirect method*
leads to

applying the technique of "case distinction":~~>

KG_{0}/\G_{1}~~>

Kunion {~G_{0}\/ ~G_{1}}F(alse)

Kunion ~G_{0}F(alse)

Kunion ~G_{1}F(alse)

We have to proveG_{0}/\G_{1}.

- Assume ~
G_{0}. Then ...(derivation of contradiction with additional assumption ~G_{0}).- Assume ~
G_{1}. Then ...(derivation of contradiction with additional assumption ~G_{1}).

Examples of proofs of conjunctions are given for Proposition *Function
Composition* for the existence of
a factorization into prime numbers.

~~>

KG_{0}\/G_{1}

Kunion ~G_{0}G_{1}

This rule is a consequence of "(`G`_{0} \/ `G`_{1})
iff (~`G`_{0} => `G`_{1})"
such that the same techniques can be applied as for the decomposition of
implications:

We have to showG_{0}\/G_{1}. Assume ~G_{0}. Then ...(proof ofG_{1}).

Of course, the roles of `G`_{0} and `G`_{1} can be inverted.

Frequently, in a particular proof situation, the additional assumption is not required and one simply says

We have to showG_{0}\/G_{1}. We have ...(proof ofG_{0}or ofG_{1}).

andp(x_{0}, ...,x_{n-1}) : <=>G,

~~>

Kunion {forallx_{0}, ...,x_{n-1}:p(x_{0}, ...,x_{n-1}) <=>G}p(a_{0}, ...,a_{n-1})

Kunion {forallx_{0}, ...,x_{n-1}:p(x_{0}, ...,x_{n-1}) <=>G}G[x_{0}<-a_{0}, ...,x_{n-1}<-a_{n-1}]

We may thus just insert the definition of a predicate into a goal formula:

We have to provep(a_{0}, ...,a_{n-1}). By definition ofp, it suffices to proveG[x_{0}<-a_{0}, ...,x_{n-1}<-a_{n-1}].

The proofs of Proposition *Equality and Subset* and of Proposition *Function
Composition* show applications of
above rule.

it suffices to proveG(x_{0}, ...,x_{n-1}) :=T,

~~>

Kunion {forallx_{0}, ...,x_{n-1}:G(x_{0}, ...,x_{n-1}) =T}G[x<-G(a_{0}, ...,a_{n-1})]

Kunion {forallx_{0}, ...,x_{n-1}:G(x_{0}, ...,x_{n-1}) =T}G[x<-T[x_{0}<-a_{0}, ...,x_{n-1}<-a_{n-1}]]

Above rule simply tells us that, if a goal contains an elementary term with an explicitly defined function, we are allowed to "insert the definition" of the function:

We have to prove F[x<-G(a_{0}, ...,a_{n-1})]. By definition ofG, it suffices to proveG[x<-T[x_{0}<-a_{0}, ...,x_{n-1}<-a_{n-1}]].

Examples are given by the proofs of Proposition *Function
Composition* and of
Proposition *Quotient*.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999