 Solution

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

Let

C = □ X \land X

. The normal distribution axiom and necessitation of

C \to X

give

□ C \to □ X

. Combining this with propositional reasoning yields the theorem

X \to (□ C \to C) .

Indeed,

X

together with

□ C

supplies both conjuncts of

C

. Necessitate this theorem and apply distribution to obtain

□ X \to □ (□ C \to C) .

The new Löb axiom at

C

now gives

□ X \to □ C

. Finally, necessitation and distribution applied to the tautology

C \to □ X

give

□ C \to □□ X

. Composition proves

G L ⊢ □ X \to □□ X .

No positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.

 New to topics? Read the docs here!