Timeline for Interpretation of the Second Incompleteness Theorem
Current License: CC BY-SA 2.5
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 9, 2010 at 19:57 | comment | added | Carl Mummert | @Andres: the proof does use the downward absoluteness of $\Pi^1_1$ formulas. There is a proof in Simpson's book on second-order arithmetic if you're interested in looking it up. The reason ACAo is needed is to reason about the satisfaction predicate of a countable $\omega$-model coded as a real. Strangely, every $\omega$-model of WKLo does contain a real that codes a countable $\omega$-model of WKLo, so the assumption of ACAo isn't trivial. | |
| Sep 9, 2010 at 19:49 | comment | added | Carl Mummert | @Kaveh: In my terminology, that approach proves the consistency of "ZFC + X" in the stronger theory ZFC + Con(ZFC). | |
| Sep 9, 2010 at 18:13 | comment | added | Andrés E. Caicedo | Carl, Is the proof of Harvey's result basically a use of $\Sigma^1_1$ absoluteness? I've proved versions of this in class for stronger theories, so perhaps I'm overlooking some technicality at the level of second order arithmetic. | |
| Sep 9, 2010 at 17:37 | comment | added | Peter Arndt | Nice example! That's also what I was pointing to in my comment to the question. If you manage to carry out a consistency proof in a setting where you shouldn't be able to (by the 2nd incompleteness theorem), then you have a contradiction - which is valuable information about your hypotheses. | |
| Sep 9, 2010 at 17:36 | comment | added | Kaveh | I thought that Cohen's proof is formalizable in $ZFC$ in the form "if $ZFC$ is consistent, then $ZFC+\lnot CH$ is consistent". | |
| Sep 9, 2010 at 17:24 | history | answered | Carl Mummert | CC BY-SA 2.5 |