Impredicative Set

The sort Set was impredicative in the original versions of Coq. For backward compatibility, or for experiments by knowledgeable users, the logic of Coq can be set impredicative for Set by calling Coq with the option -impredicative-set.

Set has been made predicative from version 8.0 of Coq. The main reason is to interact smoothly with a classical mathematical world where both excluded-middle and the axiom of description are valid (see file ClassicalDescription.v for a proof that excluded-middle and description implies the double negation of excluded-middle in Set and file Hurkens_Set.v from the user contribution Paradoxes at http://coq.inria.fr/contribs for a proof that impredicativity of Set implies the simple negation of excluded-middle in Set).

What standard axioms are inconsistent with impredicative Set?

The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative.

As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions.

The main purpose of the Set-predicative restriction of the Calculus of Inductive Constructions is precisely to accommodate these axioms which are quite standard in mathematical usage.

Why does injection not work on impredicative Set?

E.g. in this case (this occurs only in the Set-impredicative variant of Coq):

Inductive I : Type :=
  intro : forall k : Set, k -> I.

Lemma eq_jdef :
  forall x y : nat, intro _ x = intro _ y -> x = y.

Proof.
  intros x y H; injection H.

Injectivity of constructors is restricted to predicative types. If injectivity on large inductive types were not restricted, we would be allowed to derive an inconsistency (e.g. following the lines of Burali-Forti paradox). The question remains open whether injectivity is consistent on some large inductive types not expressive enough to encode known paradoxes (such as type I above).

What is a “large inductive definition”?

An inductive definition in Prop or Set is called large if its constructors embed sets or propositions. As an example, here is a large inductive type:

Inductive sigST (P : Set -> Set) : Type :=
  existST : forall X : Set, P X -> sigST P.

In the Set impredicative variant of Coq, large inductive definitions in Set have restricted elimination schemes to prevent inconsistencies. Especially, projecting the set or the proposition content of a large inductive definition is forbidden. If it were allowed, it would be possible to encode e.g. Burali-Forti paradox [5, 6].

Is Coq’s logic conservative over Coquand’s Calculus of Constructions?

In the Set-impredicative version of the Calculus of Inductive Constructions (CIC), in addition to the Prop interpretation, there is another way to interpret the Calculus of Constructions (CC) since the impredicative sort of CC can also be interpreted as Set.

If the impredicative sort of CC is interpreted as Set, there is no conservativity of CIC over CC as the discrimination of constructors of inductive types in Set transports to a discrimination of constructors of inductive types encoded impredicatively. Concretely, considering the impredicative encoding of Boolean, equality and falsity, we can prove the following CC statement DISCR in CIC which is not provable in CC, as CC has a “term-irrelevant” model.

Definition BOOL := forall X : Set, X -> X -> X.
Definition TRUE : BOOL := fun X x1 x2 => x1.
Definition FALSE : BOOL := fun X x1 x2 => x2.
Definition EQBOOL (x1 x2 : BOOL) := forall P : BOOL -> Set, P x1 -> P x2.
Definition BOT := forall X : Set, X.
Definition BOOL2bool : BOOL -> bool := fun b => b bool true false.

Theorem DISCR : EQBOOL TRUE FALSE -> BOT.
Proof.
  intro X.
  assert (H : BOOL2bool TRUE = BOOL2bool FALSE).
  { apply X. trivial. }
  discriminate H.
Qed.