Gödel proves his theorem informally by using natural languages. However, is there a way to carry out his proof in PA itself? (so that maybe PA could prove that itself could not prove its own consistency) If there isn't (and we have to carry out his proof in some stronger background theory such as ZFC), what makes his proof inexpressible in PA?
5
-
5$\begingroup$ While I understand the question you're asking, I think it's a bit misleading to characterize Gödel's proof as "informal": it was as rigorous as any mathematical proof created by humans. $\endgroup$– Greg MartinMar 19 at 16:52
-
3$\begingroup$ PA is more than enough to prove "If PA is consistent then PA does not prove that PA is consistent." Similarly, PA is more than enough to prove "If ZFC is consistent then ZFC does not prove that ZFC is consistent." $\endgroup$– Andreas BlassMar 19 at 17:32
-
$\begingroup$ Wow, thank you a lot! $\endgroup$– NicholasMar 20 at 2:20
-
$\begingroup$ @AndreasBlass it sounds like PA is not enough to prove the full Gödel incompleteness theorem. If so, do you have a reference that specifically discusses the valid choices of X and Y in "X is enough to prove 'If Y is consistent, then Y does not prove that Y is consistent'"? $\endgroup$– BananachMar 20 at 8:58
-
1$\begingroup$ @Bananach When X in your comment is PA, Y can be any computably axiomatized theory, with a $\Sigma^0_1$ definition of Y being used in the formal statement about Y. The same works for weaker X; I'm confident that I$\Sigma_1$ suffices, but I'm not sure how much weaker one can make X (maybe I$\Delta_0+\exp$) $\endgroup$– Andreas BlassMar 20 at 14:19
Add a comment
|