Go backward to B.5 Deriving New KnowledgeGo up to B Proving Propositions |

x|y: <=>existszinN:x*z=y;gcd( x,y) :=suchzinN:z|x/\z|y/\ (forallg: (g|x/\g|y) =>g<=z).

Our goal is to prove

forallminN,n<=m: gcd(m,n) = gcd(m-n,n),

i.e., the greatest common divisor of `m` and `n` is also the
greatest common divisor of `m`-`n` and `n`.

An argument as it can be found in a typical text book is the following.

Take `h` such that `h` divides `m` and `h`
divides `n`. Then `h` also divides
`m`-`n`. Since g is the gcd of m and
`m`-`n`, `h` is less than or equal `g`.

This "proof skeleton" captures on a very high-level the *key idea* that
represents the basis of a "real" proof. However, this idea is only
understandable with the knowledge of the rules introduced in the previous
sections. Then it becomes also clear that the skeleton actually reflects the
structure of a more detailed proof such as the one given below (with
additional explanations that are not part of the proof added in
*italics*).

*We have to prove a universally quantified implication. We introduce arbitrary constants m and n and add
the implication hypothesis (m in N /\ n <= m) to our knowledge. We now have to show the goal
gcd(m,
n) = gcd(m-n).*

If `m`=0 /\ `n`=0, we are done.

*We proceed by case distinction. In the first case m=0 /\ n=0, we know gcd(m, n) = gcd(0, 0) =
gcd(0-0, 0) = gcd(m-n). By transitivity of =, we have the goal.*

Otherwise, `m` != 0 \/ `n` != 0.
We can show that in this case there exists a unique `z` in **N** with

z|m/\z|n/\ (forallg: (g|m/\g|n) =>g<=z).

*The rest of the proof deals with the second case m != 0 \/ n != 0. We claim that in this case above formula holds
(which requires a separate proof) and use this as knowledge from now on.*

For every `z`' in **N**, in order to prove

it therefore suffices to provez' = gcd(m,n),

z' |m/\ z' |n/\ (forallg: (g|m/\g|n) =>g<= z').

*We justify a reasoning step that will be used below: we have to prove
that a particular object equals gcd( m, n). By the
rule of substitution, we may insert the definition of gcd and thus
have to prove that the object equals the value of a "such term". We thus
remind the reader of the proof rule for this kind of terms
and instantiate the rule with the
concrete formula. The application of this rule requires that only one object
satisfies the formula in the "such term", which is exactly what we have
added as knowledge above.*

Let `g` := gcd(`m`-`n`, `n`).
By `n` <= `m`, we know

(1)g| (m-n) /\g|n/\ (forallh: (h| (m-n) /\h|n) =>h<=g).

*We define an abbreviation g for
gcd(m-n, n). Since n <= m, we have m-n
in N. Since m != 0 \/ n != 0, also m-n != 0 \/ n != 0 (which has to be
shown in a small subproof). By the knowledge added above, we thus have an
object that satisfies the formula in the definition of
gcd(m-n, n). Therefore we may apply the
corresponding rule for "such terms" and assume that g satisfies this
formula as well.*

We have to show `g` = gcd(`m`, `n`), i.e.,
by the explanation above

(2)g|m/\g|n/\ (forallh: (h|m/\h|n) =>h<=g).

*We apply the reasoning step explained above. Now we have to
prove the conjunction by showing each conjunct in turn.*

- We show (3)
`g`|`m`. Because of (1), we have some`a`and`b`with`g``a`=`m`-`n`and`g``b`=`n`. Then we know`g`(`a`+`b`) =`g``a`+`g``b`= (`m`-`n`) +`n`=`m`;*We insert the definition of | into knowledge (1), which gives us an existential formula (***exists**`a`:`g``a`=`m`) and (**exists**`b`:`g``b`=`n`). The application of these existential formulas gives us new constants`a`and`b`with the corresponding properties. Then we apply equational reasoning which gives us our goal by the transitivity of =. - We know (4)
`g`|`n`from (1).*The goal is part of our knowledge.* - We show
(5)
**forall**h: (`h`|`m`/\`h`|`n`) =>`h`<=`g`. Take arbitrary`h`and assume(6)

`h`|`m`/\`h`|`n`.We show (7)

`h`<=`g`.*We have to show a universally quantified implication. We introduce an arbitrary constant*`h`and assume the implication hypothesis. We now have to show the new goal (7).By (6) we have some

`a`' and`b`' with`h``a`' =`m`and`h``b`' =`n`.*We insert the definition of | into knowledge (6) which gives two existential formulas that we can apply to introduce the constants*`a`' and`b`' with the knowledge denoted above.Then we know

`h`(`a`'-`b`') =`h``a`' -`h``b`' =`m`-`n``h`| (`m`-`n`).*We apply equational reasoning to yield a formula in our knowledge that is equivalent to the definition of | for arguments*`h`and`m`-`n`.With (6) and (8), (1) implies (7).

*We apply the rule of "universal quantification in knowledge" to instantiate the universally quantified implication in (1) by term*`h`. Then we apply the rule of "modus ponens" to this implication and to the conjunction of (6) and (8), which gives us the goal.

While above proof is very detailed, it still relies on the claim that the greatest common divisor is uniquely defined (which has to be shown in an extra proof). The verbosity of the proof stems from the fact that it considers details like "Is m-n actually defined?" or "Is the gcd unique?" that were neglected in the high-level proof skeleton.

Whether one is willing to bother with details is a matter of whether one is
actually interested in the truth of a formula *as it stands* or whether
one just wants to know whether the "intention is correct" (whatever this
means). For a computer scientist, exactness *is* important (a "roughly"
correct program may be the cause of an airplane crash); she should not be
*anxious* but
*eager* to find an error in a proposition and thus also check all the
details that are often neglected in typical mathematical texts.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999