 Solution

ID: past-exam-of-the-model-theory-and-godel-s-incompleteness-theorems-course-of-the-university-of-oxford/2007/a/4/c/solution

Put

Y = □ X \to X

. The Löb axiom gives

□ Y \to □ X

. Consequently

Y

implies

□ Y \to X

: if

□ Y

holds, first obtain

□ X

and then apply

Y

For the other direction,

X \to Y

is a propositional theorem. Necessitation and distribution give

□ X \to □ Y

. Hence

□ Y \to X

implies

□ X \to X

, which is

Y

. We have proved the unboxed theorem

G L ⊢ Y \leftrightarrow (□ Y \to X) .

Necessitation yields

G L ⊢ □ (Y \leftrightarrow (□ Y \to X)) .

This is the explicit fixed point for the modalized operator

Z \mapsto (□ Z \to X)

 New to topics? Read the docs here!