# Has the Gödel sentence been explicitly produced?

I do not pretend to know much about mathematical logic. But my curiosity was piqued when I read Hofstadter's Gödel, Escher, Bach, which tries to explain the proof of Gödel's first incompleteness theorem by using an invented formal system called TNT--Typographical Number Theory.

Hofstadter shows how we are able to construct an undecidable TNT string, which is a statement about number theory on one level, and asserts its own underivability within TNT on another level.

My question is: Has this statement about number theory, call it the Gödel sentence, ever been explicitly found? Of course, it would be enormously long. But it seems possible to write a computer program to print it out. I know what is important is that such a string exists, but it would be fun to see the actual string, and it seems like a nice coding problem.

Forgive me if this is a naïve question.

• How much paper/computer memory do you have? – Henry Jul 8 '14 at 23:25
• I once saw a web page that purported to have the Gödel number on it, but did not have the details of the encoding and the axioms used. In base $10$ it about filled a screen. – Ross Millikan Jul 8 '14 at 23:52
• The question supposes there is just one Gödel sentence. But producing the sentence requires choosing one particular Gödel numbering system, as well as various arbitrary choices regarding the syntax of the object language, and the proof theory. There are various different Gödel sentences depending on these choices. This makes the construction of just one of them less interesting, I would think. – MikeC Jul 9 '14 at 16:38
• I think most proofs that the Gödel sentence exists are explicit constructions -- it's just that nobody bothers to ever actually do the arithmetic. – Hurkyl Aug 30 '17 at 12:32