 Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2002/iii/paper-23/10/a/solution

Use only the variable names

x, y

. Define mutually renamed formulas by

D_{1}^{x} (x) = (x = x), D_{m + 1}^{x} (x) = \exists y [x < y \land D_{m}^{y} (y)],

where

D_{m}^{y}

is obtained from

D_{m}^{x}

by globally interchanging

x

and

y

, including their bound occurrences. By induction,

D_{m}^{x} (a)

means that an increasing chain of

m

elements starts at

a

. Hence

λ_{n} = \exists x D_{n}^{x} (x) \in L^{2}

holds exactly when the linear order has at least

n

elements. Inner quantifiers may bind the name

x

again, but their scope is only the nested subformula; the comparison

x < y

still refers to the preceding point. This finite-variable logic construction works on finite and infinite linear orders.

 New to topics? Read the docs here!