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 IntroductionA 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 SetsWhile 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 TheoryThere 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 LogicDefinition: 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 ProofWe 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.