Mon, 25 Jun 2012 16:00:00 GMT

For the best maths-club of the multiverse I will give a short talk on an already mentioned property of boolean sequences. As the audience consists of a wide range of ages and expierience, I will not do everything as formal as it should be done from a strictly mathematical point of view. My goal is to give young people an idea on what is going on, while providing to older people enough material to complete everything.

Furthermore, there is an easier way of showing the actual result, but I rather want to touch a large variety of topics than doing a short formal proof in detail. I hope to give especially young people an overview on many topics of logic and tcs.

**0 Introduction**

A boolean sequence is a sequence of boolean values "true" and "false", or 1 and 0. It can be seen as a function from the natural numbers into the boolean values . There are uncountably many such boolean sequences, as we will show later. Furthermore, in general, it is not decidable whether two such sequences are equal, even if these sequences can be enumerated by a computer program.

We are now interested in functions of the type , that is, functions that assign a boolean value to boolean sequences. In general, their equality is not decidable.

However, if two such functions can be calculated by a computer program, it is decidable whether they are equal. We will show this in a rather complicated way, as our goal is not to give a prove of this, but to touch many fields of logic and computer science.

**1 Crashcourse Infinite Sets**

While for finite sets it is rather easy to talk about "numbers" of elements, for infinite sets we need a more sophisticated notion. We may assign every set its "cardinality", however, for our purposes it is sufficient to be able to compare the size of sets.

__Definition:__ Two sets and have *the same cardinality*, iff there is a bijection .

Simple examples of infinite sets of the same cardinality are and through the bijection . Furthermore, and are of the same cardinality, one bijection is the*cantor pairing* .

__Definition:__ Sets of the same cardinality as are called *countable*.

That is, and are countable. Furthermore, is countable.

__Theorem:__ The set of boolean sequences is not countable.

__Proof:__ Assume there was a bijection from the natural numbers into the boolean sequences. But then cannot be in the image of . Contradiction. --

Furthermore, and are not countable.

**2 Crashcourse Computation Theory**

There are several equivalent formal definitions of computability. However, they are rather technical, and outside the scope of this talk.

__Improper Definition:__ A function is called *computable*, if it can be computed by a computer with inexhaustible memory in a finite amount of time.

Most functions you will usually have to deal with are computable. A simple example of a non-computable function is the following function

It takes as an argument a boolean sequence, and decides whether this boolean sequence contains a .

If you do not believe me that this function is not computable, go on, try to implement it in the programming language of your choice! In fact, trying this is probably a good exercise.

Let be a boolean function on some set . If we have a given set and such a function, we can build the set . This way, boolean functions can be seen as functions which "decide" what elements belong to a set. This yields the following definition:

__Definition:__ is *decidable*, and for every decidable set , if there is a computable function , the set is called *decidable*.

The intuition behind this definition is that a set is called decidable, if a computer can decide whether it contains a given element.

As with computable functions, also most sets one has to explicitly deal with is decidable. An exception can be derived directly by the above example : The set of (computable) boolean sequences which have at least one in their image is not decidable. In fact, quite a lot of sets one uses implicitly are not decidable.

**3 Crashcourse Logic**

__Definition:__ Formulae that only quantify over objects, but not over relations or functions of objects, are called *first-order formulae*. A *first-order theory* is a set of such formulae.

An example for such a theory is group theory

Every structure satisfying a theory is called a*model* of this theory. For example, every group is a model of group theory.

Notice that theories need not be finite.

If a formula holds in all models of a theory, the theory*implies* this formula, and it can be shown that there exists a formal proof of this formula from the theory. This is called *Completeness Theorem* and the proof requires a lot of theory.

If a formula holds for a theory, then it holds for a finite subset of this theory: By the Completeness Theorem, it must be provable, and a formal proof is a finite object and can only use finitely many axioms.

**4 The Proof**

We will now show that in fact the equality of computable functions from boolean sequences into booleans is decidable.

If two functions are not equal, we can find a boolean sequence such that . Therefore, in this case we can prove the inequality. The more interesting part is that we can prove equality if it holds.

