 Solution

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

A = S + \neg Con_{S}

. The arithmetized deduction theorem, together with double-negation elimination and formalized proof transformations, gives

S ⊢ □_{A} ⊥ \leftrightarrow □_{S} Con_{S}, S ⊢ Con_{A} \leftrightarrow \neg □_{S} Con_{S} .

From the preceding proof,

S ⊢ □_{S} G \to □_{S} ⊥

. Necessitating the equivalence between

G

and

Con_{S}

and using distribution therefore gives

S ⊢ □_{S} Con_{S} \to □_{S} ⊥

S ⊢ Con_{S} \to Con_{S + \neg Con_{S}} .

This is an internal conditional statement. It does not assert that

S

proves its own consistency or permits the consistency premise to be discarded.

 New to topics? Read the docs here!