 Solution

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

Again abbreviate provability by

□

. The Gödel sentence equivalence gives

S ⊢ G \to \neg □ G

. Internalizing this implication using the first two Hilbert-Bernays-Löb derivability conditions gives

S ⊢ □ G \to □ \neg □ G .

S ⊢ □ G \to □□ G

. Internal modus ponens rule combines proofs of a sentence and its negation into a proof of a contradiction; a contradiction implies any sentence. Consequently

S ⊢ □ G \to □ \neg G .

These are syntactic manipulations of provability, not an appeal to soundness. If

S ⊢ \neg □ \neg G

, taking the contrapositive of the last implication gives

S ⊢ \neg □ G

, and the diagonal equivalence gives

S ⊢ G

. Part (a) rules that out for a consistent theory. Hence

S ⊬ \neg □ \neg G when S is consistent .

 New to topics? Read the docs here!