Past exam of the model theory and Gödel'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.

There are no discussions about this article yet.

There are currently no matching articles.