apartness of Dedekind reals

[Michael Shulman]

Hi,

I am interested in what can be said about the following statement:

(*) For Dedekind real numbers, the usual apartness coincides with the negation of equality.  Equivalently, if a Dedekind real is >=0 and unequal to 0, then it is positive.  Equivalently, apartness of Dedekind reals is not-not-stable.

In particular, I would like to know whether it is equivalent to any better-known or more "logical" statement, such as a form of LPO, LEM, or choice.  Here is what I think do I know (but please correct me if I'm wrong):

1. The analogous principle for *Cauchy* reals is equivalent to Markov's Principle.  Hence, in the presence of a principle (like countable choice) which collapses the Cauchy and Dedekind reals, (*) is also equivalent to MP.  However, I'm interested in topos-valid mathematics where CC may not hold.

2. It holds in a "gros topos" of sheaves on a full subcategory T of topological spaces closed under finite limits and subspaces and containing the real numbers (though it generally fails in a "petit topos" of sheaves on a particular topological space).  In such toposes the Dedekind reals are the sheaf of continuous real-valued functions, while the Cauchy reals are generally the sheaf of locally constant real-valued functions, and so in particular CC fails, though LPO often holds.

3. It also holds in Johnstone's topological topos, where the Dedekind reals are the reals with their usual topology, but LPO fails.

Has anyone studied the principle (*) before?

Thanks,
Mike

[Fred Richman]

How about this variant of Markov's principle? Let A_n be a sequence of inhabited subsets of {0,1} such that 0 cannot be in A_n for all n. Then there exists n such that 1 is in A_n. You might want to add the hypothesis that if m is different from n, then A_m and A_n cannot both be {0,1}.

The sequence A_n is generated by the condition that the cut be located: you look at the rational numbers 1/(n+1) < 1/n.

--Fred

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

[Michael Shulman]

Thanks for your reply! I thought of something like that, and I agree
that such a version of MP implies (*), but I don't see how to get the
converse. (Of course maybe you didn't mean to claim the converse.)
If I have such a sequence, how would I get a Dedekind real that is
located w.r.t. all rational numbers, not just those of the form 1/n?

Mike

> You received this message because you are subscribed to a topic in the Google Groups "constructivenews" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/constructivenews/7nV13HvG-BU/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to constructivene...@googlegroups.com.

[Andrej Bauer]

If we know that a Dedekind real is Cauchy then we can limit the
logical complexity of its cuts. That is, if (L,U) is a Dedekind cut
which coincides with the limit of a rapidly convergng Cauchy sequence
(q_n)_n then we know that L and U are both Σ^0_1 propositions.

The logical complexity cannot be aribtrary I think. That is, it's
impossible to embed the powerset P(1) of a singleton into Dedekind
reals R. That would require a construction which takes a truth value p
and produces a Dedekind real x_psuch that p ⇔ q is equivalent to x_p
= x_q? But it is consistent to assume that all maps P(1) → R are
constant (realizability models, Troelstra's uniformity principle for
modest sets). So, there must be some sort of an upper bound on how
complex the Dedekind cuts are (as subsets of Q).

With kind regards,

Andrej

[Steve Vickers]

Dear Michael,

One thing that can be said - though I know it's not what you were looking for - is that in point-free topology it is true in any topos.

Equality on R, the diagonal subspace of R^2, is closed, and hence complementable, and its (open) complement is apartness. This is in line with the general principle that when dealing with topologized things in toposes you get good results by treating them as point-free spaces.

Steve.

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.

[Robert Lubarsky]

My guess is that what you want is impossible. The reason is hidden in your use of scare quotes. You want (*) equivalent with a " "logical" statement", where it is left imprecise what that would mean. Logic is usually (admittedly not always) based on finite, discrete syntax. That's why it works so nicely with sequences, in particular with Cauchy sequences. And not with Dedekind cuts. Anything we could find equivalent with (*) I believe you would (quite reasonably) not accept as logical. If you want to be more liberal in what counts as logic, then you might as well accept (*) itself as a logical principle (although I could see whereyou'd want to dress it up more nicely, but at this point that's the inessential part). There is a subject called "continuous logic" which might provide you with the closest thing to what you're looking for.

Bob Lubarsky

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.

[Michael Shulman]

On Wed, Jul 1, 2015 at 4:48 AM, Robert Lubarsky
<Lubarsk...@comcast.net> wrote:
> If you want to be more liberal in what counts as logic, then you might as well accept (*) itself as a logical principle

That sounds reasonable. I can certainly see regarding it as a sort of
Markov's Principle which allows "densely spaced increments". But I'm
surprised if no one has studied it before in any form.

Mike

[Paul Taylor]

Dear Mike,

> the usual apartness coincides with the negation of equality.

I would say that apartness (aka inequality) is the natural
relation on the real numbers and that it is unnatural to
introduce equality at all other than as negation of apartness.

Arguments in Archimedes and eg Heyting's book "Intuitionism.."
work with apartness rather than equality.

Topologically, this reflects the fact that R is Hausdorff
and not discrete.

I think most of the issues with LPO etc go away if you look
at things in this way - see my "Lambda Calculus for Real
Analysis" www.paultaylor.eu/ASD/lamcra

However, the way in which you posed your question and
others have answered it suggests that you are working in
a topos (or maybe HoTT). I have nothing to add in that
situation.

Paul

[Henri Lombardi]

Dear all

The english translation (revised and expanded) of "Algèbre commutative. Méthodes constructives" (by Claude Quitté and myself, 2011)

is now published by Springer in the series Algebra and Applications.
Title: Commutative Algebra: Constructive Methods

see

http://www.springer.com/us/book/9789401799430#otherVersion=9789401799430

More details on

http://hlombardi.free.fr/publis/LivresBrochures.html



Henri LOMBARDI
e mail : Henri.L...@univ-fcomte.fr

[Andrej Bauer]

Dear Henri,

this is excellent news, although now I have one less reason to learn French.

Speaking of which, I will be in Paris for a month, starting tomorrow,
visiting University Diderot, doing computer-sciency things. A bit of
constructive mathematics would come as a refreshment, if anyone is
interested please contact me.

With kind regards,

Andrej