This is the request for references.

It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent.

It is also know that there is a double-negation Godel-Gentzen translation from classical logic to intuitionistic. (So we can prove something in IZF.)

Does exist a similar result about CIC with axiom of choice? By CIC I mean the Calculus of Inductive Constructions, the system which The Coq proof assistant is based on.

Does exist a model of CIC+choice inside CIC? Where can I learn about it?

Definition choice :=
   forall (A B : Type) (P : A -> B -> Prop),  
   (forall a : A, exists b : B, P a b) ->
   exists f : A -> B, forall a : A, P a (f a).
  • $\begingroup$ Maybe Benjamin Werner's paper "Sets in types, types in sets" is a good reading. $\endgroup$ – Taroccoesbrocco Nov 1 '18 at 9:29
  • $\begingroup$ Isn't that the form of the axiom of choice that's actually provable in a dependent type theory like CIC? $\endgroup$ – Malice Vidrine Nov 1 '18 at 19:13
  • $\begingroup$ I don't know exactly, but I think that is not, because otherwise why would it be in the library github.com/coq-contribs/zfc ? (see Replacement.v) $\endgroup$ – ged Nov 2 '18 at 7:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.