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

# Category Archives: Gems and stones

# 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.

# 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.