[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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)
