[FOM] A question about AC in constructive mathematics
Maria Emilia Maietti
maietti at math.unipd.it
Sun Apr 29 19:02:05 EDT 2018
Dear Avron and all
many thanks for your questions and replies.
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).
EM + Ext- + ACint is equivalent to ACext. Math. Log. Q. 50(3)
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
and then completed into a two level theory
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.
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
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
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)
Maria Emilia 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
> 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
> (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
> in connection to AC. The technical details may be found here:
> 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.
> This message was sent using IMP, the Internet Messaging Program.
> FOM mailing list
> FOM at cs.nyu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM