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

# Category Archives: Constructive math

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

# 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