Proof of Gödel's Incompleteness Theorem in $bash$

Gödel's incompleteness theorem says the following:

1. Choose your axioms that uniquely define the integers (you'll need a minimum of about 10)
2. Choose your rules of inference that define what type of statements about integers follows from what other types of statements
3. Then, provided you chose a finite number of each, there will be true statements about the integers that you cannot prove using (1) and (2)

What follows is a proof of Gödel's Incompleteness Theorem, using Turing's Halting Problem, and bash scripting to illustrate ($\dagger$).

For the purpose of this high level (but consise) proof, imagine a computer running Unix which has infinite memory.  Apart from this limitless resource the computer is the same as any other Unix machine, i.e. all files must be of finite size, there are finitely many instructions and system calls, each instruction has a minimum completion time, etc. etc..

We will consider all files to be executable.  For the vast majority the output when executed will be something like "Executable format not understood" or "segfault", but some will have more interesting results.  Either way there is nothing wrong with considering "Executable format not understood" as the executable's output.

Definition

A Truth machine is an executable "t" with the following properties:

• Given any statement about the integers as input, it will eventually output "true" or "false".
• t outputs "true" if and only if it's input is a true statement about the integers $\mathbb{Z}$

Theorem

It is impossible to write a truth machine.

Proof

Now let's s suppose the opposite, i.e. that there is a truthmachine "t".  Since our Unix machine is a well understood platform describable using a finite number of statements about numbers, we can write a program "x" which takes a file "f" on stdin and outputs on stdout a statement about integers which is true if and only if the following command terminates(*).  (Note that "x" doesn't determine whether the following command terminates, it just outputs a very long statement about integers which means the same as saying the following command terminates.)

    [zeus@work]$ f < f

Now consider the following program "y".
 

It is easy to see that for all files "z"

    [zeus@work]$ y < z


will terminate if and only if

    [zeus@work]$ z < z


does not terminate, which means that the following command terminates if and only if it does not terminate.

    [zeus@work]$ y < y

This contradiction disproves our original assumption that it is possible to write a truth machine "t".

Theorem

Given any set of axioms and rules of derivation capable of describing uniquely the integers, there is a statement about the integers which is true, but not provable.

Proof

Assume the opposite, namely that there set of axioms and rules of derivation that can describe the integers uniquely in which every true statement is provable.  Implicit in the phrase "rules of derivation" is the concept that there is an algorithm "a", which can determine whether or not any given textual string is an allowed "proof" of a statement using only the initial axioms and the rules of derivation.  For example, we could stipulate that

    [zeus@work]$ echo $TEXT | a

outputs

    $TEXT proves $STATEMENT

if and only if $TEXT is an allowed proof of $STATEMENT within the rules.

We will use "a" to build a truth machine "t".  This will yield a contradiction, since we know it to be impossible to build a truth machine, and thereby prove the theorem.

First write a program "g" which generates all finite lines of text, i.e. given any finite line of text, "g" will eventually print out that line. (+) Now we can use "g" and "a" to write "t" as follows.

Now since $STATEMENT is a statement about integers, and all such statements are true or not true, "g" will eventually emit a line which proves $STATEMENT, or proves ¬($STATEMENT).  In the former case "t" will eventually output "true", in the latter it will eventually output "false".  Therefore "t" is a truth machine, which as we know cannot exist.

This contradiction completes our proof.


---- Footnotes ----
($\dagger$) For scripting noobies: `command` refers to the textual output of command; program1 | program2 is the command to run program1 and program2 at the same time using the output stream of the former as the input stream of the latter; and program < file is the command to run program using the contents of file as its input stream.
(*) Yes, this is the really boring bit.
(+) This is omitted but not actually that difficult.