 Solution

ID: past-exam-of-the-model-theory-and-godel-s-incompleteness-theorems-course-of-the-university-of-oxford/2010/a/3/d/solution

One can take

F_{1} = \neg □ ⊥, F_{2} = ⊥.

⊥

gives

□ (□ ⊥ \to ⊥) \to □ ⊥

, that is,

□ F_{1} \to □ ⊥

. Conversely, the tautology

⊥ \to F_{1}

, necessitation rule, and distribution give

□ ⊥ \to □ F_{1}

. Thus

G L ⊢ □ F_{1} \leftrightarrow □ ⊥

. Negating both sides gives

G L ⊢ \neg □ F_{1} \leftrightarrow F_{1}

\neg F_{2} = ⊤

is a theorem, so

G L ⊢ □ \neg F_{2}

. Hence

\neg □ F_{2} \land \neg □ \neg F_{2}

is false in the logic and is equivalent to

⊥ = F_{2}

. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.

 New to topics? Read the docs here!