The theorem can be formulated for any of the equivalent models of computation listed in the computability theory article. Here we will use Pascal programs.
If p is a string that describes a Pascal program which reads a single input string and produces a single output string, then we will denote the corresponding partial function from input strings to output strings by fp. (This is a partial function because for some input strings the program described by p may run into an infinite loop and never produce an output.)
The statement of the theorem is as follows: If Q is a Pascal program which takes two input strings x and y and produces a single output string Q(x,y) (which again may be undefined if Q runs into an infinite loop), then there always exists a string p describing some Pascal program such that for all input strings y:
As an application, we can show that there must exist a Pascal program which takes a single input, ignores that input and prints itself as output: Define Q(x,y) = x, then the theorem yields a Pascal program p such that for all y: fp(y) = Q(p,y) = p. It is an amusing exercise to actually write such a program p.