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

[Kreinovich, Vladik]

You are not missing anything, this is exactly my point.

We say that a number x is computable if there is an algorithm (procedure) that, given a natural number n, returns a rational number r_n for which |r_n - x| <=2^{-n}.  This is a standard definition in books on constructive mathematics, Bishop, Bridges, Kushner, anything.

To effectively check whether x > 0 or x < 1,  we apply this algorithm to n = 3 and get a rational number r_3 for which |r_3 - x| <= 1/8. Rational numbers we can efficiently compare with each other, so either r_3 < ½ or r_3 >= ½. If r_2 < ½, we take v = 0, the previous inequality implies that x < ½ + 1/8 and thus, that x < 1.

If r_3 > ½, this implies that x > ½ - 1/8 > 0 and thus, that x > 0; in this case, we take v = 1.

So, we have an algorithmic procedure that, given a computable real number x, computes a natural number v which is equal either to 0 or to 1, such that if v = 1 then x > 0 and if v = 0 then x < 1.

This is exactly what I said: that we can effectively decide whether x < 1 or whether x > 0, i.e., in the constructive sense of "or", we have x < 1 \/ x > 0. Constructive "or" Ax (B(x) \/ C(x)) means that we have an algorithm that, given x, returns either 0 or 1, in the first case we have B(x) in the second case we have C(x).

However, you are absolutely right, in my simple example, we cannot have a computable function that, given x, returns the corresponding v - and AC would means that such a choice function exists.

Literally, Axiom of Choice means that if Ax Ey P(x,y) then we can select one y for each x, i.e., we would have a function f(x) such that Ax P(x,y(x)). This is true in algorithmically understood constructive mathematics when x goes over natural numbers but not true when x goes over real numbers.

You are also absolutely true that we do not need to assume that x is computable, all we need is to have a procedure that, given n, return r_n, this procedure does not have to be an algorithm, it can be a measurement process. In this case, we can repeat the above argument and conclude that we can still algorithmically decide whether  x > 0 or whether x < 1. Here we talk about algorithms that use a procedure that transforms n to r_n as an oracle.


From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of Dennis E. Hamilton
Sent: Wednesday, May 02, 2018 10:55 AM
To: 'Foundations of Mathematics' <fom at cs.nyu.edu>
Subject: Re: [FOM] a simple constructive example when AC is not true



From: 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


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