# Posts in the category Gems and stones

### Intermediate truth values

- 30 July 2015
- Constructive math, Gems and stones, Logic

I have not written a blog post in a while, so I decided to write up a short observation about truth values in intuitionistic logic which sometimes seems a bit puzzling.

Let $\Omega$ be the set of truth values (in Coq this would be the setoid whose underlying type is $\mathsf{Prop}$ and equality is equivalence $\leftrightarrow$, while in HoTT it is the h-propostions). Call a truth value $p : \Omega$ **intermediate** if it is neither true nor false, i.e., $p \neq \bot$ and $p \neq \top$. Such a “third” truth value $p$ is proscribed by excluded middle.

The puzzle is to explain how the following two facts fit together:

**“There is no intermediate truth value”**is an intuitionistic theorem.**There are models of intuitionistic logic with many truth values.**

### Constructive gem: an injection from Baire space to natural numbers

- 15 June 2011
- Constructive math, Gems and stones, Logic, Publications

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 (3 comments)### Constructive gem: double exponentials

- 12 October 2009
- Gems and stones, Programming

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.

### Constructive gem: juggling exponentials

- 09 September 2009
- Gems and stones

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

- 08 September 2009
- Gems and stones

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: cardinality of sets

- 08 September 2009
- Gems and stones

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

- 07 September 2009
- Gems and stones

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 (3 comments)

### Constructive gems and stones

- 07 September 2009
- 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 Stone_s, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics.

A constructive *gem* is something nice about constructive mathematics that makes you want to know more about it. In contrast, a constructive *stone* is a complication in constructive mathematics which does not exist in the classical counterpart.

Here we go! The first one is about finite sets.

→ continue reading