Robert's Mistakes

A constructivist's magic

Constructive mathematics is just like ordinary mathematics, except that it tries hard to avoid the law of excluded middle. It means that you cannot do proofs by contradiction. Assuming something, and then concluding a contradiction is no longer considered a valid argumen. Cantor's proof that there is no bijection between the natural counting numbers, and the real numbers of the continuum is such a proof. And so is Gödel's incompleteness theorem, and Turing's proof that there is no program to tell wether an arbitrary program halts.

For a constructivist, these aren't undisputable facts! They hold only in some settings, but there are systems in which the real numbers are countable, where there is a formalism to cover all of mathematics, and where we can write a program to check wether any program halts! To talk about these, we might want to introduce the notion of a topos. A topos is a collection of tools with which we can do mathematics. Not a particular one, there are many toposes. The effective topos, for example, is one, were every function is computable! By definition!

I won't go into details right now, as that could take a while. But let's try and imagine what such constructive worlds might look like. How could it be, that we might be able to enumerate all real numbers?

Well, the way we do mathematics is fundamentally limited. Any concept we might want to communicate is necessarily finite in some sense. So the collection of all real numbers we can hope to name are is at least countable. And there we are. We can simply claim that the real numbers can only be ones which we're able to point at, and poof, they're countable!


Andrej Bauer gave a very nice talk in which he relates learning about constructive mathematics to Kübler-Ross' five stages of grief: denial, anger, depression, bargaining, acceptance.

Here's his talk on youtube:


Here's an updated version in form of a paper:

Infinite Turing machines

While reading a paper by Andrej Bauer1 I stumbled upon a nifty little fact separate from constructive mathematics. It's about infinite turing machines. One of those is like normal Turing machine, except that it also has a state for when it did an infinite number of steps. When it jumps to a limit ordinal, it is wound back to the beginning of its tape, and each cell is set to zero when its value settles to always zero at some point α\alpha, and to one when that's not the case.

Just like with normal Turing machines there's a special halting state, and an infinte Turing machine may halt at some ordinal, or it may run forever. Now here's the nifty fact: If it hasn't halted by step ω1\omega_1, the first uncountable ordinal, it never will! The reason is that, when it gets there, it has exhausted the number of states it can produce on its tape!

And that is a lot! Even moderately ordinal running times already allow checking arithmetic, and approaching ω1\omega_1 will allow checking every theoretically fathomable theory! Well, at least classically, right? Andrej's paper uses all of this space to construct a map N^N -> N. It makes the powerset of N countable!

Infinite Turing machines were invented by Joel David Hamkins, and he has played them out in most interesting ways! Now I want to better understand what a realizability Topos ist. Or what a topos is...