Galois Theory, 4th Edition

92 Ruler-and-Compass Constructions

Proof. The inclusions are clear. Let p

n

be the number of points in P

n

, l

n

the number

of lines in L

n

, and c

n

the number of circles in C

n

. Then

|L

n+1

| ≤

1

2

p

n

(p

n

+ 1)

|C

n+1

| ≤ p

n

1

2

p

n

(p

n

+ 1)

|P

n+1

| ≤

1

2

l

n+1

(l

n+1

+ 1) + 2l

n

c

n

+ c

n+1

(c

n+1

+ 1)

bearing in mind that a line or circle meets a distinct circle in ≤2 points. By induction,

all three sets are finite for all n.

We formalise a Euclidean ruler-and-compass construction using these sets. The

intuitive idea is that starting from 0 and 1, such a construction generates a finite

sequence of points by drawing a line through two previously constructed points, or

a circle whose centre is ...