|
This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails
proof-irrelevance.
Since, dependent elimination is derivable in the Calculus of Inductive Constructions (CCI), we get proof-irrelevance from classical logic in the CCI. Reference:
Proof skeleton: classical logic + dependent elimination of disjunction + discrimination of proofs implies the existence of a retract from Prop into bool, hence inconsistency by encoding any
paradox of system U- (e.g. Hurkens' paradox).
|
Require Import Hurkens.
Section Proof_irrelevance_CC.
Variable or : Prop -> Prop -> Prop.
Variable or_introl : forall A B:Prop, A -> or A B.
Variable or_intror : forall A B:Prop, B -> or A B.
Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
Hypothesis
or_elim_redl :
forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
f a = or_elim A B C f g (or_introl A B a).
Hypothesis
or_elim_redr :
forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
g b = or_elim A B C f g (or_intror A B b).
Hypothesis
or_dep_elim :
forall (A B:Prop) (P:or A B -> Prop),
(forall a:A, P (or_introl A B a)) ->
(forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.
Hypothesis em : forall A:Prop, or A (~ A).
Variable B : Prop.
Variables b1 b2 : B.
p2b and b2p form a retract if ~b1=b2
|
Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
Definition b2p b := b1 = b.
Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
Proof.
unfold p2b in |- *; intro A; apply or_dep_elim with (b:= em A);
unfold b2p in |- *; intros.
apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
destruct (b H).
Qed.
Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
Proof.
intro not_eq_b1_b2.
unfold p2b in |- *; intro A; apply or_dep_elim with (b:= em A);
unfold b2p in |- *; intros.
assumption.
destruct not_eq_b1_b2.
rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
assumption.
Qed.
| Using excluded-middle a second time, we get proof-irrelevance |
Theorem proof_irrelevance_cc : b1 = b2.
Proof.
refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
trivial.
apply (paradox B p2b b2p (p2p2 H) p2p1).
Qed.
End Proof_irrelevance_CC.
| The Calculus of Inductive Constructions (CCI) enjoys dependent elimination, hence classical logic in CCI entails proof-irrelevance. |
Section Proof_irrelevance_CCI.
Hypothesis em : forall A:Prop, A \/ ~ A.
Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C)
(a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a).
Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C)
(b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b).
Scheme or_indd := Induction for or Sort Prop.
Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.
Proof
proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
or_elim_redr or_indd em.
End Proof_irrelevance_CCI.
Remark: in CCI, bool can be taken in Set as well in the
paradox and since ~true=false for true and false in
bool, we get the inconsistency of em : forall A:Prop, {A}+{~A} in CCI
|