[FOM] a simple constructive example when AC is not true

[Mario Carneiro]

In this setup, I believe the critical operation is the taking of a quotient
in going from the (efficient, if you like) Cauchy sequences of rationals to
real numbers.

Given a *representative* of a real number x, that is, a sequence x_n of
rationals that converges to x, we have that there is some i such that |x_i
- x_j| < 1/2. (If the sequence has a reasonable modulus of convergence, i
can even be given as 1 or so.) Since x_i is rational, we can decide whether
x_i <= 1/2 or x_i >= 1/2, and these two cases imply that x < 1 or x > 0.

Now this is all 100% constructive, and we can view it as a function from
representatives (x_n) to {0,1} (referring to the two cases of the
disjunction). However, this function does *not* respect the equivalence
relation on real numbers, so it does not lift to a function v : R -> {0,1};
indeed this is impossible since all constructive real functions are
continuous.

So this depends in part on how the existential, or the disjunction, is
treated constructively. In the presence of proof irrelevance, we would say
that either proof of x < 1 or x > 0 via the two disjuncts amounts to equal
proof terms, or in the case of the existential we would say that all proofs
of Ev ((v = 0 /\ x < 1) \/ (v = 1 /\ x > 0)) are equal, so that we are
justified in lifting it to a universal claim on constructive reals, Ax:R,
Ev:R, ((v = 0 /\ x < 1) \/ (v = 1 /\ x > 0)). (Unless we are working in a
type theory this will be more or less a given.) But it is not possible to
justify this move while simultaneously viewing Ev, phi as {v | phi} or
Sigma v, phi, that is, while treating proofs of existentials as storing
their witnesses in a recoverable way, without losing quotient constructions
like R.

Assuming that we have proof irrelevance or an equivalent, we thus have
Ax:R, Ev:R, ((v = 0 /\ x < 1) \/ (v = 1 /\ x > 0)) but not Ev:R -> R, Ax:R,
((v(x) = 0 /\ x < 1) \/ (v(x) = 1 /\ x > 0), so this is a failure of the
axiom of choice.

Mario Carneiro

On Wed, May 2, 2018 at 12:54 PM, Dennis E. Hamilton <dennis.hamilton at acm.org
> wrote:

>
>
>
>
> *From:* fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] *On Behalf
> Of *Kreinovich, Vladik
> *Sent:* Tuesday, May 1, 2018 13:41
> *Subject:* [FOM] a simple constructive example when AC is not true
>
>
>
> In purely constructive approach, when existence is algorithmic and
> functions are computable, by computing a computable real number x with
> accuracy 0.1, we can efficiently check whether x > 0 or x < 1.
>
> *[orcmid] *
>
>
>
> *To confirm my understanding of this setup, I need to be more specific.*
>
>
>
> *Suppose that, for computable real, x, there is a computation that
> approximates x by xa/10 where xa is an integer.  It is assured that xa/10
> is not greater than x and that x is less than (xa+1)/10.  This is by
> assurance of x being a computable real and by construction of the algorithm
> for its approximation.*
>
>
>
> *One can generalize this formulation to consider a computable function for
>  xa =  xapprox(n) that produces integers such that xa/(10^n) is not greater
> than x and x is less than (xa+1)/(10^n).  *
>
>
>
> *It is trivially the case that (xa > 0 or xa < 1), and likewise for
> xa/(10^n) and for x.  No efficiency is required.  Perhaps the better
> question is to know whether x is in the closed interval [0,1] in which case
> it may be necessary to get to an xapprox(n), for sufficiently large n, that
> settles the question. *
>
>
>
> *Hence my confusion.*
>
>
>
> *I am unclear how this, with needed repairs to my understanding about (x >
> 0 or x < 1), still tells us anything about AC with respect to the reals,
> since xapprox(n) is not a real-valued function.  At best, it produces
> segments of a Cauchy sequence of pairs of rationals, {xa[i]/(10^i),
> (xa[i]+1)/(10^i) }.   Note that xapprox(n) is not a function n reals and is
> not continuous in the real-analysis sense.*
>
>
>
> *What am I missing?*
>
>
>
>    - *Dennis*
>
>
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180502/b37b8cd4/attachment-0001.html>