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

[Kreinovich, Vladik]

Exactly my point, thanks for clarifying!

From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of Mario Carneiro
Sent: Wednesday, May 02, 2018 9:09 PM
To: dennis.hamilton at acm.org; Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: [FOM] a simple constructive example when AC is not true

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<mailto:dennis.hamilton at acm.org>> wrote:


From: fom-bounces at cs.nyu.edu<mailto:fom-bounces at cs.nyu.edu> [mailto: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<mailto:FOM at cs.nyu.edu>
https://cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180503/ac52c271/attachment.html>