Goal of the Task

The statement 7 is a prime number. is true and we can prove it formally using axioms and inference rules. So is the statemtents like 2209 is a square number. and 1597 is a Fibonacci number..

Gödel showed us there a type of number $\theta$ with a number $q$.

$q$ is a $\theta$ number, the same as 7 is a prime number, but we can’t prove.

The whole idea is to define the $\theta$, and find the $q$.

Encoding and Decoding

Encoding Statements

The statement $1+1=2$ can be expressed using one unique number:

The statement $\forall x(x + 0 = x)$ means for all natural number, if you add zero to it, it will give you the same number, e.g. $2 +0 = 2$, $32093+0=32093$. And this simple statement can be expressed using one unique number (extremely long number):

The statement 3 is a prime number can be expressed a little big longer:

The encoded number will also be long:

Yet it is still a unique number for that statement. Statements are also called sentences.

Encoding Formulas

The statement has to return true or false. We can define a class of statements, for example, instead of stating $3$ is a prime number, we can define:

Replacing $3$ with $z$, we define a formula with one free varible (not associating with $\forall$ or $\exists$ ) that if you plugin a number, it will turn into a normal statement.

Such a formula with $z$ can also be encoded to a unique number:

Anothe example is the class of odd numbers:

The encoded number for this formula is:

Decoding

Not every number can be decoded as a valid statement or formula, for example, $118098 = 2^1\times 3^{10}$ means $0=$, which has no real value to us. So the number that can be decoded has to be a valid one.

Similar to argument type checking in programming, the decoded mathematical stuff may not be suitable for function parameters.

The following is valid, which asks whether the number that encodes $\mathrm{isOdd}$ is a prime number or not.

But this one is not valid, after decoding, the statement can’t use as a function.

In the coming arguments, Gödel never used an invalid number when decoding presents.

The Unprovable Statement

Checking proofs is a definable formula

Gödel shows that checking a proof for a statement is an algorithm that can be run on a computer.

So if you give me a proof of Goldbach’s conjecture, I can directly put it into a computer and wait for the computer to tell me whether this proof is valid or not. This can be decided in bounded time.

That is to say that $\mathrm{isProof}(y, x) $, where $x$ is a number that encodes a statement and $y$ is a number that encodes a proof, can be written as a formula in terms of the normal logical statement in metamathematics. To give you a hint, the formula $\text{isPower}(a, b, c)$ which checks whether $c = a^b$ can be expressed as following:

All you need to know here is that $\mathrm{isProof}(y, x)$ is a long sequence of symbols that can be precisely written down, like a python function is a long sequence of symbols that can be precisely written down. And it can be encoded as a single integer number, like a python function can be represented by a binary number.

Why is this important? Let’s say, if something you can proof with finite steps mechanically, it seems less interesting, like checking whether 6911 is a prime number or not, it can be tedious, but not too magical. But if you can show that for every rectangle triangles, $a^2 + b^2 = c^2$, this is amazing and magical for the first you see, and find it useful as well. For those Euclidean (plane) geometry statements, every such statement ($a^2 + b^2 = c^2$) is either provable or its negation is provable from the axioms.

But for the Peano Arithmetic, something like Twin Prime Conjecture

Or in its expanded long form:

is interesting and we can mechanically check its correctness. We hope PA has the potential to proof this from axioms. But PA is not powerful enough.

A New Class of Numbers

Now we define a class of numbers as:

where $x$ is a number that encodes a statement and $y$ is a number that encodes a proof.

Just like prime numbers, there is a class of number called isNotProvable numbers.

Now let’s define another class of numbers:

where $x$ is a number that encodes a formula with one free variable.

Let’s call this new class of number as theta numbers.

The Unprovable True Statement

Since,

is a number that encodes a formula with one free variable.

So,

is a valid statement which means

The number that encodes the formula of theta is a theta number.

This statement is true but not provable in the system.

That means given encode, decode and isProof are well-defined algorithms, the following programming will run forever without finding a proof.

You can argue theta(encode(theta)) is true, but you can’t find a proof to show its truth.

def theta(x):
    formula = decode(x)
    statement = formula(x)
    encoded_proof = 2
    while true:
      proof = decode(encoded_proof)
      if isProof(proof, statement):
        return true
      encoded_proof += 1

theta(encode(theta))

The Proof

is the same as:

Since $\text{decode}(\text{encode}(\theta(x)))$ means $\theta(x)$, so

That is:

If $\theta(\text{encode}(\theta(x)))$ returns false, that implies $\mathrm{isNotProvable}(\text{encode}(\theta(\text{encode}(\theta(x)))))$ returns false, which says it is provable, but this is a false statement. That means we have a contradiction here.

So if the system can’t contain contradiction, $\theta(\text{encode}(\theta(x)))$ has to return true, that implies $\mathrm{isNotProvable}(\text{encode}(\theta(\text{encode}(\theta(x)))))$, which says it is not provable. There is a true statement you can’t prove.

Reinvent the Wheel

Since we have been familiar with those functions, let us make some convinient shortcuts:

For example the statement $\theta(\text{encode}(\theta(x)))$ can be expanded as:

The Starting Point

The liar paradox which states “this statement is false” is easily to come to mind. If we borrow this idea, we can find out our goal is to find a statement that means:

This statement is not provable.

And $G$ can be defined as a combination of our three well-defined functions $\phi$, $\epsilon$ and $\delta$.

First Heuristic Trial

Apparently, $\phi$ is a great choice, signaling something like Not provable is not provable. At the same time, we should make one free variable formula becomes a statement. The goto choice for the parameter apparently should be self-referenced to make it possible to push the searching area by using more tools since we only have very limited definations here. That means:

but $\phi$ is a formula with one free variable, and it only accepts numbers encodes statements. Since $\epsilon(\phi)$ is a number encodes a formula with one free variable not a statement, this choice is invalid. But it gives us a hint that maybe we should use a formula with one free variable and this variable requires a number encodes a formula with one free variable.

Find the Right Relation

Let’s say $\rho$, and it might in a form like $\rho(x) = f(\delta(x), x)$. And also:

If we want to find $\rho(x)$, there are many hints to solve this:

1. we should make first $\rho$ in the right hand side disappear.

2. we should introduce $\epsilon(\rho(x))$, like in $f(\sin x) = \cos 2x$, we should introduce $\sin x$

3. we should introdue $\delta(x)$, that might indicate $\rho$ accepts a number encodes a formula with one free variable.

We now should replace the first $\rho$ as $\delta(\epsilon(\rho(x)))$, it becomes:

Noticing $\epsilon(\rho(x))$ is a number we plug in, so we find a suitable $\rho$:

with the statement $G$ as:

Gödel’s Paper

This article is an explanation for the following paragraphs in the Gödel’s 1931 paper.

The $[\text{R}(x); y]$ is defined as:

And $[\text{R}(x); x]$ is

And $\overline {\text{Bew}}$ is $\text{isNotProvable}$, and $\text {S} (x)$ is same as above $\theta (x)$:

And $\text K$ means when $n \in \text{K}$, $\text{S}(n)$ is true. The number $q$ is the Gödel number:

The unprovable statement is:

It is easy to show: