 Solution

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

Y = □ X \to X

. The Löb axiom at

X

□ Y \to □ X

. Therefore

Y

and

□ Y

together imply

X

, proving

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

For the converse, the tautology

X \to Y

gives

□ X \to □ Y

by necessitation and distribution. Consequently

□ Y \to X

together with

□ X

gives

X

, so

G L ⊢ (□ Y \to X) \to (□ X \to X),

whose consequent is

Y

. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly

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

 New to topics? Read the docs here!