Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 4 / c

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)) .

 Ancestors (12)

There are no discussions about this article yet.

There are currently no matching articles.