In this post we wil apply th Kolmogorov complexity to logic. To be more precise, we will answer to classical questions about foundations of mathematics. But first, let’s clarify what we mean by foundations.
For simplicity and definiteness we will stick with set theory (with
first order logic) as our foundational theory. The idea is to express
every notion we use in mathematics in terms of sets using a
formal language. Our formal language will have only two primitive
notions, namely equality, which we will denote by
Other than these two, we will have the following symbols in our
language:
The last symbol, namely
When we talk about sets, we will use only meaningful or well
formed strings in these symbols. I will not define what exactly well
formed means but you can assume that a well formed formula is a string
in our symbols which can be parsed according to some grammar.
Intuitively, strings like
One important property of well formed formulas is that there is an algorithm which can decide whether an arbitrary string is well formed or not.
We want to be able to prove statements about mathematical using our language. After all, this is supposed to be a foundational theory. Since we have statements, namely the well formed formulas, only two pieces are missing now: assumptions (or axioms) and a notion of proof.
Again for definiteness, we will work with the axioms of ZFC (Zermalo-Frenkel-Choice) set theory. The actual axioms are not important but you can look them up if you are curious. The important fact about the axioms is the following: There is an algorithm which can decide whether an arbitrary string is an axiom.
Finally a proof of a well formed formula
A theorem of ZFC is a well formed formula which has a proof. Now you might think that there is an algorithm which can decide whether an arbitrary string is a theorem of ZFC. However, as we will see soon, this is not true. The best you can do is to enumerate all theorems of ZFC. In other words there is an algorithm which generates an infinite list containing all theorems of ZFC. You can probably guess the algorithm: Generate all finite sequences of well formed formulas in, say, lexicographic ordering. If the sequence happens to be a proof, add the proven formula to the list.
If you have not heard of recursively enumerable sets before, you might want to think about why this is weaker than having an algorithm which can decide whether an arbitrary string is a theorem.
At this point, you might ask the following question: We have only
talked about sets so far but we were looking for a foundational theory
for all of mathematics. Is this really enough? The answer is yes. This
may look strange because it seems that there objects in mathematics
which are clearly not sets. For instance
Here are a few examples to give you an idea. We can define
From now on I will assume that we agreed on encodings of all the notions in mathematics as sets. Note that notions like well formed formula, proof and algorithm are also encoded in this way. So ZFC is capable of talking about Kolmogorov complexity, or even itself.
Here comes the big theorem of this post. Recall that
There is a constant
such that for no , the statement is a theorem of ZFC.
Suppose not. Then for any natural number
Let us stop here and look at what we have proved. In ZFC, there is an
upper bound on the provable Kolmogorov complexity. However,
there is no upper bound on Kolmogorov complexity! Therefore there are
some true statements of the form
We have been making an implicit assumption about our foundational
theory, namely that it was consistent. In other words, we assumed that
no contradiction is a theorem of ZFC. A contradiction is a vacuously
false statement like
Recall that ZFC can prove statements about itself. So wouldn’t it be nice to actually have a proof of this assumption in ZFC? This would be proving the consistency of our foundational theory within the theory itself, showing that the theory is self sufficient. Certainly Hilbert wanted to do it. However his efforts were crashed by, Gödel who proved that no sufficiently rich theory can prove its own consistency. Here sufficiently rich roughly means strong enough to interpret arithmetic. Now we will give a modern proof of this theorem using Kolmogorov complexity. The proof is due to Shira Kritchman and Ran Raz.
Their proof is loosely based on the surprise examination paradox:
In your introduction to logic class, you announce that the students will have an exam next week, but they will not know the exact day of the exam. So the exam cannot be on Friday because otherwise, the students will know that the exam will be on Friday after not having an exam on Thursday. Similarly the exam cannot be on Thursday, Wednesday, Tuesday or Monday.
Let
Now let us prove that
Now let us prove that
Now let us prove that