[FOM] A question about AC in constructive mathematics

[sasander at cage.ugent.be]

Dear Arnon,

I would not call myself a specialist, but here goes anyway:

Let us start with the BHK meaning of this formula:

“for all x, there exists a y such that A(x, y)”,  (*)

which is essentially:

given any x, we may compute some y satisfying A(x,y).  (**)

Now the following situation is crucial:

take x and x’ to be *different* representations of the *same* object
Then (**) only tells you that there we can compute some y such that A(x, y)
*and* that we can compute some y’ such that A(x, y’).  Note that y and y’
need *not* be the same object.

As an example, suppose x and x’ are both pi given by a binary
sequence and via a Cauchy sequence, and take A(x,y) to be
  ‘y is the k-th approximation of x’ (for some fixed k).  Clearly,
one can find very different y and y’ for x and x’.

Now, in its full generality, AC applied to (*) tells you that you can  
always find an
(extensional) function computing y from x, i.e. independent of the represen-
tation of x.  This extra function extensionality does *not* follow  
from the BHK-
interpretation.  Hence, full AC is not motivated by the  
BHK-interpretation, and
it has also been shown that full AC indeed implies the law of excluded middle
(by Diaconescu and Myhill & Goodman).

However, there are *fragments* of AC where the above point is moot:

For instance, "countable choice" only applies to (*) where x ranges over the
natural numbers, and there there are no issues of different  
representations of x.

Similarly, “unique choice” applies to (*) where there is a unique such  
y for every x.
Again, representation is not an issue, as we are poised to always find  
the same y.

Hence, the two aforementioned fragments of choice do follow from the
BHK-representation.  These are also accepted in the practice of Bishop’s
mathematics.    Bishop did write in his 1967 book that

A choice function exists in constructive mathematics,
because a choice is implied by the very meaning of existence.

Bishop was presumably talking about non-extensional functions.

Finally, as far as I know, Martin-Loef type theory is defined in such a way
that the above  problem of representation and extensionality does not occur
in connection to AC. The technical details may be found here:

https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html

It seems that the interpretation of "there exists" is such that it has to
respect equality on the types of x and y by definition.

Best,

Sam



----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.