MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Does anybody know the exact number from the Goedel's Incompleteness Theorem? Is it written down somewhere? Is there a computer program to generate it?

share|cite|improve this question

closed as too localized by Simon Thomas, Carl Mummert, quid, GH from MO, Dmitri Pavlov Sep 19 '11 at 14:33

This question is unlikely to help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet. For help making this question more broadly applicable, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

I have voted to close because this question is not in the scope of the site, as described in the FAQ linked at the top of the page. The proof of the incompleteness theorem is completely constructive and so, in principle, you could follow it step by step to write down a Goedel number of the Goedel sentence, given a Goedel numbering of formulas. However, it is unlikely that anyone has done so, because the actual number would be quite large. – Carl Mummert Sep 19 '11 at 11:43
You can use a Gödel numbering in which a given formula (e.g. your favorite Gödel sentence) has Gödel number equal to a given number (e.g. 17). So the answer to your question: the exact number you are looking for can be any number, it all depends on the Gödel numbering you use. – GH from MO Sep 19 '11 at 11:51
I would be interested to see an answer to the question, if it provided the actual Gödel number of the original "I am not provable" statement using Gödel's coding scheme, which is of historical interest. I would view such an aswer as fundamentally similar to the results I have seen, published in one of the MAA journals, to compute the digits of the transcendental number Cantor produced in his original diagonalization against the algebraic reals. – Joel David Hamkins Sep 19 '11 at 12:19
I would be interested to know if anyone has done this crazy thing, too. Please don't close. I just checked Russell O'Connors formalization in Coq (, but unfortunately his program cannot do it (see section 8 of his web page). – Andrej Bauer Sep 19 '11 at 12:51
@Joel: Google turns up but I have no idea whether that uses the same coding as the original paper. The main page for that project is . – Carl Mummert Sep 19 '11 at 12:53

Browse other questions tagged or ask your own question.