Decidability and Definability

This post is an extension of the previous one; I want to address Tarski’s Undefinability Theorem using computability-theoretic methods.


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 \alpha(x) 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 \phi(x, y, z, s) 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 (c_1, c_2, \ldots, c_s) of length s, so that c_1 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 e. By this I mean, let \phi_e(y) be the function which equals z if the algorithm coded by e halts on input y and outputs z; if the algorithm does not halt on input y, then \phi_e(y) is undefined. This function can then be considered a definable set: it’s the set of ordered pairs \{ (y, z) : \exists s (\phi(e, y, z, s) \} .

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: H = \{ (e, y) : \exists z \exists s \phi(e, y, z, s) \}. 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 \{ y : \exists s \phi(e, y, 1, s) \} 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 X^\prime is the “halting problem relativized to X”:

X^\prime = \{ (e, y) : the e^{\text{th}} X-oracle algorithm halts on input y \}.

For example, the Turing Jump of the empty set, \emptyset^\prime, is just the regular halting problem. Notice that if X is a definable set, then so is X^\prime: 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 \Phi(x, y, z, s) 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: X^\prime = \{ (e, y) : \exists z \exists s \Phi(e, y, z, s) \}.

Truth is Undefinable

This brings us to an easy, computability-theoretic proof of Tarski’s Undefinability Theorem. Let T be the set of Gödel codes of true arithmetic statements. Suppose T is definable. Then T^\prime is also definable using the results of the last section, so there is some formula \theta(e, y) 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 T^\prime to a question about whether a particular arithmetic statement is true. That is, we can decide T^\prime using T, since (e, y) \in T^\prime if and only if \lceil \theta(e, y) \rceil \in T. But this is a contradiction, because, as we saw before, for every set X, X^\prime 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.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s