Mathematics and Computation

A blog about mathematics for computers

Intermediate truth values

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:

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

Mind you, excluded middle says “every truth value is either $\bot$ or $\top$” while we are saying that there is no truth value different from $\bot$ and $\top$:
$$\lnot \exists p : \Omega \,.\, (p \neq \top) \land (p \neq \bot).$$
Coq proves this:

Theorem no_intermediate: ~ exists p : Prop, ~ (p <-> True) /\ ~ (p <-> False).
Proof.
  firstorder.
Qed.

Note that we replaced $=$ with $\leftrightarrow$ because equality on $\Omega$ is equivalence on $\mathsf{Prop}$ in Coq (this would not be neccessary if we used HoTT where h-propositions enjoy an extensionality principle). You should also try proving the theorem by yourself, it is easy.

A model of intuitionistic mathematics with many truth values is a sheaf topos $\mathsf{Sh}(X)$ over a topological space $X$, so long as $X$ has more than two open sets. The global points of the sheaf of truth values $\Omega$ are the open subsets of $X$, and more generally the elements of $\Omega(U)$ are the open subsets of $U$.

So, if we take an intermediate open set $\emptyset \subset U \subset X$, should it not be an intermediate truth value? Before reading on you should stop and think for yourself.

Really, stop reading.

Let us calculate which open set (truth value) is
$$(U \neq \top) \land (U \neq \bot).$$
Because $U = \top$ is equivalent to $U$ and $U = \bot$ to $\lnot U$ our formula is equivalent to
$$\lnot U \land \lnot\lnot U.$$
Remembering that negation is topological exterior we get
$$\mathsf{Ext}(U) \cap \mathsf{Ext}(\mathsf{Ext}(U))$$
which is empty,
$$\emptyset.$$
Indeed, $U$ is not a counterexample!

We have here a typical distinction between internal and external language:

By the way, the mathematicians on the inside also think that “yes” and “no” are valid answers, and there is no other – that is precisely the statement “there is no intermediate truth value” – but they think of it as “holding everywhere on $X$”.

There are of course many situations where the difference between iternal and external language may create confusion. For example, if $X = \mathbb{N}$ is a countable discrete space then the object of natural numbers is the sheaf of all maps into $\mathbb{N}$, of which there are uncountably many. Thus on the outside we “see” that there are uncountably many natural numbers in $\mathsf{Sh}(X)$. Those on the inside would of course disagree. This is an amusing situation, sort of a reverse of Skolem's paradox.

Comments

Marc Hamann

Is it safe to say that the difference that the translation from external language to internal language can be called "evaluation" and that a lot of the "paradoxes" of intermediate truth values arise from the known properties of the latter?

Andrej Bauer

Not really, for starters the translation goes the other way: the internal language can be translated into the external one, but not vice versa. It's not so much an evaluation than it is semantics, i.e., giving meaning to internal statements in terms of structures which are observed on the outside.

Jesse McKeown

Fair enough, Andrej, but I think what Marc is getting at (and what you're implicitly using to surprise us) is: you started with what looks like a sentence in First Order Logic, remind us that a classicwise-similar-looking looks like a formula sits where logics intuitionist and classical part ways, and then (as you say, is puzzling) point out that the first one Is Nonetheless an Intuitionistic Theorem.

And then, in the section where you first mention "internal" and "external" languages, you describe two ways of reading the formula: "mathematicians inside [...] ask [...] 'where is it true?'" vs. "mathematicians outside [...] compare the open set U to the open sets X and Ø." It sure looks like you're taking a *ternality-agnostic formula and "evaluating" it in the internal/external logics/languages. It looks like you're saying "it depends what you mean by 'is'".

At least, this is the impression one will have who is used to the classical and classically-reasonable distinctions between Languages, Theories, and Models. And perhaps the upshot is: the "internal language" and "the" "external language" (perhaps also "the forcing language") are not "Language"s in the logician's sense, but languages in the more-human sense of language-with-a-subtext.

Andrej Bauer

I think I mostly did not understand Marc.

First a technical point. The formula $\lnot \exists p \in \Omega \,.\, (p \neq \top) \land (p \neq \bot)$ is not first-order. It is written in the language of higher-order logic, as usually formulated in relation to topos theory. (If we insisted on a first-order language then we would be stuck. We could try a schema but that would not get the point across.)

Of course I am saying "it depends what you mean"! That's the whole point of the blog post: do not forget that a formula interpreted in one model may have a totally different meaning than its interpretation in another model. It is all too easy to forget this obvious bit of logic and write a book about Skolem's pardox.

All of what I am saying applies equally well to classical first-order logic and model theory, where exactly the same phenomena occur. In fact, my last example of "uncountable natural numbers" takes place in a (silly) model of classical set theory.

The phrase "internal language" can mean two things. The less formal meaning is that it just mean "the interpretation of the language in some model". The more technical meaning from categorical logic is that it is the language induced by a category (say, a topos). Such a language is not "just syntax", for instance it has a type for every object of the category. Even "traditional" logicians are used to such tricks and have no qualms about adjoining uncountably many constants to a language. So I am not sure I understand your point. There is no subtext, just two interpretations of a language.

Daniel Tung

Hi, Interesting blog post! I am particularly interested in the possible consequences of intuitionism or constructive Mathematics on Physics. Riemann took an internal viewpoint to describe geometry and created Riemannian geometry. Einstein also took an internal view on space and time measurements and realised that Riemannian geometry was a perfect fit for his ideas. I wonder if there is something like the above "internal viewpoint" in logic, or in other fields of Mathematics?

Andreas Blass

Your observation about "no intermediate truth values" brings up an unpleasantness in the standard terminology. Both of the phrases "excluded middle" and "tertium non datur" would, it understood literally, mean "no intermediate truth values." We've been trained to understand them as meaning "for all truth values p, p or not p", but the literal meaning is, because of the negative terms "excluded" and "non", weaker than the correct meaning.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.