 Solution

ID: past-exam-of-the-godel-s-incompleteness-theorems-course-of-the-university-of-oxford/2011/3/c/solution

Take

Y (p) = p \to q

and put

⊤ = (⊥ \to ⊥)

H = Y (⊤)

and

F_{0} = Y (□ H) = □ H \to q

. The first supplied substitution identity reads

GL ⊢ □ H \leftrightarrow □ Y (□ H) = □ F_{0} .

Use the supplied replacement of equivalents in the context

D (p) = p \to q

. It gives

GL ⊢ F_{0} \leftrightarrow (□ F_{0} \to q) .

But

H = (⊤ \to q)

is equivalent to

q

. Replacement under a box gives

□ H \leftrightarrow □ q

, so

F_{0}

is equivalent to

F = (□ q \to q) .

Replacing equivalents once more transfers the fixed-point equation to

F

, proving

GL ⊢ F \leftrightarrow (□ F \to q)

□ F \to □ q

, and necessitating the tautology

q \to F

gives

□ q \to □ F

K

. Thus

□ F \leftrightarrow □ q

, and replacing the antecedent in

□ F \to q

recovers

F

 New to topics? Read the docs here!