[FOM] A question about AC in constructive mathematics

Sun Apr 29 19:02:05 EDT 2018

Dear Avron and all

many thanks for your questions and replies.

According to

Martin-Lo"f 2006. “100 years of Zermelo’s axiom of choice: what was the 
problem with it?,” /The Computer Journal/, 49(3): 345–350

the status of Zermelo's axiom of choice and its constructive valid 
counterpart are  much

clearer when formulated in dependent type theory than when formulated in 
axiomatic set theory.

In his type theory Martin-Loef distinguishes between and an 
**intensional AC** ( costructively acceptable) and an **extensional AC** 
(not constructively acceptable).

See also

Jesper Carlström:
EM + Ext- + ACint is equivalent to ACext. Math. Log. Q. 50(3) 
<https://dblp.uni-trier.de/db/journals/mlq/mlq50.html#Carlstrom04>: 
236-240 (2004)

Moreover  an answer  to Avron's question concerning the different status 
of AC in constructive mathematics

was one of the original motivations  to

conceive a **two-level** Minimalist Foundation MF for constructive 
mathematics where to view the different forms of AC.

MF was conceived with Giovanni Sambin in

http://www.math.unipd.it/~maietti/papers/MaiettiSambin-rev2.pdf

and then completed into a two level theory

in

http://www.math.unipd.it/~maietti/papers/tt.pdf

MF include the following properties:

1. it  has an ***intensional*** level  (formulated as an intensional 
type theory a' la Martin-Loef) which is consistent with the Formal 
Church thesis and the Axiom of Choice

(via an extension of Kleene realizability).

2. it has an extensional level (formulated as an extensional type theory 
a' la Martin-Loef))

closed under quotients and powercollections (where AC implies the 
principle of excluded middle by the well-known Diaconescu argument).

3. the extensional level is interpreted in a quotient model of the 
intensional level in such a way that the axiom of choice written at  the 
extensional level is translated into ***Martin-Lof's extensional axiom 
of choice** which is not validated by the realizability semantics 
mentioned in 1.

In addition one has to note that the validity of AC depends on the
representation in type theory  of the existential quantifier beside that 
of the notion of function as already mentioned
by the previous replies.

For example

1. in Martin-Lof's type theory  the existential quantifier is identified 
with the so called "indexed sum type" and functions
with lambda terms; as a consequence  the so called intensional axiom of 
choice (which corresponds to a sort of set-theoretic distributivity  
property as mentioned in the plato-stanford entry on AC) is valid.

2. in the internal dependent type theory of elementary topoi as 
formulated in

Maietti, M.E., 2005. “Modular correspondence between dependent type 
theories and categories including pretopoi and topoi,” /Mathematical 
Structures in Computer Science/, 15/6: 1089–1145.

propositions are represented as mono types as recalled by U. Berger.

As a consequence in topoi unique choice is provable (= functional 
relations are in bijections with lambda terms)  but the axiom of choice 
is not valid.

3. at both levels of MF the existential quantifier is defined 
primitively and
two distinct notions of function, respectively lambda terms and 
functional relations, are present; as a consequence
no unique choice and no axiom of choice (wrt both notions of function) 
is valid.

Best wishes
Maria Emilia Maietti
http://www.math.unipd.it/~maietti/

On 29/04/2018 13:31, sasander at cage.ugent.be wrote:
> 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.
> _______________________________________________
> 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/20180430/f29785aa/attachment.html>