This post is an extension of the previous one; I want to address Tarski’s Undefinability Theorem using computability-theoretic methods.
Algorithms
In the last post, I talked about “arithmetization” — in particular, that for any formula in first order logic, there is a corresponding number which codes that formula. The key point in that discussion is that arithmetic is, essentially, the study of finiteness — anything that is essentially a finite object (or a finite sequence of finite objects) can be coded as a number.
Computability theory is no different! One could slowly work through the details of building up a Turing Machine, but it might be simpler to think of a regular computer program: it is a sequence of instructions. In machine code, somewhere, each of those instructions is assigned a particular number (and there are only finitely many instructions in a particular instruction set), and so a program is just a finite sequence of those numbers. Then there is a formula which is true if and only if x is a code for a finite sequence of valid instructions. That is: the set of all (codes for) algorithms is definable!
Further, running an algorithm can also be formalized within arithmetic. That is, there is a formula which is true if and only if the algorithm coded by x runs on input y for s steps and outputs z. This formula boils down to: “Look for a finite sequence
of length
, so that
is the start configuration of the algorithm coded by x on input y, each element of that sequence follows immediately from the previous one by running one more step of the algorithm, and the last element is the result of running the instruction ‘Output z’.”
As an aside, the input to an algorithm we always consider to just be a natural number, but through coding this can represent many other things (for example, it can represent a finite graph).
Moreover, using this formula, we can define the “partial computable function” that is defined by the algorithm coded by a particular number . By this I mean, let
be the function which equals
if the algorithm coded by
halts on input y and outputs z; if the algorithm does not halt on input y, then
is undefined. This function can then be considered a definable set: it’s the set of ordered pairs
.
The Halting Problem and Oracles
The Halting Problem is a famous undecidable problem in computability theory. The problem is simply: given a code e and an input y, determine if the algorithm coded by e halts (and outputs anything) on input y. That this problem is undecidable means that there is no algorithm which, for all pairs (e, y), outputs TRUE (or 1) if the algorithm e halts on input y, and outputs FALSE (or 0) if it does not. The proof that this problem is undecidable is well-known, so instead of providing it here I will refer you to a version in the style of Dr. Seuess.
On the other hand, we can define the set: . So the halting problem is definable, but not decidable. (Conversely: all decidable sets of numbers are definable, since if a set is decided by an algorithm e, the set
defines it). Hold this thought for a moment.
An interesting phenomenon in computability theory is that most results relativize. Given a set X, one can define the concept of an “X-oracle algorithm” — a finite sequence of instructions, where we allow an extra operation of asking whether an element is a member of the set X. Then the “relative Halting Problem” for X asks whether there is an X-oracle algorithm which decides whether a given X-oracle algorithm halts on a particular input. Essentially the same proof that the halting problem is undecidable gives us the following result:
Theorem: For any set X, the “X-oracle halting problem” is not decidable using an X-oracle algorithm.
We make the following definition: given a set X, the Turing Jump of X, denoted is the “halting problem relativized to X”:
the
X-oracle algorithm halts on input
.
For example, the Turing Jump of the empty set, , is just the regular halting problem. Notice that if
is a definable set, then so is
: an X-oracle algorithm is a finite sequence of operations, where each operation is definable. Similar to how we proceeded for ordinary algorithms, there is a formula
which is true if and only if the X-oracle algorithm coded by x halts on input y in s steps and outputs z. Therefore we can define the Turing Jump:
.
Truth is Undefinable
This brings us to an easy, computability-theoretic proof of Tarski’s Undefinability Theorem. Let be the set of Gödel codes of true arithmetic statements. Suppose
is definable. Then
is also definable using the results of the last section, so there is some formula
which is true if and only if the T-oracle algorithm coded by e halts on input y.
But now we have reduced membership in to a question about whether a particular arithmetic statement is true. That is, we can decide
using
, since
if and only if
. But this is a contradiction, because, as we saw before, for every set
is not decidable with an X-oracle algorithm. Therefore, T must not be definable!
This proof seems to hide the “self-reference” paradox that is used in the traditional proof. However, that is only because the self-reference occurs in the computability part! If you have ever looked at a proof of the halting problem (again, see the Dr. Seuss-esque version linked earlier), you see that the proof relies upon a similar self-reference problem: the ability for an algorithm to take in another algorithm as input, and run it. So in a sense, self-reference is essential to this theorem.