Gödel encoding and self-reference

A Gödel en­cod­ing is a way of us­ing the for­mal ma­chin­ery of prov­ing the­o­rems in ar­ith­metic to dis­cuss that very ma­chin­ery. Kurt Gödel rocked the world of math­e­mat­ics in 1931 by show­ing that this was pos­si­ble, and that it had sur­pris­ing con­se­quences for the sort of things that could ever be for­mally proven in a given sys­tem.

The origi­nal for­mu­la­tion of this self-refer­en­tial frame­work was re­ally messy (in­volv­ing prime fac­tor­iza­tions of huge num­bers), but we can think about it more eas­ily now by think­ing about com­puter pro­grams. In or­der to get math­e­mat­i­cal state­ments that re­fer to them­selves, we can first show that we can talk in­ter­change­ably about math­e­mat­i­cal proofs and com­puter pro­grams, and then show how to write com­puter pro­grams that re­fer to them­selves.

To be spe­cific about the ma­chin­ery of prov­ing the­o­rems, we’ll use the for­mal sys­tem of Peano Arith­metic.

What kind of self-refer­ence do we want for our com­puter pro­gram? We would like to be able to write a pro­gram that takes its own source code and performs com­pu­ta­tions on it. But it doesn’t count for the pro­gram to ac­cess its own lo­ca­tion in mem­ory; we’d like some­thing we could write di­rectly into an in­ter­preter, with no other frame­work, and get the same re­sult.

This kind of pro­gram is known as a quine.

Gödel en­cod­ing is equiv­a­lent to an en­cod­ing of a com­puter pro­gram as a bi­nary string.

If we think about any con­jec­ture in math­e­mat­ics that can be stated in terms of ar­ith­metic, you can write a pro­gram that loops over all pos­si­ble strings, checks whether any of them is a valid proof of the con­jec­ture, and halts if and only if it finds one. In the other di­rec­tion, we can imag­ine prov­ing a the­o­rem about whether a par­tic­u­lar com­puter pro­gram ever halts.


  • Quine

    A com­puter pro­gram that prints (or does other com­pu­ta­tions to) its own source code, us­ing in­di­rect self-refer­ence.


  • Mathematics

    Math­e­mat­ics is the study of num­bers and other ideal ob­jects that can be de­scribed by ax­ioms.