To improve my own understanding of type theory, I’d like to experiment with the paradoxes that occur when we drop the restriction on large elimination, i.e., the fact that pattern matching on x : P where P : Prop can only yield y : T where T : S when S is Prop (or apparently SProp), except in a special case (called “empty and singleton elimination” in the documentation page).
In particular, I’d like to understand if we can already get a paradox with just a restricted form like only adding fun {A B : Prop} (x : A \/ B) => match x with or_introl _ => false | or_intror _ => true end. (I’m interested in pointers about that, but this isn’t my main question.)
Is there a way I can turn off the check for large elimination in order to do these experiments? I found the similar flags Unset Guard Checking., Unset Positivity Checking. and Unset Universe Checking. but nothing for large elimination.
I don’t know a way to remove the singleton elimination constraint when eliminating an inductive in Prop to Type, but you can always axiomatize an eliminator targetting Type for a given inductive in Prop (and add computational content with rewrite rules if you want).
In the case of Prop, the restriction is only there to ensure that Prop is consistent with proof irrelevance. So as long as you do not assume proof irrelevance as an additional axiom, lifting this restriction should not give rise to an inconsistency, though it will probably break extraction (that erases the Prop content).
In the case of SProp, definitional proof irrelevance combined with an elimination principle for SProp-valued “booleans” will indeed allow to derive an inconsistency:
Inductive sbool : SProp := stt | sff.
Axiom sbool_ind : forall (P : sbool -> Type), P stt -> P sff -> forall b, P b.
Axiom sbool_ind_stt : forall P htt hff, sbool_ind P htt hff stt = htt.
Axiom sbool_ind_sff : forall P htt hff, sbool_ind P htt hff stt = hff.
Lemma inconsistent : False.
Proof.
enough (true = false) by discriminate.
transitivity (sbool_ind (fun _ => bool) true false stt).
1: symmetry; apply (sbool_ind_stt (fun _ => bool)).
apply (sbool_ind_sff (fun _ => bool)).
Qed.
Unset Universe Checking.
Inductive Bad (A:Type) : Prop := bad (_:A).
Set Universe Checking.
When you want to eliminate a Prop to produce some A:Type you instead produce a Bad A and eliminate that. For instance
Unset Universe Checking.
Inductive Bad (A:Type) : Prop := bad (_:A).
Set Universe Checking.
Lemma choice {A:Type} : inhabited A -> A.
Proof.
intros H.
assert (Bad A) as [x].
{ destruct H;constructor;assumption. }
exact x.
Defined.
Lemma choice_inhabits A (x:A) : choice (inhabits x) = x.
Proof. reflexivity. Qed.
Lemma inhabits_choice A (x:inhabited A) : inhabits (choice x) = x.
Proof. destruct x;reflexivity. Qed.
but this produces a paradox:
Monomorphic Definition Type2 := Type.
Monomorphic Definition Type1 := Type : Type2.
Section Hurkens.
(** Assumption of a retract from Type into Prop *)
Variable down : Type1 -> Prop.
Variable up : Prop -> Type1.
Hypothesis back : forall A, up (down A) -> A.
Hypothesis forth : forall A, A -> up (down A).
Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A),
P (back A (forth A a)) -> P a.
Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A),
P a -> P (back A (forth A a)).
(** Proof *)
Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
Definition U : Type1 := V -> Prop.
Definition sb (z:V) : V := fun A r a => r (z A r) a.
Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x).
Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))).
Definition I (x:U) : Prop :=
(forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.
Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
Proof.
intros i y.
apply y.
unfold le, WF, induct.
apply forth.
intros x H0.
apply y.
unfold sb, le', le.
compute.
apply backforth_r.
exact H0.
Qed.
Lemma lemma1 : induct (fun u => down (I u)).
Proof.
unfold induct.
intros x p.
apply forth.
intro q.
generalize (q (fun u => down (I u)) p).
intro r.
apply back in r.
apply r.
intros i j.
unfold le, sb, le', le in j |-.
apply backforth in j.
specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))).
apply q.
exact j.
Qed.
Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
Proof.
intro x.
generalize (x (fun u => down (I u)) lemma1).
intro r; apply back in r.
apply r.
intros i H0.
apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))).
unfold le, WF in H0.
apply back in H0.
exact H0.
Qed.
Theorem paradox0 : False.
Proof.
exact (lemma2 Omega).
Qed.
End Hurkens.
Lemma paradox : False.
Proof.
unshelve eapply (paradox0 inhabited (fun P => P) (@choice) (@inhabits)).
- intros ??? H. rewrite choice_inhabits in H. exact H.
- intros ??? H. rewrite choice_inhabits. exact H.
Qed.
@kyod You’re right, somehow it didn’t occur to me that I could get around it in this way…
In the special case I was interested in, which is the elimination of or (A \/ B) to bool, this would look like:
Axiom or_rect_bool : forall {A B : Prop}, (A -> bool) -> (B -> bool) -> (A \/ B) -> bool.
Axiom or_rect_bool_left : forall {A B : Prop} (f : A -> bool) (g : B -> bool) (a : A),
or_rect_bool f g (or_introl a) = f a.
Axiom or_rect_bool_right : forall {A B : Prop} (f : A -> bool) (g : B -> bool) (b : B),
or_rect_bool f g (or_intror b) = g b.
Does that sound right?
Now I’m wondering whether this is enough to introduce an inconsistency alone… Of course it is inconsistent with proof irrelevance (thus with propext) for essentially the same reason as your case:
@SkySkimmer That’s an interesting idea as well. And thanks for saving me the time to formalize Hurkens’ paradox Now I just need to understand that code…
Hurkens was more interested in studying the paradoxical lambda-term than the paradox itself, and the above Coq proof makes it even more obscure by having to deal with Coq’s logic. Below is a version that is closer to the mathematical paradox. As always, it ultimately boils down to Russell’s paradox, that is, you build a set that only contains smaller sets, then you show that it contains itself, and you derive a contradiction. You can recognize this pattern in the first few lines of the proof, that is wf (t wf) is both true and false.
Axiom U : Set.
Axiom s : U -> (U -> Prop).
Axiom t : (U -> Prop) -> U.
Axiom powerful : forall X u, s (t X) u <-> exists x, X x /\ u = t (s x).
Definition lt y x := s x y.
Definition inductive (X : U -> Prop) := forall x, (forall y, lt y x -> X y) -> X x.
Definition wf x := forall X, inductive X -> X x.
Goal False.
Proof.
absurd (wf (t wf)).
- intros wf_omega.
apply (wf_omega (fun y => not (lt (t (s y)) y))).
2: apply powerful; now exists (t wf).
intros x Hx Hx'.
apply (Hx _ Hx').
apply powerful.
now exists (t (s x)).
- intros X HX.
apply HX.
intros u Hu.
apply powerful in Hu.
destruct Hu as [o [wf_o ->]].
apply wf_o.
intros x Hx.
apply HX.
intros y Hy.
apply powerful in Hy.
destruct Hy as [u [Hu ->]].
now apply Hx.
Qed.
Now I just need to understand that code…