A note on ||X|| vs. ¬¬X

[Martin Escardo]

Despite hundreds of messages about the information content of ||X|| in
this list, I often get people to tell me that they can't see the
difference of ||X|| and ¬¬X.

Perhaps this is because of "classical bias", the instinctive assumption
of excluded middle (LEM).

Indeed, LEM = (Pi(X:U). ||X|| = ¬¬X).

What we do have without assuming (or denying) LEM is ||X|| -> ¬¬X.

The assertion ||X|| says that X has a point, without revealing it. The
assertion ¬¬X say that X is non-empty, or that it is impossible that it
is empty. So, on the face of it, none of ||X|| and ¬¬X reveal a point of
X in general.

So how can they be different?

First, none of ||X|| and ¬¬X can keep the unknown point of X absolutely
secret. For instance, if X is decidable, meaning that we have X+¬X,
then, as soon as we get to know ¬¬X, we find a point of X.

The difference of ||X|| and ¬¬X is that ||X|| gives more information
than ¬¬X in general. In particular, we can find a point of X from a
point of ||X|| more often than from a point of ¬¬X.

In the absence of excluded middle, it may be surprising that the unique
map ||X|| -> ¬¬X turns out to be an embedding with empty complement.

But any map P->Q of propositions is an embedding. And its complement is
Qx¬P, which is the empty type when Q=¬¬X and P=||X||.

In the absence of excluded middle, it should not be a surprise that
there are embeddings with empty complement which are not necessarily
equivalences.

A canonical example is the embedding of the booleans 1+1 into the type
of propositions. The fact that it has empty complement sounds like
excluded middle, but it isn't: what it says is that there is no
proposition simultaneously different from 0 and from 1,

¬Sigma(P:Prop). P/=0 x P/=1,

because this amounts to saying that

¬Sigma(P:Prop).(¬¬P x ¬P),

which is the case. There is no truth value other than 0 or 1.
Any truth value other than 0 and 1 is excluded.

What so-called excluded middle says is that we can determine
(naturally/continuously/computably/constructively/uniformly/...) which
of 0 or 1 any proposition is:

Pi(P:Prop). P=0 + P=1.

An example where we have ||X||->X but not necessarily ¬¬X->X is

X=Sigma(n:N).f(n)=0

with f:N->N. We have that ||X||->X just holds (as discussed often in
this list), but ¬¬X->X is Markov principle, which may not hold.

The type ||X|| is a proper subspace of ¬¬X in general.

There is no point of the space ¬¬X which is not in the type ||X||. But,
on the other hand, there is no
natural/continuous/computable/constructive way, for a given point of
¬¬X, of establishing that it is in ||X||.

The type ||X|| is a subspace of ¬¬X with empty complement, but far from
equivalent to ¬¬X in general, giving much more information than ¬¬X,
precisely because it is a proper subspace of ¬¬X.

To add more to the confusion, there are more notions of anonymous
existence of points of X, as in work with Nicolai, Thierry and Thorsten.
One of them is that any weakly constant endomap of X has a fixed point,
written <<X>>. We have X -> ||X|| -> <<X>> -> ¬¬X,
where none of these implications can be reversed in general. However,
||X||->X is logically equivalent to <<X>> -> X.

There are many ways of partially specifying a point of X without fully
revealing any, which give different amounts of information, or,
different amounts of revelation.

Martin

[Michael Shulman]

It can also help to think about models. In a model of sheaves on a
space U, for instance, ||X|| is the support of X, the union of all
open subsets of U over which X has a section, while ¬¬X is the
interior of the closure of ||X||. The latter is generally larger than
||X||; for instance, if ||X|| is a punctured open disc in R^2, then
¬¬X is the unpunctured disc.

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Martin Escardo]

On 07/04/16 23:58, Michael Shulman wrote:
> It can also help to think about models. In a model of sheaves on a
> space U, for instance, ||X|| is the support of X, the union of all
> open subsets of U over which X has a section, while ¬¬X is the
> interior of the closure of ||X||. The latter is generally larger than
> ||X||; for instance, if ||X|| is a punctured open disc in R^2, then
> ¬¬X is the unpunctured disc.

Yes. This is the continuous case I alluded to when I said
"naturally/continuously/computably/constructively/uniformly/...".

But it is good to have the visual picture you offer, seeing ||X|| and
¬¬X becoming different in a continuous model. They also become different
in computable models, for instance (and for related reasons).

But what I wanted to convey is that the difference of ||X|| and ¬¬X can
perhaps be understood operationally, with ||X|| giving more information
than ¬¬X when we perform mathematics in type theory before we consider
any model.

And emphasize that ||X|| is always a subspace of ¬¬X with empty
complement, in whatever moder we are talking about. In the topological
model, this amounts to density, as in your example.

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Steve Awodey]

the topological description is clearly stated in Awodey-Bauer 2004.