Timeline for Are undecidable consequences of Con recursively enumerable?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 24, 2013 at 21:55 | comment | added | mtg | I didn't know how to make a comment, sorry, but you're right. In the meantime I figured out that $\Sigma^0_1$-completeness of $PA$ is provable in $PA$, but thanks - yeah, that's pretty obvious. | |
| May 24, 2013 at 16:33 | comment | added | Andreas Blass | It might be useful to add that this "provable $\Sigma^0_1$-completeness" result can be found in textbooks as an ingredient in the proof of the second incompleteness theorem. | |
| May 24, 2013 at 15:16 | comment | added | Emil Jeřábek | PA proves $\sigma\to\Pr_{PA}(\ulcorner\sigma\urcorner)$ for every $\Sigma^0_1$-sentence $\sigma$ by formalizing the proof of $\Sigma^0_1$-completeness of Q. | |
| May 24, 2013 at 13:19 | comment | added | mtg | Adnreas, how do we know that if $¬\varphi$ is $\Sigma_1^0$, then $PA+¬\varphi$ proves $Pr_{PA}(¬\varphi)$ ? | |
| May 3, 2011 at 6:50 | comment | added | Alex Gavrilov | Thank you, Andreas. This is nice! Why didn't I see it before? | |
| May 3, 2011 at 0:58 | history | answered | Andreas Blass | CC BY-SA 3.0 |