Defining the greatest common divisor

Defining the greatest common divisor

In this note, all variables are of type natural number; "d divides n" is denoted by d e n and defined by

(0) $d \leq n \equiv \left\langle {\exists q : d \cdot q = n}\right\rangle$

from which we deduce

(1) $\left\langle {\forall d : d \in 0}\right\rangle$

Proof We observe for arbitrary $d$

$$ \begin{array}{l} d \leq 0 \ \equiv \quad \left{ \begin{array}{l l} (0) & \text {w i t h} \quad n := 0 \end{array} \right} \ \langle \exists q: d \cdot q = 0 \rangle \ \Leftrightarrow \quad {\mathrm {i n s t a n t i a t i o n}: q := 0 } \ d \cdot 0 = 0 \ \equiv {\mathrm {z e r o p r o p e r t y} } \ t r u e. \ \end{array} $$

(End of Proof.)

I would like to stress that (0) is "only" a choice, but by far the wisest one. Some-one who is not attracted by its consequence that zero has an unbounded number of divisors, might, for instance, consider the alternative definition for $\mathtt{d}\mathtt{s}\mathtt{n}$ :

$$ \langle \exists q: q \geq 1: d \cdot q = n \rangle $$

something some people may have had in mind when the natural numbers still started at 1 . But the consequences would be unattractive , for laws like

$$ 1 \leq n $$

$$ d \equiv m \wedge d \equiv n \Rightarrow d \equiv (m - n) $$

would no longer hold.

In the rest of this note we shall denote the greatest common divisor of $x$ and $y$ by $x \downarrow y$ (and their least common multiple, if we need it, by $x \uparrow y$ ). Historically, the "greatest common divisor" is not only the name of that function but also its verbal definition: if you are interested, say, in 12↓21, you observe:

the divisors of 12 are {1,2,3,4,6,12} the divisors of 21 are ${1,3,7,21}$ their common divisors are ${1,3}$ their greatest common divisor is 3 .

The most attractive formal definition of $x\downarrow y$ is as the (only!) solution for

(2) $w : \left\langle {\forall z : z \equiv w \equiv z \equiv x \land z \equiv y}\right\rangle$

Because we have $- A \equiv {A}_{A} -$

$$ \langle \forall z: z \leq x \equiv z \leq x \land z \leq x \rangle $$

and -not proved here- the solution of (2) is unique, we have derived

(3) $x \downarrow x = x$ for any $x$ .

But now we have to make up our minds about $0\downarrow 0!$ According to the verbal definition, o.o is, on account of (1), the greatest natural number, i.e.

(i) 0.10 is undefined , or, perhaps, (ii) $0 \downarrow 0 = + \infty$

According to the formal definition, which gives rise to (3), we conclude (iii) $0 \downarrow 0 = 0$ .

I propose to choose (iii), i.e. to let the formal definition prevail, thus ensuring the general validity of the laws about (such as

$$ \begin{array}{l} x \uparrow y = x \uparrow (y - x) \ x \uparrow 0 = x, e t c.) \ \end{array} $$

Remark 010 is the only case where verbal and formal definition disagree. For $x \uparrow y$ , the least common multiple of $x$ and $y$ , the most attractive formal definition is as the (only!) solution for $w$ of the equation

$$ w: \langle \forall z: w \in z \equiv x \in z \land y \in z \rangle , $$

from which $x \uparrow x = x$ -and ${010} = 0$ in particular- follows. Note that,when we read d = n also as "n is a mul- tiple of cl", 010 is the only case where verbal and formal definition agree! (End of Remark.)

$$ A u s t i n, 7 F e b r u a r y 1 9 9 7 $$

prof. dr Edsger W.Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA