You know, you

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 \mathbb{N}_0\rightarrow\mathbb{B} from the natural numbers \mbox{N}_0 into the boolean values \mathbb{B}=\{0,1\}. 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 (\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}, 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 A and B have the same cardinality, iff there is a bijection f:A\rightarrow B.

Simple examples of infinite sets of the same cardinality are \mathbb{N}_0 and \mathbb{Z} through the bijection z\mapsto |2z|+\frac{1}{2}|\mbox{sgn}(z)|(\mbox{sgn}(z)-1). Furthermore, \mathbb{N}_0^2 and \mathbb{N}_0 are of the same cardinality, one bijection is the cantor pairing (x,y)\mapsto\frac{1}{2}(x+y)(x+y+1)+y.

Definition: Sets of the same cardinality as \mathbb{N}_0 are called countable.

That is, \mathbb{Z} and \mathbb{N}_0^2 are countable. Furthermore, \mathbb{Q} is countable.

Theorem: The set \mathbb{N}_0\rightarrow\mathbb{B} of boolean sequences is not countable.
Proof: Assume there was a bijection f:\mathbb{N}_0\rightarrow(\mathbb{N}_0\rightarrow\mathbb{B}) from the natural numbers into the boolean sequences. But then x\mapsto 1 - f(x)(x) cannot be in the image of f. Contradiction. --

Furthermore, \mathbb{R} and \mathbb{C} 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 nc:(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B}

nc(f) = \left\{\begin{array}{cl} 0 & \mbox{if } f(x)=0 \mbox{ for all } x\in\mathbb{N}_0 \\ 1 & \mbox{otherwise} \end{array}\right.

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

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 b:X\rightarrow\mathbb{B} be a boolean function on some set X. If we have a given set X and such a function, we can build the set \{x\in X|f(x)=1\}. This way, boolean functions can be seen as functions which "decide" what elements belong to a set. This yields the following definition:

Definition: \mathbb{N}_0 is decidable, and for every decidable set X, if there is a computable function f:X\rightarrow\mathbb{B}, the set \{x\in X|f(x)=1\} 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 nc: The set of (computable) boolean sequences which have at least one 1 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

\{ \forall_xx=x+0, \forall_x\exists_y x+y=0, \forall_x\forall_y\forall_z (x+y)+z=x+(y+z)\}

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 (\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B} from boolean sequences into booleans is decidable.

If two functions f,f' are not equal, we can find a boolean sequence g such that fg\neq f'g. 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 f can, as it only runs for a finite amount of time, only access finitely many elements of its argument. That is, when calculating f(g) for some g:\mathbb{N}_0\rightarrow\mathbb{B}, there is a maximal m_g\in\mathbb{N}_0 such that the calculation depends on g(m_g), but not on g(m'), m'>m_g. For a given sequence g we can find this m_g by tracking which image values of g the calculation of f uses.

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

Let f:(\mathbb{N}_0\rightarrow\mathbb{B})\rightarrow\mathbb{B} and a:\mathbb{N}_0\rightarrow\mathbb{B}. Then we encode the information that f(a)=k by

M_{c,f,a}:=(\bigwedge_{a(i)=1,i\le m_f} A_i \wedge \bigwedge_{a(i)=0,i\le m_f} \lnot A_i)\rightarrow c=k

That is, we postulate that if A_i is true for a(i)=1 and false for a(i)=0 for all i\le m_f, then c=k. This is a straightforward encoding. To encode f completely, we define the theory

T_{c,f}:=\{M_{c,f,a}|a\in\mbox{dom}(f)\}

Now assume a second function g is given, with f = g. Then, PA\cup T_{c,f}\cup T_{d,g}\cup\{c\neq d\} 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.