What axioms are used to prove Godel's Incompleteness Theorems? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-23T15:34:07Z http://mathoverflow.net/feeds/question/118183 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/118183/what-axioms-are-used-to-prove-godels-incompleteness-theorems What axioms are used to prove Godel's Incompleteness Theorems? Andrew Critch 2013-01-06T05:58:18Z 2013-01-07T21:45:59Z <p>I understand <a href="http://en.wikipedia.org/wiki/G%25C3%25B6del%27s_incompleteness_theorems" rel="nofollow">Godel's Incompleteness Theorems</a> to be statements <em>about</em> effectively generated <a href="http://en.wikipedia.org/wiki/Formal_system" rel="nofollow">formal systems</a>, which basically makes them theorems <em>about</em> algorithms. This is cool, because despite being very abstract, they actually constrain my expectations about how computers and human beings can behave. But, being theorems, what formal system are they theorems <em>in</em>? That is, what <a href="http://en.wikipedia.org/wiki/Formal_language" rel="nofollow">formal language</a> is used to express them, how do I <a href="http://en.wikipedia.org/wiki/Interpretation_%28logic%29" rel="nofollow">interpret</a> that language as being about algorithms, what axioms are assumed, and what rules of inference are used to derive the incompleteness theorems?</p> <p>I ask because I am looking for a better answer than "<a href="http://en.wikipedia.org/wiki/Zermelo%25E2%2580%2593Fraenkel_set_theory" rel="nofollow">ZFC</a>", which has been given to me in person a few times now. ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families...), at least not in the same way I believe in concrete things like computers and algorithms. I can see from skimming the proofs that I could probably make up a formal system in which the theorems could be expressed and proven, which did not refer to all the monstrosities of ZFC. I just want to know what standard, "simplest" formal system(s) can be used for this purpose.</p> http://mathoverflow.net/questions/118183/what-axioms-are-used-to-prove-godels-incompleteness-theorems/118189#118189 Answer by Ali Enayat for What axioms are used to prove Godel's Incompleteness Theorems? Ali Enayat 2013-01-06T08:06:39Z 2013-01-07T21:45:59Z <p>As Andres Caicedo points out in his comment (to the Question), the modest fragment $\sf{PRA}$ (Primitive Recursive Arithmetic) of $\sf{PA}$ (Peano arithmetic) is already is able to verify the incompleteness theorems.</p> <blockquote> <blockquote> <p>Indeed, the proof of the Gödel-Rosser incompleteness proof is entirely syntactic and can be readily implemented in a fragment of $\sf{PRA}$ known as $I\Delta_0 + exp$, where $I\Delta_0$ is the weakening of $PA$ in which the induction scheme is only available for $\Delta_0$-formulas, and $exp$ asserts the totality of the exponential function $2^x$ (it is well-known that $I\Delta_0$ is unable to prove the totality of the exponential function).</p> </blockquote> </blockquote> <p>It is worth noting that in the above $I\Delta_0 + exp$ can be even reduced to $I\Delta_0 + \Omega_1$, where $\Omega_1$ is the axiom asserting the totality of the function $2^{\left| x\right|^2 }$, where $\left| x\right|$ denotes the length of the binary expansion of $x$. The theory $I\Delta_0 + \Omega_1$ is commonly viewed as the weakest fragment of $\sf{PA}$ in which one can develop a workable "theory of syntax".</p> <p><strong>PS.</strong> As pointed out by Jeřábek, the incompleteness theorems can be implemented in even weaker systems. </p> http://mathoverflow.net/questions/118183/what-axioms-are-used-to-prove-godels-incompleteness-theorems/118198#118198 Answer by abo for What axioms are used to prove Godel's Incompleteness Theorems? abo 2013-01-06T12:39:35Z 2013-01-06T12:39:35Z <p>Here's a different way of looking at things. Use FPA to denote second-order Peano Arithmetic minus the Successor Axiom (the axiom which says that every natural number has a successor). FPA is neither weaker nor stronger than IΔ0+Ω1, since the latter assumes the Successor Axiom but assumes a weaker form of induction. </p> <p>FPA can prove the First Incompleteness Theorem. Undoubtedly, fragments of FPA can as well.</p> <p>More interesting is when one clarifies the nature of the logical system under metalogical study. Usually, the syntax of first-order logic is defined so that one can always concatenate two strings to form a larger one. E.g. one uses this principle in the Deduction Theorem, which is one of the first metalogical theorems one tends to prove. But this assumption, essentially equivalent to the Successor Axiom, is not necessary, and one can refrain from making it. </p> <p>In this environment (where the syntax is not assumed to be unboundedly long), one can say this: FPA can prove the First Incompleteness Theorem. But Godel's proof seems only to work in the case of FPA + Successor Axiom. In the case FPA + not Successor Axiom, one basically formalizes the idea that a proof is generally longer than any axiom. It does not appear that Godel's proof of the Second Completeness Theorem goes through, and I do not know whether this can be repaired.</p> http://mathoverflow.net/questions/118183/what-axioms-are-used-to-prove-godels-incompleteness-theorems/118231#118231 Answer by Timothy Chow for What axioms are used to prove Godel's Incompleteness Theorems? Timothy Chow 2013-01-06T23:04:29Z 2013-01-06T23:04:29Z <p>You might already know this, but if you're looking for foundations of mathematics which are so weak that they don't prove the existence of non-r.e. sets, then you should study Simpson's book <a href="http://www.math.psu.edu/simpson/sosoa/" rel="nofollow"><i>Subsystems of Second-Order Arithmetic</i></a>, the "bible" of <a href="http://en.wikipedia.org/wiki/Reverse_mathematics" rel="nofollow">reverse mathematics</a>. The weakest system in that book, RCA<sub>0</sub>, has as a model the recursive sets, and suffices for Goedel's first incompleteness theorem and even a weak version of Goedel's completeness theorem. More importantly, RCA<sub>0</sub> suffices for a large amount of mathematics.</p> <p>Simpson's book of course also investigates what <i>can't</i> be proved in RCA<sub>0</sub>. For example, Brouwer's fixed point theorem is unprovable in RCA<sub>0</sub>, roughly speaking because one can construct a continuous recursive map from the square into itself that has no recursive fixed point.</p>