[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