You are viewing version 1.0.0 of this page. Click here to view the latest version.

Gödel encoding and self-reference

Written by orthonormal last updated
You are viewing revision 1.0.0, last edited by orthonormal

Kurt Gödel rocked the world of mathematics in 1931 by showing that the way mathematicians proved things about arithmetic was also able to prove things about the process of proving things, and that it was possible to set up self-referential statements akin to the Liar's Paradox. The original formulation of this self-referential framework was really messy, but we can think about it more easily now by thinking about computer programs.

In order to get mathematical statements that refer to themselves, we can first show how to write computer programs that refer to themselves, and then show that we can talk interchangeably about mathematical proofs and computer programs.

What kind of self-reference do we want for our computer program? We would like to be able to write a program that takes its own source code and performs computations on it. But it doesn't count for the program to access its own location in memory; we'd like something we could write directly into an interpreter, with no other framework, and get the same result.

This kind of program is known as a quine, after the logician W.V.O. Quine.

Gödel encoding is equivalent to an encoding of a computer program as a binary string.

Parents:
Children: