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.

Comments

Post a Comment

Popular posts from this blog

How To Make ASCII Diagrams Beautifuller

Image
I've discovered an excellent tool in asciiflow.com .  The website makes it really easy to create ASCII box diagrams like this They put these things in fruit machines you know! This is ideal for source code banners, which I think should contain helpful documentation - but most programmers think it's a good place for the COPYRIGHT information and nothing else. But wait! we can make it beautifuller... and easier to read... by replacing some of the ASCII characters with ones available in UTF-8: There!  Isn't that better?  (Although some purists may object to non-ASCII characters in your code base.) SOURCE CODE: #!/usr/bin/python2 # coding: utf-8 # + gets converted in different ways depending on it's 4 neighbours # # . N . { nsew(N,S,E,W) has bit 3 set if N in "+|<>" # W + E { nsew(N,S,E,W) has bit 2 set if S in "+|<>" # . S . { nsew(N,S,E,W) has bit 1 set if W in "+-^v" # { nsew(N,S,E,W) has bit 0 set if E in
Read more

Calculation of ECS using simple convection model

Image
Contents Intro Simple stratified model Alternative convection model Tropospheric temperature gradient Approach used in convection model Calculation of Radiative Forcing from CO₂ increase Calculation of Radiative Forcing from H₂O increase Calculation of zero-feedback ECS Effect of including feedbacks Effect of water vapour Effect of cloud cover change Effect of sea ice loss Calculation of ECS including feedbacks Limitations One more thing: Changes to Troposphere depth Intro The goal of this post is to see if we can come up with an estimate of Equilibrium Climate Sensitivity using a simple model in which the atmosphere is treated as well-mixed.  By "simple" I mean that using the model will not require any advanced mathematics or computation, but will still be realistic enough to come up with an estimate within the likely range of 2.5 - 4.0°C predicted by the IPCC Assessment Report 6 .  I will try to take as little on trust as possible and show how the results are arrived at.
Read more

Why growth is falling in all developed countries (as a long term trend)

Image
In this post I argue that economic growth is not the normal state of affairs, it is a blip caused by the discovery of a one-off resource of non-renewable energy.   The logistic equation $$ \frac{dy}{dt} = y(1-y) $$ Here's a simple model.  Humans discover an exploitable but limited resource and start consuming it.  The amount consumed, $y(t)$, is a function of time.  The general form of the equation is $\frac{dy}{dt} = \alpha y (\beta - y)$, but if you choose the right units $\alpha$ and $\beta$ both become $1$. Why should this work, in principle? Early on, the factor $1-y$ is approximately $1$ and can be ignored.  So the model states that annual consumption $dy/dt$ starts off proportional to $y$.  In other words, $y$ grows exponentially at first.  This could happen if exploiting the resource enables further exploitation of the resource.  For example, suppose a few humans are shipwrecked on an island with 1000 trees: they take ages to cut down the first tree as they are using their
Read more