Constructive gem: an injection from Baire space to natural numbers

I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$. Continue reading Constructive gem: an injection from Baire space to natural numbers

Constructive gem: double exponentials

In the last constructive gem we studied the exponential $2^\mathbb{N}$ and its isomorphic copies. This time we shall compute the double exponential $2^{2^\mathbb{N}}$ and even write some Haskell code. Continue reading Constructive gem: double exponentials

Constructive gem: juggling exponentials

Constructive gems are usually not about particular results, because all constructive results can be proved classically as well, but rather about the method and the way of thinking. I demonstrate a constructive proof which can be reused in three different settings (set theory, topology, computability) because constructive mathematics has many different interpretations.

Continue reading Constructive gem: juggling exponentials

Constructive stone: minima of sets of natural numbers

I promise I will post a constructive gem soon. This constructive stone came up as a reaction to the cardinality of finite sets stone. I show that inhabited sets of natural numbers need not have minima, constructively.

Continue reading Constructive stone: minima of sets of natural numbers

Constructive stone: cardinality of sets

Cardinality of sets in constructive mathematics is not as well behaved as in classical mathematics. Cardinalities of finite sets are not natural numbers, and cardinalities are not linearly ordered.

Continue reading Constructive stone: cardinality of sets

Constructive stone: finite sets

Just like in real life, constructive stones are easier to find than constructive gems, so let me start the series with a stone about constructive finite sets.

Two girl one cup

Continue reading Constructive stone: finite sets

Constructive gems and stones

In various mathematical forums, mostly those of a logical flavor, I regularly see people asking basic questions about constructive mathematics. I also see misconceptions about constructive mathematics. I shall make a series of posts, Constructive Gems and Stones, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics.

A [...]