[TYPES] independence of AC! or AC from CIC

Maria Emilia Maietti maietti at math.unipd.it
Wed Dec 28 05:59:52 EST 2016


Dear all

is it known whether the axiom of unique choice  (AC!)  or even
the only axiom of choice (both as formulas in Prop)

are independent from the Calculus of Inductive Constructions ?

Any reference?

For the pure Calculus of Constructions the  independence of AC! and AC 
was shown
in
T. Streicher " Independence of the induction principle and the axiom of 
choice in the pure calculus of constructions." TCS, 1992, vol.103.

Many thanks for your cooperation
Milly
(Maria Emilia Maietti)


More information about the Types-list mailing list