Firstly we notice that such a function can, as it only runs for a finite amount of time, only access finitely many elements of its argument. That is, when calculating for some , there is a maximal such that the calculation depends on , but not on . For a given sequence we can find this by tracking which image values of the calculation of uses.

Our strategy is now to use this property to encode functions into a first-order theory. Denote by the theory of peano arithmetic (usual elementary number theory). We define an additional relation on natural numbers .

Let and . Then we encode the information that by

That is, we postulate that if is true for and false for for all , then . This is a straightforward encoding. To encode completely, we define the theory

Now assume a second function is given, with . Then, implies a contradiction. By the Completeness Theorem, there is therefore a formal proof of a contradiction. We can use an exhaustive proof search (a "blast") to find a contradiction proof in that case, as we know it exists.

Furthermore, there is an easier way of showing the actual result, but I rather want to touch a large variety of topics than doing a short formal proof in detail. I hope to give especially young people an overview on many topics of logic and tcs.

A boolean sequence is a sequence of boolean values "true" and "false", or 1 and 0. It can be seen as a function from the natural numbers into the boolean values . There are uncountably many such boolean sequences, as we will show later. Furthermore, in general, it is not decidable whether two such sequences are equal, even if these sequences can be enumerated by a computer program.

We are now interested in functions of the type , that is, functions that assign a boolean value to boolean sequences. In general, their equality is not decidable.

However, if two such functions can be calculated by a computer program, it is decidable whether they are equal. We will show this in a rather complicated way, as our goal is not to give a prove of this, but to touch many fields of logic and computer science.

While for finite sets it is rather easy to talk about "numbers" of elements, for infinite sets we need a more sophisticated notion. We may assign every set its "cardinality", however, for our purposes it is sufficient to be able to compare the size of sets.

Simple examples of infinite sets of the same cardinality are and through the bijection . Furthermore, and are of the same cardinality, one bijection is the

That is, and are countable. Furthermore, is countable.

Furthermore, and are not countable.

There are several equivalent formal definitions of computability. However, they are rather technical, and outside the scope of this talk.

Most functions you will usually have to deal with are computable. A simple example of a non-computable function is the following function

It takes as an argument a boolean sequence, and decides whether this boolean sequence contains a .

If you do not believe me that this function is not computable, go on, try to implement it in the programming language of your choice! In fact, trying this is probably a good exercise.

Let be a boolean function on some set . If we have a given set and such a function, we can build the set . This way, boolean functions can be seen as functions which "decide" what elements belong to a set. This yields the following definition:

The intuition behind this definition is that a set is called decidable, if a computer can decide whether it contains a given element.

As with computable functions, also most sets one has to explicitly deal with is decidable. An exception can be derived directly by the above example : The set of (computable) boolean sequences which have at least one in their image is not decidable. In fact, quite a lot of sets one uses implicitly are not decidable.

An example for such a theory is group theory

Every structure satisfying a theory is called a

Notice that theories need not be finite.

If a formula holds in all models of a theory, the theory

If a formula holds for a theory, then it holds for a finite subset of this theory: By the Completeness Theorem, it must be provable, and a formal proof is a finite object and can only use finitely many axioms.

We will now show that in fact the equality of computable functions from boolean sequences into booleans is decidable.

If two functions are not equal, we can find a boolean sequence such that . Therefore, in this case we can prove the inequality. The more interesting part is that we can prove equality if it holds.

Firstly we notice that such a function can, as it only runs for a finite amount of time, only access finitely many elements of its argument. That is, when calculating for some , there is a maximal such that the calculation depends on , but not on . For a given sequence we can find this by tracking which image values of the calculation of uses.

Our strategy is now to use this property to encode functions into a first-order theory. Denote by the theory of peano arithmetic (usual elementary number theory). We define an additional relation on natural numbers .

Let and . Then we encode the information that by

That is, we postulate that if is true for and false for for all , then . This is a straightforward encoding. To encode completely, we define the theory

Now assume a second function is given, with . Then, implies a contradiction. By the Completeness Theorem, there is therefore a formal proof of a contradiction. We can use an exhaustive proof search (a "blast") to find a contradiction proof in that case, as we know it exists.

Show comments (Requires JavaScript, loads external content from Disqus.com)