Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 1 / a / Solution

Write $\square A$ for the arithmetical provability predicate applied to the Gödel number of $A$. Use the Hilbert-Bernays-Löb derivability conditions that belong to the course meaning of a provability predicate: external necessitation rule, internal modus ponens rule, and positive introspection. No incompleteness theorem is needed here.

If $S⊢G$, necessitation rule gives $S⊢\square G$. The displayed Gödel sentence equivalence also gives $S⊢\neg \square G$. These two theorems contradict the assumption that $S$ is a consistent first-order theory. ThereforeFor this part alone, the external necessitation rule condition suffices; the stronger internal conditions are used in the next part.