Does the set of real numbers have decidable equality ?

[louis...@free.fr]

I am looking for an example of set with undecidable equality.

In nlabs ( http://ncatlab.org/nlab/show/decidable+equality ) I have found:
- "Of course, in classical mathematics, every set has decidable equality"
but also:
- "the set of real numbers may not have decidable equality"

Does that mean that among the different definitions for real numbers, some of them have decidable equality, and some others (not 'classical') not ?
Where can I find an example of Set with undecidable equality?

Louis.

[Hendrik Boom]

On Sun, Jan 04, 2015 at 06:25:34AM -0800, louis...@free.fr wrote:
> I am looking for an example of set with undecidable equality.

You have to be clear what you mean by 'decidable'.

If you mean there is an algorithm that will answer all instances of the
question, then you will have to restrict the question to finite
symbolic representations of the elements of your set; that's what
algorithms can tale as input. As such, the classical real numbers
don't qualify.

But if you look at the constructive real numbers, and if you define a
constructive real to be an algorithm that will, so to speak, compute
arbitrarily close approximatinos to it, then they do qualify.

Just imagine real numbers whose digits are 5's as long as a
particular turing machine has not yet terminated, but change to
4's as soon as it does terminate. Then testing for equality of
these numbers with 5/9 (which is all 5's) would give a way to
tell whether Turing machines terminate.

-- hendrik

>
> In nlabs ( http://ncatlab.org/nlab/show/decidable+equality ) I have found:
> - "Of course, in classical mathematics, every set has decidable equality"

Only in the sense that classically, every proposition is considereed
true or false, no matter whetehr there's a way of deciding it.

> but also:
> - "the set of real numbers may not have decidable equality"

Probably more realistic.

>
> Does that mean that among the different definitions for real
> numbers, some of them have decidable equality, and some others (not
> 'classical') not ?
> Where can I find an example of Set with undecidable equality?

The constructive reals.

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

[Michael Shulman]

In constructive mathematics, a set A is said to have decidable
equality if the statement "for all x,y\in A, either x=y or x<>y" is
true. On its face this has nothing to do with computation. However,
since constructive mathematics has computable models, for a set to
*provably* have decidable equality in unaugmented constructive
mathematics, there must be an algorithm which decides the equality of
its elements. Since there is no such algorithm for the real numbers
(with any definition), it is not possible to prove, in unaugmented
constructive mathematics, that the real numbers have decidable
equalty.

But if we assume additional axioms, then more sets can have decidable
equality. E.g. if we assume the law of excluded middle to obtain
classical mathematics, then all sets will have decidable equality.
(Also, in models of constructive mathematics other than computable
ones, decidable equality means something different, e.g. in
topological models it means a sort of "discreteness".) Thus, since
LEM is consistent, it is not possible to prove, in unaugmented
constructive mathematics, that any particular set (including the real
numbers) does *not* have decidable equality.

HTH,
Mike

On Sun, Jan 4, 2015 at 6:25 AM, louis...@free.fr <louis...@free.fr> wrote:
> I am looking for an example of set with undecidable equality.
>

> In nlabs ( http://ncatlab.org/nlab/show/decidable+equality ) I have found:
> - "Of course, in classical mathematics, every set has decidable equality"

> but also:
> - "the set of real numbers may not have decidable equality"
>

> Does that mean that among the different definitions for real numbers, some of them have decidable equality, and some others (not 'classical') not ?
> Where can I find an example of Set with undecidable equality?
>

[Andrej Bauer]

As you note, classically all sets have decidable equality. In fact,
the statement "all sets have decidable equality" is equivalent to
excluded middle.

In general, a statement such as "constructively X may happen" should
be understood as "there is a model of constructive mathematics in
which X happens". Also, people do not bother to say "constructively X
may happen" for X which is actually provable constructively.

The real numbers (either Cauchy or Dedekind) may have undecidable
equality. Here are two models:

1. As already metnioned by Hendrik, in the effective topos a real is
represented by a Turing machine that computes arbitrarily good
rational approximations, and here it is easy to see that equality on
reals cannot be decided, because it would give us a non-computable
map, but all maps in the effective topos are computable.

2. In a topos of sheaves Sh(X) the reals tend to have undecidable
equality. The Dedekind reals in Sh(X) is the sheaf of real-valued
continuous maps. For reals to have decidable equality the following
has to happen: given any two continuous maps f, g : U -> R (where U is
an open subset of X and R is the usual space of reals) the sets

V = { f(x) = g(x) | x in U }

and

W = { f(x) <> g(x) | x in U }

must be open. Unless X is quite trivial, this wil not be the case. For
example, if X is Hausdorff the set V will be closed, and so unlikely
to be also open.

But if you are just looking for sets whose equality cannot be proved
decidable, you've got other possibilities:

1. The powerset of a singleton P({0}) has decidable equality iff
excluded middle holds

2. Cantor space N -> {0,1} (the set of infinite binary sequences) has
decidable equality iff LLPO holds
(http://en.wikipedia.org/wiki/Limited_principle_of_omniscience).

With kind regards,

Andrej

[louis...@free.fr]

Thanks !
Decidability with power sets is indeed addressed clearly in the HoTT book (p. 36, 116, 344).